aks6d1c1 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > aks6d1c1		Structured version Visualization version GIF version

Theorem aks6d1c1 42486

Description: Claim 1 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. (Contributed by metakunt, 30-Apr-2025.)

**Hypotheses**
Ref	Expression
aks6d1c1.1	⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))}
aks6d1c1.2	⊢ 𝑆 = (Poly₁‘𝐾)
aks6d1c1.3	⊢ 𝐵 = (Base‘𝑆)
aks6d1c1.4	⊢ 𝑋 = (var₁‘𝐾)
aks6d1c1.5	⊢ 𝑊 = (mulGrp‘𝑆)
aks6d1c1.6	⊢ 𝑉 = (mulGrp‘𝐾)
aks6d1c1.7	⊢ ↑ = (._g‘𝑉)
aks6d1c1.8	⊢ 𝐶 = (algSc‘𝑆)
aks6d1c1.9	⊢ 𝐷 = (._g‘𝑊)
aks6d1c1.10	⊢ 𝑃 = (chr‘𝐾)
aks6d1c1.11	⊢ 𝑂 = (eval₁‘𝐾)
aks6d1c1.12	⊢ + = (+_g‘𝑆)
aks6d1c1.13	⊢ (𝜑 → 𝐾 ∈ Field)
aks6d1c1.14	⊢ (𝜑 → 𝑃 ∈ ℙ)
aks6d1c1.15	⊢ (𝜑 → 𝑅 ∈ ℕ)
aks6d1c1.16	⊢ (𝜑 → 𝑁 ∈ ℕ)
aks6d1c1.17	⊢ (𝜑 → 𝑃 ∥ 𝑁)
aks6d1c1.18	⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
aks6d1c1.19	⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ₀)
aks6d1c1.20	⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
aks6d1c1.21	⊢ (𝜑 → 𝐴 ∈ ℕ₀)
aks6d1c1.22	⊢ (𝜑 → 𝑈 ∈ ℕ₀)
aks6d1c1.23	⊢ (𝜑 → 𝐿 ∈ ℕ₀)
aks6d1c1.24	⊢ 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿))
aks6d1c1.25	⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
aks6d1c1.26	⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾))

**Assertion**
Ref	Expression
aks6d1c1	⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹))

Distinct variable groups: + ,𝑎 + ,𝑒,𝑓,𝑦 + ,𝑔,𝑖 ↑ ,𝑒,𝑓,𝑦 𝑥, ↑ ,𝑦 ∼ ,𝑎 𝑦, ∼ 𝐴,𝑎 𝐴,𝑔,𝑖 𝑦,𝐴,𝑖 𝑥,𝐴 𝐵,𝑒,𝑓 𝐶,𝑎 𝐶,𝑒,𝑓,𝑦 𝐶,𝑔,𝑖 𝐷,𝑒,𝑓,𝑦 𝐷,𝑔,𝑖 𝑒,𝐸,𝑓,𝑦 𝑒,𝐹,𝑓,𝑦 𝑔,𝐹,𝑖 𝐾,𝑎 𝑒,𝐾,𝑓,𝑦 𝑔,𝐾,𝑖 𝑥,𝐾 𝑒,𝐿,𝑓,𝑦 𝑁,𝑎 𝑒,𝑁,𝑓,𝑦 𝑥,𝑁 𝑒,𝑂,𝑓,𝑦 𝑃,𝑒,𝑓,𝑦 𝑥,𝑃 𝑅,𝑒,𝑓,𝑦 𝑥,𝑅 𝑈,𝑒,𝑓,𝑦 𝑒,𝑉,𝑓,𝑦 𝑥,𝑉 𝑒,𝑊,𝑓,𝑦 𝑔,𝑊,𝑖 𝑋,𝑎 𝑒,𝑋,𝑓,𝑦 𝑔,𝑋,𝑖 𝜑,𝑎 𝜑,𝑔,𝑖 𝜑,𝑦,𝑥 Allowed substitution hints: 𝜑(𝑒,𝑓) 𝐴(𝑒,𝑓) 𝐵(𝑥,𝑦,𝑔,𝑖,𝑎) 𝐶(𝑥) 𝐷(𝑥,𝑎) 𝑃(𝑔,𝑖,𝑎) + (𝑥) ∼ (𝑥,𝑒,𝑓,𝑔,𝑖) 𝑅(𝑔,𝑖,𝑎) 𝑆(𝑥,𝑦,𝑒,𝑓,𝑔,𝑖,𝑎) 𝑈(𝑥,𝑔,𝑖,𝑎) 𝐸(𝑥,𝑔,𝑖,𝑎) ↑ (𝑔,𝑖,𝑎) 𝐹(𝑥,𝑎) 𝐺(𝑥,𝑦,𝑒,𝑓,𝑔,𝑖,𝑎) 𝐿(𝑥,𝑔,𝑖,𝑎) 𝑁(𝑔,𝑖) 𝑂(𝑥,𝑔,𝑖,𝑎) 𝑉(𝑔,𝑖,𝑎) 𝑊(𝑥,𝑎) 𝑋(𝑥)

