Step
*
1
3
of Lemma
fermat-little
1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g o rot(p)))
6. {x@0:ℕp ⟶ ℕx| ((λg.(g o rot(p))) x@0) = x@0 ∈ (ℕp ⟶ ℕx)} ~ ℕx
7. x@0 : ℕp ⟶ ℕx
⊢ (λg.(g o rot(p))^p x@0) = x@0 ∈ (ℕp ⟶ ℕx)
BY
{ TACTIC:((InstLemma `fun_exp_compose2` [⌜ℕp⌝;⌜ℕx⌝;⌜rot(p)⌝;⌜p⌝]⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Auto) }
1
1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g o rot(p)))
6. {x@0:ℕp ⟶ ℕx| ((λg.(g o rot(p))) x@0) = x@0 ∈ (ℕp ⟶ ℕx)} ~ ℕx
7. x@0 : ℕp ⟶ ℕx
8. λg.(g o rot(p))^p = (λg.(g o rot(p)^p)) ∈ ((ℕp ⟶ ℕx) ⟶ ℕp ⟶ ℕx)
⊢ ((λg.(g o rot(p)^p)) x@0) = x@0 ∈ (ℕp ⟶ ℕx)
Latex:
Latex:
1. p : \mBbbN{}
2. prime(p)
3. x : \mBbbN{}
4. \mBbbN{}p {}\mrightarrow{} \mBbbN{}x \msim{} \mBbbN{}x\^{}p
5. Inj(\mBbbN{}p {}\mrightarrow{} \mBbbN{}x;\mBbbN{}p {}\mrightarrow{} \mBbbN{}x;\mlambda{}g.(g o rot(p)))
6. \{x@0:\mBbbN{}p {}\mrightarrow{} \mBbbN{}x| ((\mlambda{}g.(g o rot(p))) x@0) = x@0\} \msim{} \mBbbN{}x
7. x@0 : \mBbbN{}p {}\mrightarrow{} \mBbbN{}x
\mvdash{} (\mlambda{}g.(g o rot(p))\^{}p x@0) = x@0
By
Latex:
TACTIC:((InstLemma `fun\_exp\_compose2` [\mkleeneopen{}\mBbbN{}p\mkleeneclose{};\mkleeneopen{}\mBbbN{}x\mkleeneclose{};\mkleeneopen{}rot(p)\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{} THENA Auto)
THEN HypSubst' (-1) 0
THEN Auto)
Home
Index