Step
*
1
1
1
of Lemma
wilson-theorem
.....assertion.....
1. n : {i:ℤ| 1 < i}
2. prime(n)
⊢ (∀b:ℕn. ((rotate-by(n;1) (rotate-by(n;n - 1) b)) = b ∈ ℕn))
∧ (∀b:ℕn. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b ∈ ℕn))
BY
{ (Auto
THEN RWO "rotate-by-rotate-by" 0
THEN Auto
THEN Try ((Unfold `label` 0 THEN HypSubst' (-1) 0 THEN Auto))
THEN RW IntNormC 0
THEN Auto
THEN BLemma `rotate-by-trivial`
THEN Auto) }
Latex:
Latex:
.....assertion.....
1. n : \{i:\mBbbZ{}| 1 < i\}
2. prime(n)
\mvdash{} (\mforall{}b:\mBbbN{}n. ((rotate-by(n;1) (rotate-by(n;n - 1) b)) = b))
\mwedge{} (\mforall{}b:\mBbbN{}n. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b))
By
Latex:
(Auto
THEN RWO "rotate-by-rotate-by" 0
THEN Auto
THEN Try ((Unfold `label` 0 THEN HypSubst' (-1) 0 THEN Auto))
THEN RW IntNormC 0
THEN Auto
THEN BLemma `rotate-by-trivial`
THEN Auto)
Home
Index