Proof of Theorem aks6d1c1 Dummy variables 𝑗 𝑘 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aks6d1c1.21	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
2	1	nn0zd 12525	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1	nn0ge0d 12477	. . . 4 ⊢ (𝜑 → 0 ≤ 𝐴)
4	1	nn0red 12475	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	4	leidd 11715	. . . 4 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
6	2, 3, 5	3jca 1129	. . 3 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴))
7		oveq2 7376	. . . . . . . 8 ⊢ (ℎ = 0 → (0...ℎ) = (0...0))
8	7	mpteq1d 5190	. . . . . . 7 ⊢ (ℎ = 0 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
9	8	oveq2d 7384	. . . . . 6 ⊢ (ℎ = 0 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
10	9	breq2d 5112	. . . . 5 ⊢ (ℎ = 0 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
11		oveq2 7376	. . . . . . . 8 ⊢ (ℎ = 𝑗 → (0...ℎ) = (0...𝑗))
12	11	mpteq1d 5190	. . . . . . 7 ⊢ (ℎ = 𝑗 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
13	12	oveq2d 7384	. . . . . 6 ⊢ (ℎ = 𝑗 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
14	13	breq2d 5112	. . . . 5 ⊢ (ℎ = 𝑗 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
15		oveq2 7376	. . . . . . . 8 ⊢ (ℎ = (𝑗 + 1) → (0...ℎ) = (0...(𝑗 + 1)))
16	15	mpteq1d 5190	. . . . . . 7 ⊢ (ℎ = (𝑗 + 1) → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
17	16	oveq2d 7384	. . . . . 6 ⊢ (ℎ = (𝑗 + 1) → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
18	17	breq2d 5112	. . . . 5 ⊢ (ℎ = (𝑗 + 1) → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
19		oveq2 7376	. . . . . . . 8 ⊢ (ℎ = 𝐴 → (0...ℎ) = (0...𝐴))
20	19	mpteq1d 5190	. . . . . . 7 ⊢ (ℎ = 𝐴 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
21	20	oveq2d 7384	. . . . . 6 ⊢ (ℎ = 𝐴 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
22	21	breq2d 5112	. . . . 5 ⊢ (ℎ = 𝐴 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
23		aks6d1c1.1	. . . . . . . 8 ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))}
24		aks6d1c1.2	. . . . . . . 8 ⊢ 𝑆 = (Poly₁‘𝐾)
25		aks6d1c1.3	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑆)
26		aks6d1c1.4	. . . . . . . 8 ⊢ 𝑋 = (var₁‘𝐾)
27		aks6d1c1.5	. . . . . . . 8 ⊢ 𝑊 = (mulGrp‘𝑆)
28		aks6d1c1.6	. . . . . . . 8 ⊢ 𝑉 = (mulGrp‘𝐾)
29		aks6d1c1.7	. . . . . . . 8 ⊢ ↑ = (._g‘𝑉)
30		aks6d1c1.8	. . . . . . . 8 ⊢ 𝐶 = (algSc‘𝑆)
31		aks6d1c1.9	. . . . . . . 8 ⊢ 𝐷 = (._g‘𝑊)
32		aks6d1c1.10	. . . . . . . 8 ⊢ 𝑃 = (chr‘𝐾)
33		aks6d1c1.11	. . . . . . . 8 ⊢ 𝑂 = (eval₁‘𝐾)
34		aks6d1c1.12	. . . . . . . 8 ⊢ + = (+_g‘𝑆)
35		aks6d1c1.13	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ Field)
36		aks6d1c1.14	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℙ)
37		aks6d1c1.15	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ ℕ)
38		aks6d1c1.16	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
39		aks6d1c1.17	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
40		aks6d1c1.18	. . . . . . . 8 ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
41		aks6d1c1.24	. . . . . . . . . . . 12 ⊢ 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿))
42		prmnn 16613	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
43	36, 42	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℕ)
44		aks6d1c1.22	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℕ₀)
45	43, 44	nnexpcld 14180	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃↑𝑈) ∈ ℕ)
46	43	nnzd 12526	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℤ)
47	43	nnne0d 12207	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ≠ 0)
48	38	nnzd 12526	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℤ)
49		dvdsval2 16194	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
50	46, 47, 48, 49	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
51	39, 50	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℤ)
52	38	nnred 12172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53	43	nnred 12172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
54	38	nngt0d 12206	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑁)
55	43	nngt0d 12206	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑃)
56	52, 53, 54, 55	divgt0d 12089	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < (𝑁 / 𝑃))
57	51, 56	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
58		elnnz 12510	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 / 𝑃) ∈ ℕ ↔ ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
59	57, 58	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℕ)
60		aks6d1c1.23	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℕ₀)
61	59, 60	nnexpcld 14180	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 / 𝑃)↑𝐿) ∈ ℕ)
62	45, 61	nnmulcld 12210	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∈ ℕ)
63	41, 62	eqeltrid 2841	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℕ)
64	23, 24, 25, 26, 28, 29, 32, 33, 35, 36, 37, 38, 39, 40, 63	aks6d1c1p7 42483	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∼ 𝑋)
65	35	fldcrngd 20687	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
66	24	ply1crng 22151	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing)
67	65, 66	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ CRing)
68		crngring 20192	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
69		ringcmn 20229	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
70	68, 69	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ CMnd)
71	67, 70	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ CMnd)
72		cmnmnd 19738	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ CMnd → 𝑆 ∈ Mnd)
73	71, 72	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Mnd)
74		crngring 20192	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
75	65, 74	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
76		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Base‘𝑆) = (Base‘𝑆)
77	26, 24, 76	vr1cl 22170	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑋 ∈ (Base‘𝑆))
78	75, 77	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆))
79		eqid 2737	. . . . . . . . . . . 12 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
80	76, 34, 79	mndrid 18692	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆)) → (𝑋 + (0_g‘𝑆)) = 𝑋)
81	73, 78, 80	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (0_g‘𝑆)) = 𝑋)
82	64, 81	breqtrrd 5128	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (0_g‘𝑆)))
83		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
84		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
85	83, 84	zrh0 21480	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
86	75, 85	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
87	86	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (𝐶‘(0_g‘𝐾)))
88	24, 30, 84, 79, 75	ply1ascl0 22207	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(0_g‘𝐾)) = (0_g‘𝑆))
89	87, 88	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (0_g‘𝑆))
90	89	oveq2d 7384	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) = (𝑋 + (0_g‘𝑆)))
91	82, 90	breqtrrd 5128	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
92		aks6d1c1.19	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ₀)
93		0zd 12512	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℤ)
94		0red 11147	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
95	94	leidd 11715	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 0)
96	93, 2, 93, 95, 3	elfzd 13443	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝐴))
97	92, 96	ffvelcdmd 7039	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
98	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 91, 97	aks6d1c1p6 42484	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∼ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
99	27	crngmgp 20188	. . . . . . . . . 10 ⊢ (𝑆 ∈ CRing → 𝑊 ∈ CMnd)
100	67, 99	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ CMnd)
101	100	cmnmndd 19745	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Mnd)
102		0z 12511	. . . . . . . . 9 ⊢ 0 ∈ ℤ
103	102	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
104		eqid 2737	. . . . . . . . 9 ⊢ (Base‘𝑊) = (Base‘𝑊)
105		0le0 12258	. . . . . . . . . . . 12 ⊢ 0 ≤ 0
106	105	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 0)
107	103, 2, 103, 106, 3	elfzd 13443	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (0...𝐴))
108	92, 107	ffvelcdmd 7039	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
109	83	zrhrhm 21478	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
110	75, 109	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
111		zringbas 21420	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤ_ring)
112		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐾) = (Base‘𝐾)
113	111, 112	rhmf 20432	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
114	110, 113	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
115	114, 93	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾))
116	24, 30, 112, 76	ply1sclcl 22240	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
117	75, 115, 116	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
118	76, 34	mndcl 18679	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
119	73, 78, 117, 118	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
120	27, 76	mgpbas 20092	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑊)
121	119, 120	eleqtrdi 2847	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑊))
122	104, 31, 101, 108, 121	mulgnn0cld 19037	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊))
123		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝐹‘𝑖) = (𝐹‘0))
124		2fveq3 6847	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
125	124	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
126	123, 125	oveq12d 7386	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
127	104, 126	gsumsn 19895	. . . . . . . 8 ⊢ ((𝑊 ∈ Mnd ∧ 0 ∈ ℤ ∧ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊)) → (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
128	101, 103, 122, 127	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
129	98, 128	breqtrrd 5128	. . . . . 6 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
130		fzsn 13494	. . . . . . . . . 10 ⊢ (0 ∈ ℤ → (0...0) = {0})
131	102, 130	ax-mp 5	. . . . . . . . 9 ⊢ (0...0) = {0}
132	131	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (0...0) = {0})
133	132	mpteq1d 5190	. . . . . . 7 ⊢ (𝜑 → (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
134	133	oveq2d 7384	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
135	129, 134	breqtrrd 5128	. . . . 5 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
136	35	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Field)
137	36	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∈ ℙ)
138	37	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑅 ∈ ℕ)
139	40	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑁 gcd 𝑅) = 1)
140	39	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∥ 𝑁)
141		simp3 1139	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
142		nfcv 2899	. . . . . . . . . . 11 ⊢ Ⅎ𝑘((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))
143		nfcv 2899	. . . . . . . . . . 11 ⊢ Ⅎ𝑖((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
144		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹‘𝑖) = (𝐹‘𝑘))
145		2fveq3 6847	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘𝑘)))
146	145	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
147	144, 146	oveq12d 7386	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
148	142, 143, 147	cbvmpt 5202	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
149	148	oveq2i 7379	. . . . . . . . 9 ⊢ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))
150	149	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
151	141, 150	breqtrd 5126	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
152	35	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Field)
153	36	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∈ ℙ)
154	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑅 ∈ ℕ)
155	38	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∈ ℕ)
156	39	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∥ 𝑁)
157	40	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 gcd 𝑅) = 1)
158	41	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)))
159	37	nnzd 12526	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ ℤ)
160	51, 159, 60	3jca 1129	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀))
161	159, 51, 48	3jca 1129	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ))
162	48, 159	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ))
163		gcdcom 16452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
165		eqeq1 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 gcd 𝑅) = (𝑅 gcd 𝑁) → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1))
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1))
167	166	pm5.74i 271	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 → (𝑁 gcd 𝑅) = 1) ↔ (𝜑 → (𝑅 gcd 𝑁) = 1))
168	40, 167	mpbi 230	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd 𝑁) = 1)
169	52	recnd 11172	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℂ)
170	53	recnd 11172	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℂ)
171	94, 54	gtned 11280	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ≠ 0)
172	169, 169, 170, 171, 47	divdiv2d 11961	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) = ((𝑁 · 𝑃) / 𝑁))
173	169, 170	mulcomd 11165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 · 𝑃) = (𝑃 · 𝑁))
174	173	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = ((𝑃 · 𝑁) / 𝑁))
175	170, 169, 169, 171, 171	divdiv2d 11961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = ((𝑃 · 𝑁) / 𝑁))
176	175	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑃 · 𝑁) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
177	174, 176	eqtrd 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
178	169, 171	dividd 11927	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
179	178	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = (𝑃 / 1))
180	170	div1d 11921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / 1) = 𝑃)
181	179, 180	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = 𝑃)
182	181, 46	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) ∈ ℤ)
183	177, 182	eqeltrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) ∈ ℤ)
184	172, 183	eqeltrd 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)
185	94, 56	gtned 11280	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / 𝑃) ≠ 0)
186		dvdsval2 16194	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ (𝑁 / 𝑃) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ))
187	51, 185, 48, 186	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ))
188	184, 187	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 / 𝑃) ∥ 𝑁)
189	168, 188	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁))
190		rpdvds 16599	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) → (𝑅 gcd (𝑁 / 𝑃)) = 1)
191	161, 189, 190	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1)
192	159, 51	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ))
193		gcdcom 16452	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ) → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
194	192, 193	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
195		eqeq1 2741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅) → ((𝑅 gcd (𝑁 / 𝑃)) = 1 ↔ ((𝑁 / 𝑃) gcd 𝑅) = 1))
196	194, 195	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd (𝑁 / 𝑃)) = 1 ↔ ((𝑁 / 𝑃) gcd 𝑅) = 1))
197	196	pm5.74i 271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1) ↔ (𝜑 → ((𝑁 / 𝑃) gcd 𝑅) = 1))
198	191, 197	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃) gcd 𝑅) = 1)
199		rpexp1i 16662	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀) → (((𝑁 / 𝑃) gcd 𝑅) = 1 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1))
200	199	imp 406	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀) ∧ ((𝑁 / 𝑃) gcd 𝑅) = 1) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
201	160, 198, 200	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
202	201	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
203		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
204		simpr1 1196	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℤ)
205	204	peano2zd 12611	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ ℤ)
206	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205	aks6d1c1p2 42479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
207	44	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑈 ∈ ℕ₀)
208	159, 46, 48	3jca 1129	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ))
209	168, 39	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁))
210		rpdvds 16599	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) → (𝑅 gcd 𝑃) = 1)
211	208, 209, 210	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd 𝑃) = 1)
212	159, 46	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ))
213		gcdcom 16452	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
214	212, 213	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
215		eqeq1 2741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 gcd 𝑃) = (𝑃 gcd 𝑅) → ((𝑅 gcd 𝑃) = 1 ↔ (𝑃 gcd 𝑅) = 1))
216	214, 215	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑃) = 1 ↔ (𝑃 gcd 𝑅) = 1))
217	216	pm5.74i 271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 → (𝑅 gcd 𝑃) = 1) ↔ (𝜑 → (𝑃 gcd 𝑅) = 1))
218	211, 217	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 gcd 𝑅) = 1)
219	218	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃 gcd 𝑅) = 1)
220	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 155, 156, 157, 206, 207, 219	aks6d1c1p8 42485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃↑𝑈) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
221		2fveq3 6847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
222	221	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
223	222	breq2d 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑗 + 1) → (𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) ↔ 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
224		aks6d1c1.25	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
225	23, 24, 25, 26, 28, 29, 32, 33, 35, 36, 37, 38, 39, 40, 38	aks6d1c1p7 42483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∼ 𝑋)
226	225, 81	breqtrrd 5128	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (0_g‘𝑆)))
227	226, 90	breqtrrd 5128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
228	227	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
229		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑎 = 0)
230	229	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑎 = 0) → ((ℤRHom‘𝐾)‘𝑎) = ((ℤRHom‘𝐾)‘0))
231	230	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
232	231	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
233	228, 232	breqtrrd 5128	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
234	233	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
235	234	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
236		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
237		1cnd 11139	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 1 ∈ ℂ)
238	237	addlidd 11346	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (0 + 1) = 1)
239	238	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((0 + 1)...𝐴) = (1...𝐴))
240	239	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ ((0 + 1)...𝐴) ↔ 𝑎 ∈ (1...𝐴)))
241	240	imbi1d 341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 ∈ ((0 + 1)...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) ↔ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
242	236, 241	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ ((0 + 1)...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
243	235, 242	jaod 860	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
244	2, 3	jca 511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
245		eluz1 12767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ ℤ → (𝐴 ∈ (ℤ_≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)))
246	93, 245	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)))
247	244, 246	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
248	247	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 𝐴 ∈ (ℤ_≥‘0))
249		elfzp12 13531	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (ℤ_≥‘0) → (𝑎 ∈ (0...𝐴) ↔ (𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴))))
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (0...𝐴) ↔ (𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴))))
251	250	imbi1d 341	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) ↔ ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
252	243, 251	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
253	252	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
254	253	ralimdv2 3147	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
255	224, 254	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
256	255	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
257		0zd 12512	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ∈ ℤ)
258	2	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐴 ∈ ℤ)
259	204	zred 12608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℝ)
260		1red 11145	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 1 ∈ ℝ)
261		simpr2 1197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 𝑗)
262		0le1 11672	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 1
263	262	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 1)
264	259, 260, 261, 263	addge0d 11725	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ (𝑗 + 1))
265		simpr3 1198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 < 𝐴)
266	204, 258	zltp1led 42349	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴))
267	265, 266	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ≤ 𝐴)
268	257, 258, 205, 264, 267	elfzd 13443	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ (0...𝐴))
269	223, 256, 268	rspcdva 3579	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
270		aks6d1c1.26	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾))
271	270	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾))
272	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205, 269, 271	aks6d1c1p3 42480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 / 𝑃) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
273	60	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐿 ∈ ℕ₀)
274	198	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃) gcd 𝑅) = 1)
275	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 155, 156, 157, 272, 273, 274	aks6d1c1p8 42485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃)↑𝐿) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
276	23, 24, 25, 26, 27, 28, 29, 30, 32, 33, 34, 152, 153, 154, 202, 156, 220, 275	aks6d1c1p5 42482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
277	158, 276	eqbrtrd 5122	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
278	92	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐹:(0...𝐴)⟶ℕ₀)
279	278, 268	ffvelcdmd 7039	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝐹‘(𝑗 + 1)) ∈ ℕ₀)
280	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 155, 156, 157, 277, 279	aks6d1c1p6 42484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
281	101	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑊 ∈ Mnd)
282		ovexd 7403	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ V)
283	73	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑆 ∈ Mnd)
284	78	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑋 ∈ (Base‘𝑆))
285	75	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Ring)
286	114	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
287	286, 205	ffvelcdmd 7039	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾))
288	24, 30, 112, 76	ply1sclcl 22240	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
289	285, 287, 288	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
290	76, 34	mndcl 18679	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆))
291	283, 284, 289, 290	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆))
292	291, 120	eleqtrdi 2847	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑊))
293	104, 31, 281, 279, 292	mulgnn0cld 19037	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊))
294		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
295		2fveq3 6847	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
296	295	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
297	294, 296	oveq12d 7386	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
298	104, 297	gsumsn 19895	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ (𝑗 + 1) ∈ V ∧ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊)) → (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
299	281, 282, 293, 298	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
300	280, 299	breqtrrd 5128	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
301	300	3adant3 1133	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
302	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 136, 137, 138, 139, 140, 151, 301	aks6d1c1p4 42481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
303	142, 143, 147	cbvmpt 5202	. . . . . . . . 9 ⊢ (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
304	303	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))
305	304	oveq2d 7384	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
306		eqid 2737	. . . . . . . 8 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
307	100	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ CMnd)
308		simp21 1208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℤ)
309		simp22 1209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 0 ≤ 𝑗)
310	308, 309	jca 511	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
311		elnn0z 12513	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ₀ ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
312	310, 311	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℕ₀)
313	281	3adant3 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ Mnd)
314	313	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑊 ∈ Mnd)
315	92	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐹:(0...𝐴)⟶ℕ₀)
316	315	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐹:(0...𝐴)⟶ℕ₀)
317		0zd 12512	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ∈ ℤ)
318	2	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐴 ∈ ℤ)
319	318	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℤ)
320		elfzelz 13452	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ∈ ℤ)
321	320	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℤ)
322		elfzle1 13455	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 0 ≤ 𝑘)
323	322	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ≤ 𝑘)
324	321	zred 12608	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℝ)
325	308	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℤ)
326	325	zred 12608	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℝ)
327		1red 11145	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 1 ∈ ℝ)
328	326, 327	readdcld 11173	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ∈ ℝ)
329	319	zred 12608	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℝ)
330		elfzle2 13456	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ≤ (𝑗 + 1))
331	330	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ (𝑗 + 1))
332		simpl23 1255	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 < 𝐴)
333	325, 319	zltp1led 42349	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴))
334	332, 333	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ≤ 𝐴)
335	324, 328, 329, 331, 334	letrd 11302	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ 𝐴)
336	317, 319, 321, 323, 335	elfzd 13443	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ (0...𝐴))
337	316, 336	ffvelcdmd 7039	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℕ₀)
338	283	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑆 ∈ Mnd)
339	338	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑆 ∈ Mnd)
340	284	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑋 ∈ (Base‘𝑆))
341	340	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑋 ∈ (Base‘𝑆))
342	285	3adant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Ring)
343	342	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐾 ∈ Ring)
344	343, 109, 113	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
345	344, 321	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾))
346	24, 30, 112, 76	ply1sclcl 22240	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆))
347	343, 345, 346	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆))
348	76, 34	mndcl 18679	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆))
349	339, 341, 347, 348	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆))
350	349, 120	eleqtrdi 2847	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑊))
351	104, 31, 314, 337, 350	mulgnn0cld 19037	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) ∈ (Base‘𝑊))
352	104, 306, 307, 312, 351	gsummptfzsplit 19873	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
353	305, 352	eqtrd 2772	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
354	302, 353	breqtrrd 5128	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
355	10, 14, 18, 22, 135, 354, 93, 2, 3	fzindd 12606	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴)) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
356	355	ex 412	. . 3 ⊢ (𝜑 → ((𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
357	6, 356	mpd 15	. 2 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
358		aks6d1c1.20	. . . 4 ⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
359	358	a1i 11	. . 3 ⊢ (𝜑 → 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
360		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → 𝑔 = 𝐹)
361	360	fveq1d 6844	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → (𝑔‘𝑖) = (𝐹‘𝑖))
362	361	oveq1d 7383	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))
363	362	mpteq2dva 5193	. . . 4 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
364	363	oveq2d 7384	. . 3 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
365		nn0ex 12419	. . . . . 6 ⊢ ℕ₀ ∈ V
366	365	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ₀ ∈ V)
367		ovexd 7403	. . . . 5 ⊢ (𝜑 → (0...𝐴) ∈ V)
368	366, 367	elmapd 8789	. . . 4 ⊢ (𝜑 → (𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)) ↔ 𝐹:(0...𝐴)⟶ℕ₀))
369	92, 368	mpbird 257	. . 3 ⊢ (𝜑 → 𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)))
370		ovexd 7403	. . 3 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ∈ V)
371	359, 364, 369, 370	fvmptd 6957	. 2 ⊢ (𝜑 → (𝐺‘𝐹) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
372	357, 371	breqtrrd 5128	1 ⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 Vcvv 3442 {csn 4582 class class class wbr 5100 {copab 5162 ↦ cmpt 5181 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ↑_m cmap 8775 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11178 ≤ cle 11179 / cdiv 11806 ℕcn 12157 ℕ₀cn0 12413 ℤcz 12500 ℤ_≥cuz 12763 ...cfz 13435 ↑cexp 13996 ∥ cdvds 16191 gcd cgcd 16433 ℙcprime 16610 Basecbs 17148 +_gcplusg 17189 0_gc0g 17371 Σ_g cgsu 17372 Mndcmnd 18671 ._gcmg 19009 CMndccmn 19721 mulGrpcmgp 20087 Ringcrg 20180 CRingccrg 20181 RingHom crh 20417 RingIso crs 20418 Fieldcfield 20675 ℤ_ringczring 21413 ℤRHomczrh 21466 chrcchr 21468 algSccascl 21819 var₁cv1 22128 Poly₁cpl1 22129 eval₁ce1 22270 PrimRoots cprimroots 42461

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117 ax-mulf 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-ofr 7633 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-tpos 8178 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-oadd 8411 df-er 8645 df-map 8777 df-pm 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-sup 9357 df-inf 9358 df-oi 9427 df-dju 9825 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-xnn0 12487 df-z 12501 df-dec 12620 df-uz 12764 df-rp 12918 df-fz 13436 df-fzo 13583 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-fac 14209 df-bc 14238 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-dvds 16192 df-gcd 16434 df-prm 16611 df-phi 16705 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-hom 17213 df-cco 17214 df-0g 17373 df-gsum 17374 df-prds 17379 df-pws 17381 df-mre 17517 df-mrc 17518 df-acs 17520 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-mhm 18720 df-submnd 18721 df-grp 18878 df-minusg 18879 df-sbg 18880 df-mulg 19010 df-subg 19065 df-ghm 19154 df-cntz 19258 df-od 19469 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100 df-ur 20129 df-srg 20134 df-ring 20182 df-cring 20183 df-oppr 20285 df-dvdsr 20305 df-unit 20306 df-invr 20336 df-dvr 20349 df-rhm 20420 df-rim 20421 df-subrng 20491 df-subrg 20515 df-drng 20676 df-field 20677 df-lmod 20825 df-lss 20895 df-lsp 20935 df-cnfld 21322 df-zring 21414 df-zrh 21470 df-chr 21472 df-assa 21820 df-asp 21821 df-ascl 21822 df-psr 21877 df-mvr 21878 df-mpl 21879 df-opsr 21881 df-evls 22041 df-evl 22042 df-psr1 22132 df-vr1 22133 df-ply1 22134 df-coe1 22135 df-evl1 22272 df-primroots 42462

This theorem is referenced by: aks6d1c1rh 42495

W3C validator