Step
*
of Lemma
rotate-by-transitive
∀n,b:ℕ. (gcd(b;n) = 1 ∈ ℤ supposing 0 < n
⇐⇒ ∀x,y:ℕn. ∃k:ℕ. ((rotate-by(n;b)^k x) = y ∈ ℤ))
BY
{ Auto }
1
1. n : ℕ
2. b : ℕ
3. gcd(b;n) = 1 ∈ ℤ supposing 0 < n
4. x : ℕn
5. y : ℕn
⊢ ∃k:ℕ. ((rotate-by(n;b)^k x) = y ∈ ℤ)
2
1. n : ℕ
2. b : ℕ
3. ∀x,y:ℕn. ∃k:ℕ. ((rotate-by(n;b)^k x) = y ∈ ℤ)
4. 0 < n
⊢ gcd(b;n) = 1 ∈ ℤ
Latex:
Latex:
\mforall{}n,b:\mBbbN{}. (gcd(b;n) = 1 supposing 0 < n \mLeftarrow{}{}\mRightarrow{} \mforall{}x,y:\mBbbN{}n. \mexists{}k:\mBbbN{}. ((rotate-by(n;b)\^{}k x) = y))
By
Latex:
Auto
Home
Index