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 43146

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 12711	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1	nn0ge0d 12663	. . . 4 ⊢ (𝜑 → 0 ≤ 𝐴)
4	1	nn0red 12661	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	4	leidd 11875	. . . 4 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
6	2, 3, 5	3jca 1146	. . 3 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴))
7		oveq2 7426	. . . . . . . 8 ⊢ (ℎ = 0 → (0...ℎ) = (0...0))
8	7	mpteq1d 5195	. . . . . . 7 ⊢ (ℎ = 0 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
9	8	oveq2d 7434	. . . . . 6 ⊢ (ℎ = 0 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
10	9	breq2d 5115	. . . . 5 ⊢ (ℎ = 0 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
11		oveq2 7426	. . . . . . . 8 ⊢ (ℎ = 𝑗 → (0...ℎ) = (0...𝑗))
12	11	mpteq1d 5195	. . . . . . 7 ⊢ (ℎ = 𝑗 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
13	12	oveq2d 7434	. . . . . 6 ⊢ (ℎ = 𝑗 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
14	13	breq2d 5115	. . . . 5 ⊢ (ℎ = 𝑗 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
15		oveq2 7426	. . . . . . . 8 ⊢ (ℎ = (𝑗 + 1) → (0...ℎ) = (0...(𝑗 + 1)))
16	15	mpteq1d 5195	. . . . . . 7 ⊢ (ℎ = (𝑗 + 1) → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
17	16	oveq2d 7434	. . . . . 6 ⊢ (ℎ = (𝑗 + 1) → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
18	17	breq2d 5115	. . . . 5 ⊢ (ℎ = (𝑗 + 1) → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
19		oveq2 7426	. . . . . . . 8 ⊢ (ℎ = 𝐴 → (0...ℎ) = (0...𝐴))
20	19	mpteq1d 5195	. . . . . . 7 ⊢ (ℎ = 𝐴 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
21	20	oveq2d 7434	. . . . . 6 ⊢ (ℎ = 𝐴 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
22	21	breq2d 5115	. . . . 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 16842	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
43	36, 42	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℕ)
44		aks6d1c1.22	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℕ₀)
45	43, 44	nnexpcld 14382	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃↑𝑈) ∈ ℕ)
46	43	nnzd 12712	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℤ)
47	43	nnne0d 12381	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ≠ 0)
48	38	nnzd 12712	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℤ)
49		dvdsval2 16418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
50	46, 47, 48, 49	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
51	39, 50	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℤ)
52	38	nnred 12343	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53	43	nnred 12343	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
54	38	nngt0d 12380	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑁)
55	43	nngt0d 12380	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑃)
56	52, 53, 54, 55	divgt0d 12245	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < (𝑁 / 𝑃))
57	51, 56	jca 521	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
58		elnnz 12696	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 / 𝑃) ∈ ℕ ↔ ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
59	57, 58	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℕ)
60		aks6d1c1.23	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℕ₀)
61	59, 60	nnexpcld 14382	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 / 𝑃)↑𝐿) ∈ ℕ)
62	45, 61	nnmulcld 12384	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∈ ℕ)
63	41, 62	eqeltrid 2865	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℕ)
64	23, 24, 25, 26, 28, 29, 32, 33, 35, 36, 37, 38, 39, 40, 63	aks6d1c1p7 43143	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∼ 𝑋)
65	35	fldcrngd 20988	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
66	24	ply1crng 22509	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing)
67	65, 66	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ CRing)
68		crngring 20465	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
69		ringcmn 20504	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
70	68, 69	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ CMnd)
71	67, 70	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ CMnd)
72		cmnmnd 20004	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ CMnd → 𝑆 ∈ Mnd)
73	71, 72	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Mnd)
74		crngring 20465	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
75	65, 74	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
76		eqid 2761	. . . . . . . . . . . . 13 ⊢ (Base‘𝑆) = (Base‘𝑆)
77	26, 24, 76	vr1cl 22528	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑋 ∈ (Base‘𝑆))
78	75, 77	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆))
79		eqid 2761	. . . . . . . . . . . 12 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
80	76, 34, 79	mndrid 18938	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆)) → (𝑋 + (0_g‘𝑆)) = 𝑋)
81	73, 78, 80	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (0_g‘𝑆)) = 𝑋)
82	64, 81	breqtrrd 5133	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (0_g‘𝑆)))
83		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
84		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
85	83, 84	zrh0 21812	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
86	75, 85	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
87	86	fveq2d 6887	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (𝐶‘(0_g‘𝐾)))
88	24, 30, 84, 79, 75	ply1ascl0 22565	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(0_g‘𝐾)) = (0_g‘𝑆))
89	87, 88	eqtrd 2796	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (0_g‘𝑆))
90	89	oveq2d 7434	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) = (𝑋 + (0_g‘𝑆)))
91	82, 90	breqtrrd 5133	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
92		aks6d1c1.19	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ₀)
93		0zd 12698	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℤ)
94		0red 11304	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
95	94	leidd 11875	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 0)
96	93, 2, 93, 95, 3	elfzd 13640	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝐴))
97	92, 96	ffvelcdmd 7083	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
98	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 91, 97	aks6d1c1p6 43144	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∼ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
99	27	crngmgp 20460	. . . . . . . . . 10 ⊢ (𝑆 ∈ CRing → 𝑊 ∈ CMnd)
100	67, 99	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ CMnd)
101	100	cmnmndd 20011	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Mnd)
102		0z 12697	. . . . . . . . 9 ⊢ 0 ∈ ℤ
103	102	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
104		eqid 2761	. . . . . . . . 9 ⊢ (Base‘𝑊) = (Base‘𝑊)
105		0le0 12437	. . . . . . . . . . . 12 ⊢ 0 ≤ 0
106	105	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 0)
107	103, 2, 103, 106, 3	elfzd 13640	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (0...𝐴))
108	92, 107	ffvelcdmd 7083	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
109	83	zrhrhm 21810	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
110	75, 109	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
111		zringbas 21752	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤ_ring)
112		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐾) = (Base‘𝐾)
113	111, 112	rhmf 20708	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
114	110, 113	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
115	114, 93	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾))
116	24, 30, 112, 76	ply1sclcl 22598	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
117	75, 115, 116	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
118	76, 34	mndcl 18924	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
119	73, 78, 117, 118	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
120	27, 76	mgpbas 20358	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑊)
121	119, 120	eleqtrdi 2871	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑊))
122	104, 31, 101, 108, 121	mulgnn0cld 19298	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊))
123		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝐹‘𝑖) = (𝐹‘0))
124		2fveq3 6888	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
125	124	oveq2d 7434	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
126	123, 125	oveq12d 7436	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
127	104, 126	gsumsn 20161	. . . . . . . 8 ⊢ ((𝑊 ∈ Mnd ∧ 0 ∈ ℤ ∧ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊)) → (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
128	101, 103, 122, 127	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
129	98, 128	breqtrrd 5133	. . . . . 6 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
130		fzsn 13693	. . . . . . . . . 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 5195	. . . . . . 7 ⊢ (𝜑 → (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
134	133	oveq2d 7434	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
135	129, 134	breqtrrd 5133	. . . . 5 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
136	35	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Field)
137	36	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∈ ℙ)
138	37	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑅 ∈ ℕ)
139	40	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑁 gcd 𝑅) = 1)
140	39	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∥ 𝑁)
141		simp3 1156	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
142		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑘((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))
143		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑖((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
144		fveq2 6883	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹‘𝑖) = (𝐹‘𝑘))
145		2fveq3 6888	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘𝑘)))
146	145	oveq2d 7434	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
147	144, 146	oveq12d 7436	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
148	142, 143, 147	cbvmpt 5207	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
149	148	oveq2i 7429	. . . . . . . . 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 5131	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
152	35	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Field)
153	36	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∈ ℙ)
154	37	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑅 ∈ ℕ)
155	38	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∈ ℕ)
156	39	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∥ 𝑁)
157	40	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 gcd 𝑅) = 1)
158	41	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)))
159	37	nnzd 12712	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ ℤ)
160	51, 159, 60	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀))
161	159, 51, 48	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ))
162	48, 159	jca 521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ))
163		gcdcom 16678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
164	162, 163	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
165		eqeq1 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 gcd 𝑅) = (𝑅 gcd 𝑁) → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1))
166	164, 165	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1))
167	166	pm5.74i 274	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 → (𝑁 gcd 𝑅) = 1) ↔ (𝜑 → (𝑅 gcd 𝑁) = 1))
168	40, 167	mpbi 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd 𝑁) = 1)
169	52	recnd 11330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℂ)
170	53	recnd 11330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℂ)
171	94, 54	gtned 11438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ≠ 0)
172	169, 169, 170, 171, 47	divdiv2d 12118	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) = ((𝑁 · 𝑃) / 𝑁))
173	169, 170	mulcomd 11323	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 · 𝑃) = (𝑃 · 𝑁))
174	173	oveq1d 7433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = ((𝑃 · 𝑁) / 𝑁))
175	170, 169, 169, 171, 171	divdiv2d 12118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = ((𝑃 · 𝑁) / 𝑁))
176	175	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑃 · 𝑁) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
177	174, 176	eqtrd 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
178	169, 171	dividd 12084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
179	178	oveq2d 7434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = (𝑃 / 1))
180	170	div1d 12078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / 1) = 𝑃)
181	179, 180	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = 𝑃)
182	181, 46	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) ∈ ℤ)
183	177, 182	eqeltrd 2861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) ∈ ℤ)
184	172, 183	eqeltrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)
185	94, 56	gtned 11438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / 𝑃) ≠ 0)
186		dvdsval2 16418	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ (𝑁 / 𝑃) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ))
187	51, 185, 48, 186	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ))
188	184, 187	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 / 𝑃) ∥ 𝑁)
189	168, 188	jca 521	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁))
190		rpdvds 16828	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) → (𝑅 gcd (𝑁 / 𝑃)) = 1)
191	161, 189, 190	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1)
192	159, 51	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ))
193		gcdcom 16678	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ) → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
194	192, 193	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
195		eqeq1 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅) → ((𝑅 gcd (𝑁 / 𝑃)) = 1 ↔ ((𝑁 / 𝑃) gcd 𝑅) = 1))
196	194, 195	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd (𝑁 / 𝑃)) = 1 ↔ ((𝑁 / 𝑃) gcd 𝑅) = 1))
197	196	pm5.74i 274	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1) ↔ (𝜑 → ((𝑁 / 𝑃) gcd 𝑅) = 1))
198	191, 197	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃) gcd 𝑅) = 1)
199		rpexp1i 16892	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀) → (((𝑁 / 𝑃) gcd 𝑅) = 1 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1))
200	199	imp 412	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀) ∧ ((𝑁 / 𝑃) gcd 𝑅) = 1) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
201	160, 198, 200	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
202	201	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
203		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
204		simpr1 1213	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℤ)
205	204	peano2zd 12799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ ℤ)
206	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205	aks6d1c1p2 43139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
207	44	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑈 ∈ ℕ₀)
208	159, 46, 48	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ))
209	168, 39	jca 521	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁))
210		rpdvds 16828	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) → (𝑅 gcd 𝑃) = 1)
211	208, 209, 210	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd 𝑃) = 1)
212	159, 46	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ))
213		gcdcom 16678	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
214	212, 213	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
215		eqeq1 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 gcd 𝑃) = (𝑃 gcd 𝑅) → ((𝑅 gcd 𝑃) = 1 ↔ (𝑃 gcd 𝑅) = 1))
216	214, 215	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑃) = 1 ↔ (𝑃 gcd 𝑅) = 1))
217	216	pm5.74i 274	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 → (𝑅 gcd 𝑃) = 1) ↔ (𝜑 → (𝑃 gcd 𝑅) = 1))
218	211, 217	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 gcd 𝑅) = 1)
219	218	adantr 486	. . . . . . . . . . . . 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 43145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃↑𝑈) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
221		2fveq3 6888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
222	221	oveq2d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
223	222	breq2d 5115	. . . . . . . . . . . . . . 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 43143	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∼ 𝑋)
226	225, 81	breqtrrd 5133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (0_g‘𝑆)))
227	226, 90	breqtrrd 5133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
228	227	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
229		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑎 = 0)
230	229	fveq2d 6887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑎 = 0) → ((ℤRHom‘𝐾)‘𝑎) = ((ℤRHom‘𝐾)‘0))
231	230	fveq2d 6887	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
232	231	oveq2d 7434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
233	228, 232	breqtrrd 5133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
234	233	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
235	234	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
236		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
237		1cnd 11295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 1 ∈ ℂ)
238	237	addlidd 11504	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (0 + 1) = 1)
239	238	oveq1d 7433	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((0 + 1)...𝐴) = (1...𝐴))
240	239	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ ((0 + 1)...𝐴) ↔ 𝑎 ∈ (1...𝐴)))
241	240	imbi1d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 ∈ ((0 + 1)...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) ↔ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
242	236, 241	mpbird 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ ((0 + 1)...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
243	235, 242	jaod 873	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
244	2, 3	jca 521	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
245		eluz1 12962	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ ℤ → (𝐴 ∈ (ℤ_≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)))
246	93, 245	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)))
247	244, 246	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
248	247	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 𝐴 ∈ (ℤ_≥‘0))
249		elfzp12 13730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (ℤ_≥‘0) → (𝑎 ∈ (0...𝐴) ↔ (𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴))))
250	248, 249	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (0...𝐴) ↔ (𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴))))
251	250	imbi1d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) ↔ ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
252	243, 251	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
253	252	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
254	253	ralimdv2 3172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
255	224, 254	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
256	255	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
257		0zd 12698	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ∈ ℤ)
258	2	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐴 ∈ ℤ)
259	204	zred 12796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℝ)
260		1red 11302	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 1 ∈ ℝ)
261		simpr2 1214	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 𝑗)
262		0le1 11832	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 1
263	262	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 1)
264	259, 260, 261, 263	addge0d 11885	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ (𝑗 + 1))
265		simpr3 1215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 < 𝐴)
266	204, 258	zltp1led 12744	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴))
267	265, 266	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ≤ 𝐴)
268	257, 258, 205, 264, 267	elfzd 13640	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ (0...𝐴))
269	223, 256, 268	rspcdva 3578	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
270		aks6d1c1.26	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾))
271	270	adantr 486	. . . . . . . . . . . . . 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 43140	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 / 𝑃) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
273	60	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐿 ∈ ℕ₀)
274	198	adantr 486	. . . . . . . . . . . . 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 43145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃)↑𝐿) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
276	23, 24, 25, 26, 27, 28, 29, 30, 32, 33, 34, 152, 153, 154, 202, 156, 220, 275	aks6d1c1p5 43142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
277	158, 276	eqbrtrd 5127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
278	92	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐹:(0...𝐴)⟶ℕ₀)
279	278, 268	ffvelcdmd 7083	. . . . . . . . . 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 43144	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
281	101	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑊 ∈ Mnd)
282		ovexd 7453	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ V)
283	73	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑆 ∈ Mnd)
284	78	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑋 ∈ (Base‘𝑆))
285	75	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Ring)
286	114	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
287	286, 205	ffvelcdmd 7083	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾))
288	24, 30, 112, 76	ply1sclcl 22598	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
289	285, 287, 288	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
290	76, 34	mndcl 18924	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆))
291	283, 284, 289, 290	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆))
292	291, 120	eleqtrdi 2871	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑊))
293	104, 31, 281, 279, 292	mulgnn0cld 19298	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊))
294		fveq2 6883	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
295		2fveq3 6888	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
296	295	oveq2d 7434	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
297	294, 296	oveq12d 7436	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
298	104, 297	gsumsn 20161	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ (𝑗 + 1) ∈ V ∧ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊)) → (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
299	281, 282, 293, 298	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
300	280, 299	breqtrrd 5133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
301	300	3adant3 1150	. . . . . . 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 43141	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
303	142, 143, 147	cbvmpt 5207	. . . . . . . . 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 7434	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
306		eqid 2761	. . . . . . . 8 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
307	100	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ CMnd)
308		simp21 1225	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℤ)
309		simp22 1226	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 0 ≤ 𝑗)
310	308, 309	jca 521	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
311		elnn0z 12699	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ₀ ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
312	310, 311	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℕ₀)
313	281	3adant3 1150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ Mnd)
314	313	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑊 ∈ Mnd)
315	92	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐹:(0...𝐴)⟶ℕ₀)
316	315	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐹:(0...𝐴)⟶ℕ₀)
317		0zd 12698	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ∈ ℤ)
318	2	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐴 ∈ ℤ)
319	318	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℤ)
320		elfzelz 13649	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ∈ ℤ)
321	320	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℤ)
322		elfzle1 13653	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 0 ≤ 𝑘)
323	322	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ≤ 𝑘)
324	321	zred 12796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℝ)
325	308	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℤ)
326	325	zred 12796	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℝ)
327		1red 11302	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 1 ∈ ℝ)
328	326, 327	readdcld 11331	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ∈ ℝ)
329	319	zred 12796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℝ)
330		elfzle2 13654	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ≤ (𝑗 + 1))
331	330	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ (𝑗 + 1))
332		simpl23 1272	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 < 𝐴)
333	325, 319	zltp1led 12744	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴))
334	332, 333	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ≤ 𝐴)
335	324, 328, 329, 331, 334	letrd 11460	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ 𝐴)
336	317, 319, 321, 323, 335	elfzd 13640	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ (0...𝐴))
337	316, 336	ffvelcdmd 7083	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℕ₀)
338	283	3adant3 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑆 ∈ Mnd)
339	338	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑆 ∈ Mnd)
340	284	3adant3 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑋 ∈ (Base‘𝑆))
341	340	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑋 ∈ (Base‘𝑆))
342	285	3adant3 1150	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Ring)
343	342	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐾 ∈ Ring)
344	343, 109, 113	3syl 19	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
345	344, 321	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾))
346	24, 30, 112, 76	ply1sclcl 22598	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆))
347	343, 345, 346	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆))
348	76, 34	mndcl 18924	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆))
349	339, 341, 347, 348	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆))
350	349, 120	eleqtrdi 2871	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑊))
351	104, 31, 314, 337, 350	mulgnn0cld 19298	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) ∈ (Base‘𝑊))
352	104, 306, 307, 312, 351	gsummptfzsplit 20139	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
353	305, 352	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
354	302, 353	breqtrrd 5133	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
355	10, 14, 18, 22, 135, 354, 93, 2, 3	fzindd 12794	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴)) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
356	355	ex 418	. . 3 ⊢ (𝜑 → ((𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
357	6, 356	mpd 16	. 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 781	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → 𝑔 = 𝐹)
361	360	fveq1d 6885	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → (𝑔‘𝑖) = (𝐹‘𝑖))
362	361	oveq1d 7433	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))
363	362	mpteq2dva 5198	. . . 4 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
364	363	oveq2d 7434	. . 3 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
365		nn0ex 12605	. . . . . 6 ⊢ ℕ₀ ∈ V
366	365	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ₀ ∈ V)
367		ovexd 7453	. . . . 5 ⊢ (𝜑 → (0...𝐴) ∈ V)
368	366, 367	elmapd 8853	. . . 4 ⊢ (𝜑 → (𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)) ↔ 𝐹:(0...𝐴)⟶ℕ₀))
369	92, 368	mpbird 260	. . 3 ⊢ (𝜑 → 𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)))
370		ovexd 7453	. . 3 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ∈ V)
371	359, 364, 369, 370	fvmptd 6999	. 2 ⊢ (𝜑 → (𝐺‘𝐹) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
372	357, 371	breqtrrd 5133	1 ⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 Vcvv 3451 {csn 4584 class class class wbr 5103 {copab 5167 ↦ cmpt 5186 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 ↑_m cmap 8840 0cc0 11193 1c1 11194 + caddc 11196 · cmul 11198 < clt 11336 ≤ cle 11337 / cdiv 11966 ℕcn 12328 ℕ₀cn0 12599 ℤcz 12686 ℤ_≥cuz 12958 ...cfz 13632 ↑cexp 14197 ∥ cdvds 16415 gcd cgcd 16657 ℙcprime 16839 Basecbs 17380 +_gcplusg 17421 0_gc0g 17603 Σ_g cgsu 17604 Mndcmnd 18916 ._gcmg 19270 CMndccmn 19987 mulGrpcmgp 20353 Ringcrg 20452 CRingccrg 20453 RingHom crh 20692 RingIso crs 20693 Fieldcfield 20974 ℤ_ringczring 21745 ℤRHomczrh 21798 chrcchr 21800 algSccascl 22153 var₁cv1 22487 Poly₁cpl1 22488 eval₁ce1 22625 PrimRoots cprimroots 43121

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271 ax-addf 11272 ax-mulf 11273

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-ofr 7692 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-tpos 8236 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-oadd 8473 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-sup 9427 df-inf 9428 df-oi 9497 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-xnn0 12673 df-z 12687 df-dec 12808 df-uz 12959 df-rp 13114 df-fz 13633 df-fzo 13782 df-fl 13925 df-mod 14003 df-seq 14138 df-exp 14198 df-fac 14411 df-bc 14440 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-dvds 16416 df-gcd 16658 df-prm 16840 df-phi 16936 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-starv 17436 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-hom 17445 df-cco 17446 df-0g 17605 df-gsum 17606 df-prds 17611 df-pws 17613 df-mre 17749 df-mrc 17750 df-acs 17752 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-mhm 18971 df-submnd 18972 df-grp 19140 df-minusg 19141 df-sbg 19142 df-mulg 19271 df-subg 19326 df-ghm 19421 df-cntz 19524 df-od 19735 df-cmn 19989 df-abl 19990 df-mgp 20354 df-rng 20368 df-ur 20401 df-srg 20406 df-ring 20454 df-cring 20455 df-oppr 20560 df-dvdsr 20580 df-unit 20581 df-invr 20611 df-dvr 20624 df-rhm 20695 df-rim 20696 df-subrng 20791 df-subrg 20815 df-drng 20975 df-field 20976 df-lmod 21130 df-lss 21200 df-lsp 21240 df-cnfld 21672 df-zring 21746 df-zrh 21802 df-chr 21804 df-assa 22154 df-asp 22155 df-ascl 22156 df-psr 22210 df-mvr 22211 df-mpl 22212 df-opsr 22214 df-evls 22376 df-evl 22377 df-psr1 22491 df-vr1 22492 df-ply1 22493 df-coe1 22494 df-evl1 22627 df-primroots 43122

This theorem is used by: aks6d1c1rh 43155

W3C validator