eulerthlema - Intuitionistic Logic Explorer

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

Theorem eulerthlema 12991

Description: Lemma for eulerth 12994. (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 1040	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	phicld 12979	. . . 4 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
4		elnnuz 9942	. . . 4 ⊢ ((ϕ‘𝑁) ∈ ℕ ↔ (ϕ‘𝑁) ∈ (ℤ_≥‘1))
5	3, 4	sylib 122	. . 3 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (ℤ_≥‘1))
6		eluzfz2 10419	. . 3 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘1) → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
7	5, 6	syl 14	. 2 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
8		oveq2 6087	. . . . . . 7 ⊢ (𝑤 = 1 → (𝐴↑𝑤) = (𝐴↑1))
9		oveq2 6087	. . . . . . . 8 ⊢ (𝑤 = 1 → (1...𝑤) = (1...1))
10	9	prodeq1d 12314	. . . . . . 7 ⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...1)(𝐹‘𝑥))
11	8, 10	oveq12d 6097	. . . . . 6 ⊢ (𝑤 = 1 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)))
12	11	oveq1d 6094	. . . . 5 ⊢ (𝑤 = 1 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁))
13	9	prodeq1d 12314	. . . . . 6 ⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁))
14	13	oveq1d 6094	. . . . 5 ⊢ (𝑤 = 1 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
15	12, 14	eqeq12d 2253	. . . 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 6087	. . . . . . 7 ⊢ (𝑤 = 𝑘 → (𝐴↑𝑤) = (𝐴↑𝑘))
18		oveq2 6087	. . . . . . . 8 ⊢ (𝑤 = 𝑘 → (1...𝑤) = (1...𝑘))
19	18	prodeq1d 12314	. . . . . . 7 ⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥))
20	17, 19	oveq12d 6097	. . . . . 6 ⊢ (𝑤 = 𝑘 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)))
21	20	oveq1d 6094	. . . . 5 ⊢ (𝑤 = 𝑘 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁))
22	18	prodeq1d 12314	. . . . . 6 ⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁))
23	22	oveq1d 6094	. . . . 5 ⊢ (𝑤 = 𝑘 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
24	21, 23	eqeq12d 2253	. . . 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 6087	. . . . . . 7 ⊢ (𝑤 = (𝑘 + 1) → (𝐴↑𝑤) = (𝐴↑(𝑘 + 1)))
27		oveq2 6087	. . . . . . . 8 ⊢ (𝑤 = (𝑘 + 1) → (1...𝑤) = (1...(𝑘 + 1)))
28	27	prodeq1d 12314	. . . . . . 7 ⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥))
29	26, 28	oveq12d 6097	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)))
30	29	oveq1d 6094	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁))
31	27	prodeq1d 12314	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁))
32	31	oveq1d 6094	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
33	30, 32	eqeq12d 2253	. . . 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 6087	. . . . . . 7 ⊢ (𝑤 = (ϕ‘𝑁) → (𝐴↑𝑤) = (𝐴↑(ϕ‘𝑁)))
36		oveq2 6087	. . . . . . . 8 ⊢ (𝑤 = (ϕ‘𝑁) → (1...𝑤) = (1...(ϕ‘𝑁)))
37	36	prodeq1d 12314	. . . . . . 7 ⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥))
38	35, 37	oveq12d 6097	. . . . . 6 ⊢ (𝑤 = (ϕ‘𝑁) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)))
39	38	oveq1d 6094	. . . . 5 ⊢ (𝑤 = (ϕ‘𝑁) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁))
40	36	prodeq1d 12314	. . . . . 6 ⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁))
41	40	oveq1d 6094	. . . . 5 ⊢ (𝑤 = (ϕ‘𝑁) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
42	39, 41	eqeq12d 2253	. . . 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 1041	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℤ)
45		eulerth.2	. . . . . . . . . . . 12 ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
46		ssrab2 3333	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
47	45, 46	eqsstri 3280	. . . . . . . . . . 11 ⊢ 𝑆 ⊆ (0..^𝑁)
48		fzo0ssnn0 10616	. . . . . . . . . . 11 ⊢ (0..^𝑁) ⊆ ℕ₀
49	47, 48	sstri 3257	. . . . . . . . . 10 ⊢ 𝑆 ⊆ ℕ₀
50		nn0ssz 9645	. . . . . . . . . 10 ⊢ ℕ₀ ⊆ ℤ
51	49, 50	sstri 3257	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℤ
52		eulerth.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)
53		f1of 5637	. . . . . . . . . . 11 ⊢ (𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
54	52, 53	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
55		1nn 9298	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
56	55	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℕ)
57	3	nnge1d 9330	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ (ϕ‘𝑁))
58		elfz1b 10480	. . . . . . . . . . 11 ⊢ (1 ∈ (1...(ϕ‘𝑁)) ↔ (1 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 1 ≤ (ϕ‘𝑁)))
59	56, 3, 57, 58	syl3anbrc 1212	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ (1...(ϕ‘𝑁)))
60	54, 59	ffvelcdmd 5838	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘1) ∈ 𝑆)
61	51, 60	sselid 3246	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘1) ∈ ℤ)
62	44, 61	zmulcld 9757	. . . . . . 7 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ)
63		zq 10009	. . . . . . 7 ⊢ ((𝐴 · (𝐹‘1)) ∈ ℤ → (𝐴 · (𝐹‘1)) ∈ ℚ)
64	62, 63	syl 14	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℚ)
65		nnq 10016	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
66	2, 65	syl 14	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℚ)
67	2	nngt0d 9331	. . . . . 6 ⊢ (𝜑 → 0 < 𝑁)
68		modqabs2 10778	. . . . . 6 ⊢ (((𝐴 · (𝐹‘1)) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
69	64, 66, 67, 68	syl3anc 1278	. . . . 5 ⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
70		1z 9653	. . . . . . 7 ⊢ 1 ∈ ℤ
71	62, 2	zmodcld 10765	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℕ₀)
72	71	nn0cnd 9605	. . . . . . 7 ⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ)
73		fveq2 5693	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1))
74	73	oveq2d 6095	. . . . . . . . 9 ⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
75	74	oveq1d 6094	. . . . . . . 8 ⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
76	75	fprod1 12344	. . . . . . 7 ⊢ ((1 ∈ ℤ ∧ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ) → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
77	70, 72, 76	sylancr 418	. . . . . 6 ⊢ (𝜑 → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
78	77	oveq1d 6094	. . . . 5 ⊢ (𝜑 → (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁))
79	44	zcnd 9752	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
80	79	exp1d 11089	. . . . . . 7 ⊢ (𝜑 → (𝐴↑1) = 𝐴)
81		nn0sscn 9551	. . . . . . . . . 10 ⊢ ℕ₀ ⊆ ℂ
82	49, 81	sstri 3257	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℂ
83	82, 60	sselid 3246	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘1) ∈ ℂ)
84	73	fprod1 12344	. . . . . . . 8 ⊢ ((1 ∈ ℤ ∧ (𝐹‘1) ∈ ℂ) → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1))
85	70, 83, 84	sylancr 418	. . . . . . 7 ⊢ (𝜑 → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1))
86	80, 85	oveq12d 6097	. . . . . 6 ⊢ (𝜑 → ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
87	86	oveq1d 6094	. . . . 5 ⊢ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
88	69, 78, 87	3eqtr4rd 2282	. . . 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 10586	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) ↔ (𝑘 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 𝑘 < (ϕ‘𝑁)))
92	91	simp1bi 1043	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ ℕ)
93	92	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ)
94	93	nnnn0d 9603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ₀)
95		zexpcl 10974	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ₀) → (𝐴↑𝑘) ∈ ℤ)
96	90, 94, 95	syl2anc 415	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℤ)
97	70	a1i 9	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 1 ∈ ℤ)
98	93	nnzd 9750	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℤ)
99	97, 98	fzfigd 10851	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (1...𝑘) ∈ Fin)
100	54	ad2antrr 492	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
101		elfzelz 10411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
102	101	zred 9751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℝ)
103	102	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ ℝ)
104	3	nnzd 9750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℤ)
105	104	ad2antrr 492	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℤ)
106	105	zred 9751	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℝ)
107	93	nnred 9300	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℝ)
108	107	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
109		elfzle2 10415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ≤ 𝑘)
110	109	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ 𝑘)
111		elfzolt2 10547	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 < (ϕ‘𝑁))
112	111	ad2antlr 493	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 < (ϕ‘𝑁))
113	103, 108, 106, 110, 112	lelttrd 8445	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 < (ϕ‘𝑁))
114	103, 106, 113	ltled 8439	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ (ϕ‘𝑁))
115		elfzuz 10407	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (ℤ_≥‘1))
116		elfz5 10403	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (ℤ_≥‘1) ∧ (ϕ‘𝑁) ∈ ℤ) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
117	115, 105, 116	syl2an2 602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
118	114, 117	mpbird 167	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ (1...(ϕ‘𝑁)))
119	100, 118	ffvelcdmd 5838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ 𝑆)
120	51, 119	sselid 3246	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ ℤ)
121	99, 120	fprodzcl 12359	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℤ)
122	96, 121	zmulcld 9757	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℤ)
123		zq 10009	. . . . . . . . . 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 9757	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ)
128	2	ad2antrr 492	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑁 ∈ ℕ)
129	127, 128	zmodcld 10765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℕ₀)
130	129	nn0zd 9749	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ)
131	99, 130	fprodzcl 12359	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ)
132		zq 10009	. . . . . . . . . 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 492	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝐴 ∈ ℤ)
136	54	ad2antrr 492	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
137		fzofzp1 10628	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
138	137	ad2antlr 493	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
139	136, 138	ffvelcdmd 5838	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
140	51, 139	sselid 3246	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
141	135, 140	zmulcld 9757	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
142	66	ad2antrr 492	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝑁 ∈ ℚ)
143	67	ad2antrr 492	. . . . . . . 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 10797	. . . . . . 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 9752	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℂ)
148	121	zcnd 9752	. . . . . . . . . 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 5838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
153	82, 152	sselid 3246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
154	147, 148, 149, 153	mul4d 8475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))))
155	149, 94	expp1d 11095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
156		elfzouz 10541	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ (ℤ_≥‘1))
157	156	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ (ℤ_≥‘1))
158	150	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
159		elfzelz 10411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℤ)
160	159	zred 9751	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℝ)
161	160	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ ℝ)
162		peano2re 8456	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
163	107, 162	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ ℝ)
164	163	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
165	104	ad2antrr 492	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℤ)
166	165	zred 9751	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℝ)
167		elfzle2 10415	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ≤ (𝑘 + 1))
168	167	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (𝑘 + 1))
169	137	ad2antlr 493	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
170		elfzle2 10415	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ (1...(ϕ‘𝑁)) → (𝑘 + 1) ≤ (ϕ‘𝑁))
171	169, 170	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ≤ (ϕ‘𝑁))
172	161, 164, 166, 168, 171	letrd 8444	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (ϕ‘𝑁))
173		elfzuz 10407	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ (ℤ_≥‘1))
174	173, 165, 116	syl2an2 602	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
175	172, 174	mpbird 167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ (1...(ϕ‘𝑁)))
176	158, 175	ffvelcdmd 5838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ 𝑆)
177	82, 176	sselid 3246	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℂ)
178		fveq2 5693	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1)))
179	157, 177, 178	fprodp1 12350	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥) = (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1))))
180	155, 179	oveq12d 6097	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))))
181	154, 180	eqtr4d 2274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)))
182	181	oveq1d 6094	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁))
183	51, 152	sselid 3246	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
184	90, 183	zmulcld 9757	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
185	2	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℕ)
186	184, 185	zmodcld 10765	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℕ₀)
187	186	nn0zd 9749	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ)
188		zq 10009	. . . . . . . . . 10 ⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
189	187, 188	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
190		zq 10009	. . . . . . . . . 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 10778	. . . . . . . . . 10 ⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
195	191, 192, 193, 194	syl3anc 1278	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
196	189, 191, 131, 192, 193, 195	modqmul1 10797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
197	90	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐴 ∈ ℤ)
198	51, 176	sselid 3246	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℤ)
199	197, 198	zmulcld 9757	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ)
200	185	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑁 ∈ ℕ)
201	199, 200	zmodcld 10765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℕ₀)
202	201	nn0cnd 9605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ)
203	178	oveq2d 6095	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑘 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑘 + 1))))
204	203	oveq1d 6094	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
205	157, 202, 204	fprodp1 12350	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
206	186	nn0cnd 9605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℂ)
207	131	zcnd 9752	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ)
208	206, 207	mulcomd 8341	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
209	205, 208	eqtr4d 2274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)))
210	209	oveq1d 6094	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
211	149, 153	mulcld 8340	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℂ)
212	207, 211	mulcomd 8341	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)))
213	212	oveq1d 6094	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
214	196, 210, 213	3eqtr4rd 2282	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
215	182, 214	eqeq12d 2253	. . . . . 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 10641	. 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 1009 = wceq 1402 ∈ wcel 2209 {crab 2532 class class class wbr 4128 ⟶wf 5371 –1-1-onto→wf1o 5374 ‘cfv 5375 (class class class)co 6079 ℂcc 8171 ℝcr 8172 0cc0 8173 1c1 8174 + caddc 8176 · cmul 8178 < clt 8354 ≤ cle 8355 ℕcn 9287 ℕ₀cn0 9546 ℤcz 9627 ℤ_≥cuz 9904 ℚcq 10002 ...cfz 10394 ..^cfzo 10532 mod cmo 10742 ↑cexp 10958 ∏cprod 12300 gcd cgcd 12713 ϕcphi 12970

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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733 ax-cnex 8264 ax-resscn 8265 ax-1cn 8266 ax-1re 8267 ax-icn 8268 ax-addcl 8269 ax-addrcl 8270 ax-mulcl 8271 ax-mulrcl 8272 ax-addcom 8273 ax-mulcom 8274 ax-addass 8275 ax-mulass 8276 ax-distr 8277 ax-i2m1 8278 ax-0lt1 8279 ax-1rid 8280 ax-0id 8281 ax-rnegex 8282 ax-precex 8283 ax-cnre 8284 ax-pre-ltirr 8285 ax-pre-ltwlin 8286 ax-pre-lttrn 8287 ax-pre-apti 8288 ax-pre-ltadd 8289 ax-pre-mulgt0 8290 ax-pre-mulext 8291 ax-arch 8292 ax-caucvg 8293

This theorem depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-id 4436 df-po 4439 df-iso 4440 df-iord 4509 df-on 4511 df-ilim 4512 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-isom 5384 df-riota 6032 df-ov 6082 df-oprab 6083 df-mpo 6084 df-1st 6368 df-2nd 6369 df-recs 6570 df-irdg 6635 df-frec 6656 df-1o 6681 df-oadd 6685 df-er 6801 df-en 7017 df-dom 7018 df-fin 7019 df-sup 7318 df-pnf 8356 df-mnf 8357 df-xr 8358 df-ltxr 8359 df-le 8360 df-sub 8493 df-neg 8494 df-reap 8897 df-ap 8904 df-div 8997 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-n0 9547 df-z 9628 df-uz 9905 df-q 10003 df-rp 10038 df-fz 10395 df-fzo 10533 df-fl 10688 df-mod 10743 df-seqfrec 10868 df-exp 10959 df-ihash 11198 df-cj 11590 df-re 11591 df-im 11592 df-rsqrt 11747 df-abs 11748 df-clim 12028 df-proddc 12301 df-dvds 12538 df-gcd 12714 df-phi 12972

This theorem is referenced by: eulerthlemth 12993

W3C validator