Nuprl Lemma : residues-permute
∀n:{2...}. ∀a:ℕ+. (CoPrime(n,a) ⇒ permutation(residue(n);map(λi.(ai mod n);residues-mod(n));residues-mod(n)))
Proof
Definitions occuring in Statement :
residues-mod: residues-mod(n),
residue-mul: (ai mod n),
residue: residue(n),
coprime: CoPrime(a,b),
permutation: permutation(T;L1;L2),
map: map(f;as),
int_upper: {i...},
nat_plus: ℕ+,
all: ∀x:A. B[x],
implies: P ⇒ Q,
lambda: λx.A[x],
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
subtype_rel: A ⊆r B,
exists: ∃x:A. B[x],
and: P ∧ Q,
uall: ∀[x:A]. B[x],
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
false: False,
not: ¬A,
prop: ℙ,
nat_plus: ℕ+,
int_upper: {i...},
decidable: Dec(P),
or: P ∨ Q,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
uimplies: b supposing a,
top: Top,
true: True,
residue: residue(n),
int_seg: {i..j-},
cand: A c∧ B,
sq_stable: SqStable(P),
squash: ↓T,
inject: Inj(A;B;f),
l_member: (x ∈ l),
lelt: i ≤ j < k,
guard: {T},
so_lambda: λ2x.t[x],
so_apply: x[s],
less_than: a < b
Lemmas referenced :
residue-mul-inverse,
nat_plus_subtype_nat,
permutation-when-no_repeats,
residue_wf,
int_upper_subtype_nat,
false_wf,
le_wf,
residues-mod_wf,
map_wf,
residue-mul_wf,
decidable__lt,
not-lt-2,
add_functionality_wrt_le,
add-commutes,
zero-add,
le-add-cancel,
less_than_wf,
sq_stable__coprime,
l_member_wf,
member-residues-mod,
no_repeats-residues-mod,
coprime_wf,
nat_plus_wf,
int_upper_wf,
member-map,
equal_wf,
less_than_transitivity2,
set_wf,
no_repeats_map,
lelt_wf,
squash_wf,
int_seg_wf,
true_wf,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
applyEquality,
hypothesis,
sqequalRule,
independent_functionElimination,
productElimination,
isectElimination,
dependent_set_memberEquality,
natural_numberEquality,
independent_pairFormation,
because_Cache,
lambdaEquality,
setElimination,
rename,
unionElimination,
voidElimination,
independent_isectElimination,
isect_memberEquality,
voidEquality,
intEquality,
imageMemberEquality,
baseClosed,
imageElimination,
dependent_pairFormation,
productEquality,
equalitySymmetry,
setEquality,
equalityElimination,
applyLambdaEquality,
equalityTransitivity,
universeEquality
Latex:
\mforall{}n:\{2...\}. \mforall{}a:\mBbbN{}\msupplus{}.
(CoPrime(n,a) {}\mRightarrow{} permutation(residue(n);map(\mlambda{}i.(ai mod n);residues-mod(n));residues-mod(n)))
Date html generated:
2018_05_21-PM-08_58_42
Last ObjectModification:
2017_07_26-PM-06_22_15
Theory : general
Home
Index