Metamath Proof Explorer

Theorem eulerthlem2

Description: Lemma for eulerth . (Contributed by Mario Carneiro, 28-Feb-2014)

Ref Expression
Hypotheses eulerth.1 ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) )
eulerth.2 ⊢ 𝑆 = { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 }
eulerth.3 ⊢ 𝑇 = ( 1 ... ( ϕ ‘ 𝑁 ) )
eulerth.4 ⊢ ( 𝜑 → 𝐹 : 𝑇 –1-1-onto→ 𝑆 )
eulerth.5 ⊢ 𝐺 = ( 𝑥 ∈ 𝑇 ↦ ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) )
Assertion eulerthlem2 ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eulerth.1 ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) )
2 eulerth.2 ⊢ 𝑆 = { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 }
3 eulerth.3 ⊢ 𝑇 = ( 1 ... ( ϕ ‘ 𝑁 ) )
4 eulerth.4 ⊢ ( 𝜑 → 𝐹 : 𝑇 –1-1-onto→ 𝑆 )
5 eulerth.5 ⊢ 𝐺 = ( 𝑥 ∈ 𝑇 ↦ ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) )
6 1 simp1d ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 6 phicld ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ )
8 7 nnred ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℝ )
9 8 leidd ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) )
10 7 adantr ⊢ ( ( 𝜑 ∧ ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ϕ ‘ 𝑁 ) ∈ ℕ )
11 breq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ≤ ( ϕ ‘ 𝑁 ) ↔ 1 ≤ ( ϕ ‘ 𝑁 ) ) )
12 11 anbi2d ⊢ ( 𝑥 = 1 → ( ( 𝜑 ∧ 𝑥 ≤ ( ϕ ‘ 𝑁 ) ) ↔ ( 𝜑 ∧ 1 ≤ ( ϕ ‘ 𝑁 ) ) ) )
13 oveq2 ⊢ ( 𝑥 = 1 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 1 ) )
14 fveq2 ⊢ ( 𝑥 = 1 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 1 ) )
15 13 14 oveq12d ⊢ ( 𝑥 = 1 → ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) )
16 15 oveq1d ⊢ ( 𝑥 = 1 → ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) )
17 fveq2 ⊢ ( 𝑥 = 1 → ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐺 ) ‘ 1 ) )
18 17 oveq1d ⊢ ( 𝑥 = 1 → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) )
19 16 18 eqeq12d ⊢ ( 𝑥 = 1 → ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ↔ ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) ) )
20 14 oveq2d ⊢ ( 𝑥 = 1 → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) )
21 20 eqeq1d ⊢ ( 𝑥 = 1 → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ↔ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 ) )
22 19 21 anbi12d ⊢ ( 𝑥 = 1 → ( ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ) ↔ ( ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 ) ) )
23 12 22 imbi12d ⊢ ( 𝑥 = 1 → ( ( ( 𝜑 ∧ 𝑥 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ) ) ↔ ( ( 𝜑 ∧ 1 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 ) ) ) )
24 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≤ ( ϕ ‘ 𝑁 ) ↔ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
25 24 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ 𝑥 ≤ ( ϕ ‘ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) ) )
26 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑧 ) )
27 fveq2 ⊢ ( 𝑥 = 𝑧 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) )
28 26 27 oveq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) )
29 28 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) )
30 fveq2 ⊢ ( 𝑥 = 𝑧 → ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) )
31 30 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) )
32 29 31 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ↔ ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ) )
33 27 oveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) )
34 33 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ↔ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) )
35 32 34 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ) ↔ ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) ) )
36 25 35 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ 𝑥 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ) ) ↔ ( ( 𝜑 ∧ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) ) ) )
37 breq1 ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( 𝑥 ≤ ( ϕ ‘ 𝑁 ) ↔ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) )
38 37 anbi2d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( 𝜑 ∧ 𝑥 ≤ ( ϕ ‘ 𝑁 ) ) ↔ ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) )
39 oveq2 ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ ( 𝑧 + 1 ) ) )
40 fveq2 ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) )
41 39 40 oveq12d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) )
42 41 oveq1d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
43 fveq2 ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) )
44 43 oveq1d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) )
45 42 44 eqeq12d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ↔ ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ) )
46 40 oveq2d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) )
47 46 eqeq1d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ↔ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) )
48 45 47 anbi12d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ) ↔ ( ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) ) )
49 38 48 imbi12d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( ( 𝜑 ∧ 𝑥 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ) ) ↔ ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) ) ) )
50 breq1 ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( 𝑥 ≤ ( ϕ ‘ 𝑁 ) ↔ ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) ) )
51 50 anbi2d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( ( 𝜑 ∧ 𝑥 ≤ ( ϕ ‘ 𝑁 ) ) ↔ ( 𝜑 ∧ ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) ) ) )
52 oveq2 ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) )
53 fveq2 ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) )
54 52 53 oveq12d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) )
55 54 oveq1d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) )
56 fveq2 ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) )
57 56 oveq1d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) )
58 55 57 eqeq12d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ↔ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ) )
59 53 oveq2d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) )
60 59 eqeq1d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ↔ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) )
61 58 60 anbi12d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ) ↔ ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) ) )
62 51 61 imbi12d ⊢ ( 𝑥 = ( ϕ ‘ 𝑁 ) → ( ( ( 𝜑 ∧ 𝑥 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑥 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑥 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = 1 ) ) ↔ ( ( 𝜑 ∧ ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) ) ) )
63 1 simp2d ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
64 f1of ⊢ ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 → 𝐹 : 𝑇 ⟶ 𝑆 )
65 4 64 syl ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ 𝑆 )
66 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
67 7 66 eleqtrdi ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
68 eluzfz1 ⊢ ( ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
69 67 68 syl ⊢ ( 𝜑 → 1 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
70 69 3 eleqtrrdi ⊢ ( 𝜑 → 1 ∈ 𝑇 )
71 65 70 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ 𝑆 )
72 oveq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 1 ) → ( 𝑦 gcd 𝑁 ) = ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) )
73 72 eqeq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 1 ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) = 1 ) )
74 73 2 elrab2 ⊢ ( ( 𝐹 ‘ 1 ) ∈ 𝑆 ↔ ( ( 𝐹 ‘ 1 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) = 1 ) )
75 71 74 sylib ⊢ ( 𝜑 → ( ( 𝐹 ‘ 1 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) = 1 ) )
76 75 simpld ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ ( 0 ..^ 𝑁 ) )
77 elfzoelz ⊢ ( ( 𝐹 ‘ 1 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 1 ) ∈ ℤ )
78 76 77 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ ℤ )
79 63 78 zmulcld ⊢ ( 𝜑 → ( 𝐴 · ( 𝐹 ‘ 1 ) ) ∈ ℤ )
80 79 zred ⊢ ( 𝜑 → ( 𝐴 · ( 𝐹 ‘ 1 ) ) ∈ ℝ )
81 6 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
82 modabs2 ⊢ ( ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) )
83 80 81 82 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) )
84 1z ⊢ 1 ∈ ℤ
85 fveq2 ⊢ ( 𝑥 = 1 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 1 ) )
86 85 oveq2d ⊢ ( 𝑥 = 1 → ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐹 ‘ 1 ) ) )
87 86 oveq1d ⊢ ( 𝑥 = 1 → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) )
88 ovex ⊢ ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) ∈ V
89 87 5 88 fvmpt ⊢ ( 1 ∈ 𝑇 → ( 𝐺 ‘ 1 ) = ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) )
90 70 89 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) )
91 84 90 seq1i ⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 1 ) = ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) )
92 91 oveq1d ⊢ ( 𝜑 → ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) = ( ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) mod 𝑁 ) )
93 63 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
94 93 exp1d ⊢ ( 𝜑 → ( 𝐴 ↑ 1 ) = 𝐴 )
95 seq1 ⊢ ( 1 ∈ ℤ → ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
96 84 95 ax-mp ⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 )
97 96 a1i ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
98 94 97 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = ( 𝐴 · ( 𝐹 ‘ 1 ) ) )
99 98 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 1 ) ) mod 𝑁 ) )
100 83 92 99 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) )
101 96 oveq2i ⊢ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = ( 𝑁 gcd ( 𝐹 ‘ 1 ) )
102 6 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
103 102 78 gcdcomd ⊢ ( 𝜑 → ( 𝑁 gcd ( 𝐹 ‘ 1 ) ) = ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) )
104 75 simprd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) = 1 )
105 103 104 eqtrd ⊢ ( 𝜑 → ( 𝑁 gcd ( 𝐹 ‘ 1 ) ) = 1 )
106 101 105 eqtrid ⊢ ( 𝜑 → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 )
107 100 106 jca ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 ) )
108 107 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 ) )
109 nnre ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℝ )
110 109 adantr ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → 𝑧 ∈ ℝ )
111 110 lep1d ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → 𝑧 ≤ ( 𝑧 + 1 ) )
112 peano2re ⊢ ( 𝑧 ∈ ℝ → ( 𝑧 + 1 ) ∈ ℝ )
113 110 112 syl ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → ( 𝑧 + 1 ) ∈ ℝ )
114 8 adantl ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → ( ϕ ‘ 𝑁 ) ∈ ℝ )
115 letr ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 + 1 ) ∈ ℝ ∧ ( ϕ ‘ 𝑁 ) ∈ ℝ ) → ( ( 𝑧 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
116 110 113 114 115 syl3anc ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → ( ( 𝑧 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
117 111 116 mpand ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → ( ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) → 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
118 117 imdistanda ⊢ ( 𝑧 ∈ ℕ → ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( 𝜑 ∧ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) ) )
119 118 imim1d ⊢ ( 𝑧 ∈ ℕ → ( ( ( 𝜑 ∧ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) ) → ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) ) ) )
120 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝐴 ∈ ℤ )
121 nnnn0 ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℕ0 )
122 121 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ℕ0 )
123 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑧 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑧 ) ∈ ℤ )
124 120 122 123 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 ↑ 𝑧 ) ∈ ℤ )
125 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ℕ )
126 125 66 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ( ℤ≥ ‘ 1 ) )
127 109 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ℝ )
128 127 112 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ ℝ )
129 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ϕ ‘ 𝑁 ) ∈ ℝ )
130 127 lep1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ≤ ( 𝑧 + 1 ) )
131 simprr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) )
132 127 128 129 130 131 letrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ≤ ( ϕ ‘ 𝑁 ) )
133 nnz ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℤ )
134 133 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ℤ )
135 7 nnzd ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℤ )
136 135 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ϕ ‘ 𝑁 ) ∈ ℤ )
137 eluz ⊢ ( ( 𝑧 ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℤ ) → ( ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑧 ) ↔ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
138 134 136 137 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑧 ) ↔ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
139 132 138 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑧 ) )
140 fzss2 ⊢ ( ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑧 ) → ( 1 ... 𝑧 ) ⊆ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
141 139 140 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 1 ... 𝑧 ) ⊆ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
142 141 3 sseqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 1 ... 𝑧 ) ⊆ 𝑇 )
143 142 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑧 ) ) → 𝑥 ∈ 𝑇 )
144 65 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
145 oveq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 gcd 𝑁 ) = ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) )
146 145 eqeq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
147 146 2 elrab2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
148 144 147 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
149 148 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
150 elfzoelz ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
151 149 150 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
152 151 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
153 143 152 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑧 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
154 zmulcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
155 154 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
156 126 153 155 seqcl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ∈ ℤ )
157 124 156 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) ∈ ℤ )
158 157 zred ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) ∈ ℝ )
159 2 ssrab3 ⊢ 𝑆 ⊆ ( 0 ..^ 𝑁 )
160 1 2 3 4 5 eulerthlem1 ⊢ ( 𝜑 → 𝐺 : 𝑇 ⟶ 𝑆 )
161 160 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑆 )
162 159 161 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
163 elfzoelz ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
164 162 163 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
165 164 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
166 143 165 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑧 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
167 126 166 155 seqcl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℤ )
168 167 zred ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℝ )
169 65 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝐹 : 𝑇 ⟶ 𝑆 )
170 peano2nn ⊢ ( 𝑧 ∈ ℕ → ( 𝑧 + 1 ) ∈ ℕ )
171 170 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ ℕ )
172 171 nnge1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 1 ≤ ( 𝑧 + 1 ) )
173 171 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ ℤ )
174 elfz ⊢ ( ( ( 𝑧 + 1 ) ∈ ℤ ∧ 1 ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝑧 + 1 ) ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ↔ ( 1 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) )
175 84 174 mp3an2 ⊢ ( ( ( 𝑧 + 1 ) ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝑧 + 1 ) ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ↔ ( 1 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) )
176 173 136 175 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝑧 + 1 ) ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ↔ ( 1 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) )
177 172 131 176 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
178 177 3 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ 𝑇 )
179 169 178 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ 𝑆 )
180 oveq1 ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑧 + 1 ) ) → ( 𝑦 gcd 𝑁 ) = ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) )
181 180 eqeq1d ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑧 + 1 ) ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) = 1 ) )
182 181 2 elrab2 ⊢ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ 𝑆 ↔ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) = 1 ) )
183 179 182 sylib ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) = 1 ) )
184 183 simpld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ( 0 ..^ 𝑁 ) )
185 elfzoelz ⊢ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℤ )
186 184 185 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℤ )
187 120 186 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℤ )
188 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑁 ∈ ℝ+ )
189 modmul1 ⊢ ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) ∈ ℝ ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℝ ) ∧ ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℝ+ ) ∧ ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) )
190 189 3expia ⊢ ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) ∈ ℝ ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℝ ) ∧ ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℝ+ ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) ) )
191 158 168 187 188 190 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) ) )
192 124 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 ↑ 𝑧 ) ∈ ℂ )
193 156 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ∈ ℂ )
194 93 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝐴 ∈ ℂ )
195 186 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℂ )
196 192 193 194 195 mul4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = ( ( ( 𝐴 ↑ 𝑧 ) · 𝐴 ) · ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) )
197 194 122 expp1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 ↑ ( 𝑧 + 1 ) ) = ( ( 𝐴 ↑ 𝑧 ) · 𝐴 ) )
198 seqp1 ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) )
199 126 198 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) )
200 197 199 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = ( ( ( 𝐴 ↑ 𝑧 ) · 𝐴 ) · ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) )
201 196 200 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) )
202 201 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
203 187 zred ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℝ )
204 203 188 modcld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ∈ ℝ )
205 modabs2 ⊢ ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
206 203 188 205 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
207 modmul1 ⊢ ( ( ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ∈ ℝ ∧ ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℝ ) ∧ ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℤ ∧ 𝑁 ∈ ℝ+ ) ∧ ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ) → ( ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) )
208 204 203 167 188 206 207 syl221anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) )
209 fveq2 ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑧 + 1 ) ) )
210 209 oveq2d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) )
211 210 oveq1d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
212 ovex ⊢ ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ∈ V
213 211 5 212 fvmpt ⊢ ( ( 𝑧 + 1 ) ∈ 𝑇 → ( 𝐺 ‘ ( 𝑧 + 1 ) ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
214 178 213 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐺 ‘ ( 𝑧 + 1 ) ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
215 214 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐺 ‘ ( 𝑧 + 1 ) ) ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ) )
216 seqp1 ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐺 ‘ ( 𝑧 + 1 ) ) ) )
217 126 216 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐺 ‘ ( 𝑧 + 1 ) ) ) )
218 204 recnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ∈ ℂ )
219 167 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℂ )
220 218 219 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ) )
221 215 217 220 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) = ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) )
222 221 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) = ( ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) )
223 187 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℂ )
224 219 223 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) )
225 224 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) )
226 208 222 225 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) )
227 202 226 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) ↔ ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ) )
228 191 227 sylibd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) → ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ) )
229 102 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑁 ∈ ℤ )
230 229 186 gcdcomd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) )
231 183 simprd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) = 1 )
232 230 231 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = 1 )
233 rpmul ⊢ ( ( 𝑁 ∈ ℤ ∧ ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ∈ ℤ ∧ ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℤ ) → ( ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ∧ ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = 1 ) → ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = 1 ) )
234 229 156 186 233 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ∧ ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = 1 ) → ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = 1 ) )
235 232 234 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 → ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = 1 ) )
236 199 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) )
237 236 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ↔ ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = 1 ) )
238 235 237 sylibrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) )
239 228 238 anim12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) → ( ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) ) )
240 239 an12s ⊢ ( ( 𝑧 ∈ ℕ ∧ ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) → ( ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) ) )
241 240 ex ⊢ ( 𝑧 ∈ ℕ → ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) → ( ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) ) ) )
242 241 a2d ⊢ ( 𝑧 ∈ ℕ → ( ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) ) → ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) ) ) )
243 119 242 syld ⊢ ( 𝑧 ∈ ℕ → ( ( ( 𝜑 ∧ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) ) → ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) ) ) )
244 23 36 49 62 108 243 nnind ⊢ ( ( ϕ ‘ 𝑁 ) ∈ ℕ → ( ( 𝜑 ∧ ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) ) )
245 10 244 mpcom ⊢ ( ( 𝜑 ∧ ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) )
246 9 245 mpdan ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) )
247 246 simpld ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) )
248 7 nnnn0d ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
249 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
250 63 248 249 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
251 3 eleq2i ⊢ ( 𝑥 ∈ 𝑇 ↔ 𝑥 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
252 251 151 sylan2br ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
253 154 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
254 67 252 253 seqcl ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
255 250 254 zmulcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ∈ ℤ )
256 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
257 256 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
258 mulcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
259 258 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
260 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
261 260 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
262 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
263 f1ocnv ⊢ ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 → ◡ 𝐹 : 𝑆 –1-1-onto→ 𝑇 )
264 4 263 syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑆 –1-1-onto→ 𝑇 )
265 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑁 ∈ ℕ )
266 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝐴 ∈ ℤ )
267 65 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑆 )
268 267 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑆 )
269 159 268 sselid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) )
270 elfzoelz ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℤ )
271 269 270 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℤ )
272 266 271 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ∈ ℤ )
273 65 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
274 273 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
275 159 274 sselid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ 𝑁 ) )
276 elfzoelz ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
277 275 276 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
278 266 277 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ )
279 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ∈ ℤ ∧ ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ ) → ( ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) − ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ) ) )
280 265 272 278 279 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) − ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ) ) )
281 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
282 281 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) )
283 282 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) )
284 ovex ⊢ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) ∈ V
285 283 5 284 fvmpt ⊢ ( 𝑦 ∈ 𝑇 → ( 𝐺 ‘ 𝑦 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) )
286 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
287 286 oveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) )
288 287 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) )
289 ovex ⊢ ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ∈ V
290 288 5 289 fvmpt ⊢ ( 𝑧 ∈ 𝑇 → ( 𝐺 ‘ 𝑧 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) )
291 285 290 eqeqan12d ⊢ ( ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ) )
292 291 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ) )
293 93 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝐴 ∈ ℂ )
294 271 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
295 277 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
296 293 294 295 subdid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) − ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ) )
297 296 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ↔ 𝑁 ∥ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) − ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ) ) )
298 280 292 297 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ) )
299 102 63 gcdcomd ⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = ( 𝐴 gcd 𝑁 ) )
300 1 simp3d ⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = 1 )
301 299 300 eqtrd ⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = 1 )
302 301 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑁 gcd 𝐴 ) = 1 )
303 102 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑁 ∈ ℤ )
304 271 277 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ )
305 coprmdvds ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ ) → ( ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ∧ ( 𝑁 gcd 𝐴 ) = 1 ) → 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
306 303 266 304 305 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ∧ ( 𝑁 gcd 𝐴 ) = 1 ) → 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
307 271 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
308 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑁 ∈ ℝ+ )
309 elfzole1 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
310 269 309 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
311 elfzolt2 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑦 ) < 𝑁 )
312 269 311 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) < 𝑁 )
313 modid ⊢ ( ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) < 𝑁 ) ) → ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( 𝐹 ‘ 𝑦 ) )
314 307 308 310 312 313 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( 𝐹 ‘ 𝑦 ) )
315 277 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
316 elfzole1 ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ 𝑁 ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
317 275 316 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
318 elfzolt2 ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑧 ) < 𝑁 )
319 275 318 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) < 𝑁 )
320 modid ⊢ ( ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) < 𝑁 ) ) → ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) = ( 𝐹 ‘ 𝑧 ) )
321 315 308 317 319 320 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) = ( 𝐹 ‘ 𝑧 ) )
322 314 321 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) )
323 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℤ ) → ( ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
324 265 271 277 323 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
325 f1of1 ⊢ ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 → 𝐹 : 𝑇 –1-1→ 𝑆 )
326 4 325 syl ⊢ ( 𝜑 → 𝐹 : 𝑇 –1-1→ 𝑆 )
327 f1fveq ⊢ ( ( 𝐹 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
328 326 327 sylan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
329 322 324 328 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ↔ 𝑦 = 𝑧 ) )
330 306 329 sylibd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ∧ ( 𝑁 gcd 𝐴 ) = 1 ) → 𝑦 = 𝑧 ) )
331 302 330 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) → 𝑦 = 𝑧 ) )
332 298 331 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
333 332 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑇 ∀ 𝑧 ∈ 𝑇 ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
334 dff13 ⊢ ( 𝐺 : 𝑇 –1-1→ 𝑆 ↔ ( 𝐺 : 𝑇 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝑇 ∀ 𝑧 ∈ 𝑇 ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
335 160 333 334 sylanbrc ⊢ ( 𝜑 → 𝐺 : 𝑇 –1-1→ 𝑆 )
336 3 ovexi ⊢ 𝑇 ∈ V
337 336 f1oen ⊢ ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 → 𝑇 ≈ 𝑆 )
338 4 337 syl ⊢ ( 𝜑 → 𝑇 ≈ 𝑆 )
339 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
340 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ 𝑆 ⊆ ( 0 ..^ 𝑁 ) ) → 𝑆 ∈ Fin )
341 339 159 340 mp2an ⊢ 𝑆 ∈ Fin
342 f1finf1o ⊢ ( ( 𝑇 ≈ 𝑆 ∧ 𝑆 ∈ Fin ) → ( 𝐺 : 𝑇 –1-1→ 𝑆 ↔ 𝐺 : 𝑇 –1-1-onto→ 𝑆 ) )
343 338 341 342 sylancl ⊢ ( 𝜑 → ( 𝐺 : 𝑇 –1-1→ 𝑆 ↔ 𝐺 : 𝑇 –1-1-onto→ 𝑆 ) )
344 335 343 mpbid ⊢ ( 𝜑 → 𝐺 : 𝑇 –1-1-onto→ 𝑆 )
345 f1oco ⊢ ( ( ◡ 𝐹 : 𝑆 –1-1-onto→ 𝑇 ∧ 𝐺 : 𝑇 –1-1-onto→ 𝑆 ) → ( ◡ 𝐹 ∘ 𝐺 ) : 𝑇 –1-1-onto→ 𝑇 )
346 264 344 345 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐺 ) : 𝑇 –1-1-onto→ 𝑇 )
347 f1oeq23 ⊢ ( ( 𝑇 = ( 1 ... ( ϕ ‘ 𝑁 ) ) ∧ 𝑇 = ( 1 ... ( ϕ ‘ 𝑁 ) ) ) → ( ( ◡ 𝐹 ∘ 𝐺 ) : 𝑇 –1-1-onto→ 𝑇 ↔ ( ◡ 𝐹 ∘ 𝐺 ) : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) )
348 3 3 347 mp2an ⊢ ( ( ◡ 𝐹 ∘ 𝐺 ) : 𝑇 –1-1-onto→ 𝑇 ↔ ( ◡ 𝐹 ∘ 𝐺 ) : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
349 346 348 sylib ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐺 ) : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
350 252 zcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
351 3 eleq2i ⊢ ( 𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
352 fvco3 ⊢ ( ( 𝐺 : 𝑇 ⟶ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) = ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) )
353 160 352 sylan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) = ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) )
354 353 fveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) )
355 4 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → 𝐹 : 𝑇 –1-1-onto→ 𝑆 )
356 160 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
357 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝐺 ‘ 𝑤 ) )
358 355 356 357 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝐺 ‘ 𝑤 ) )
359 354 358 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) ) )
360 351 359 sylan2br ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) ) )
361 257 259 261 67 262 349 350 360 seqf1o ⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) = ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) )
362 361 254 eqeltrd ⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
363 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ∈ ℤ ∧ ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ) → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
364 6 255 362 363 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
365 247 364 mpbid ⊢ ( 𝜑 → 𝑁 ∥ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) )
366 254 zcnd ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℂ )
367 366 mulid2d ⊢ ( 𝜑 → ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) )
368 361 367 eqtr4d ⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) = ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) )
369 368 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
370 250 zcnd ⊢ ( 𝜑 → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℂ )
371 ax-1cn ⊢ 1 ∈ ℂ
372 subdir ⊢ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℂ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
373 371 372 mp3an2 ⊢ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℂ ∧ ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℂ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
374 370 366 373 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
375 zsubcl ⊢ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ ℤ )
376 250 84 375 sylancl ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ ℤ )
377 376 zcnd ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ ℂ )
378 377 366 mulcomd ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
379 369 374 378 3eqtr2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
380 365 379 breqtrd ⊢ ( 𝜑 → 𝑁 ∥ ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
381 246 simprd ⊢ ( 𝜑 → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 )
382 coprmdvds ⊢ ( ( 𝑁 ∈ ℤ ∧ ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ∧ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ ℤ ) → ( ( 𝑁 ∥ ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) → 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
383 102 254 376 382 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ∥ ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) → 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
384 380 381 383 mp2and ⊢ ( 𝜑 → 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
385 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
386 84 385 mp3an3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
387 6 250 386 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
388 384 387 mpbird ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )