eulerthlema - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > eulerthlema		GIF version

Theorem eulerthlema 12423

Description: Lemma for eulerth 12426. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)

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

**Assertion**
Ref	Expression
eulerthlema	⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))

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

Proof of Theorem eulerthlema Dummy variables 𝑘 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerth.1	. . . . . 6 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))
2	1	simp1d 1011	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	phicld 12411	. . . 4 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
4		elnnuz 9655	. . . 4 ⊢ ((ϕ‘𝑁) ∈ ℕ ↔ (ϕ‘𝑁) ∈ (ℤ_≥‘1))
5	3, 4	sylib 122	. . 3 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (ℤ_≥‘1))
6		eluzfz2 10124	. . 3 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘1) → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
7	5, 6	syl 14	. 2 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
8		oveq2 5933	. . . . . . 7 ⊢ (𝑤 = 1 → (𝐴↑𝑤) = (𝐴↑1))
9		oveq2 5933	. . . . . . . 8 ⊢ (𝑤 = 1 → (1...𝑤) = (1...1))
10	9	prodeq1d 11746	. . . . . . 7 ⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...1)(𝐹‘𝑥))
11	8, 10	oveq12d 5943	. . . . . 6 ⊢ (𝑤 = 1 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)))
12	11	oveq1d 5940	. . . . 5 ⊢ (𝑤 = 1 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁))
13	9	prodeq1d 11746	. . . . . 6 ⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁))
14	13	oveq1d 5940	. . . . 5 ⊢ (𝑤 = 1 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
15	12, 14	eqeq12d 2211	. . . 4 ⊢ (𝑤 = 1 → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
16	15	imbi2d 230	. . 3 ⊢ (𝑤 = 1 → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
17		oveq2 5933	. . . . . . 7 ⊢ (𝑤 = 𝑘 → (𝐴↑𝑤) = (𝐴↑𝑘))
18		oveq2 5933	. . . . . . . 8 ⊢ (𝑤 = 𝑘 → (1...𝑤) = (1...𝑘))
19	18	prodeq1d 11746	. . . . . . 7 ⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥))
20	17, 19	oveq12d 5943	. . . . . 6 ⊢ (𝑤 = 𝑘 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)))
21	20	oveq1d 5940	. . . . 5 ⊢ (𝑤 = 𝑘 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁))
22	18	prodeq1d 11746	. . . . . 6 ⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁))
23	22	oveq1d 5940	. . . . 5 ⊢ (𝑤 = 𝑘 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
24	21, 23	eqeq12d 2211	. . . 4 ⊢ (𝑤 = 𝑘 → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
25	24	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑘 → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
26		oveq2 5933	. . . . . . 7 ⊢ (𝑤 = (𝑘 + 1) → (𝐴↑𝑤) = (𝐴↑(𝑘 + 1)))
27		oveq2 5933	. . . . . . . 8 ⊢ (𝑤 = (𝑘 + 1) → (1...𝑤) = (1...(𝑘 + 1)))
28	27	prodeq1d 11746	. . . . . . 7 ⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥))
29	26, 28	oveq12d 5943	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)))
30	29	oveq1d 5940	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁))
31	27	prodeq1d 11746	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁))
32	31	oveq1d 5940	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
33	30, 32	eqeq12d 2211	. . . 4 ⊢ (𝑤 = (𝑘 + 1) → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
34	33	imbi2d 230	. . 3 ⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
35		oveq2 5933	. . . . . . 7 ⊢ (𝑤 = (ϕ‘𝑁) → (𝐴↑𝑤) = (𝐴↑(ϕ‘𝑁)))
36		oveq2 5933	. . . . . . . 8 ⊢ (𝑤 = (ϕ‘𝑁) → (1...𝑤) = (1...(ϕ‘𝑁)))
37	36	prodeq1d 11746	. . . . . . 7 ⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥))
38	35, 37	oveq12d 5943	. . . . . 6 ⊢ (𝑤 = (ϕ‘𝑁) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)))
39	38	oveq1d 5940	. . . . 5 ⊢ (𝑤 = (ϕ‘𝑁) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁))
40	36	prodeq1d 11746	. . . . . 6 ⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁))
41	40	oveq1d 5940	. . . . 5 ⊢ (𝑤 = (ϕ‘𝑁) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
42	39, 41	eqeq12d 2211	. . . 4 ⊢ (𝑤 = (ϕ‘𝑁) → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
43	42	imbi2d 230	. . 3 ⊢ (𝑤 = (ϕ‘𝑁) → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
44	1	simp2d 1012	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℤ)
45		eulerth.2	. . . . . . . . . . . 12 ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
46		ssrab2 3269	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
47	45, 46	eqsstri 3216	. . . . . . . . . . 11 ⊢ 𝑆 ⊆ (0..^𝑁)
48		fzo0ssnn0 10308	. . . . . . . . . . 11 ⊢ (0..^𝑁) ⊆ ℕ₀
49	47, 48	sstri 3193	. . . . . . . . . 10 ⊢ 𝑆 ⊆ ℕ₀
50		nn0ssz 9361	. . . . . . . . . 10 ⊢ ℕ₀ ⊆ ℤ
51	49, 50	sstri 3193	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℤ
52		eulerth.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)
53		f1of 5507	. . . . . . . . . . 11 ⊢ (𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
54	52, 53	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
55		1nn 9018	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
56	55	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℕ)
57	3	nnge1d 9050	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ (ϕ‘𝑁))
58		elfz1b 10182	. . . . . . . . . . 11 ⊢ (1 ∈ (1...(ϕ‘𝑁)) ↔ (1 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 1 ≤ (ϕ‘𝑁)))
59	56, 3, 57, 58	syl3anbrc 1183	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ (1...(ϕ‘𝑁)))
60	54, 59	ffvelcdmd 5701	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘1) ∈ 𝑆)
61	51, 60	sselid 3182	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘1) ∈ ℤ)
62	44, 61	zmulcld 9471	. . . . . . 7 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ)
63		zq 9717	. . . . . . 7 ⊢ ((𝐴 · (𝐹‘1)) ∈ ℤ → (𝐴 · (𝐹‘1)) ∈ ℚ)
64	62, 63	syl 14	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℚ)
65		nnq 9724	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
66	2, 65	syl 14	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℚ)
67	2	nngt0d 9051	. . . . . 6 ⊢ (𝜑 → 0 < 𝑁)
68		modqabs2 10467	. . . . . 6 ⊢ (((𝐴 · (𝐹‘1)) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
69	64, 66, 67, 68	syl3anc 1249	. . . . 5 ⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
70		1z 9369	. . . . . . 7 ⊢ 1 ∈ ℤ
71	62, 2	zmodcld 10454	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℕ₀)
72	71	nn0cnd 9321	. . . . . . 7 ⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ)
73		fveq2 5561	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1))
74	73	oveq2d 5941	. . . . . . . . 9 ⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
75	74	oveq1d 5940	. . . . . . . 8 ⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
76	75	fprod1 11776	. . . . . . 7 ⊢ ((1 ∈ ℤ ∧ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ) → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
77	70, 72, 76	sylancr 414	. . . . . 6 ⊢ (𝜑 → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
78	77	oveq1d 5940	. . . . 5 ⊢ (𝜑 → (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁))
79	44	zcnd 9466	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
80	79	exp1d 10777	. . . . . . 7 ⊢ (𝜑 → (𝐴↑1) = 𝐴)
81		nn0sscn 9271	. . . . . . . . . 10 ⊢ ℕ₀ ⊆ ℂ
82	49, 81	sstri 3193	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℂ
83	82, 60	sselid 3182	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘1) ∈ ℂ)
84	73	fprod1 11776	. . . . . . . 8 ⊢ ((1 ∈ ℤ ∧ (𝐹‘1) ∈ ℂ) → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1))
85	70, 83, 84	sylancr 414	. . . . . . 7 ⊢ (𝜑 → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1))
86	80, 85	oveq12d 5943	. . . . . 6 ⊢ (𝜑 → ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
87	86	oveq1d 5940	. . . . 5 ⊢ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
88	69, 78, 87	3eqtr4rd 2240	. . . 4 ⊢ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
89	88	a1i 9	. . 3 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘1) → (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
90	44	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐴 ∈ ℤ)
91		elfzo1 10283	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) ↔ (𝑘 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 𝑘 < (ϕ‘𝑁)))
92	91	simp1bi 1014	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ ℕ)
93	92	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ)
94	93	nnnn0d 9319	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ₀)
95		zexpcl 10663	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ₀) → (𝐴↑𝑘) ∈ ℤ)
96	90, 94, 95	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℤ)
97	70	a1i 9	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 1 ∈ ℤ)
98	93	nnzd 9464	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℤ)
99	97, 98	fzfigd 10540	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (1...𝑘) ∈ Fin)
100	54	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
101		elfzelz 10117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
102	101	zred 9465	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℝ)
103	102	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ ℝ)
104	3	nnzd 9464	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℤ)
105	104	ad2antrr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℤ)
106	105	zred 9465	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℝ)
107	93	nnred 9020	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℝ)
108	107	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
109		elfzle2 10120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ≤ 𝑘)
110	109	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ 𝑘)
111		elfzolt2 10249	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 < (ϕ‘𝑁))
112	111	ad2antlr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 < (ϕ‘𝑁))
113	103, 108, 106, 110, 112	lelttrd 8168	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 < (ϕ‘𝑁))
114	103, 106, 113	ltled 8162	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ (ϕ‘𝑁))
115		elfzuz 10113	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (ℤ_≥‘1))
116		elfz5 10109	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (ℤ_≥‘1) ∧ (ϕ‘𝑁) ∈ ℤ) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
117	115, 105, 116	syl2an2 594	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
118	114, 117	mpbird 167	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ (1...(ϕ‘𝑁)))
119	100, 118	ffvelcdmd 5701	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ 𝑆)
120	51, 119	sselid 3182	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ ℤ)
121	99, 120	fprodzcl 11791	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℤ)
122	96, 121	zmulcld 9471	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℤ)
123		zq 9717	. . . . . . . . . 10 ⊢ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℤ → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ)
124	122, 123	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ)
125	124	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ)
126	90	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐴 ∈ ℤ)
127	126, 120	zmulcld 9471	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ)
128	2	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑁 ∈ ℕ)
129	127, 128	zmodcld 10454	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℕ₀)
130	129	nn0zd 9463	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ)
131	99, 130	fprodzcl 11791	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ)
132		zq 9717	. . . . . . . . . 10 ⊢ (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ)
133	131, 132	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ)
134	133	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ)
135	44	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝐴 ∈ ℤ)
136	54	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
137		fzofzp1 10320	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
138	137	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
139	136, 138	ffvelcdmd 5701	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
140	51, 139	sselid 3182	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
141	135, 140	zmulcld 9471	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
142	66	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝑁 ∈ ℚ)
143	67	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 0 < 𝑁)
144		simpr 110	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
145	125, 134, 141, 142, 143, 144	modqmul1 10486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁))
146	145	ex 115	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁)))
147	96	zcnd 9466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℂ)
148	121	zcnd 9466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℂ)
149	79	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐴 ∈ ℂ)
150	54	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
151	137	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
152	150, 151	ffvelcdmd 5701	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
153	82, 152	sselid 3182	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
154	147, 148, 149, 153	mul4d 8198	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))))
155	149, 94	expp1d 10783	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
156		elfzouz 10243	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ (ℤ_≥‘1))
157	156	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ (ℤ_≥‘1))
158	150	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
159		elfzelz 10117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℤ)
160	159	zred 9465	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℝ)
161	160	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ ℝ)
162		peano2re 8179	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
163	107, 162	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ ℝ)
164	163	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
165	104	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℤ)
166	165	zred 9465	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℝ)
167		elfzle2 10120	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ≤ (𝑘 + 1))
168	167	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (𝑘 + 1))
169	137	ad2antlr 489	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
170		elfzle2 10120	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ (1...(ϕ‘𝑁)) → (𝑘 + 1) ≤ (ϕ‘𝑁))
171	169, 170	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ≤ (ϕ‘𝑁))
172	161, 164, 166, 168, 171	letrd 8167	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (ϕ‘𝑁))
173		elfzuz 10113	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ (ℤ_≥‘1))
174	173, 165, 116	syl2an2 594	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
175	172, 174	mpbird 167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ (1...(ϕ‘𝑁)))
176	158, 175	ffvelcdmd 5701	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ 𝑆)
177	82, 176	sselid 3182	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℂ)
178		fveq2 5561	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1)))
179	157, 177, 178	fprodp1 11782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥) = (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1))))
180	155, 179	oveq12d 5943	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))))
181	154, 180	eqtr4d 2232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)))
182	181	oveq1d 5940	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁))
183	51, 152	sselid 3182	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
184	90, 183	zmulcld 9471	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
185	2	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℕ)
186	184, 185	zmodcld 10454	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℕ₀)
187	186	nn0zd 9463	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ)
188		zq 9717	. . . . . . . . . 10 ⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
189	187, 188	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
190		zq 9717	. . . . . . . . . 10 ⊢ ((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ)
191	184, 190	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ)
192	66	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℚ)
193	67	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 0 < 𝑁)
194		modqabs2 10467	. . . . . . . . . 10 ⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
195	191, 192, 193, 194	syl3anc 1249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
196	189, 191, 131, 192, 193, 195	modqmul1 10486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
197	90	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐴 ∈ ℤ)
198	51, 176	sselid 3182	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℤ)
199	197, 198	zmulcld 9471	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ)
200	185	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑁 ∈ ℕ)
201	199, 200	zmodcld 10454	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℕ₀)
202	201	nn0cnd 9321	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ)
203	178	oveq2d 5941	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑘 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑘 + 1))))
204	203	oveq1d 5940	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
205	157, 202, 204	fprodp1 11782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
206	186	nn0cnd 9321	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℂ)
207	131	zcnd 9466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ)
208	206, 207	mulcomd 8065	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
209	205, 208	eqtr4d 2232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)))
210	209	oveq1d 5940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
211	149, 153	mulcld 8064	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℂ)
212	207, 211	mulcomd 8065	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)))
213	212	oveq1d 5940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
214	196, 210, 213	3eqtr4rd 2240	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
215	182, 214	eqeq12d 2211	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
216	146, 215	sylibd 149	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
217	216	expcom 116	. . . 4 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝜑 → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
218	217	a2d 26	. . 3 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → ((𝜑 → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝜑 → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
219	16, 25, 34, 43, 89, 218	fzind2 10332	. 2 ⊢ ((ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)) → (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
220	7, 219	mpcom 36	1 ⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 {crab 2479 class class class wbr 4034 ⟶wf 5255 –1-1-onto→wf1o 5258 ‘cfv 5259 (class class class)co 5925 ℂcc 7894 ℝcr 7895 0cc0 7896 1c1 7897 + caddc 7899 · cmul 7901 < clt 8078 ≤ cle 8079 ℕcn 9007 ℕ₀cn0 9266 ℤcz 9343 ℤ_≥cuz 9618 ℚcq 9710 ...cfz 10100 ..^cfzo 10234 mod cmo 10431 ↑cexp 10647 ∏cprod 11732 gcd cgcd 12145 ϕcphi 12402

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-mulrcl 7995 ax-addcom 7996 ax-mulcom 7997 ax-addass 7998 ax-mulass 7999 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-1rid 8003 ax-0id 8004 ax-rnegex 8005 ax-precex 8006 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012 ax-pre-mulgt0 8013 ax-pre-mulext 8014 ax-arch 8015 ax-caucvg 8016

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1st 6207 df-2nd 6208 df-recs 6372 df-irdg 6437 df-frec 6458 df-1o 6483 df-oadd 6487 df-er 6601 df-en 6809 df-dom 6810 df-fin 6811 df-sup 7059 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-reap 8619 df-ap 8626 df-div 8717 df-inn 9008 df-2 9066 df-3 9067 df-4 9068 df-n0 9267 df-z 9344 df-uz 9619 df-q 9711 df-rp 9746 df-fz 10101 df-fzo 10235 df-fl 10377 df-mod 10432 df-seqfrec 10557 df-exp 10648 df-ihash 10885 df-cj 11024 df-re 11025 df-im 11026 df-rsqrt 11180 df-abs 11181 df-clim 11461 df-proddc 11733 df-dvds 11970 df-gcd 12146 df-phi 12404

This theorem is referenced by: eulerthlemth 12425

W3C validator