eulerthlema - Intuitionistic Logic Explorer

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

Theorem eulerthlema 12760

Description: Lemma for eulerth 12763. (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 1033	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	phicld 12748	. . . 4 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
4		elnnuz 9767	. . . 4 ⊢ ((ϕ‘𝑁) ∈ ℕ ↔ (ϕ‘𝑁) ∈ (ℤ_≥‘1))
5	3, 4	sylib 122	. . 3 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (ℤ_≥‘1))
6		eluzfz2 10236	. . 3 ⊢ ((ϕ‘𝑁) ∈ (ℤ_≥‘1) → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
7	5, 6	syl 14	. 2 ⊢ (𝜑 → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
8		oveq2 6015	. . . . . . 7 ⊢ (𝑤 = 1 → (𝐴↑𝑤) = (𝐴↑1))
9		oveq2 6015	. . . . . . . 8 ⊢ (𝑤 = 1 → (1...𝑤) = (1...1))
10	9	prodeq1d 12083	. . . . . . 7 ⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...1)(𝐹‘𝑥))
11	8, 10	oveq12d 6025	. . . . . 6 ⊢ (𝑤 = 1 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)))
12	11	oveq1d 6022	. . . . 5 ⊢ (𝑤 = 1 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁))
13	9	prodeq1d 12083	. . . . . 6 ⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁))
14	13	oveq1d 6022	. . . . 5 ⊢ (𝑤 = 1 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
15	12, 14	eqeq12d 2244	. . . 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 6015	. . . . . . 7 ⊢ (𝑤 = 𝑘 → (𝐴↑𝑤) = (𝐴↑𝑘))
18		oveq2 6015	. . . . . . . 8 ⊢ (𝑤 = 𝑘 → (1...𝑤) = (1...𝑘))
19	18	prodeq1d 12083	. . . . . . 7 ⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥))
20	17, 19	oveq12d 6025	. . . . . 6 ⊢ (𝑤 = 𝑘 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)))
21	20	oveq1d 6022	. . . . 5 ⊢ (𝑤 = 𝑘 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁))
22	18	prodeq1d 12083	. . . . . 6 ⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁))
23	22	oveq1d 6022	. . . . 5 ⊢ (𝑤 = 𝑘 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
24	21, 23	eqeq12d 2244	. . . 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 6015	. . . . . . 7 ⊢ (𝑤 = (𝑘 + 1) → (𝐴↑𝑤) = (𝐴↑(𝑘 + 1)))
27		oveq2 6015	. . . . . . . 8 ⊢ (𝑤 = (𝑘 + 1) → (1...𝑤) = (1...(𝑘 + 1)))
28	27	prodeq1d 12083	. . . . . . 7 ⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥))
29	26, 28	oveq12d 6025	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)))
30	29	oveq1d 6022	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁))
31	27	prodeq1d 12083	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁))
32	31	oveq1d 6022	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
33	30, 32	eqeq12d 2244	. . . 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 6015	. . . . . . 7 ⊢ (𝑤 = (ϕ‘𝑁) → (𝐴↑𝑤) = (𝐴↑(ϕ‘𝑁)))
36		oveq2 6015	. . . . . . . 8 ⊢ (𝑤 = (ϕ‘𝑁) → (1...𝑤) = (1...(ϕ‘𝑁)))
37	36	prodeq1d 12083	. . . . . . 7 ⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥))
38	35, 37	oveq12d 6025	. . . . . 6 ⊢ (𝑤 = (ϕ‘𝑁) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)))
39	38	oveq1d 6022	. . . . 5 ⊢ (𝑤 = (ϕ‘𝑁) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁))
40	36	prodeq1d 12083	. . . . . 6 ⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁))
41	40	oveq1d 6022	. . . . 5 ⊢ (𝑤 = (ϕ‘𝑁) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
42	39, 41	eqeq12d 2244	. . . 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 1034	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℤ)
45		eulerth.2	. . . . . . . . . . . 12 ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
46		ssrab2 3309	. . . . . . . . . . . 12 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
47	45, 46	eqsstri 3256	. . . . . . . . . . 11 ⊢ 𝑆 ⊆ (0..^𝑁)
48		fzo0ssnn0 10429	. . . . . . . . . . 11 ⊢ (0..^𝑁) ⊆ ℕ₀
49	47, 48	sstri 3233	. . . . . . . . . 10 ⊢ 𝑆 ⊆ ℕ₀
50		nn0ssz 9472	. . . . . . . . . 10 ⊢ ℕ₀ ⊆ ℤ
51	49, 50	sstri 3233	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℤ
52		eulerth.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)
53		f1of 5574	. . . . . . . . . . 11 ⊢ (𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
54	52, 53	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
55		1nn 9129	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
56	55	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℕ)
57	3	nnge1d 9161	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ (ϕ‘𝑁))
58		elfz1b 10294	. . . . . . . . . . 11 ⊢ (1 ∈ (1...(ϕ‘𝑁)) ↔ (1 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 1 ≤ (ϕ‘𝑁)))
59	56, 3, 57, 58	syl3anbrc 1205	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ (1...(ϕ‘𝑁)))
60	54, 59	ffvelcdmd 5773	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘1) ∈ 𝑆)
61	51, 60	sselid 3222	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘1) ∈ ℤ)
62	44, 61	zmulcld 9583	. . . . . . 7 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ)
63		zq 9829	. . . . . . 7 ⊢ ((𝐴 · (𝐹‘1)) ∈ ℤ → (𝐴 · (𝐹‘1)) ∈ ℚ)
64	62, 63	syl 14	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℚ)
65		nnq 9836	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
66	2, 65	syl 14	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℚ)
67	2	nngt0d 9162	. . . . . 6 ⊢ (𝜑 → 0 < 𝑁)
68		modqabs2 10588	. . . . . 6 ⊢ (((𝐴 · (𝐹‘1)) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
69	64, 66, 67, 68	syl3anc 1271	. . . . 5 ⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
70		1z 9480	. . . . . . 7 ⊢ 1 ∈ ℤ
71	62, 2	zmodcld 10575	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℕ₀)
72	71	nn0cnd 9432	. . . . . . 7 ⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ)
73		fveq2 5629	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1))
74	73	oveq2d 6023	. . . . . . . . 9 ⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
75	74	oveq1d 6022	. . . . . . . 8 ⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
76	75	fprod1 12113	. . . . . . 7 ⊢ ((1 ∈ ℤ ∧ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ) → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
77	70, 72, 76	sylancr 414	. . . . . 6 ⊢ (𝜑 → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
78	77	oveq1d 6022	. . . . 5 ⊢ (𝜑 → (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁))
79	44	zcnd 9578	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
80	79	exp1d 10898	. . . . . . 7 ⊢ (𝜑 → (𝐴↑1) = 𝐴)
81		nn0sscn 9382	. . . . . . . . . 10 ⊢ ℕ₀ ⊆ ℂ
82	49, 81	sstri 3233	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℂ
83	82, 60	sselid 3222	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘1) ∈ ℂ)
84	73	fprod1 12113	. . . . . . . 8 ⊢ ((1 ∈ ℤ ∧ (𝐹‘1) ∈ ℂ) → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1))
85	70, 83, 84	sylancr 414	. . . . . . 7 ⊢ (𝜑 → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1))
86	80, 85	oveq12d 6025	. . . . . 6 ⊢ (𝜑 → ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = (𝐴 · (𝐹‘1)))
87	86	oveq1d 6022	. . . . 5 ⊢ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
88	69, 78, 87	3eqtr4rd 2273	. . . 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 10399	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) ↔ (𝑘 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 𝑘 < (ϕ‘𝑁)))
92	91	simp1bi 1036	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ ℕ)
93	92	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ)
94	93	nnnn0d 9430	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ₀)
95		zexpcl 10784	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ₀) → (𝐴↑𝑘) ∈ ℤ)
96	90, 94, 95	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℤ)
97	70	a1i 9	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 1 ∈ ℤ)
98	93	nnzd 9576	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℤ)
99	97, 98	fzfigd 10661	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (1...𝑘) ∈ Fin)
100	54	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
101		elfzelz 10229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
102	101	zred 9577	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℝ)
103	102	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ ℝ)
104	3	nnzd 9576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℤ)
105	104	ad2antrr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℤ)
106	105	zred 9577	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℝ)
107	93	nnred 9131	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℝ)
108	107	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
109		elfzle2 10232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ≤ 𝑘)
110	109	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ 𝑘)
111		elfzolt2 10361	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 < (ϕ‘𝑁))
112	111	ad2antlr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 < (ϕ‘𝑁))
113	103, 108, 106, 110, 112	lelttrd 8279	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 < (ϕ‘𝑁))
114	103, 106, 113	ltled 8273	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ (ϕ‘𝑁))
115		elfzuz 10225	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (ℤ_≥‘1))
116		elfz5 10221	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (ℤ_≥‘1) ∧ (ϕ‘𝑁) ∈ ℤ) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
117	115, 105, 116	syl2an2 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
118	114, 117	mpbird 167	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ (1...(ϕ‘𝑁)))
119	100, 118	ffvelcdmd 5773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ 𝑆)
120	51, 119	sselid 3222	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ ℤ)
121	99, 120	fprodzcl 12128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℤ)
122	96, 121	zmulcld 9583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℤ)
123		zq 9829	. . . . . . . . . 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 9583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ)
128	2	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑁 ∈ ℕ)
129	127, 128	zmodcld 10575	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℕ₀)
130	129	nn0zd 9575	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ)
131	99, 130	fprodzcl 12128	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ)
132		zq 9829	. . . . . . . . . 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 10441	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
138	137	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
139	136, 138	ffvelcdmd 5773	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
140	51, 139	sselid 3222	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
141	135, 140	zmulcld 9583	. . . . . . . 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 10607	. . . . . . 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 9578	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℂ)
148	121	zcnd 9578	. . . . . . . . . 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 5773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
153	82, 152	sselid 3222	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
154	147, 148, 149, 153	mul4d 8309	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))))
155	149, 94	expp1d 10904	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
156		elfzouz 10355	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ (ℤ_≥‘1))
157	156	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ (ℤ_≥‘1))
158	150	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
159		elfzelz 10229	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℤ)
160	159	zred 9577	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℝ)
161	160	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ ℝ)
162		peano2re 8290	. . . . . . . . . . . . . . . . 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 9577	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℝ)
167		elfzle2 10232	. . . . . . . . . . . . . . . 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 10232	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ (1...(ϕ‘𝑁)) → (𝑘 + 1) ≤ (ϕ‘𝑁))
171	169, 170	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ≤ (ϕ‘𝑁))
172	161, 164, 166, 168, 171	letrd 8278	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (ϕ‘𝑁))
173		elfzuz 10225	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ (ℤ_≥‘1))
174	173, 165, 116	syl2an2 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
175	172, 174	mpbird 167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ (1...(ϕ‘𝑁)))
176	158, 175	ffvelcdmd 5773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ 𝑆)
177	82, 176	sselid 3222	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℂ)
178		fveq2 5629	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1)))
179	157, 177, 178	fprodp1 12119	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥) = (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1))))
180	155, 179	oveq12d 6025	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))))
181	154, 180	eqtr4d 2265	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)))
182	181	oveq1d 6022	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁))
183	51, 152	sselid 3222	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
184	90, 183	zmulcld 9583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
185	2	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℕ)
186	184, 185	zmodcld 10575	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℕ₀)
187	186	nn0zd 9575	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ)
188		zq 9829	. . . . . . . . . 10 ⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
189	187, 188	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
190		zq 9829	. . . . . . . . . 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 10588	. . . . . . . . . 10 ⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
195	191, 192, 193, 194	syl3anc 1271	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
196	189, 191, 131, 192, 193, 195	modqmul1 10607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
197	90	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐴 ∈ ℤ)
198	51, 176	sselid 3222	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℤ)
199	197, 198	zmulcld 9583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ)
200	185	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑁 ∈ ℕ)
201	199, 200	zmodcld 10575	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℕ₀)
202	201	nn0cnd 9432	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ)
203	178	oveq2d 6023	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑘 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑘 + 1))))
204	203	oveq1d 6022	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑘 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
205	157, 202, 204	fprodp1 12119	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
206	186	nn0cnd 9432	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℂ)
207	131	zcnd 9578	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ)
208	206, 207	mulcomd 8176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
209	205, 208	eqtr4d 2265	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)))
210	209	oveq1d 6022	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
211	149, 153	mulcld 8175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℂ)
212	207, 211	mulcomd 8176	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)))
213	212	oveq1d 6022	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁))
214	196, 210, 213	3eqtr4rd 2273	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
215	182, 214	eqeq12d 2244	. . . . . 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 10453	. 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 1002 = wceq 1395 ∈ wcel 2200 {crab 2512 class class class wbr 4083 ⟶wf 5314 –1-1-onto→wf1o 5317 ‘cfv 5318 (class class class)co 6007 ℂcc 8005 ℝcr 8006 0cc0 8007 1c1 8008 + caddc 8010 · cmul 8012 < clt 8189 ≤ cle 8190 ℕcn 9118 ℕ₀cn0 9377 ℤcz 9454 ℤ_≥cuz 9730 ℚcq 9822 ...cfz 10212 ..^cfzo 10346 mod cmo 10552 ↑cexp 10768 ∏cprod 12069 gcd cgcd 12482 ϕcphi 12739

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-nul 4210 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-iinf 4680 ax-cnex 8098 ax-resscn 8099 ax-1cn 8100 ax-1re 8101 ax-icn 8102 ax-addcl 8103 ax-addrcl 8104 ax-mulcl 8105 ax-mulrcl 8106 ax-addcom 8107 ax-mulcom 8108 ax-addass 8109 ax-mulass 8110 ax-distr 8111 ax-i2m1 8112 ax-0lt1 8113 ax-1rid 8114 ax-0id 8115 ax-rnegex 8116 ax-precex 8117 ax-cnre 8118 ax-pre-ltirr 8119 ax-pre-ltwlin 8120 ax-pre-lttrn 8121 ax-pre-apti 8122 ax-pre-ltadd 8123 ax-pre-mulgt0 8124 ax-pre-mulext 8125 ax-arch 8126 ax-caucvg 8127

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4384 df-po 4387 df-iso 4388 df-iord 4457 df-on 4459 df-ilim 4460 df-suc 4462 df-iom 4683 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-isom 5327 df-riota 5960 df-ov 6010 df-oprab 6011 df-mpo 6012 df-1st 6292 df-2nd 6293 df-recs 6457 df-irdg 6522 df-frec 6543 df-1o 6568 df-oadd 6572 df-er 6688 df-en 6896 df-dom 6897 df-fin 6898 df-sup 7159 df-pnf 8191 df-mnf 8192 df-xr 8193 df-ltxr 8194 df-le 8195 df-sub 8327 df-neg 8328 df-reap 8730 df-ap 8737 df-div 8828 df-inn 9119 df-2 9177 df-3 9178 df-4 9179 df-n0 9378 df-z 9455 df-uz 9731 df-q 9823 df-rp 9858 df-fz 10213 df-fzo 10347 df-fl 10498 df-mod 10553 df-seqfrec 10678 df-exp 10769 df-ihash 11006 df-cj 11361 df-re 11362 df-im 11363 df-rsqrt 11517 df-abs 11518 df-clim 11798 df-proddc 12070 df-dvds 12307 df-gcd 12483 df-phi 12741

This theorem is referenced by: eulerthlemth 12762

W3C validator