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 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∈ ℕ ∧ 𝑁 ∥ ( ( 𝐴 ↑ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ) − 1 ) ) )

Proof

Step Hyp Ref Expression
1 odzval ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) = inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )
2 ssrab2 ⊢ { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } ⊆ ℕ
3 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
4 2 3 sseqtri ⊢ { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } ⊆ ( ℤ≥ ‘ 1 )
5 phicl ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ )
6 5 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ϕ ‘ 𝑁 ) ∈ ℕ )
7 eulerth ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )
8 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℕ )
9 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝐴 ∈ ℤ )
10 6 nnnn0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
11 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
12 9 10 11 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
13 1z ⊢ 1 ∈ ℤ
14 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
15 13 14 mp3an3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
16 8 12 15 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
17 7 16 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
18 oveq2 ⊢ ( 𝑛 = ( ϕ ‘ 𝑁 ) → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) )
19 18 oveq1d ⊢ ( 𝑛 = ( ϕ ‘ 𝑁 ) → ( ( 𝐴 ↑ 𝑛 ) − 1 ) = ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
20 19 breq2d ⊢ ( 𝑛 = ( ϕ ‘ 𝑁 ) → ( 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
21 20 rspcev ⊢ ( ( ( ϕ ‘ 𝑁 ) ∈ ℕ ∧ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) → ∃ 𝑛 ∈ ℕ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) )
22 6 17 21 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ∃ 𝑛 ∈ ℕ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) )
23 rabn0 ⊢ ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } ≠ ∅ ↔ ∃ 𝑛 ∈ ℕ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) )
24 22 23 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } ≠ ∅ )
25 infssuzcl ⊢ ( ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } )
26 4 24 25 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } )
27 1 26 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∈ { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } )
28 oveq2 ⊢ ( 𝑛 = ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ) )
29 28 oveq1d ⊢ ( 𝑛 = ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) → ( ( 𝐴 ↑ 𝑛 ) − 1 ) = ( ( 𝐴 ↑ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ) − 1 ) )
30 29 breq2d ⊢ ( 𝑛 = ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) → ( 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ) − 1 ) ) )
31 30 elrab ⊢ ( ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∈ { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } ↔ ( ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∈ ℕ ∧ 𝑁 ∥ ( ( 𝐴 ↑ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ) − 1 ) ) )
32 27 31 sylib ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∈ ℕ ∧ 𝑁 ∥ ( ( 𝐴 ↑ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ) − 1 ) ) )