eulerthlema - Intuitionistic Logic Explorer

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

Theorem eulerthlema 12162

Description: Lemma for eulerth 12165. (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 999	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	phicld 12150	. . . 4 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
4		elnnuz 9502	. . . 4 ⊢ ((ϕ‘𝑁) ∈ ℕ ↔ (ϕ‘𝑁) ∈ (ℤ_≥‘1))
5	3, 4	sylib 121	. . 3 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (ℤ_≥‘1))
6		eluzfz2 9967	. . 3 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘1) → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
7	5, 6	syl 14	. 2 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
8		oveq2 5850	. . . . . . 7 ⊢ (𝑤 = 1 → (𝐴↑𝑤) = (𝐴↑1))
9		oveq2 5850	. . . . . . . 8 ⊢ (𝑤 = 1 → (1...𝑤) = (1...1))
10	9	prodeq1d 11505	. . . . . . 7 ⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...1)(𝐹‘𝑥))
11	8, 10	oveq12d 5860	. . . . . 6 ⊢ (𝑤 = 1 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)))
12	11	oveq1d 5857	. . . . 5 ⊢ (𝑤 = 1 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁))
13	9	prodeq1d 11505	. . . . . 6 ⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁))
14	13	oveq1d 5857	. . . . 5 ⊢ (𝑤 = 1 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
15	12, 14	eqeq12d 2180	. . . 4 ⊢ (𝑤 = 1 → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
16	15	imbi2d 229	. . 3 ⊢ (𝑤 = 1 → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
17		oveq2 5850	. . . . . . 7 ⊢ (𝑤 = 𝑘 → (𝐴↑𝑤) = (𝐴↑𝑘))
18		oveq2 5850	. . . . . . . 8 ⊢ (𝑤 = 𝑘 → (1...𝑤) = (1...𝑘))
19	18	prodeq1d 11505	. . . . . . 7 ⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥))
20	17, 19	oveq12d 5860	. . . . . 6 ⊢ (𝑤 = 𝑘 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)))
21	20	oveq1d 5857	. . . . 5 ⊢ (𝑤 = 𝑘 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁))
22	18	prodeq1d 11505	. . . . . 6 ⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁))
23	22	oveq1d 5857	. . . . 5 ⊢ (𝑤 = 𝑘 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
24	21, 23	eqeq12d 2180	. . . 4 ⊢ (𝑤 = 𝑘 → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
25	24	imbi2d 229	. . 3 ⊢ (𝑤 = 𝑘 → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
26		oveq2 5850	. . . . . . 7 ⊢ (𝑤 = (𝑘 + 1) → (𝐴↑𝑤) = (𝐴↑(𝑘 + 1)))
27		oveq2 5850	. . . . . . . 8 ⊢ (𝑤 = (𝑘 + 1) → (1...𝑤) = (1...(𝑘 + 1)))
28	27	prodeq1d 11505	. . . . . . 7 ⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥))
29	26, 28	oveq12d 5860	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)))
30	29	oveq1d 5857	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁))
31	27	prodeq1d 11505	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁))
32	31	oveq1d 5857	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
33	30, 32	eqeq12d 2180	. . . 4 ⊢ (𝑤 = (𝑘 + 1) → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
34	33	imbi2d 229	. . 3 ⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
35		oveq2 5850	. . . . . . 7 ⊢ (𝑤 = (ϕ‘𝑁) → (𝐴↑𝑤) = (𝐴↑(ϕ‘𝑁)))
36		oveq2 5850	. . . . . . . 8 ⊢ (𝑤 = (ϕ‘𝑁) → (1...𝑤) = (1...(ϕ‘𝑁)))
37	36	prodeq1d 11505	. . . . . . 7 ⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥))
38	35, 37	oveq12d 5860	. . . . . 6 ⊢ (𝑤 = (ϕ‘𝑁) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)))
39	38	oveq1d 5857	. . . . 5 ⊢ (𝑤 = (ϕ‘𝑁) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁))
40	36	prodeq1d 11505	. . . . . 6 ⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁))
41	40	oveq1d 5857	. . . . 5 ⊢ (𝑤 = (ϕ‘𝑁) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
42	39, 41	eqeq12d 2180	. . . 4 ⊢ (𝑤 = (ϕ‘𝑁) → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
43	42	imbi2d 229	. . 3 ⊢ (𝑤 = (ϕ‘𝑁) → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))))
44	1	simp2d 1000	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℤ)
45		eulerth.2	. . . . . . . . . . . 12 ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
46		ssrab2 3227	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
47	45, 46	eqsstri 3174	. . . . . . . . . . 11 ⊢ 𝑆 ⊆ (0..^𝑁)
48		fzo0ssnn0 10150	. . . . . . . . . . 11 ⊢ (0..^𝑁) ⊆ ℕ₀
49	47, 48	sstri 3151	. . . . . . . . . 10 ⊢ 𝑆 ⊆ ℕ₀
50		nn0ssz 9209	. . . . . . . . . 10 ⊢ ℕ₀ ⊆ ℤ
51	49, 50	sstri 3151	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℤ
52		eulerth.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)
53		f1of 5432	. . . . . . . . . . 11 ⊢ (𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
54	52, 53	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
55		1nn 8868	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
56	55	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℕ)
57	3	nnge1d 8900	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ (ϕ‘𝑁))
58		elfz1b 10025	. . . . . . . . . . 11 ⊢ (1 ∈ (1...(ϕ‘𝑁)) ↔ (1 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 1 ≤ (ϕ‘𝑁)))
59	56, 3, 57, 58	syl3anbrc 1171	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ (1...(ϕ‘𝑁)))
60	54, 59	ffvelrnd 5621	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘1) ∈ 𝑆)
61	51, 60	sselid 3140	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘1) ∈ ℤ)
62	44, 61	zmulcld 9319	. . . . . . 7 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ)
63		zq 9564	. . . . . . 7 ⊢ ((𝐴 · (𝐹‘1)) ∈ ℤ → (𝐴 · (𝐹‘1)) ∈ ℚ)
64	62, 63	syl 14	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℚ)
65		nnq 9571	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
66	2, 65	syl 14	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℚ)
67	2	nngt0d 8901	. . . . . 6 ⊢ (𝜑 → 0 < 𝑁)
68		modqabs2 10293	. . . . . 6 ⊢ (((𝐴 · (𝐹‘1)) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
69	64, 66, 67, 68	syl3anc 1228	. . . . 5 ⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
70		1z 9217	. . . . . . 7 ⊢ 1 ∈ ℤ
71	62, 2	zmodcld 10280	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℕ₀)
72	71	nn0cnd 9169	. . . . . . 7 ⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ)
73		fveq2 5486	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1))
74	73	oveq2d 5858	. . . . . . . . 9 ⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
75	74	oveq1d 5857	. . . . . . . 8 ⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
76	75	fprod1 11535	. . . . . . 7 ⊢ ((1 ∈ ℤ ∧ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ) → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
77	70, 72, 76	sylancr 411	. . . . . 6 ⊢ (𝜑 → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
78	77	oveq1d 5857	. . . . 5 ⊢ (𝜑 → (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁))
79	44	zcnd 9314	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
80	79	exp1d 10583	. . . . . . 7 ⊢ (𝜑 → (𝐴↑1) = 𝐴)
81		nn0sscn 9119	. . . . . . . . . 10 ⊢ ℕ₀ ⊆ ℂ
82	49, 81	sstri 3151	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℂ
83	82, 60	sselid 3140	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘1) ∈ ℂ)
84	73	fprod1 11535	. . . . . . . 8 ⊢ ((1 ∈ ℤ ∧ (𝐹‘1) ∈ ℂ) → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1))
85	70, 83, 84	sylancr 411	. . . . . . 7 ⊢ (𝜑 → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1))
86	80, 85	oveq12d 5860	. . . . . 6 ⊢ (𝜑 → ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
87	86	oveq1d 5857	. . . . 5 ⊢ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
88	69, 78, 87	3eqtr4rd 2209	. . . 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 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐴 ∈ ℤ)
91		elfzo1 10125	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) ↔ (𝑘 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 𝑘 < (ϕ‘𝑁)))
92	91	simp1bi 1002	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ ℕ)
93	92	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ)
94	93	nnnn0d 9167	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ₀)
95		zexpcl 10470	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ₀) → (𝐴↑𝑘) ∈ ℤ)
96	90, 94, 95	syl2anc 409	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℤ)
97	70	a1i 9	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 1 ∈ ℤ)
98	93	nnzd 9312	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℤ)
99	97, 98	fzfigd 10366	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (1...𝑘) ∈ Fin)
100	54	ad2antrr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
101		elfzelz 9960	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
102	101	zred 9313	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℝ)
103	102	adantl 275	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ ℝ)
104	3	nnzd 9312	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℤ)
105	104	ad2antrr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℤ)
106	105	zred 9313	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℝ)
107	93	nnred 8870	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℝ)
108	107	adantr 274	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
109		elfzle2 9963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ≤ 𝑘)
110	109	adantl 275	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ 𝑘)
111		elfzolt2 10091	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 < (ϕ‘𝑁))
112	111	ad2antlr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 < (ϕ‘𝑁))
113	103, 108, 106, 110, 112	lelttrd 8023	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 < (ϕ‘𝑁))
114	103, 106, 113	ltled 8017	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ (ϕ‘𝑁))
115		elfzuz 9956	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (ℤ_≥‘1))
116		elfz5 9952	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (ℤ_≥‘1) ∧ (ϕ‘𝑁) ∈ ℤ) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
117	115, 105, 116	syl2an2 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
118	114, 117	mpbird 166	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ (1...(ϕ‘𝑁)))
119	100, 118	ffvelrnd 5621	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ 𝑆)
120	51, 119	sselid 3140	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ ℤ)
121	99, 120	fprodzcl 11550	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℤ)
122	96, 121	zmulcld 9319	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℤ)
123		zq 9564	. . . . . . . . . 10 ⊢ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℤ → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ)
124	122, 123	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ)
125	124	adantr 274	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ)
126	90	adantr 274	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐴 ∈ ℤ)
127	126, 120	zmulcld 9319	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ)
128	2	ad2antrr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑁 ∈ ℕ)
129	127, 128	zmodcld 10280	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℕ₀)
130	129	nn0zd 9311	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ)
131	99, 130	fprodzcl 11550	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ)
132		zq 9564	. . . . . . . . . 10 ⊢ (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ)
133	131, 132	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ)
134	133	adantr 274	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ)
135	44	ad2antrr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝐴 ∈ ℤ)
136	54	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
137		fzofzp1 10162	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
138	137	ad2antlr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
139	136, 138	ffvelrnd 5621	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
140	51, 139	sselid 3140	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
141	135, 140	zmulcld 9319	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
142	66	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝑁 ∈ ℚ)
143	67	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 0 < 𝑁)
144		simpr 109	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
145	125, 134, 141, 142, 143, 144	modqmul1 10312	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁))
146	145	ex 114	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁)))
147	96	zcnd 9314	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℂ)
148	121	zcnd 9314	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℂ)
149	79	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐴 ∈ ℂ)
150	54	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
151	137	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
152	150, 151	ffvelrnd 5621	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
153	82, 152	sselid 3140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
154	147, 148, 149, 153	mul4d 8053	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))))
155	149, 94	expp1d 10589	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
156		elfzouz 10086	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ (ℤ_≥‘1))
157	156	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ (ℤ_≥‘1))
158	150	adantr 274	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
159		elfzelz 9960	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℤ)
160	159	zred 9313	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℝ)
161	160	adantl 275	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ ℝ)
162		peano2re 8034	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
163	107, 162	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ ℝ)
164	163	adantr 274	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
165	104	ad2antrr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℤ)
166	165	zred 9313	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℝ)
167		elfzle2 9963	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ≤ (𝑘 + 1))
168	167	adantl 275	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (𝑘 + 1))
169	137	ad2antlr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
170		elfzle2 9963	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ (1...(ϕ‘𝑁)) → (𝑘 + 1) ≤ (ϕ‘𝑁))
171	169, 170	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ≤ (ϕ‘𝑁))
172	161, 164, 166, 168, 171	letrd 8022	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (ϕ‘𝑁))
173		elfzuz 9956	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ (ℤ_≥‘1))
174	173, 165, 116	syl2an2 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
175	172, 174	mpbird 166	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ (1...(ϕ‘𝑁)))
176	158, 175	ffvelrnd 5621	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ 𝑆)
177	82, 176	sselid 3140	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℂ)
178		fveq2 5486	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1)))
179	157, 177, 178	fprodp1 11541	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥) = (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1))))
180	155, 179	oveq12d 5860	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))))
181	154, 180	eqtr4d 2201	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)))
182	181	oveq1d 5857	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁))
183	51, 152	sselid 3140	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
184	90, 183	zmulcld 9319	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
185	2	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℕ)
186	184, 185	zmodcld 10280	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℕ₀)
187	186	nn0zd 9311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ)
188		zq 9564	. . . . . . . . . 10 ⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
189	187, 188	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
190		zq 9564	. . . . . . . . . 10 ⊢ ((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ)
191	184, 190	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ)
192	66	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℚ)
193	67	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 0 < 𝑁)
194		modqabs2 10293	. . . . . . . . . 10 ⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
195	191, 192, 193, 194	syl3anc 1228	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
196	189, 191, 131, 192, 193, 195	modqmul1 10312	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
197	90	adantr 274	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐴 ∈ ℤ)
198	51, 176	sselid 3140	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℤ)
199	197, 198	zmulcld 9319	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ)
200	185	adantr 274	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑁 ∈ ℕ)
201	199, 200	zmodcld 10280	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℕ₀)
202	201	nn0cnd 9169	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ)
203	178	oveq2d 5858	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑘 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑘 + 1))))
204	203	oveq1d 5857	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
205	157, 202, 204	fprodp1 11541	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
206	186	nn0cnd 9169	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℂ)
207	131	zcnd 9314	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ)
208	206, 207	mulcomd 7920	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
209	205, 208	eqtr4d 2201	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)))
210	209	oveq1d 5857	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
211	149, 153	mulcld 7919	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℂ)
212	207, 211	mulcomd 7920	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)))
213	212	oveq1d 5857	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
214	196, 210, 213	3eqtr4rd 2209	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
215	182, 214	eqeq12d 2180	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
216	146, 215	sylibd 148	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))
217	216	expcom 115	. . . 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 10174	. 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 103 ↔ wb 104 ∧ w3a 968 = wceq 1343 ∈ wcel 2136 {crab 2448 class class class wbr 3982 ⟶wf 5184 –1-1-onto→wf1o 5187 ‘cfv 5188 (class class class)co 5842 ℂcc 7751 ℝcr 7752 0cc0 7753 1c1 7754 + caddc 7756 · cmul 7758 < clt 7933 ≤ cle 7934 ℕcn 8857 ℕ₀cn0 9114 ℤcz 9191 ℤ_≥cuz 9466 ℚcq 9557 ...cfz 9944 ..^cfzo 10077 mod cmo 10257 ↑cexp 10454 ∏cprod 11491 gcd cgcd 11875 ϕcphi 12141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871 ax-arch 7872 ax-caucvg 7873

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-isom 5197 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-irdg 6338 df-frec 6359 df-1o 6384 df-oadd 6388 df-er 6501 df-en 6707 df-dom 6708 df-fin 6709 df-sup 6949 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-3 8917 df-4 8918 df-n0 9115 df-z 9192 df-uz 9467 df-q 9558 df-rp 9590 df-fz 9945 df-fzo 10078 df-fl 10205 df-mod 10258 df-seqfrec 10381 df-exp 10455 df-ihash 10689 df-cj 10784 df-re 10785 df-im 10786 df-rsqrt 10940 df-abs 10941 df-clim 11220 df-proddc 11492 df-dvds 11728 df-gcd 11876 df-phi 12143

This theorem is referenced by: eulerthlemth 12164

W3C validator