Step * 3 1 of Lemma fermat-little2


1. : ℕ@i
2. prime(p)@i
3. : ℕ@i
4. ¬(p x)
5. x^p ≡ mod p
⊢ (x x^p 1) x^p ∈ ℤ
BY
(InstLemma `exp_add` [⌜1⌝;⌜1⌝;⌜x⌝]⋅ THENA Auto) }

1
.....wf..... 
1. : ℕ@i
2. prime(p)@i
3. : ℕ@i
4. ¬(p x)
5. x^p ≡ mod p
⊢ 1 ∈ ℕ

2
1. : ℕ@i
2. prime(p)@i
3. : ℕ@i
4. ¬(p x)
5. x^p ≡ mod p
6. x^1 (p 1) (x^1 x^p 1) ∈ ℤ
⊢ (x x^p 1) x^p ∈ ℤ


Latex:


Latex:

1.  p  :  \mBbbN{}@i
2.  prime(p)@i
3.  x  :  \mBbbN{}@i
4.  \mneg{}(p  |  x)
5.  x\^{}p  \mequiv{}  x  mod  p
\mvdash{}  (x  *  x\^{}p  -  1)  =  x\^{}p


By


Latex:
(InstLemma  `exp\_add`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}p  -  1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)




Home Index