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 gcdcom ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐹 ‘ 1 ) ∈ ℤ ) → ( 𝑁 gcd ( 𝐹 ‘ 1 ) ) = ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) )
104 102 78 103 syl2anc ⊢ ( 𝜑 → ( 𝑁 gcd ( 𝐹 ‘ 1 ) ) = ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) )
105 75 simprd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 1 ) gcd 𝑁 ) = 1 )
106 104 105 eqtrd ⊢ ( 𝜑 → ( 𝑁 gcd ( 𝐹 ‘ 1 ) ) = 1 )
107 101 106 syl5eq ⊢ ( 𝜑 → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 )
108 100 107 jca ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 1 ) · ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 1 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = 1 ) )
110 nnre ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℝ )
111 110 adantr ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → 𝑧 ∈ ℝ )
112 111 lep1d ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → 𝑧 ≤ ( 𝑧 + 1 ) )
113 peano2re ⊢ ( 𝑧 ∈ ℝ → ( 𝑧 + 1 ) ∈ ℝ )
114 111 113 syl ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → ( 𝑧 + 1 ) ∈ ℝ )
115 8 adantl ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → ( ϕ ‘ 𝑁 ) ∈ ℝ )
116 letr ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 + 1 ) ∈ ℝ ∧ ( ϕ ‘ 𝑁 ) ∈ ℝ ) → ( ( 𝑧 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
117 111 114 115 116 syl3anc ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → ( ( 𝑧 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
118 112 117 mpand ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝜑 ) → ( ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) → 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
119 118 imdistanda ⊢ ( 𝑧 ∈ ℕ → ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( 𝜑 ∧ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) ) )
120 119 imim1d ⊢ ( 𝑧 ∈ ℕ → ( ( ( 𝜑 ∧ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) ) → ( ( 𝜑 ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ) ) ) )
121 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝐴 ∈ ℤ )
122 nnnn0 ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℕ0 )
123 122 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ℕ0 )
124 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑧 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑧 ) ∈ ℤ )
125 121 123 124 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 ↑ 𝑧 ) ∈ ℤ )
126 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ℕ )
127 126 66 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ( ℤ≥ ‘ 1 ) )
128 110 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ℝ )
129 128 113 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ ℝ )
130 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ϕ ‘ 𝑁 ) ∈ ℝ )
131 128 lep1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ≤ ( 𝑧 + 1 ) )
132 simprr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) )
133 128 129 130 131 132 letrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ≤ ( ϕ ‘ 𝑁 ) )
134 nnz ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℤ )
135 134 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑧 ∈ ℤ )
136 7 nnzd ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℤ )
137 136 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ϕ ‘ 𝑁 ) ∈ ℤ )
138 eluz ⊢ ( ( 𝑧 ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℤ ) → ( ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑧 ) ↔ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
139 135 137 138 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑧 ) ↔ 𝑧 ≤ ( ϕ ‘ 𝑁 ) ) )
140 133 139 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑧 ) )
141 fzss2 ⊢ ( ( ϕ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 𝑧 ) → ( 1 ... 𝑧 ) ⊆ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
142 140 141 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 1 ... 𝑧 ) ⊆ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
143 142 3 sseqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 1 ... 𝑧 ) ⊆ 𝑇 )
144 143 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑧 ) ) → 𝑥 ∈ 𝑇 )
145 65 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
146 oveq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 gcd 𝑁 ) = ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) )
147 146 eqeq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
148 147 2 elrab2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
149 145 148 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
150 149 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
151 elfzoelz ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
152 150 151 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
153 152 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
154 144 153 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑧 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
155 zmulcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
156 155 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
157 127 154 156 seqcl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ∈ ℤ )
158 125 157 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) ∈ ℤ )
159 158 zred ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) ∈ ℝ )
160 2 ssrab3 ⊢ 𝑆 ⊆ ( 0 ..^ 𝑁 )
161 1 2 3 4 5 eulerthlem1 ⊢ ( 𝜑 → 𝐺 : 𝑇 ⟶ 𝑆 )
162 161 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑆 )
163 160 162 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
164 elfzoelz ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
165 163 164 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
166 165 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
167 144 166 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑧 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℤ )
168 127 167 156 seqcl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℤ )
169 168 zred ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℝ )
170 65 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝐹 : 𝑇 ⟶ 𝑆 )
171 peano2nn ⊢ ( 𝑧 ∈ ℕ → ( 𝑧 + 1 ) ∈ ℕ )
172 171 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ ℕ )
173 172 nnge1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 1 ≤ ( 𝑧 + 1 ) )
174 172 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ ℤ )
175 elfz ⊢ ( ( ( 𝑧 + 1 ) ∈ ℤ ∧ 1 ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝑧 + 1 ) ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ↔ ( 1 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) )
176 84 175 mp3an2 ⊢ ( ( ( 𝑧 + 1 ) ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝑧 + 1 ) ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ↔ ( 1 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) )
177 174 137 176 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝑧 + 1 ) ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ↔ ( 1 ≤ ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) )
178 173 132 177 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
179 178 3 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑧 + 1 ) ∈ 𝑇 )
180 170 179 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ 𝑆 )
181 oveq1 ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑧 + 1 ) ) → ( 𝑦 gcd 𝑁 ) = ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) )
182 181 eqeq1d ⊢ ( 𝑦 = ( 𝐹 ‘ ( 𝑧 + 1 ) ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) = 1 ) )
183 182 2 elrab2 ⊢ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ 𝑆 ↔ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) = 1 ) )
184 180 183 sylib ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) = 1 ) )
185 184 simpld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ( 0 ..^ 𝑁 ) )
186 elfzoelz ⊢ ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℤ )
187 185 186 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℤ )
188 121 187 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℤ )
189 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑁 ∈ ℝ+ )
190 modmul1 ⊢ ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) ∈ ℝ ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℝ ) ∧ ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℝ+ ) ∧ ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) )
191 190 3expia ⊢ ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) ∈ ℝ ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℝ ) ∧ ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℝ+ ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) ) )
192 159 169 188 189 191 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) ) )
193 125 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 ↑ 𝑧 ) ∈ ℂ )
194 157 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ∈ ℂ )
195 93 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝐴 ∈ ℂ )
196 187 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℂ )
197 193 194 195 196 mul4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = ( ( ( 𝐴 ↑ 𝑧 ) · 𝐴 ) · ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) )
198 195 123 expp1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 ↑ ( 𝑧 + 1 ) ) = ( ( 𝐴 ↑ 𝑧 ) · 𝐴 ) )
199 seqp1 ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) )
200 127 199 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) )
201 198 200 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = ( ( ( 𝐴 ↑ 𝑧 ) · 𝐴 ) · ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) )
202 197 201 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) )
203 202 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
204 188 zred ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℝ )
205 204 189 modcld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ∈ ℝ )
206 modabs2 ⊢ ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
207 204 189 206 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
208 modmul1 ⊢ ( ( ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ∈ ℝ ∧ ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℝ ) ∧ ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℤ ∧ 𝑁 ∈ ℝ+ ) ∧ ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ) → ( ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) )
209 205 204 168 189 207 208 syl221anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) )
210 fveq2 ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑧 + 1 ) ) )
211 210 oveq2d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) )
212 211 oveq1d ⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
213 ovex ⊢ ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ∈ V
214 212 5 213 fvmpt ⊢ ( ( 𝑧 + 1 ) ∈ 𝑇 → ( 𝐺 ‘ ( 𝑧 + 1 ) ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
215 179 214 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐺 ‘ ( 𝑧 + 1 ) ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) )
216 215 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐺 ‘ ( 𝑧 + 1 ) ) ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ) )
217 seqp1 ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐺 ‘ ( 𝑧 + 1 ) ) ) )
218 127 217 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐺 ‘ ( 𝑧 + 1 ) ) ) )
219 205 recnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ∈ ℂ )
220 168 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ∈ ℂ )
221 219 220 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) ) )
222 216 218 221 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) = ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) )
223 222 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) = ( ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) )
224 188 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ℂ )
225 220 224 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) )
226 225 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) · ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) ) mod 𝑁 ) )
227 209 223 226 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) )
228 203 227 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) = ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) · ( 𝐴 · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) mod 𝑁 ) ↔ ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ) )
229 192 228 sylibd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 ↑ 𝑧 ) · ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ 𝑧 ) mod 𝑁 ) → ( ( ( 𝐴 ↑ ( 𝑧 + 1 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( 𝑧 + 1 ) ) mod 𝑁 ) ) )
230 102 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → 𝑁 ∈ ℤ )
231 gcdcom ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℤ ) → ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) )
232 230 187 231 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) )
233 184 simprd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝐹 ‘ ( 𝑧 + 1 ) ) gcd 𝑁 ) = 1 )
234 232 233 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = 1 )
235 rpmul ⊢ ( ( 𝑁 ∈ ℤ ∧ ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ∈ ℤ ∧ ( 𝐹 ‘ ( 𝑧 + 1 ) ) ∈ ℤ ) → ( ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ∧ ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = 1 ) → ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = 1 ) )
236 230 157 187 235 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 ∧ ( 𝑁 gcd ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = 1 ) → ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = 1 ) )
237 234 236 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 → ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = 1 ) )
238 200 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) )
239 238 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ↔ ( 𝑁 gcd ( ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) · ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = 1 ) )
240 237 239 sylibrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 1 ) ≤ ( ϕ ‘ 𝑁 ) ) ) → ( ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ 𝑧 ) ) = 1 → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) = 1 ) )
241 229 240 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 ) ) )
242 241 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 ) ) )
243 242 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 ) ) ) )
244 243 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 ) ) ) )
245 120 244 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 ) ) ) )
246 23 36 49 62 109 245 nnind ⊢ ( ( ϕ ‘ 𝑁 ) ∈ ℕ → ( ( 𝜑 ∧ ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) ) )
247 10 246 mpcom ⊢ ( ( 𝜑 ∧ ( ϕ ‘ 𝑁 ) ≤ ( ϕ ‘ 𝑁 ) ) → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) )
248 9 247 mpdan ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) )
249 248 simpld ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) )
250 7 nnnn0d ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
251 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
252 63 250 251 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
253 3 eleq2i ⊢ ( 𝑥 ∈ 𝑇 ↔ 𝑥 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
254 253 152 sylan2br ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
255 155 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
256 67 254 255 seqcl ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
257 252 256 zmulcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ∈ ℤ )
258 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
259 258 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
260 mulcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
261 260 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
262 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
263 262 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
264 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
265 f1ocnv ⊢ ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 → ◡ 𝐹 : 𝑆 –1-1-onto→ 𝑇 )
266 4 265 syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑆 –1-1-onto→ 𝑇 )
267 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑁 ∈ ℕ )
268 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝐴 ∈ ℤ )
269 65 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑆 )
270 269 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑆 )
271 160 270 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) )
272 elfzoelz ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℤ )
273 271 272 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℤ )
274 268 273 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ∈ ℤ )
275 65 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
276 275 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
277 160 276 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ 𝑁 ) )
278 elfzoelz ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
279 277 278 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℤ )
280 268 279 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ )
281 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ∈ ℤ ∧ ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ ) → ( ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) − ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ) ) )
282 267 274 280 281 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) − ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ) ) )
283 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
284 283 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) )
285 284 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) )
286 ovex ⊢ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) ∈ V
287 285 5 286 fvmpt ⊢ ( 𝑦 ∈ 𝑇 → ( 𝐺 ‘ 𝑦 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) )
288 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
289 288 oveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) )
290 289 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) )
291 ovex ⊢ ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ∈ V
292 290 5 291 fvmpt ⊢ ( 𝑧 ∈ 𝑇 → ( 𝐺 ‘ 𝑧 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) )
293 287 292 eqeqan12d ⊢ ( ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ) )
294 293 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) mod 𝑁 ) ) )
295 93 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝐴 ∈ ℂ )
296 273 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
297 279 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
298 295 296 297 subdid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) − ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ) )
299 298 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ↔ 𝑁 ∥ ( ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) − ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) ) ) )
300 282 294 299 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ) )
301 gcdcom ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑁 gcd 𝐴 ) = ( 𝐴 gcd 𝑁 ) )
302 102 63 301 syl2anc ⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = ( 𝐴 gcd 𝑁 ) )
303 1 simp3d ⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = 1 )
304 302 303 eqtrd ⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = 1 )
305 304 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑁 gcd 𝐴 ) = 1 )
306 102 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑁 ∈ ℤ )
307 273 279 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ )
308 coprmdvds ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ℤ ) → ( ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ∧ ( 𝑁 gcd 𝐴 ) = 1 ) → 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
309 306 268 307 308 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ∧ ( 𝑁 gcd 𝐴 ) = 1 ) → 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
310 273 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
311 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑁 ∈ ℝ+ )
312 elfzole1 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
313 271 312 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
314 elfzolt2 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑦 ) < 𝑁 )
315 271 314 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) < 𝑁 )
316 modid ⊢ ( ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) < 𝑁 ) ) → ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( 𝐹 ‘ 𝑦 ) )
317 310 311 313 315 316 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( 𝐹 ‘ 𝑦 ) )
318 279 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
319 elfzole1 ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ 𝑁 ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
320 277 319 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
321 elfzolt2 ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑧 ) < 𝑁 )
322 277 321 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑧 ) < 𝑁 )
323 modid ⊢ ( ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) < 𝑁 ) ) → ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) = ( 𝐹 ‘ 𝑧 ) )
324 318 311 320 322 323 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) = ( 𝐹 ‘ 𝑧 ) )
325 317 324 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) )
326 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℤ ) → ( ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
327 267 273 279 326 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) mod 𝑁 ) = ( ( 𝐹 ‘ 𝑧 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
328 f1of1 ⊢ ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 → 𝐹 : 𝑇 –1-1→ 𝑆 )
329 4 328 syl ⊢ ( 𝜑 → 𝐹 : 𝑇 –1-1→ 𝑆 )
330 f1fveq ⊢ ( ( 𝐹 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
331 329 330 sylan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
332 325 327 331 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑁 ∥ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ↔ 𝑦 = 𝑧 ) )
333 309 332 sylibd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) ∧ ( 𝑁 gcd 𝐴 ) = 1 ) → 𝑦 = 𝑧 ) )
334 305 333 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝑁 ∥ ( 𝐴 · ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) → 𝑦 = 𝑧 ) )
335 300 334 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
336 335 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑇 ∀ 𝑧 ∈ 𝑇 ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
337 dff13 ⊢ ( 𝐺 : 𝑇 –1-1→ 𝑆 ↔ ( 𝐺 : 𝑇 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝑇 ∀ 𝑧 ∈ 𝑇 ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
338 161 336 337 sylanbrc ⊢ ( 𝜑 → 𝐺 : 𝑇 –1-1→ 𝑆 )
339 3 ovexi ⊢ 𝑇 ∈ V
340 339 f1oen ⊢ ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 → 𝑇 ≈ 𝑆 )
341 4 340 syl ⊢ ( 𝜑 → 𝑇 ≈ 𝑆 )
342 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
343 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ 𝑆 ⊆ ( 0 ..^ 𝑁 ) ) → 𝑆 ∈ Fin )
344 342 160 343 mp2an ⊢ 𝑆 ∈ Fin
345 f1finf1o ⊢ ( ( 𝑇 ≈ 𝑆 ∧ 𝑆 ∈ Fin ) → ( 𝐺 : 𝑇 –1-1→ 𝑆 ↔ 𝐺 : 𝑇 –1-1-onto→ 𝑆 ) )
346 341 344 345 sylancl ⊢ ( 𝜑 → ( 𝐺 : 𝑇 –1-1→ 𝑆 ↔ 𝐺 : 𝑇 –1-1-onto→ 𝑆 ) )
347 338 346 mpbid ⊢ ( 𝜑 → 𝐺 : 𝑇 –1-1-onto→ 𝑆 )
348 f1oco ⊢ ( ( ◡ 𝐹 : 𝑆 –1-1-onto→ 𝑇 ∧ 𝐺 : 𝑇 –1-1-onto→ 𝑆 ) → ( ◡ 𝐹 ∘ 𝐺 ) : 𝑇 –1-1-onto→ 𝑇 )
349 266 347 348 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐺 ) : 𝑇 –1-1-onto→ 𝑇 )
350 f1oeq23 ⊢ ( ( 𝑇 = ( 1 ... ( ϕ ‘ 𝑁 ) ) ∧ 𝑇 = ( 1 ... ( ϕ ‘ 𝑁 ) ) ) → ( ( ◡ 𝐹 ∘ 𝐺 ) : 𝑇 –1-1-onto→ 𝑇 ↔ ( ◡ 𝐹 ∘ 𝐺 ) : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) )
351 3 3 350 mp2an ⊢ ( ( ◡ 𝐹 ∘ 𝐺 ) : 𝑇 –1-1-onto→ 𝑇 ↔ ( ◡ 𝐹 ∘ 𝐺 ) : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
352 349 351 sylib ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐺 ) : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
353 254 zcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
354 3 eleq2i ⊢ ( 𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) )
355 fvco3 ⊢ ( ( 𝐺 : 𝑇 ⟶ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) = ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) )
356 161 355 sylan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) = ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) )
357 356 fveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) )
358 4 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → 𝐹 : 𝑇 –1-1-onto→ 𝑆 )
359 161 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
360 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝐺 ‘ 𝑤 ) )
361 358 359 360 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝐺 ‘ 𝑤 ) )
362 357 361 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) ) )
363 354 362 sylan2br ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( ( ◡ 𝐹 ∘ 𝐺 ) ‘ 𝑤 ) ) )
364 259 261 263 67 264 352 353 363 seqf1o ⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) = ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) )
365 364 256 eqeltrd ⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℤ )
366 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ∈ ℤ ∧ ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ) → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
367 6 257 365 366 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) mod 𝑁 ) = ( ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
368 249 367 mpbid ⊢ ( 𝜑 → 𝑁 ∥ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) )
369 256 zcnd ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℂ )
370 369 mulid2d ⊢ ( 𝜑 → ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) )
371 364 370 eqtr4d ⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) = ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) )
372 371 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
373 252 zcnd ⊢ ( 𝜑 → ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℂ )
374 ax-1cn ⊢ 1 ∈ ℂ
375 subdir ⊢ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℂ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
376 374 375 mp3an2 ⊢ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℂ ∧ ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℂ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
377 373 369 376 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( 1 · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) ) )
378 zsubcl ⊢ ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ ℤ )
379 252 84 378 sylancl ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ ℤ )
380 379 zcnd ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ ℂ )
381 380 369 mulcomd ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
382 372 377 381 3eqtr2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) · ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) − ( seq 1 ( · , 𝐺 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
383 368 382 breqtrd ⊢ ( 𝜑 → 𝑁 ∥ ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
384 248 simprd ⊢ ( 𝜑 → ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 )
385 coprmdvds ⊢ ( ( 𝑁 ∈ ℤ ∧ ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ∧ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ ℤ ) → ( ( 𝑁 ∥ ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) → 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
386 102 256 379 385 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ∥ ( ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) · ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ∧ ( 𝑁 gcd ( seq 1 ( · , 𝐹 ) ‘ ( ϕ ‘ 𝑁 ) ) ) = 1 ) → 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
387 383 384 386 mp2and ⊢ ( 𝜑 → 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
388 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
389 84 388 mp3an3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) ∈ ℤ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
390 6 252 389 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
391 387 390 mpbird ⊢ ( 𝜑 → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )