eulerthlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > eulerthlem2		Structured version Visualization version GIF version

Theorem eulerthlem2 16789

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

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

**Assertion**
Ref	Expression
eulerthlem2	⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐹,𝑦 𝑥,𝐺,𝑦 𝑥,𝑁,𝑦 𝑥,𝑆 𝜑,𝑥,𝑦 𝑥,𝑇,𝑦 Allowed substitution hint: 𝑆(𝑦)

Proof of Theorem eulerthlem2 Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerth.1	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))
2	1	simp1d 1151	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	phicld 16779	. . . . . . . . 9 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
4	3	nnred 12211	. . . . . . . 8 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℝ)
5	4	leidd 11739	. . . . . . 7 ⊢ (𝜑 → (ϕ‘𝑁) ≤ (ϕ‘𝑁))
6	3	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → (ϕ‘𝑁) ∈ ℕ)
7		breq1 5093	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 ≤ (ϕ‘𝑁) ↔ 1 ≤ (ϕ‘𝑁)))
8	7	anbi2d 638	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 1 ≤ (ϕ‘𝑁))))
9		oveq2 7389	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝐴↑𝑥) = (𝐴↑1))
10		fveq2 6852	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
11	9, 10	oveq12d 7399	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑1) · (seq1( · , 𝐹)‘1)))
12	11	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁))
13		fveq2 6852	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘1))
14	13	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))
15	12, 14	eqeq12d 2768	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)))
16	10	oveq2d 7397	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘1)))
17	16	eqeq1d 2754	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
18	15, 17	anbi12d 640	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)))
19	8, 18	imbi12d 346	. . . . . . . . 9 ⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))))
20		breq1 5093	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥 ≤ (ϕ‘𝑁) ↔ 𝑧 ≤ (ϕ‘𝑁)))
21	20	anbi2d 638	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁))))
22		oveq2 7389	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧))
23		fveq2 6852	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑧))
24	22, 23	oveq12d 7399	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)))
25	24	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁))
26		fveq2 6852	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘𝑧))
27	26	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁))
28	25, 27	eqeq12d 2768	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)))
29	23	oveq2d 7397	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘𝑧)))
30	29	eqeq1d 2754	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))
31	28, 30	anbi12d 640	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)))
32	21, 31	imbi12d 346	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))))
33		breq1 5093	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → (𝑥 ≤ (ϕ‘𝑁) ↔ (𝑧 + 1) ≤ (ϕ‘𝑁)))
34	33	anbi2d 638	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 + 1) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
35		oveq2 7389	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑧 + 1) → (𝐴↑𝑥) = (𝐴↑(𝑧 + 1)))
36		fveq2 6852	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑧 + 1)))
37	35, 36	oveq12d 7399	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑧 + 1) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))))
38	37	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁))
39		fveq2 6852	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(𝑧 + 1)))
40	39	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))
41	38, 40	eqeq12d 2768	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
42	36	oveq2d 7397	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))))
43	42	eqeq1d 2754	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))
44	41, 43	anbi12d 640	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 + 1) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
45	34, 44	imbi12d 346	. . . . . . . . 9 ⊢ (𝑥 = (𝑧 + 1) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))))
46		breq1 5093	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → (𝑥 ≤ (ϕ‘𝑁) ↔ (ϕ‘𝑁) ≤ (ϕ‘𝑁)))
47	46	anbi2d 638	. . . . . . . . . 10 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁))))
48		oveq2 7389	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (ϕ‘𝑁) → (𝐴↑𝑥) = (𝐴↑(ϕ‘𝑁)))
49		fveq2 6852	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
50	48, 49	oveq12d 7399	. . . . . . . . . . . . 13 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))))
51	50	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁))
52		fveq2 6852	. . . . . . . . . . . . 13 ⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(ϕ‘𝑁)))
53	52	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))
54	51, 53	eqeq12d 2768	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)))
55	49	oveq2d 7397	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))))
56	55	eqeq1d 2754	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))
57	54, 56	anbi12d 640	. . . . . . . . . 10 ⊢ (𝑥 = (ϕ‘𝑁) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)))
58	47, 57	imbi12d 346	. . . . . . . . 9 ⊢ (𝑥 = (ϕ‘𝑁) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))))
59	1	simp2d 1152	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℤ)
60		eulerth.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)
61		f1of 6791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇⟶𝑆)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹:𝑇⟶𝑆)
63		nnuz 12864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
64	3, 63	eleqtrdi 2862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (ℤ_≥‘1))
65		eluzfz1 13522	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘1) → 1 ∈ (1...(ϕ‘𝑁)))
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ (1...(ϕ‘𝑁)))
67		eulerth.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑇 = (1...(ϕ‘𝑁))
68	66, 67	eleqtrrdi 2863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ 𝑇)
69	62, 68	ffvelcdmd 7051	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘1) ∈ 𝑆)
70		oveq1 7388	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝐹‘1) → (𝑦 gcd 𝑁) = ((𝐹‘1) gcd 𝑁))
71	70	eqeq1d 2754	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝐹‘1) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘1) gcd 𝑁) = 1))
72		eulerth.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
73	71, 72	elrab2 3644	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘1) ∈ 𝑆 ↔ ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1))
74	69, 73	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1))
75	74	simpld 497	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘1) ∈ (0..^𝑁))
76		elfzoelz 13650	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘1) ∈ (0..^𝑁) → (𝐹‘1) ∈ ℤ)
77	75, 76	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘1) ∈ ℤ)
78	59, 77	zmulcld 12669	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ)
79	78	zred 12663	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℝ)
80	2	nnrpd 13021	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
81		modabs2 13901	. . . . . . . . . . . . 13 ⊢ (((𝐴 · (𝐹‘1)) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
82	79, 80, 81	syl2anc 592	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
83		1z 12587	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
84		fveq2 6852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1))
85	84	oveq2d 7397	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
86	85	oveq1d 7396	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
87		eulerth.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))
88		ovex 7414	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ V
89	86, 87, 88	fvmpt 6960	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ 𝑇 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
90	68, 89	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
91	83, 90	seq1i 14014	. . . . . . . . . . . . 13 ⊢ (𝜑 → (seq1( · , 𝐺)‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
92	91	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝜑 → ((seq1( · , 𝐺)‘1) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁))
93	59	zcnd 12664	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℂ)
94	93	exp1d 14140	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴↑1) = 𝐴)
95		seq1 14013	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
96	83, 95	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (seq1( · , 𝐹)‘1) = (𝐹‘1)
97	96	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (seq1( · , 𝐹)‘1) = (𝐹‘1))
98	94, 97	oveq12d 7399	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴↑1) · (seq1( · , 𝐹)‘1)) = (𝐴 · (𝐹‘1)))
99	98	oveq1d 7396	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
100	82, 92, 99	3eqtr4rd 2798	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))
101	96	oveq2i 7392	. . . . . . . . . . . 12 ⊢ (𝑁 gcd (seq1( · , 𝐹)‘1)) = (𝑁 gcd (𝐹‘1))
102	2	nnzd 12580	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
103	102, 77	gcdcomd 16520	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁))
104	74	simprd 498	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹‘1) gcd 𝑁) = 1)
105	103, 104	eqtrd 2787	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = 1)
106	101, 105	eqtrid 2799	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)
107	100, 106	jca 518	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
108	107	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
109		nnre 12203	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
110	109	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ∈ ℝ)
111	110	lep1d 12109	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ≤ (𝑧 + 1))
112		peano2re 11342	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ → (𝑧 + 1) ∈ ℝ)
113	110, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (𝑧 + 1) ∈ ℝ)
114	4	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (ϕ‘𝑁) ∈ ℝ)
115		letr 11263	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ (𝑧 + 1) ∈ ℝ ∧ (ϕ‘𝑁) ∈ ℝ) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁)))
116	110, 113, 114, 115	syl3anc 1382	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁)))
117	111, 116	mpand 703	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 + 1) ≤ (ϕ‘𝑁) → 𝑧 ≤ (ϕ‘𝑁)))
118	117	imdistanda 578	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁))))
119	118	imim1d 82	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))))
120	59	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℤ)
121		nnnn0 12474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ₀)
122	121	ad2antrl 736	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ₀)
123		zexpcl 14075	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℤ ∧ 𝑧 ∈ ℕ₀) → (𝐴↑𝑧) ∈ ℤ)
124	120, 122, 123	syl2anc 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℤ)
125		simprl 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ)
126	125, 63	eleqtrdi 2862	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ (ℤ_≥‘1))
127	109	ad2antrl 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℝ)
128	127, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℝ)
129	4	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℝ)
130	127	lep1d 12109	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (𝑧 + 1))
131		simprr 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ≤ (ϕ‘𝑁))
132	127, 128, 129, 130, 131	letrd 11326	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (ϕ‘𝑁))
133		nnz 12575	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
134	133	ad2antrl 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℤ)
135	3	nnzd 12580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℤ)
136	135	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℤ)
137		eluz 12839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁)))
138	134, 136, 137	syl2anc 592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁)))
139	132, 138	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ (ℤ_≥‘𝑧))
140		fzss2 13555	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) → (1...𝑧) ⊆ (1...(ϕ‘𝑁)))
141	139, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ (1...(ϕ‘𝑁)))
142	141, 67	sseqtrrdi 3968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ 𝑇)
143	142	sselda 3927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → 𝑥 ∈ 𝑇)
144	62	ffvelcdmda 7050	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ 𝑆)
145		oveq1 7388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 gcd 𝑁) = ((𝐹‘𝑥) gcd 𝑁))
146	145	eqeq1d 2754	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝐹‘𝑥) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘𝑥) gcd 𝑁) = 1))
147	146, 72	elrab2 3644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑥) ∈ 𝑆 ↔ ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1))
148	144, 147	sylib 220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1))
149	148	simpld 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ (0..^𝑁))
150		elfzoelz 13650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ ℤ)
151	149, 150	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ)
152	151	adantlr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ)
153	143, 152	syldan 599	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐹‘𝑥) ∈ ℤ)
154		zmulcl 12606	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ)
155	154	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ)
156	126, 153, 155	seqcl 14021	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℤ)
157	124, 156	zmulcld 12669	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℤ)
158	157	zred 12663	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ)
159	72	ssrab3 4026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 ⊆ (0..^𝑁)
160	1, 72, 67, 60, 87	eulerthlem1 16788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐺:𝑇⟶𝑆)
161	160	ffvelcdmda 7050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ 𝑆)
162	159, 161	sselid 3925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ (0..^𝑁))
163		elfzoelz 13650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑥) ∈ (0..^𝑁) → (𝐺‘𝑥) ∈ ℤ)
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ)
165	164	adantlr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ)
166	143, 165	syldan 599	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐺‘𝑥) ∈ ℤ)
167	126, 166, 155	seqcl 14021	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℤ)
168	167	zred 12663	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℝ)
169	62	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐹:𝑇⟶𝑆)
170		peano2nn 12208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈ ℕ)
171	170	ad2antrl 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℕ)
172	171	nnge1d 12247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 1 ≤ (𝑧 + 1))
173	171	nnzd 12580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℤ)
174		elfz 13504	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑧 + 1) ∈ ℤ ∧ 1 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
175	83, 174	mp3an2 1460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑧 + 1) ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
176	173, 136, 175	syl2anc 592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
177	172, 131, 176	mpbir2and 721	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ (1...(ϕ‘𝑁)))
178	177, 67	eleqtrrdi 2863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ 𝑇)
179	169, 178	ffvelcdmd 7051	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ 𝑆)
180		oveq1 7388	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → (𝑦 gcd 𝑁) = ((𝐹‘(𝑧 + 1)) gcd 𝑁))
181	180	eqeq1d 2754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
182	181, 72	elrab2 3644	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑧 + 1)) ∈ 𝑆 ↔ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
183	179, 182	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
184	183	simpld 497	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ (0..^𝑁))
185		elfzoelz 13650	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) → (𝐹‘(𝑧 + 1)) ∈ ℤ)
186	184, 185	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℤ)
187	120, 186	zmulcld 12669	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ)
188	80	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℝ⁺)
189		modmul1 13923	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · , 𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ⁺) ∧ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))
190	189	3expia 1130	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · , 𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ⁺)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)))
191	158, 168, 187, 188, 190	syl22anc 847	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)))
192	124	zcnd 12664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℂ)
193	156	zcnd 12664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℂ)
194	93	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℂ)
195	186	zcnd 12664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℂ)
196	192, 193, 194, 195	mul4d 11381	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
197	194, 122	expp1d 14146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑(𝑧 + 1)) = ((𝐴↑𝑧) · 𝐴))
198		seqp1 14015	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℤ_≥‘1) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))
199	126, 198	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))
200	197, 199	oveq12d 7399	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
201	196, 200	eqtr4d 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))))
202	201	oveq1d 7396	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁))
203	187	zred 12663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ)
204	203, 188	modcld 13871	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ)
205		modabs2 13901	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
206	203, 188, 205	syl2anc 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
207		modmul1 13923	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ ∧ (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ) ∧ ((seq1( · , 𝐺)‘𝑧) ∈ ℤ ∧ 𝑁 ∈ ℝ⁺) ∧ (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
208	204, 203, 167, 188, 206, 207	syl221anc 1392	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
209		fveq2 6852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑧 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑧 + 1)))
210	209	oveq2d 7397	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑧 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑧 + 1))))
211	210	oveq1d 7396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑧 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
212		ovex 7414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ V
213	211, 87, 212	fvmpt 6960	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 + 1) ∈ 𝑇 → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
214	178, 213	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
215	214	oveq2d 7397	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)))
216		seqp1 14015	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℤ_≥‘1) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))))
217	126, 216	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))))
218	204	recnd 11196	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℂ)
219	167	zcnd 12664	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℂ)
220	218, 219	mulcomd 11189	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)))
221	215, 217, 220	3eqtr4d 2797	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)))
222	221	oveq1d 7396	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
223	187	zcnd 12664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℂ)
224	219, 223	mulcomd 11189	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)))
225	224	oveq1d 7396	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
226	208, 222, 225	3eqtr4rd 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))
227	202, 226	eqeq12d 2768	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
228	191, 227	sylibd 241	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
229	102	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℤ)
230	229, 186	gcdcomd 16520	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = ((𝐹‘(𝑧 + 1)) gcd 𝑁))
231	183	simprd 498	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)
232	230, 231	eqtrd 2787	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1)
233		rpmul 16665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ (seq1( · , 𝐹)‘𝑧) ∈ ℤ ∧ (𝐹‘(𝑧 + 1)) ∈ ℤ) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
234	229, 156, 186, 233	syl3anc 1382	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
235	232, 234	mpan2d 702	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
236	199	oveq2d 7397	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
237	236	eqeq1d 2754	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1 ↔ (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
238	235, 237	sylibrd 261	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))
239	228, 238	anim12d 617	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
240	239	an12s 657	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℕ ∧ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
241	240	ex 415	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))))
242	241	a2d 29	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))))
243	119, 242	syld 47	. . . . . . . . 9 ⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))))
244	19, 32, 45, 58, 108, 243	nnind 12214	. . . . . . . 8 ⊢ ((ϕ‘𝑁) ∈ ℕ → ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)))
245	6, 244	mpcom 38	. . . . . . 7 ⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))
246	5, 245	mpdan 695	. . . . . 6 ⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))
247	246	simpld 497	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))
248	3	nnnn0d 12528	. . . . . . . 8 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ₀)
249		zexpcl 14075	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℕ₀) → (𝐴↑(ϕ‘𝑁)) ∈ ℤ)
250	59, 248, 249	syl2anc 592	. . . . . . 7 ⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℤ)
251	67	eleq2i 2844	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ (1...(ϕ‘𝑁)))
252	251, 151	sylan2br 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℤ)
253	154	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ)
254	64, 252, 253	seqcl 14021	. . . . . . 7 ⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ)
255	250, 254	zmulcld 12669	. . . . . 6 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈ ℤ)
256		mulcl 11143	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
257	256	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
258		mulcom 11145	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
259	258	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
260		mulass 11147	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
261	260	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
262		ssidd 3950	. . . . . . . 8 ⊢ (𝜑 → ℂ ⊆ ℂ)
263		f1ocnv 6804	. . . . . . . . . . 11 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → ^◡𝐹:𝑆–1-1-onto→𝑇)
264	60, 263	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹:𝑆–1-1-onto→𝑇)
265	2	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℕ)
266	59	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℤ)
267	62	ffvelcdmda 7050	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → (𝐹‘𝑦) ∈ 𝑆)
268	267	adantrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ 𝑆)
269	159, 268	sselid 3925	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ (0..^𝑁))
270		elfzoelz 13650	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) ∈ ℤ)
271	269, 270	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℤ)
272	266, 271	zmulcld 12669	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑦)) ∈ ℤ)
273	62	ffvelcdmda 7050	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑇) → (𝐹‘𝑧) ∈ 𝑆)
274	273	adantrl 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ 𝑆)
275	159, 274	sselid 3925	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ (0..^𝑁))
276		elfzoelz 13650	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) ∈ ℤ)
277	275, 276	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℤ)
278	266, 277	zmulcld 12669	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑧)) ∈ ℤ)
279		moddvds 16269	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 · (𝐹‘𝑦)) ∈ ℤ ∧ (𝐴 · (𝐹‘𝑧)) ∈ ℤ) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
280	265, 272, 278, 279	syl3anc 1382	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
281		fveq2 6852	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
282	281	oveq2d 7397	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑦)))
283	282	oveq1d 7396	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁))
284		ovex 7414	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) ∈ V
285	283, 87, 284	fvmpt 6960	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝑇 → (𝐺‘𝑦) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁))
286		fveq2 6852	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
287	286	oveq2d 7397	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑧)))
288	287	oveq1d 7396	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑧 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))
289		ovex 7414	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ∈ V
290	288, 87, 289	fvmpt 6960	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑇 → (𝐺‘𝑧) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))
291	285, 290	eqeqan12d 2766	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)))
292	291	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)))
293	93	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℂ)
294	271	zcnd 12664	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℂ)
295	277	zcnd 12664	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℂ)
296	293, 294, 295	subdid 11629	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) = ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))
297	296	breq2d 5102	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
298	280, 292, 297	3bitr4d 313	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ 𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧)))))
299	102, 59	gcdcomd 16520	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁))
300	1	simp3d 1153	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 gcd 𝑁) = 1)
301	299, 300	eqtrd 2787	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 gcd 𝐴) = 1)
302	301	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 gcd 𝐴) = 1)
303	102	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℤ)
304	271, 277	zsubcld 12668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ)
305		coprmdvds 16659	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
306	303, 266, 304, 305	syl3anc 1382	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
307	271	zred 12663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℝ)
308	80	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℝ⁺)
309		elfzole1 13659	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑦))
310	269, 309	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑦))
311		elfzolt2 13660	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) < 𝑁)
312	269, 311	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) < 𝑁)
313		modid 13892	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑦) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) ∧ (0 ≤ (𝐹‘𝑦) ∧ (𝐹‘𝑦) < 𝑁)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦))
314	307, 308, 310, 312, 313	syl22anc 847	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦))
315	277	zred 12663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℝ)
316		elfzole1 13659	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑧))
317	275, 316	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑧))
318		elfzolt2 13660	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) < 𝑁)
319	275, 318	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) < 𝑁)
320		modid 13892	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑧) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) ∧ (0 ≤ (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑁)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧))
321	315, 308, 317, 319, 320	syl22anc 847	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧))
322	314, 321	eqeq12d 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ (𝐹‘𝑦) = (𝐹‘𝑧)))
323		moddvds 16269	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ (𝐹‘𝑦) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
324	265, 271, 277, 323	syl3anc 1382	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
325		f1of1 6790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇–1-1→𝑆)
326	60, 325	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:𝑇–1-1→𝑆)
327		f1fveq 7231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝑇–1-1→𝑆 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧))
328	326, 327	sylan 588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧))
329	322, 324, 328	3bitr3d 311	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)) ↔ 𝑦 = 𝑧))
330	306, 329	sylibd 241	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑦 = 𝑧))
331	302, 330	mpan2d 702	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) → 𝑦 = 𝑧))
332	298, 331	sylbid 242	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))
333	332	ralrimivva 3195	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))
334		dff13 7223	. . . . . . . . . . . 12 ⊢ (𝐺:𝑇–1-1→𝑆 ↔ (𝐺:𝑇⟶𝑆 ∧ ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)))
335	160, 333, 334	sylanbrc 591	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:𝑇–1-1→𝑆)
336	67	ovexi 7415	. . . . . . . . . . . . . 14 ⊢ 𝑇 ∈ V
337	336	f1oen 8938	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝑇 ≈ 𝑆)
338	60, 337	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ≈ 𝑆)
339		fzofi 13973	. . . . . . . . . . . . 13 ⊢ (0..^𝑁) ∈ Fin
340		ssfi 9126	. . . . . . . . . . . . 13 ⊢ (((0..^𝑁) ∈ Fin ∧ 𝑆 ⊆ (0..^𝑁)) → 𝑆 ∈ Fin)
341	339, 159, 340	mp2an 700	. . . . . . . . . . . 12 ⊢ 𝑆 ∈ Fin
342		f1finf1o 9202	. . . . . . . . . . . 12 ⊢ ((𝑇 ≈ 𝑆 ∧ 𝑆 ∈ Fin) → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆))
343	338, 341, 342	sylancl 594	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆))
344	335, 343	mpbid 234	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝑇–1-1-onto→𝑆)
345		f1oco 6815	. . . . . . . . . 10 ⊢ ((^◡𝐹:𝑆–1-1-onto→𝑇 ∧ 𝐺:𝑇–1-1-onto→𝑆) → (^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇)
346	264, 344, 345	syl2anc 592	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇)
347		f1oeq23 6782	. . . . . . . . . 10 ⊢ ((𝑇 = (1...(ϕ‘𝑁)) ∧ 𝑇 = (1...(ϕ‘𝑁))) → ((^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))))
348	67, 67, 347	mp2an 700	. . . . . . . . 9 ⊢ ((^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))
349	346, 348	sylib 220	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))
350	252	zcnd 12664	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℂ)
351	67	eleq2i 2844	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ (1...(ϕ‘𝑁)))
352		fvco3 6952	. . . . . . . . . . . 12 ⊢ ((𝐺:𝑇⟶𝑆 ∧ 𝑤 ∈ 𝑇) → ((^◡𝐹 ∘ 𝐺)‘𝑤) = (^◡𝐹‘(𝐺‘𝑤)))
353	160, 352	sylan 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((^◡𝐹 ∘ 𝐺)‘𝑤) = (^◡𝐹‘(𝐺‘𝑤)))
354	353	fveq2d 6856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)) = (𝐹‘(^◡𝐹‘(𝐺‘𝑤))))
355	60	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝐹:𝑇–1-1-onto→𝑆)
356	160	ffvelcdmda 7050	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) ∈ 𝑆)
357		f1ocnvfv2 7246	. . . . . . . . . . 11 ⊢ ((𝐹:𝑇–1-1-onto→𝑆 ∧ (𝐺‘𝑤) ∈ 𝑆) → (𝐹‘(^◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤))
358	355, 356, 357	syl2anc 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘(^◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤))
359	354, 358	eqtr2d 2788	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) = (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)))
360	351, 359	sylan2br 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (1...(ϕ‘𝑁))) → (𝐺‘𝑤) = (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)))
361	257, 259, 261, 64, 262, 349, 350, 360	seqf1o 14042	. . . . . . 7 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
362	361, 254	eqeltrd 2852	. . . . . 6 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈ ℤ)
363		moddvds 16269	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈ ℤ ∧ (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈ ℤ) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁)))))
364	2, 255, 362, 363	syl3anc 1382	. . . . 5 ⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁)))))
365	247, 364	mpbid 234	. . . 4 ⊢ (𝜑 → 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))))
366	254	zcnd 12664	. . . . . . . 8 ⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ)
367	366	mullidd 11186	. . . . . . 7 ⊢ (𝜑 → (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
368	361, 367	eqtr4d 2790	. . . . . 6 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁))))
369	368	oveq2d 7397	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
370	250	zcnd 12664	. . . . . 6 ⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℂ)
371		ax-1cn 11117	. . . . . . 7 ⊢ 1 ∈ ℂ
372		subdir 11607	. . . . . . 7 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
373	371, 372	mp3an2 1460	. . . . . 6 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
374	370, 366, 373	syl2anc 592	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
375		zsubcl 12599	. . . . . . . 8 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ)
376	250, 83, 375	sylancl 594	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ)
377	376	zcnd 12664	. . . . . 6 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℂ)
378	377, 366	mulcomd 11189	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
379	369, 374, 378	3eqtr2d 2793	. . . 4 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
380	365, 379	breqtrd 5116	. . 3 ⊢ (𝜑 → 𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
381	246	simprd 498	. . 3 ⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)
382		coprmdvds 16659	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ ∧ ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ) → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
383	102, 254, 376, 382	syl3anc 1382	. . 3 ⊢ (𝜑 → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
384	380, 381, 383	mp2and 707	. 2 ⊢ (𝜑 → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))
385		moddvds 16269	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
386	83, 385	mp3an3 1461	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
387	2, 250, 386	syl2anc 592	. 2 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
388	384, 387	mpbird 259	1 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1095 = wceq 1550 ∈ wcel 2132 ∀wral 3066 {crab 3404 ⊆ wss 3895 class class class wbr 5090 ↦ cmpt 5171 ^◡ccnv 5635 ∘ ccom 5640 ⟶wf 6502 –1-1→wf1 6503 –1-1-onto→wf1o 6505 ‘cfv 6506 (class class class)co 7381 ≈ cen 8909 Fincfn 8912 ℂcc 11057 ℝcr 11058 0cc0 11059 1c1 11060 + caddc 11062 · cmul 11064 < clt 11202 ≤ cle 11203 − cmin 11400 ℕcn 12196 ℕ₀cn0 12467 ℤcz 12554 ℤ_≥cuz 12825 ℝ⁺crp 12979 ...cfz 13498 ..^cfzo 13645 mod cmo 13865 seqcseq 14000 ↑cexp 14060 ∥ cdvds 16258 gcd cgcd 16500 ϕcphi 16771

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-10 2165 ax-11 2181 ax-12 2202 ax-ext 2724 ax-rep 5217 ax-sep 5236 ax-nul 5246 ax-pow 5312 ax-pr 5380 ax-un 7703 ax-cnex 11115 ax-resscn 11116 ax-1cn 11117 ax-icn 11118 ax-addcl 11119 ax-addrcl 11120 ax-mulcl 11121 ax-mulrcl 11122 ax-mulcom 11123 ax-addass 11124 ax-mulass 11125 ax-distr 11126 ax-i2m1 11127 ax-1ne0 11128 ax-1rid 11129 ax-rnegex 11130 ax-rrecex 11131 ax-cnre 11132 ax-pre-lttri 11133 ax-pre-lttrn 11134 ax-pre-ltadd 11135 ax-pre-mulgt0 11136 ax-pre-sup 11137

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-nf 1794 df-sb 2081 df-mo 2556 df-eu 2586 df-clab 2731 df-cleq 2744 df-clel 2827 df-nfc 2901 df-ne 2948 df-nel 3052 df-ral 3067 df-rex 3077 df-rmo 3357 df-reu 3358 df-rab 3405 df-v 3446 df-sbc 3736 df-csb 3844 df-dif 3898 df-un 3900 df-in 3902 df-ss 3912 df-pss 3915 df-nul 4277 df-if 4471 df-pw 4547 df-sn 4573 df-pr 4575 df-op 4579 df-uni 4856 df-int 4896 df-iun 4941 df-br 5091 df-opab 5153 df-mpt 5172 df-tr 5198 df-id 5531 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5589 df-we 5591 df-xp 5642 df-rel 5643 df-cnv 5644 df-co 5645 df-dm 5646 df-rn 5647 df-res 5648 df-ima 5649 df-pred 6273 df-ord 6334 df-on 6335 df-lim 6336 df-suc 6337 df-iota 6462 df-fun 6508 df-fn 6509 df-f 6510 df-f1 6511 df-fo 6512 df-f1o 6513 df-fv 6514 df-riota 7338 df-ov 7384 df-oprab 7385 df-mpo 7386 df-om 7832 df-1st 7955 df-2nd 7956 df-frecs 8246 df-wrecs 8277 df-recs 8326 df-rdg 8365 df-1o 8421 df-oadd 8425 df-er 8662 df-en 8913 df-dom 8914 df-sdom 8915 df-fin 8916 df-sup 9374 df-inf 9375 df-card 9883 df-pnf 11204 df-mnf 11205 df-xr 11206 df-ltxr 11207 df-le 11208 df-sub 11402 df-neg 11403 df-div 11831 df-nn 12197 df-2 12266 df-3 12267 df-n0 12468 df-xnn0 12541 df-z 12555 df-uz 12826 df-rp 12980 df-fz 13499 df-fzo 13646 df-fl 13788 df-mod 13866 df-seq 14001 df-exp 14061 df-hash 14330 df-cj 15098 df-re 15099 df-im 15100 df-sqrt 15234 df-abs 15235 df-dvds 16259 df-gcd 16501 df-phi 16773

This theorem is referenced by: eulerth 16790

W3C validator