Metamath Proof Explorer

Theorem odzcllem

Description: - Lemma for odzcl , showing existence of a recurrent point for the exponential. (Contributed by Mario Carneiro, 28-Feb-2014) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Assertion odzcllem ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→odℤ⁡N⁡A∈ℕ∧N∥Aodℤ⁡N⁡A−1

Proof

Step Hyp Ref Expression
1 odzval ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→odℤ⁡N⁡A=supn∈ℕ|N∥An−1ℝ<
2 ssrab2 ⊢n∈ℕ|N∥An−1⊆ℕ
3 nnuz ⊢ℕ=ℤ≥1
4 2 3 sseqtri ⊢n∈ℕ|N∥An−1⊆ℤ≥1
5 phicl ⊢N∈ℕ→ϕ⁡N∈ℕ
6 5 3ad2ant1 ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→ϕ⁡N∈ℕ
7 eulerth ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→Aϕ⁡NmodN=1modN
8 simp1 ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→N∈ℕ
9 simp2 ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→A∈ℤ
10 6 nnnn0d ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→ϕ⁡N∈ℕ0
11 zexpcl ⊢A∈ℤ∧ϕ⁡N∈ℕ0→Aϕ⁡N∈ℤ
12 9 10 11 syl2anc ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→Aϕ⁡N∈ℤ
13 1z ⊢1∈ℤ
14 moddvds ⊢N∈ℕ∧Aϕ⁡N∈ℤ∧1∈ℤ→Aϕ⁡NmodN=1modN↔N∥Aϕ⁡N−1
15 13 14 mp3an3 ⊢N∈ℕ∧Aϕ⁡N∈ℤ→Aϕ⁡NmodN=1modN↔N∥Aϕ⁡N−1
16 8 12 15 syl2anc ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→Aϕ⁡NmodN=1modN↔N∥Aϕ⁡N−1
17 7 16 mpbid ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→N∥Aϕ⁡N−1
18 oveq2 ⊢n=ϕ⁡N→An=Aϕ⁡N
19 18 oveq1d ⊢n=ϕ⁡N→An−1=Aϕ⁡N−1
20 19 breq2d ⊢n=ϕ⁡N→N∥An−1↔N∥Aϕ⁡N−1
21 20 rspcev ⊢ϕ⁡N∈ℕ∧N∥Aϕ⁡N−1→∃n∈ℕN∥An−1
22 6 17 21 syl2anc ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→∃n∈ℕN∥An−1
23 rabn0 ⊢n∈ℕ|N∥An−1≠∅↔∃n∈ℕN∥An−1
24 22 23 sylibr ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→n∈ℕ|N∥An−1≠∅
25 infssuzcl ⊢n∈ℕ|N∥An−1⊆ℤ≥1∧n∈ℕ|N∥An−1≠∅→supn∈ℕ|N∥An−1ℝ<∈n∈ℕ|N∥An−1
26 4 24 25 sylancr ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→supn∈ℕ|N∥An−1ℝ<∈n∈ℕ|N∥An−1
27 1 26 eqeltrd ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→odℤ⁡N⁡A∈n∈ℕ|N∥An−1
28 oveq2 ⊢n=odℤ⁡N⁡A→An=Aodℤ⁡N⁡A
29 28 oveq1d ⊢n=odℤ⁡N⁡A→An−1=Aodℤ⁡N⁡A−1
30 29 breq2d ⊢n=odℤ⁡N⁡A→N∥An−1↔N∥Aodℤ⁡N⁡A−1
31 30 elrab ⊢odℤ⁡N⁡A∈n∈ℕ|N∥An−1↔odℤ⁡N⁡A∈ℕ∧N∥Aodℤ⁡N⁡A−1
32 27 31 sylib ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→odℤ⁡N⁡A∈ℕ∧N∥Aodℤ⁡N⁡A−1