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 16920

Description: Lemma for eulerth 16921. (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 1160	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	phicld 16910	. . . . . . . . 9 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
4	3	nnred 12319	. . . . . . . 8 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℝ)
5	4	leidd 11851	. . . . . . 7 ⊢ (𝜑 → (ϕ‘𝑁) ≤ (ϕ‘𝑁))
6	3	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → (ϕ‘𝑁) ∈ ℕ)
7		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 ≤ (ϕ‘𝑁) ↔ 1 ≤ (ϕ‘𝑁)))
8	7	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 1 ≤ (ϕ‘𝑁))))
9		oveq2 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝐴↑𝑥) = (𝐴↑1))
10		fveq2 6873	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
11	9, 10	oveq12d 7426	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑1) · (seq1( · , 𝐹)‘1)))
12	11	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁))
13		fveq2 6873	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘1))
14	13	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))
15	12, 14	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)))
16	10	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘1)))
17	16	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
18	15, 17	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)))
19	8, 18	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))))
20		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥 ≤ (ϕ‘𝑁) ↔ 𝑧 ≤ (ϕ‘𝑁)))
21	20	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁))))
22		oveq2 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧))
23		fveq2 6873	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑧))
24	22, 23	oveq12d 7426	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)))
25	24	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁))
26		fveq2 6873	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘𝑧))
27	26	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁))
28	25, 27	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)))
29	23	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘𝑧)))
30	29	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))
31	28, 30	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)))
32	21, 31	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))))
33		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → (𝑥 ≤ (ϕ‘𝑁) ↔ (𝑧 + 1) ≤ (ϕ‘𝑁)))
34	33	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 + 1) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
35		oveq2 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑧 + 1) → (𝐴↑𝑥) = (𝐴↑(𝑧 + 1)))
36		fveq2 6873	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑧 + 1)))
37	35, 36	oveq12d 7426	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑧 + 1) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))))
38	37	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁))
39		fveq2 6873	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(𝑧 + 1)))
40	39	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))
41	38, 40	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
42	36	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))))
43	42	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))
44	41, 43	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 + 1) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
45	34, 44	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = (𝑧 + 1) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))))
46		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → (𝑥 ≤ (ϕ‘𝑁) ↔ (ϕ‘𝑁) ≤ (ϕ‘𝑁)))
47	46	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁))))
48		oveq2 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (ϕ‘𝑁) → (𝐴↑𝑥) = (𝐴↑(ϕ‘𝑁)))
49		fveq2 6873	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
50	48, 49	oveq12d 7426	. . . . . . . . . . . . 13 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))))
51	50	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁))
52		fveq2 6873	. . . . . . . . . . . . 13 ⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(ϕ‘𝑁)))
53	52	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))
54	51, 53	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)))
55	49	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))))
56	55	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))
57	54, 56	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑥 = (ϕ‘𝑁) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)))
58	47, 57	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = (ϕ‘𝑁) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))))
59	1	simp2d 1161	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℤ)
60		eulerth.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)
61		f1of 6812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇⟶𝑆)
62	60, 61	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹:𝑇⟶𝑆)
63		nnuz 12973	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
64	3, 63	eleqtrdi 2870	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (ℤ_≥‘1))
65		eluzfz1 13632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘1) → 1 ∈ (1...(ϕ‘𝑁)))
66	64, 65	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ (1...(ϕ‘𝑁)))
67		eulerth.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑇 = (1...(ϕ‘𝑁))
68	66, 67	eleqtrrdi 2871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ 𝑇)
69	62, 68	ffvelcdmd 7073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘1) ∈ 𝑆)
70		oveq1 7415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝐹‘1) → (𝑦 gcd 𝑁) = ((𝐹‘1) gcd 𝑁))
71	70	eqeq1d 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝐹‘1) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘1) gcd 𝑁) = 1))
72		eulerth.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
73	71, 72	elrab2 3648	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘1) ∈ 𝑆 ↔ ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1))
74	69, 73	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1))
75	74	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘1) ∈ (0..^𝑁))
76		elfzoelz 13761	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘1) ∈ (0..^𝑁) → (𝐹‘1) ∈ ℤ)
77	75, 76	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘1) ∈ ℤ)
78	59, 77	zmulcld 12778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ)
79	78	zred 12772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℝ)
80	2	nnrpd 13131	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
81		modabs2 14013	. . . . . . . . . . . . 13 ⊢ (((𝐴 · (𝐹‘1)) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
82	79, 80, 81	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
83		1z 12695	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
84		fveq2 6873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1))
85	84	oveq2d 7424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
86	85	oveq1d 7423	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
87		eulerth.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))
88		ovex 7441	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ V
89	86, 87, 88	fvmpt 6981	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ 𝑇 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
90	68, 89	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
91	83, 90	seq1i 14126	. . . . . . . . . . . . 13 ⊢ (𝜑 → (seq1( · , 𝐺)‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
92	91	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝜑 → ((seq1( · , 𝐺)‘1) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁))
93	59	zcnd 12773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℂ)
94	93	exp1d 14252	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴↑1) = 𝐴)
95		seq1 14125	. . . . . . . . . . . . . . . 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 7426	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴↑1) · (seq1( · , 𝐹)‘1)) = (𝐴 · (𝐹‘1)))
99	98	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
100	82, 92, 99	3eqtr4rd 2806	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))
101	96	oveq2i 7419	. . . . . . . . . . . 12 ⊢ (𝑁 gcd (seq1( · , 𝐹)‘1)) = (𝑁 gcd (𝐹‘1))
102	2	nnzd 12688	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
103	102, 77	gcdcomd 16651	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁))
104	74	simprd 501	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹‘1) gcd 𝑁) = 1)
105	103, 104	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = 1)
106	101, 105	eqtrid 2807	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)
107	100, 106	jca 521	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
108	107	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
109		nnre 12311	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
110	109	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ∈ ℝ)
111	110	lep1d 12217	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ≤ (𝑧 + 1))
112		peano2re 11454	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ → (𝑧 + 1) ∈ ℝ)
113	110, 112	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (𝑧 + 1) ∈ ℝ)
114	4	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (ϕ‘𝑁) ∈ ℝ)
115		letr 11375	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ (𝑧 + 1) ∈ ℝ ∧ (ϕ‘𝑁) ∈ ℝ) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁)))
116	110, 113, 114, 115	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁)))
117	111, 116	mpand 708	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 + 1) ≤ (ϕ‘𝑁) → 𝑧 ≤ (ϕ‘𝑁)))
118	117	imdistanda 582	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁))))
119	118	imim1d 83	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))))
120	59	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℤ)
121		nnnn0 12582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ₀)
122	121	ad2antrl 741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ₀)
123		zexpcl 14187	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℤ ∧ 𝑧 ∈ ℕ₀) → (𝐴↑𝑧) ∈ ℤ)
124	120, 122, 123	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℤ)
125		simprl 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ)
126	125, 63	eleqtrdi 2870	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ (ℤ_≥‘1))
127	109	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℝ)
128	127, 112	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℝ)
129	4	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℝ)
130	127	lep1d 12217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (𝑧 + 1))
131		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ≤ (ϕ‘𝑁))
132	127, 128, 129, 130, 131	letrd 11438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (ϕ‘𝑁))
133		nnz 12683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
134	133	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℤ)
135	3	nnzd 12688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℤ)
136	135	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℤ)
137		eluz 12948	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁)))
138	134, 136, 137	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁)))
139	132, 138	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ (ℤ_≥‘𝑧))
140		fzss2 13666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) → (1...𝑧) ⊆ (1...(ϕ‘𝑁)))
141	139, 140	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ (1...(ϕ‘𝑁)))
142	141, 67	sseqtrrdi 3971	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ 𝑇)
143	142	sselda 3930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → 𝑥 ∈ 𝑇)
144	62	ffvelcdmda 7072	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ 𝑆)
145		oveq1 7415	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 gcd 𝑁) = ((𝐹‘𝑥) gcd 𝑁))
146	145	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝐹‘𝑥) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘𝑥) gcd 𝑁) = 1))
147	146, 72	elrab2 3648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑥) ∈ 𝑆 ↔ ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1))
148	144, 147	sylib 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1))
149	148	simpld 500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ (0..^𝑁))
150		elfzoelz 13761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ ℤ)
151	149, 150	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ)
152	151	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ)
153	143, 152	syldan 603	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐹‘𝑥) ∈ ℤ)
154		zmulcl 12714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ)
155	154	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ)
156	126, 153, 155	seqcl 14133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℤ)
157	124, 156	zmulcld 12778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℤ)
158	157	zred 12772	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ)
159	72	ssrab3 4029	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 ⊆ (0..^𝑁)
160	1, 72, 67, 60, 87	eulerthlem1 16919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐺:𝑇⟶𝑆)
161	160	ffvelcdmda 7072	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ 𝑆)
162	159, 161	sselid 3928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ (0..^𝑁))
163		elfzoelz 13761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑥) ∈ (0..^𝑁) → (𝐺‘𝑥) ∈ ℤ)
164	162, 163	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ)
165	164	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ)
166	143, 165	syldan 603	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐺‘𝑥) ∈ ℤ)
167	126, 166, 155	seqcl 14133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℤ)
168	167	zred 12772	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℝ)
169	62	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐹:𝑇⟶𝑆)
170		peano2nn 12316	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈ ℕ)
171	170	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℕ)
172	171	nnge1d 12355	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 1 ≤ (𝑧 + 1))
173	171	nnzd 12688	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℤ)
174		elfz 13614	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑧 + 1) ∈ ℤ ∧ 1 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
175	83, 174	mp3an2 1478	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑧 + 1) ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
176	173, 136, 175	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
177	172, 131, 176	mpbir2and 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ (1...(ϕ‘𝑁)))
178	177, 67	eleqtrrdi 2871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ 𝑇)
179	169, 178	ffvelcdmd 7073	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ 𝑆)
180		oveq1 7415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → (𝑦 gcd 𝑁) = ((𝐹‘(𝑧 + 1)) gcd 𝑁))
181	180	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
182	181, 72	elrab2 3648	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑧 + 1)) ∈ 𝑆 ↔ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
183	179, 182	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
184	183	simpld 500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ (0..^𝑁))
185		elfzoelz 13761	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) → (𝐹‘(𝑧 + 1)) ∈ ℤ)
186	184, 185	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℤ)
187	120, 186	zmulcld 12778	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ)
188	80	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℝ⁺)
189		modmul1 14035	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · , 𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ⁺) ∧ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))
190	189	3expia 1139	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · , 𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ⁺)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)))
191	158, 168, 187, 188, 190	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)))
192	124	zcnd 12773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℂ)
193	156	zcnd 12773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℂ)
194	93	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℂ)
195	186	zcnd 12773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℂ)
196	192, 193, 194, 195	mul4d 11493	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
197	194, 122	expp1d 14258	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑(𝑧 + 1)) = ((𝐴↑𝑧) · 𝐴))
198		seqp1 14127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℤ_≥‘1) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))
199	126, 198	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))
200	197, 199	oveq12d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
201	196, 200	eqtr4d 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))))
202	201	oveq1d 7423	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁))
203	187	zred 12772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ)
204	203, 188	modcld 13983	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ)
205		modabs2 14013	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
206	203, 188, 205	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
207		modmul1 14035	. . . . . . . . . . . . . . . . . 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 1408	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
209		fveq2 6873	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑧 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑧 + 1)))
210	209	oveq2d 7424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑧 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑧 + 1))))
211	210	oveq1d 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑧 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
212		ovex 7441	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ V
213	211, 87, 212	fvmpt 6981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 + 1) ∈ 𝑇 → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
214	178, 213	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
215	214	oveq2d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)))
216		seqp1 14127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℤ_≥‘1) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))))
217	126, 216	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))))
218	204	recnd 11308	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℂ)
219	167	zcnd 12773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℂ)
220	218, 219	mulcomd 11301	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)))
221	215, 217, 220	3eqtr4d 2805	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)))
222	221	oveq1d 7423	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
223	187	zcnd 12773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℂ)
224	219, 223	mulcomd 11301	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)))
225	224	oveq1d 7423	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
226	208, 222, 225	3eqtr4rd 2806	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))
227	202, 226	eqeq12d 2776	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
228	191, 227	sylibd 242	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
229	102	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℤ)
230	229, 186	gcdcomd 16651	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = ((𝐹‘(𝑧 + 1)) gcd 𝑁))
231	183	simprd 501	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)
232	230, 231	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1)
233		rpmul 16796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ (seq1( · , 𝐹)‘𝑧) ∈ ℤ ∧ (𝐹‘(𝑧 + 1)) ∈ ℤ) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
234	229, 156, 186, 233	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
235	232, 234	mpan2d 707	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
236	199	oveq2d 7424	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
237	236	eqeq1d 2762	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1 ↔ (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
238	235, 237	sylibrd 262	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))
239	228, 238	anim12d 621	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
240	239	an12s 662	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℕ ∧ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
241	240	ex 418	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))))
242	241	a2d 30	. . . . . . . . . 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 48	. . . . . . . . 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 12322	. . . . . . . 8 ⊢ ((ϕ‘𝑁) ∈ ℕ → ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)))
245	6, 244	mpcom 39	. . . . . . 7 ⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))
246	5, 245	mpdan 700	. . . . . 6 ⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))
247	246	simpld 500	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))
248	3	nnnn0d 12636	. . . . . . . 8 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ₀)
249		zexpcl 14187	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℕ₀) → (𝐴↑(ϕ‘𝑁)) ∈ ℤ)
250	59, 248, 249	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℤ)
251	67	eleq2i 2852	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ (1...(ϕ‘𝑁)))
252	251, 151	sylan2br 607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℤ)
253	154	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ)
254	64, 252, 253	seqcl 14133	. . . . . . 7 ⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ)
255	250, 254	zmulcld 12778	. . . . . 6 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈ ℤ)
256		mulcl 11255	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
257	256	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
258		mulcom 11257	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
259	258	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
260		mulass 11259	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
261	260	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
262		ssidd 3953	. . . . . . . 8 ⊢ (𝜑 → ℂ ⊆ ℂ)
263		f1ocnv 6825	. . . . . . . . . . 11 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → ^◡𝐹:𝑆–1-1-onto→𝑇)
264	60, 263	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹:𝑆–1-1-onto→𝑇)
265	2	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℕ)
266	59	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℤ)
267	62	ffvelcdmda 7072	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → (𝐹‘𝑦) ∈ 𝑆)
268	267	adantrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ 𝑆)
269	159, 268	sselid 3928	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ (0..^𝑁))
270		elfzoelz 13761	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) ∈ ℤ)
271	269, 270	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℤ)
272	266, 271	zmulcld 12778	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑦)) ∈ ℤ)
273	62	ffvelcdmda 7072	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑇) → (𝐹‘𝑧) ∈ 𝑆)
274	273	adantrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ 𝑆)
275	159, 274	sselid 3928	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ (0..^𝑁))
276		elfzoelz 13761	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) ∈ ℤ)
277	275, 276	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℤ)
278	266, 277	zmulcld 12778	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑧)) ∈ ℤ)
279		moddvds 16400	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 · (𝐹‘𝑦)) ∈ ℤ ∧ (𝐴 · (𝐹‘𝑧)) ∈ ℤ) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
280	265, 272, 278, 279	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
281		fveq2 6873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
282	281	oveq2d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑦)))
283	282	oveq1d 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁))
284		ovex 7441	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) ∈ V
285	283, 87, 284	fvmpt 6981	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝑇 → (𝐺‘𝑦) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁))
286		fveq2 6873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
287	286	oveq2d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑧)))
288	287	oveq1d 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑧 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))
289		ovex 7441	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ∈ V
290	288, 87, 289	fvmpt 6981	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑇 → (𝐺‘𝑧) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))
291	285, 290	eqeqan12d 2774	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)))
292	291	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)))
293	93	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℂ)
294	271	zcnd 12773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℂ)
295	277	zcnd 12773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℂ)
296	293, 294, 295	subdid 11741	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) = ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))
297	296	breq2d 5114	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
298	280, 292, 297	3bitr4d 314	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ 𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧)))))
299	102, 59	gcdcomd 16651	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁))
300	1	simp3d 1162	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 gcd 𝑁) = 1)
301	299, 300	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 gcd 𝐴) = 1)
302	301	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 gcd 𝐴) = 1)
303	102	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℤ)
304	271, 277	zsubcld 12777	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ)
305		coprmdvds 16790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
306	303, 266, 304, 305	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
307	271	zred 12772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℝ)
308	80	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℝ⁺)
309		elfzole1 13770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑦))
310	269, 309	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑦))
311		elfzolt2 13771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) < 𝑁)
312	269, 311	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) < 𝑁)
313		modid 14004	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑦) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) ∧ (0 ≤ (𝐹‘𝑦) ∧ (𝐹‘𝑦) < 𝑁)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦))
314	307, 308, 310, 312, 313	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦))
315	277	zred 12772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℝ)
316		elfzole1 13770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑧))
317	275, 316	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑧))
318		elfzolt2 13771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) < 𝑁)
319	275, 318	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) < 𝑁)
320		modid 14004	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑧) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) ∧ (0 ≤ (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑁)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧))
321	315, 308, 317, 319, 320	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧))
322	314, 321	eqeq12d 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ (𝐹‘𝑦) = (𝐹‘𝑧)))
323		moddvds 16400	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ (𝐹‘𝑦) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
324	265, 271, 277, 323	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
325		f1of1 6811	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇–1-1→𝑆)
326	60, 325	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:𝑇–1-1→𝑆)
327		f1fveq 7254	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝑇–1-1→𝑆 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧))
328	326, 327	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧))
329	322, 324, 328	3bitr3d 312	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)) ↔ 𝑦 = 𝑧))
330	306, 329	sylibd 242	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑦 = 𝑧))
331	302, 330	mpan2d 707	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) → 𝑦 = 𝑧))
332	298, 331	sylbid 243	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))
333	332	ralrimivva 3205	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))
334		dff13 7246	. . . . . . . . . . . 12 ⊢ (𝐺:𝑇–1-1→𝑆 ↔ (𝐺:𝑇⟶𝑆 ∧ ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)))
335	160, 333, 334	sylanbrc 595	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:𝑇–1-1→𝑆)
336	67	ovexi 7442	. . . . . . . . . . . . . 14 ⊢ 𝑇 ∈ V
337	336	f1oen 8977	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝑇 ≈ 𝑆)
338	60, 337	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ≈ 𝑆)
339		fzofi 14085	. . . . . . . . . . . . 13 ⊢ (0..^𝑁) ∈ Fin
340		ssfi 9166	. . . . . . . . . . . . 13 ⊢ (((0..^𝑁) ∈ Fin ∧ 𝑆 ⊆ (0..^𝑁)) → 𝑆 ∈ Fin)
341	339, 159, 340	mp2an 705	. . . . . . . . . . . 12 ⊢ 𝑆 ∈ Fin
342		f1finf1o 9242	. . . . . . . . . . . 12 ⊢ ((𝑇 ≈ 𝑆 ∧ 𝑆 ∈ Fin) → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆))
343	338, 341, 342	sylancl 598	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆))
344	335, 343	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝑇–1-1-onto→𝑆)
345		f1oco 6836	. . . . . . . . . 10 ⊢ ((^◡𝐹:𝑆–1-1-onto→𝑇 ∧ 𝐺:𝑇–1-1-onto→𝑆) → (^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇)
346	264, 344, 345	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇)
347		f1oeq23 6803	. . . . . . . . . 10 ⊢ ((𝑇 = (1...(ϕ‘𝑁)) ∧ 𝑇 = (1...(ϕ‘𝑁))) → ((^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))))
348	67, 67, 347	mp2an 705	. . . . . . . . 9 ⊢ ((^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))
349	346, 348	sylib 221	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))
350	252	zcnd 12773	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℂ)
351	67	eleq2i 2852	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ (1...(ϕ‘𝑁)))
352		fvco3 6973	. . . . . . . . . . . 12 ⊢ ((𝐺:𝑇⟶𝑆 ∧ 𝑤 ∈ 𝑇) → ((^◡𝐹 ∘ 𝐺)‘𝑤) = (^◡𝐹‘(𝐺‘𝑤)))
353	160, 352	sylan 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((^◡𝐹 ∘ 𝐺)‘𝑤) = (^◡𝐹‘(𝐺‘𝑤)))
354	353	fveq2d 6877	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)) = (𝐹‘(^◡𝐹‘(𝐺‘𝑤))))
355	60	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝐹:𝑇–1-1-onto→𝑆)
356	160	ffvelcdmda 7072	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) ∈ 𝑆)
357		f1ocnvfv2 7273	. . . . . . . . . . 11 ⊢ ((𝐹:𝑇–1-1-onto→𝑆 ∧ (𝐺‘𝑤) ∈ 𝑆) → (𝐹‘(^◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤))
358	355, 356, 357	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘(^◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤))
359	354, 358	eqtr2d 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) = (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)))
360	351, 359	sylan2br 607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (1...(ϕ‘𝑁))) → (𝐺‘𝑤) = (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)))
361	257, 259, 261, 64, 262, 349, 350, 360	seqf1o 14154	. . . . . . 7 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
362	361, 254	eqeltrd 2860	. . . . . 6 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈ ℤ)
363		moddvds 16400	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈ ℤ ∧ (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈ ℤ) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁)))))
364	2, 255, 362, 363	syl3anc 1398	. . . . 5 ⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁)))))
365	247, 364	mpbid 235	. . . 4 ⊢ (𝜑 → 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))))
366	254	zcnd 12773	. . . . . . . 8 ⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ)
367	366	mullidd 11298	. . . . . . 7 ⊢ (𝜑 → (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
368	361, 367	eqtr4d 2798	. . . . . 6 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁))))
369	368	oveq2d 7424	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
370	250	zcnd 12773	. . . . . 6 ⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℂ)
371		ax-1cn 11229	. . . . . . 7 ⊢ 1 ∈ ℂ
372		subdir 11719	. . . . . . 7 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
373	371, 372	mp3an2 1478	. . . . . 6 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
374	370, 366, 373	syl2anc 596	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
375		zsubcl 12707	. . . . . . . 8 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ)
376	250, 83, 375	sylancl 598	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ)
377	376	zcnd 12773	. . . . . 6 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℂ)
378	377, 366	mulcomd 11301	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
379	369, 374, 378	3eqtr2d 2801	. . . 4 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
380	365, 379	breqtrd 5130	. . 3 ⊢ (𝜑 → 𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
381	246	simprd 501	. . 3 ⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)
382		coprmdvds 16790	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ ∧ ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ) → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
383	102, 254, 376, 382	syl3anc 1398	. . 3 ⊢ (𝜑 → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
384	380, 381, 383	mp2and 712	. 2 ⊢ (𝜑 → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))
385		moddvds 16400	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
386	83, 385	mp3an3 1479	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
387	2, 250, 386	syl2anc 596	. 2 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
388	384, 387	mpbird 260	1 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3076 {crab 3412 ⊆ wss 3898 class class class wbr 5102 ↦ cmpt 5185 ^◡ccnv 5646 ∘ ccom 5651 ⟶wf 6523 –1-1→wf1 6524 –1-1-onto→wf1o 6526 ‘cfv 6527 (class class class)co 7408 ≈ cen 8948 Fincfn 8951 ℂcc 11169 ℝcr 11170 0cc0 11171 1c1 11172 + caddc 11174 · cmul 11176 < clt 11314 ≤ cle 11315 − cmin 11512 ℕcn 12304 ℕ₀cn0 12575 ℤcz 12662 ℤ_≥cuz 12934 ℝ⁺crp 13089 ...cfz 13608 ..^cfzo 13756 mod cmo 13977 seqcseq 14112 ↑cexp 14172 ∥ cdvds 16389 gcd cgcd 16631 ϕcphi 16902

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11227 ax-resscn 11228 ax-1cn 11229 ax-icn 11230 ax-addcl 11231 ax-addrcl 11232 ax-mulcl 11233 ax-mulrcl 11234 ax-mulcom 11235 ax-addass 11236 ax-mulass 11237 ax-distr 11238 ax-i2m1 11239 ax-1ne0 11240 ax-1rid 11241 ax-rnegex 11242 ax-rrecex 11243 ax-cnre 11244 ax-pre-lttri 11245 ax-pre-lttrn 11246 ax-pre-ltadd 11247 ax-pre-mulgt0 11248 ax-pre-sup 11249

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-oadd 8458 df-er 8695 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-sup 9412 df-inf 9413 df-card 9991 df-pnf 11316 df-mnf 11317 df-xr 11318 df-ltxr 11319 df-le 11320 df-sub 11514 df-neg 11515 df-div 11943 df-nn 12305 df-2 12374 df-3 12375 df-n0 12576 df-xnn0 12649 df-z 12663 df-uz 12935 df-rp 13090 df-fz 13609 df-fzo 13757 df-fl 13900 df-mod 13978 df-seq 14113 df-exp 14173 df-hash 14442 df-cj 15233 df-re 15234 df-im 15235 df-sqrt 15369 df-abs 15370 df-dvds 16390 df-gcd 16632 df-phi 16904

This theorem is used by: eulerth 16921

W3C validator