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 16411

Description: Lemma for eulerth 16412. (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 1140	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	phicld 16401	. . . . . . . . 9 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
4	3	nnred 11918	. . . . . . . 8 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℝ)
5	4	leidd 11471	. . . . . . 7 ⊢ (𝜑 → (ϕ‘𝑁) ≤ (ϕ‘𝑁))
6	3	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → (ϕ‘𝑁) ∈ ℕ)
7		breq1 5073	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 ≤ (ϕ‘𝑁) ↔ 1 ≤ (ϕ‘𝑁)))
8	7	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 1 ≤ (ϕ‘𝑁))))
9		oveq2 7263	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝐴↑𝑥) = (𝐴↑1))
10		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
11	9, 10	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑1) · (seq1( · , 𝐹)‘1)))
12	11	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁))
13		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘1))
14	13	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))
15	12, 14	eqeq12d 2754	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)))
16	10	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘1)))
17	16	eqeq1d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
18	15, 17	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)))
19	8, 18	imbi12d 344	. . . . . . . . 9 ⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))))
20		breq1 5073	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑥 ≤ (ϕ‘𝑁) ↔ 𝑧 ≤ (ϕ‘𝑁)))
21	20	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁))))
22		oveq2 7263	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧))
23		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑧))
24	22, 23	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)))
25	24	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁))
26		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘𝑧))
27	26	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁))
28	25, 27	eqeq12d 2754	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)))
29	23	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘𝑧)))
30	29	eqeq1d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))
31	28, 30	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)))
32	21, 31	imbi12d 344	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))))
33		breq1 5073	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → (𝑥 ≤ (ϕ‘𝑁) ↔ (𝑧 + 1) ≤ (ϕ‘𝑁)))
34	33	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 + 1) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
35		oveq2 7263	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑧 + 1) → (𝐴↑𝑥) = (𝐴↑(𝑧 + 1)))
36		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑧 + 1)))
37	35, 36	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑧 + 1) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))))
38	37	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁))
39		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(𝑧 + 1)))
40	39	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))
41	38, 40	eqeq12d 2754	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
42	36	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑧 + 1) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))))
43	42	eqeq1d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 + 1) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))
44	41, 43	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 + 1) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
45	34, 44	imbi12d 344	. . . . . . . . 9 ⊢ (𝑥 = (𝑧 + 1) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))))
46		breq1 5073	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → (𝑥 ≤ (ϕ‘𝑁) ↔ (ϕ‘𝑁) ≤ (ϕ‘𝑁)))
47	46	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁))))
48		oveq2 7263	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (ϕ‘𝑁) → (𝐴↑𝑥) = (𝐴↑(ϕ‘𝑁)))
49		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
50	48, 49	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))))
51	50	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁))
52		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(ϕ‘𝑁)))
53	52	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))
54	51, 53	eqeq12d 2754	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)))
55	49	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑥 = (ϕ‘𝑁) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))))
56	55	eqeq1d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = (ϕ‘𝑁) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))
57	54, 56	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑥 = (ϕ‘𝑁) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)))
58	47, 57	imbi12d 344	. . . . . . . . 9 ⊢ (𝑥 = (ϕ‘𝑁) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))))
59	1	simp2d 1141	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℤ)
60		eulerth.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)
61		f1of 6700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇⟶𝑆)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹:𝑇⟶𝑆)
63		nnuz 12550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
64	3, 63	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (ℤ_≥‘1))
65		eluzfz1 13192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘1) → 1 ∈ (1...(ϕ‘𝑁)))
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ (1...(ϕ‘𝑁)))
67		eulerth.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑇 = (1...(ϕ‘𝑁))
68	66, 67	eleqtrrdi 2850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 1 ∈ 𝑇)
69	62, 68	ffvelrnd 6944	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘1) ∈ 𝑆)
70		oveq1 7262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝐹‘1) → (𝑦 gcd 𝑁) = ((𝐹‘1) gcd 𝑁))
71	70	eqeq1d 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝐹‘1) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘1) gcd 𝑁) = 1))
72		eulerth.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
73	71, 72	elrab2 3620	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘1) ∈ 𝑆 ↔ ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1))
74	69, 73	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1))
75	74	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘1) ∈ (0..^𝑁))
76		elfzoelz 13316	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘1) ∈ (0..^𝑁) → (𝐹‘1) ∈ ℤ)
77	75, 76	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘1) ∈ ℤ)
78	59, 77	zmulcld 12361	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ)
79	78	zred 12355	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℝ)
80	2	nnrpd 12699	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
81		modabs2 13553	. . . . . . . . . . . . 13 ⊢ (((𝐴 · (𝐹‘1)) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
82	79, 80, 81	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
83		1z 12280	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
84		fveq2 6756	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1))
85	84	oveq2d 7271	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
86	85	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
87		eulerth.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))
88		ovex 7288	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ V
89	86, 87, 88	fvmpt 6857	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ 𝑇 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
90	68, 89	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
91	83, 90	seq1i 13663	. . . . . . . . . . . . 13 ⊢ (𝜑 → (seq1( · , 𝐺)‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁))
92	91	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝜑 → ((seq1( · , 𝐺)‘1) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁))
93	59	zcnd 12356	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℂ)
94	93	exp1d 13787	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴↑1) = 𝐴)
95		seq1 13662	. . . . . . . . . . . . . . . 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 7273	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴↑1) · (seq1( · , 𝐹)‘1)) = (𝐴 · (𝐹‘1)))
99	98	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
100	82, 92, 99	3eqtr4rd 2789	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))
101	96	oveq2i 7266	. . . . . . . . . . . 12 ⊢ (𝑁 gcd (seq1( · , 𝐹)‘1)) = (𝑁 gcd (𝐹‘1))
102	2	nnzd 12354	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
103	102, 77	gcdcomd 16149	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁))
104	74	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹‘1) gcd 𝑁) = 1)
105	103, 104	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = 1)
106	101, 105	eqtrid 2790	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)
107	100, 106	jca 511	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
108	107	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))
109		nnre 11910	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
110	109	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ∈ ℝ)
111	110	lep1d 11836	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ≤ (𝑧 + 1))
112		peano2re 11078	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ → (𝑧 + 1) ∈ ℝ)
113	110, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (𝑧 + 1) ∈ ℝ)
114	4	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (ϕ‘𝑁) ∈ ℝ)
115		letr 10999	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ (𝑧 + 1) ∈ ℝ ∧ (ϕ‘𝑁) ∈ ℝ) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁)))
116	110, 113, 114, 115	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁)))
117	111, 116	mpand 691	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 + 1) ≤ (ϕ‘𝑁) → 𝑧 ≤ (ϕ‘𝑁)))
118	117	imdistanda 571	. . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℤ)
121		nnnn0 12170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ₀)
122	121	ad2antrl 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ₀)
123		zexpcl 13725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℤ ∧ 𝑧 ∈ ℕ₀) → (𝐴↑𝑧) ∈ ℤ)
124	120, 122, 123	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℤ)
125		simprl 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ)
126	125, 63	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ (ℤ_≥‘1))
127	109	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℝ)
128	127, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℝ)
129	4	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℝ)
130	127	lep1d 11836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (𝑧 + 1))
131		simprr 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ≤ (ϕ‘𝑁))
132	127, 128, 129, 130, 131	letrd 11062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (ϕ‘𝑁))
133		nnz 12272	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
134	133	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℤ)
135	3	nnzd 12354	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℤ)
136	135	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℤ)
137		eluz 12525	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁)))
138	134, 136, 137	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁)))
139	132, 138	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ (ℤ_≥‘𝑧))
140		fzss2 13225	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘𝑧) → (1...𝑧) ⊆ (1...(ϕ‘𝑁)))
141	139, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ (1...(ϕ‘𝑁)))
142	141, 67	sseqtrrdi 3968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ 𝑇)
143	142	sselda 3917	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → 𝑥 ∈ 𝑇)
144	62	ffvelrnda 6943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ 𝑆)
145		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 gcd 𝑁) = ((𝐹‘𝑥) gcd 𝑁))
146	145	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝐹‘𝑥) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘𝑥) gcd 𝑁) = 1))
147	146, 72	elrab2 3620	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑥) ∈ 𝑆 ↔ ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1))
148	144, 147	sylib 217	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1))
149	148	simpld 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ (0..^𝑁))
150		elfzoelz 13316	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ ℤ)
151	149, 150	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ)
152	151	adantlr 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ)
153	143, 152	syldan 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐹‘𝑥) ∈ ℤ)
154		zmulcl 12299	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ)
155	154	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ)
156	126, 153, 155	seqcl 13671	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℤ)
157	124, 156	zmulcld 12361	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℤ)
158	157	zred 12355	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ)
159	72	ssrab3 4011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 ⊆ (0..^𝑁)
160	1, 72, 67, 60, 87	eulerthlem1 16410	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐺:𝑇⟶𝑆)
161	160	ffvelrnda 6943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ 𝑆)
162	159, 161	sselid 3915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ (0..^𝑁))
163		elfzoelz 13316	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑥) ∈ (0..^𝑁) → (𝐺‘𝑥) ∈ ℤ)
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ)
165	164	adantlr 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ)
166	143, 165	syldan 590	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐺‘𝑥) ∈ ℤ)
167	126, 166, 155	seqcl 13671	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℤ)
168	167	zred 12355	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℝ)
169	62	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐹:𝑇⟶𝑆)
170		peano2nn 11915	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈ ℕ)
171	170	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℕ)
172	171	nnge1d 11951	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 1 ≤ (𝑧 + 1))
173	171	nnzd 12354	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℤ)
174		elfz 13174	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑧 + 1) ∈ ℤ ∧ 1 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
175	83, 174	mp3an2 1447	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑧 + 1) ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
176	173, 136, 175	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))))
177	172, 131, 176	mpbir2and 709	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ (1...(ϕ‘𝑁)))
178	177, 67	eleqtrrdi 2850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ 𝑇)
179	169, 178	ffvelrnd 6944	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ 𝑆)
180		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → (𝑦 gcd 𝑁) = ((𝐹‘(𝑧 + 1)) gcd 𝑁))
181	180	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
182	181, 72	elrab2 3620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑧 + 1)) ∈ 𝑆 ↔ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
183	179, 182	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1))
184	183	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ (0..^𝑁))
185		elfzoelz 13316	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) → (𝐹‘(𝑧 + 1)) ∈ ℤ)
186	184, 185	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℤ)
187	120, 186	zmulcld 12361	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ)
188	80	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℝ⁺)
189		modmul1 13572	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · , 𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ⁺) ∧ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))
190	189	3expia 1119	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · , 𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ⁺)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)))
191	158, 168, 187, 188, 190	syl22anc 835	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)))
192	124	zcnd 12356	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℂ)
193	156	zcnd 12356	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℂ)
194	93	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℂ)
195	186	zcnd 12356	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℂ)
196	192, 193, 194, 195	mul4d 11117	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
197	194, 122	expp1d 13793	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑(𝑧 + 1)) = ((𝐴↑𝑧) · 𝐴))
198		seqp1 13664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℤ_≥‘1) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))
199	126, 198	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))
200	197, 199	oveq12d 7273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
201	196, 200	eqtr4d 2781	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))))
202	201	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁))
203	187	zred 12355	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ)
204	203, 188	modcld 13523	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ)
205		modabs2 13553	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
206	203, 188, 205	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
207		modmul1 13572	. . . . . . . . . . . . . . . . . 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 1379	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
209		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑧 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑧 + 1)))
210	209	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑧 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑧 + 1))))
211	210	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑧 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
212		ovex 7288	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ V
213	211, 87, 212	fvmpt 6857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 + 1) ∈ 𝑇 → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
214	178, 213	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))
215	214	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)))
216		seqp1 13664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (ℤ_≥‘1) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))))
217	126, 216	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))))
218	204	recnd 10934	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℂ)
219	167	zcnd 12356	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℂ)
220	218, 219	mulcomd 10927	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)))
221	215, 217, 220	3eqtr4d 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)))
222	221	oveq1d 7270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
223	187	zcnd 12356	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℂ)
224	219, 223	mulcomd 10927	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)))
225	224	oveq1d 7270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁))
226	208, 222, 225	3eqtr4rd 2789	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))
227	202, 226	eqeq12d 2754	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
228	191, 227	sylibd 238	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)))
229	102	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℤ)
230	229, 186	gcdcomd 16149	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = ((𝐹‘(𝑧 + 1)) gcd 𝑁))
231	183	simprd 495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)
232	230, 231	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1)
233		rpmul 16292	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ (seq1( · , 𝐹)‘𝑧) ∈ ℤ ∧ (𝐹‘(𝑧 + 1)) ∈ ℤ) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
234	229, 156, 186, 233	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
235	232, 234	mpan2d 690	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
236	199	oveq2d 7271	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))))
237	236	eqeq1d 2740	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1 ↔ (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1))
238	235, 237	sylibrd 258	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))
239	228, 238	anim12d 608	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
240	239	an12s 645	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℕ ∧ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))
241	240	ex 412	. . . . . . . . . . 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 11921	. . . . . . . 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 683	. . . . . 6 ⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))
247	246	simpld 494	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))
248	3	nnnn0d 12223	. . . . . . . 8 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ₀)
249		zexpcl 13725	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ (ϕ‘𝑁) ∈ ℕ₀) → (𝐴↑(ϕ‘𝑁)) ∈ ℤ)
250	59, 248, 249	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℤ)
251	67	eleq2i 2830	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ (1...(ϕ‘𝑁)))
252	251, 151	sylan2br 594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℤ)
253	154	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ)
254	64, 252, 253	seqcl 13671	. . . . . . 7 ⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ)
255	250, 254	zmulcld 12361	. . . . . 6 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈ ℤ)
256		mulcl 10886	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
257	256	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
258		mulcom 10888	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
259	258	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
260		mulass 10890	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
261	260	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
262		ssidd 3940	. . . . . . . 8 ⊢ (𝜑 → ℂ ⊆ ℂ)
263		f1ocnv 6712	. . . . . . . . . . 11 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → ^◡𝐹:𝑆–1-1-onto→𝑇)
264	60, 263	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹:𝑆–1-1-onto→𝑇)
265	2	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℕ)
266	59	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℤ)
267	62	ffvelrnda 6943	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → (𝐹‘𝑦) ∈ 𝑆)
268	267	adantrr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ 𝑆)
269	159, 268	sselid 3915	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ (0..^𝑁))
270		elfzoelz 13316	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) ∈ ℤ)
271	269, 270	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℤ)
272	266, 271	zmulcld 12361	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑦)) ∈ ℤ)
273	62	ffvelrnda 6943	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑇) → (𝐹‘𝑧) ∈ 𝑆)
274	273	adantrl 712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ 𝑆)
275	159, 274	sselid 3915	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ (0..^𝑁))
276		elfzoelz 13316	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) ∈ ℤ)
277	275, 276	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℤ)
278	266, 277	zmulcld 12361	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑧)) ∈ ℤ)
279		moddvds 15902	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 · (𝐹‘𝑦)) ∈ ℤ ∧ (𝐴 · (𝐹‘𝑧)) ∈ ℤ) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
280	265, 272, 278, 279	syl3anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
281		fveq2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
282	281	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑦)))
283	282	oveq1d 7270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁))
284		ovex 7288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) ∈ V
285	283, 87, 284	fvmpt 6857	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝑇 → (𝐺‘𝑦) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁))
286		fveq2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
287	286	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑧)))
288	287	oveq1d 7270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑧 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))
289		ovex 7288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ∈ V
290	288, 87, 289	fvmpt 6857	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑇 → (𝐺‘𝑧) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))
291	285, 290	eqeqan12d 2752	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)))
292	291	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)))
293	93	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℂ)
294	271	zcnd 12356	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℂ)
295	277	zcnd 12356	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℂ)
296	293, 294, 295	subdid 11361	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) = ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))
297	296	breq2d 5082	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))))
298	280, 292, 297	3bitr4d 310	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ 𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧)))))
299	102, 59	gcdcomd 16149	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁))
300	1	simp3d 1142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 gcd 𝑁) = 1)
301	299, 300	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 gcd 𝐴) = 1)
302	301	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 gcd 𝐴) = 1)
303	102	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℤ)
304	271, 277	zsubcld 12360	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ)
305		coprmdvds 16286	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
306	303, 266, 304, 305	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
307	271	zred 12355	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℝ)
308	80	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℝ⁺)
309		elfzole1 13324	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑦))
310	269, 309	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑦))
311		elfzolt2 13325	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) < 𝑁)
312	269, 311	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) < 𝑁)
313		modid 13544	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑦) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) ∧ (0 ≤ (𝐹‘𝑦) ∧ (𝐹‘𝑦) < 𝑁)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦))
314	307, 308, 310, 312, 313	syl22anc 835	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦))
315	277	zred 12355	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℝ)
316		elfzole1 13324	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑧))
317	275, 316	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑧))
318		elfzolt2 13325	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) < 𝑁)
319	275, 318	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) < 𝑁)
320		modid 13544	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑧) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) ∧ (0 ≤ (𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑁)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧))
321	315, 308, 317, 319, 320	syl22anc 835	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧))
322	314, 321	eqeq12d 2754	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ (𝐹‘𝑦) = (𝐹‘𝑧)))
323		moddvds 15902	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ (𝐹‘𝑦) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
324	265, 271, 277, 323	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧))))
325		f1of1 6699	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇–1-1→𝑆)
326	60, 325	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:𝑇–1-1→𝑆)
327		f1fveq 7116	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝑇–1-1→𝑆 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧))
328	326, 327	sylan 579	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧))
329	322, 324, 328	3bitr3d 308	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)) ↔ 𝑦 = 𝑧))
330	306, 329	sylibd 238	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑦 = 𝑧))
331	302, 330	mpan2d 690	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) → 𝑦 = 𝑧))
332	298, 331	sylbid 239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))
333	332	ralrimivva 3114	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))
334		dff13 7109	. . . . . . . . . . . 12 ⊢ (𝐺:𝑇–1-1→𝑆 ↔ (𝐺:𝑇⟶𝑆 ∧ ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)))
335	160, 333, 334	sylanbrc 582	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:𝑇–1-1→𝑆)
336	67	ovexi 7289	. . . . . . . . . . . . . 14 ⊢ 𝑇 ∈ V
337	336	f1oen 8716	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝑇 ≈ 𝑆)
338	60, 337	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ≈ 𝑆)
339		fzofi 13622	. . . . . . . . . . . . 13 ⊢ (0..^𝑁) ∈ Fin
340		ssfi 8918	. . . . . . . . . . . . 13 ⊢ (((0..^𝑁) ∈ Fin ∧ 𝑆 ⊆ (0..^𝑁)) → 𝑆 ∈ Fin)
341	339, 159, 340	mp2an 688	. . . . . . . . . . . 12 ⊢ 𝑆 ∈ Fin
342		f1finf1o 8975	. . . . . . . . . . . 12 ⊢ ((𝑇 ≈ 𝑆 ∧ 𝑆 ∈ Fin) → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆))
343	338, 341, 342	sylancl 585	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆))
344	335, 343	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝑇–1-1-onto→𝑆)
345		f1oco 6722	. . . . . . . . . 10 ⊢ ((^◡𝐹:𝑆–1-1-onto→𝑇 ∧ 𝐺:𝑇–1-1-onto→𝑆) → (^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇)
346	264, 344, 345	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇)
347		f1oeq23 6691	. . . . . . . . . 10 ⊢ ((𝑇 = (1...(ϕ‘𝑁)) ∧ 𝑇 = (1...(ϕ‘𝑁))) → ((^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))))
348	67, 67, 347	mp2an 688	. . . . . . . . 9 ⊢ ((^◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))
349	346, 348	sylib 217	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))
350	252	zcnd 12356	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℂ)
351	67	eleq2i 2830	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ (1...(ϕ‘𝑁)))
352		fvco3 6849	. . . . . . . . . . . 12 ⊢ ((𝐺:𝑇⟶𝑆 ∧ 𝑤 ∈ 𝑇) → ((^◡𝐹 ∘ 𝐺)‘𝑤) = (^◡𝐹‘(𝐺‘𝑤)))
353	160, 352	sylan 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((^◡𝐹 ∘ 𝐺)‘𝑤) = (^◡𝐹‘(𝐺‘𝑤)))
354	353	fveq2d 6760	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)) = (𝐹‘(^◡𝐹‘(𝐺‘𝑤))))
355	60	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝐹:𝑇–1-1-onto→𝑆)
356	160	ffvelrnda 6943	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) ∈ 𝑆)
357		f1ocnvfv2 7130	. . . . . . . . . . 11 ⊢ ((𝐹:𝑇–1-1-onto→𝑆 ∧ (𝐺‘𝑤) ∈ 𝑆) → (𝐹‘(^◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤))
358	355, 356, 357	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘(^◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤))
359	354, 358	eqtr2d 2779	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) = (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)))
360	351, 359	sylan2br 594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (1...(ϕ‘𝑁))) → (𝐺‘𝑤) = (𝐹‘((^◡𝐹 ∘ 𝐺)‘𝑤)))
361	257, 259, 261, 64, 262, 349, 350, 360	seqf1o 13692	. . . . . . 7 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
362	361, 254	eqeltrd 2839	. . . . . 6 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈ ℤ)
363		moddvds 15902	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈ ℤ ∧ (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈ ℤ) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁)))))
364	2, 255, 362, 363	syl3anc 1369	. . . . 5 ⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁)))))
365	247, 364	mpbid 231	. . . 4 ⊢ (𝜑 → 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))))
366	254	zcnd 12356	. . . . . . . 8 ⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ)
367	366	mulid2d 10924	. . . . . . 7 ⊢ (𝜑 → (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (seq1( · , 𝐹)‘(ϕ‘𝑁)))
368	361, 367	eqtr4d 2781	. . . . . 6 ⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁))))
369	368	oveq2d 7271	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
370	250	zcnd 12356	. . . . . 6 ⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℂ)
371		ax-1cn 10860	. . . . . . 7 ⊢ 1 ∈ ℂ
372		subdir 11339	. . . . . . 7 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
373	371, 372	mp3an2 1447	. . . . . 6 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
374	370, 366, 373	syl2anc 583	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1( · , 𝐹)‘(ϕ‘𝑁)))))
375		zsubcl 12292	. . . . . . . 8 ⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ)
376	250, 83, 375	sylancl 585	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ)
377	376	zcnd 12356	. . . . . 6 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℂ)
378	377, 366	mulcomd 10927	. . . . 5 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
379	369, 374, 378	3eqtr2d 2784	. . . 4 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · , 𝐺)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
380	365, 379	breqtrd 5096	. . 3 ⊢ (𝜑 → 𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)))
381	246	simprd 495	. . 3 ⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)
382		coprmdvds 16286	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ ∧ ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ) → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
383	102, 254, 376, 382	syl3anc 1369	. . 3 ⊢ (𝜑 → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
384	380, 381, 383	mp2and 695	. 2 ⊢ (𝜑 → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))
385		moddvds 15902	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
386	83, 385	mp3an3 1448	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
387	2, 250, 386	syl2anc 583	. 2 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)))
388	384, 387	mpbird 256	1 ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∀wral 3063 {crab 3067 ⊆ wss 3883 class class class wbr 5070 ↦ cmpt 5153 ^◡ccnv 5579 ∘ ccom 5584 ⟶wf 6414 –1-1→wf1 6415 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 ≈ cen 8688 Fincfn 8691 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 < clt 10940 ≤ cle 10941 − cmin 11135 ℕcn 11903 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ℝ⁺crp 12659 ...cfz 13168 ..^cfzo 13311 mod cmo 13517 seqcseq 13649 ↑cexp 13710 ∥ cdvds 15891 gcd cgcd 16129 ϕcphi 16393

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-oadd 8271 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-xnn0 12236 df-z 12250 df-uz 12512 df-rp 12660 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-dvds 15892 df-gcd 16130 df-phi 16395

This theorem is referenced by: eulerth 16412

W3C validator