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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑆 )
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	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ( 𝑧 + 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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑆 )
268	267	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑆 )
269	159 268	sselid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) )
270		elfzoelz	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℤ )
271	269 270	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℤ )
272	266 271	zmulcld	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ∈ ℤ )
273	65	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
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	mullidd	⊢ ( 𝜑 → ( 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 𝑁 ) )