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 43275

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 12725	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1	nn0ge0d 12677	. . . 4 ⊢ (𝜑 → 0 ≤ 𝐴)
4	1	nn0red 12675	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	4	leidd 11889	. . . 4 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
6	2, 3, 5	3jca 1146	. . 3 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴))
7		oveq2 7432	. . . . . . . 8 ⊢ (ℎ = 0 → (0...ℎ) = (0...0))
8	7	mpteq1d 5194	. . . . . . 7 ⊢ (ℎ = 0 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
9	8	oveq2d 7440	. . . . . 6 ⊢ (ℎ = 0 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
10	9	breq2d 5114	. . . . 5 ⊢ (ℎ = 0 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
11		oveq2 7432	. . . . . . . 8 ⊢ (ℎ = 𝑗 → (0...ℎ) = (0...𝑗))
12	11	mpteq1d 5194	. . . . . . 7 ⊢ (ℎ = 𝑗 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
13	12	oveq2d 7440	. . . . . 6 ⊢ (ℎ = 𝑗 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
14	13	breq2d 5114	. . . . 5 ⊢ (ℎ = 𝑗 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
15		oveq2 7432	. . . . . . . 8 ⊢ (ℎ = (𝑗 + 1) → (0...ℎ) = (0...(𝑗 + 1)))
16	15	mpteq1d 5194	. . . . . . 7 ⊢ (ℎ = (𝑗 + 1) → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
17	16	oveq2d 7440	. . . . . 6 ⊢ (ℎ = (𝑗 + 1) → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
18	17	breq2d 5114	. . . . 5 ⊢ (ℎ = (𝑗 + 1) → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
19		oveq2 7432	. . . . . . . 8 ⊢ (ℎ = 𝐴 → (0...ℎ) = (0...𝐴))
20	19	mpteq1d 5194	. . . . . . 7 ⊢ (ℎ = 𝐴 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
21	20	oveq2d 7440	. . . . . 6 ⊢ (ℎ = 𝐴 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
22	21	breq2d 5114	. . . . 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 16858	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
43	36, 42	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℕ)
44		aks6d1c1.22	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℕ₀)
45	43, 44	nnexpcld 14396	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃↑𝑈) ∈ ℕ)
46	43	nnzd 12726	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℤ)
47	43	nnne0d 12395	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ≠ 0)
48	38	nnzd 12726	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℤ)
49		dvdsval2 16434	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
50	46, 47, 48, 49	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
51	39, 50	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℤ)
52	38	nnred 12357	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53	43	nnred 12357	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
54	38	nngt0d 12394	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑁)
55	43	nngt0d 12394	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑃)
56	52, 53, 54, 55	divgt0d 12259	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < (𝑁 / 𝑃))
57	51, 56	jca 521	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
58		elnnz 12710	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 / 𝑃) ∈ ℕ ↔ ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
59	57, 58	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℕ)
60		aks6d1c1.23	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℕ₀)
61	59, 60	nnexpcld 14396	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 / 𝑃)↑𝐿) ∈ ℕ)
62	45, 61	nnmulcld 12398	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∈ ℕ)
63	41, 62	eqeltrid 2864	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℕ)
64	23, 24, 25, 26, 28, 29, 32, 33, 35, 36, 37, 38, 39, 40, 63	aks6d1c1p7 43272	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∼ 𝑋)
65	35	fldcrngd 21004	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
66	24	ply1crng 22525	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing)
67	65, 66	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ CRing)
68		crngring 20481	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
69		ringcmn 20520	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
70	68, 69	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ CMnd)
71	67, 70	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ CMnd)
72		cmnmnd 20020	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ CMnd → 𝑆 ∈ Mnd)
73	71, 72	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Mnd)
74		crngring 20481	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
75	65, 74	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
76		eqid 2760	. . . . . . . . . . . . 13 ⊢ (Base‘𝑆) = (Base‘𝑆)
77	26, 24, 76	vr1cl 22544	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑋 ∈ (Base‘𝑆))
78	75, 77	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆))
79		eqid 2760	. . . . . . . . . . . 12 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
80	76, 34, 79	mndrid 18954	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆)) → (𝑋 + (0_g‘𝑆)) = 𝑋)
81	73, 78, 80	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (0_g‘𝑆)) = 𝑋)
82	64, 81	breqtrrd 5132	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (0_g‘𝑆)))
83		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
84		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
85	83, 84	zrh0 21828	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
86	75, 85	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
87	86	fveq2d 6894	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (𝐶‘(0_g‘𝐾)))
88	24, 30, 84, 79, 75	ply1ascl0 22581	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(0_g‘𝐾)) = (0_g‘𝑆))
89	87, 88	eqtrd 2795	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (0_g‘𝑆))
90	89	oveq2d 7440	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) = (𝑋 + (0_g‘𝑆)))
91	82, 90	breqtrrd 5132	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
92		aks6d1c1.19	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ₀)
93		0zd 12712	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℤ)
94		0red 11318	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
95	94	leidd 11889	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 0)
96	93, 2, 93, 95, 3	elfzd 13654	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝐴))
97	92, 96	ffvelcdmd 7090	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
98	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 91, 97	aks6d1c1p6 43273	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∼ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
99	27	crngmgp 20476	. . . . . . . . . 10 ⊢ (𝑆 ∈ CRing → 𝑊 ∈ CMnd)
100	67, 99	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ CMnd)
101	100	cmnmndd 20027	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Mnd)
102		0z 12711	. . . . . . . . 9 ⊢ 0 ∈ ℤ
103	102	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
104		eqid 2760	. . . . . . . . 9 ⊢ (Base‘𝑊) = (Base‘𝑊)
105		0le0 12451	. . . . . . . . . . . 12 ⊢ 0 ≤ 0
106	105	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 0)
107	103, 2, 103, 106, 3	elfzd 13654	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (0...𝐴))
108	92, 107	ffvelcdmd 7090	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
109	83	zrhrhm 21826	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
110	75, 109	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
111		zringbas 21768	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤ_ring)
112		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐾) = (Base‘𝐾)
113	111, 112	rhmf 20724	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
114	110, 113	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
115	114, 93	ffvelcdmd 7090	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾))
116	24, 30, 112, 76	ply1sclcl 22614	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
117	75, 115, 116	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
118	76, 34	mndcl 18940	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
119	73, 78, 117, 118	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
120	27, 76	mgpbas 20374	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑊)
121	119, 120	eleqtrdi 2870	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑊))
122	104, 31, 101, 108, 121	mulgnn0cld 19314	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊))
123		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝐹‘𝑖) = (𝐹‘0))
124		2fveq3 6895	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
125	124	oveq2d 7440	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
126	123, 125	oveq12d 7442	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
127	104, 126	gsumsn 20177	. . . . . . . 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 5132	. . . . . 6 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
130		fzsn 13707	. . . . . . . . . 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 5194	. . . . . . 7 ⊢ (𝜑 → (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
134	133	oveq2d 7440	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
135	129, 134	breqtrrd 5132	. . . . 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 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑘((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))
143		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑖((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
144		fveq2 6890	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹‘𝑖) = (𝐹‘𝑘))
145		2fveq3 6895	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘𝑘)))
146	145	oveq2d 7440	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
147	144, 146	oveq12d 7442	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
148	142, 143, 147	cbvmpt 5206	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
149	148	oveq2i 7435	. . . . . . . . 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 5130	. . . . . . 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 12726	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ ℤ)
160	51, 159, 60	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀))
161	159, 51, 48	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ))
162	48, 159	jca 521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ))
163		gcdcom 16694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
164	162, 163	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
165		eqeq1 2764	. . . . . . . . . . . . . . . . . . . 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 11344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℂ)
170	53	recnd 11344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℂ)
171	94, 54	gtned 11452	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ≠ 0)
172	169, 169, 170, 171, 47	divdiv2d 12132	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) = ((𝑁 · 𝑃) / 𝑁))
173	169, 170	mulcomd 11337	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 · 𝑃) = (𝑃 · 𝑁))
174	173	oveq1d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = ((𝑃 · 𝑁) / 𝑁))
175	170, 169, 169, 171, 171	divdiv2d 12132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = ((𝑃 · 𝑁) / 𝑁))
176	175	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑃 · 𝑁) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
177	174, 176	eqtrd 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
178	169, 171	dividd 12098	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
179	178	oveq2d 7440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = (𝑃 / 1))
180	170	div1d 12092	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / 1) = 𝑃)
181	179, 180	eqtrd 2795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = 𝑃)
182	181, 46	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) ∈ ℤ)
183	177, 182	eqeltrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) ∈ ℤ)
184	172, 183	eqeltrd 2860	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)
185	94, 56	gtned 11452	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / 𝑃) ≠ 0)
186		dvdsval2 16434	. . . . . . . . . . . . . . . . . . 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 16844	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) → (𝑅 gcd (𝑁 / 𝑃)) = 1)
191	161, 189, 190	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1)
192	159, 51	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ))
193		gcdcom 16694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ) → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
194	192, 193	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
195		eqeq1 2764	. . . . . . . . . . . . . . . . 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 16908	. . . . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . 14 ⊢ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
204		simpr1 1213	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℤ)
205	204	peano2zd 12813	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ ℤ)
206	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205	aks6d1c1p2 43268	. . . . . . . . . . . . 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 16844	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) → (𝑅 gcd 𝑃) = 1)
211	208, 209, 210	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd 𝑃) = 1)
212	159, 46	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ))
213		gcdcom 16694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
214	212, 213	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
215		eqeq1 2764	. . . . . . . . . . . . . . . . 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 43274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃↑𝑈) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
221		2fveq3 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
222	221	oveq2d 7440	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
223	222	breq2d 5114	. . . . . . . . . . . . . . 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 43272	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∼ 𝑋)
226	225, 81	breqtrrd 5132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (0_g‘𝑆)))
227	226, 90	breqtrrd 5132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
228	227	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
229		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑎 = 0)
230	229	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑎 = 0) → ((ℤRHom‘𝐾)‘𝑎) = ((ℤRHom‘𝐾)‘0))
231	230	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
232	231	oveq2d 7440	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
233	228, 232	breqtrrd 5132	. . . . . . . . . . . . . . . . . . . . . . 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 11309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 1 ∈ ℂ)
238	237	addlidd 11518	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (0 + 1) = 1)
239	238	oveq1d 7439	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((0 + 1)...𝐴) = (1...𝐴))
240	239	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . . . 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 12976	. . . . . . . . . . . . . . . . . . . . . . . . 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 13744	. . . . . . . . . . . . . . . . . . . . . 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 3171	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
255	224, 254	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
256	255	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
257		0zd 12712	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ∈ ℤ)
258	2	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐴 ∈ ℤ)
259	204	zred 12810	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℝ)
260		1red 11316	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 1 ∈ ℝ)
261		simpr2 1214	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 𝑗)
262		0le1 11846	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 1
263	262	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 1)
264	259, 260, 261, 263	addge0d 11899	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ (𝑗 + 1))
265		simpr3 1215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 < 𝐴)
266	204, 258	zltp1led 12758	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴))
267	265, 266	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ≤ 𝐴)
268	257, 258, 205, 264, 267	elfzd 13654	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ (0...𝐴))
269	223, 256, 268	rspcdva 3577	. . . . . . . . . . . . . 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 43269	. . . . . . . . . . . . 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 43274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃)↑𝐿) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
276	23, 24, 25, 26, 27, 28, 29, 30, 32, 33, 34, 152, 153, 154, 202, 156, 220, 275	aks6d1c1p5 43271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
277	158, 276	eqbrtrd 5126	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
278	92	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐹:(0...𝐴)⟶ℕ₀)
279	278, 268	ffvelcdmd 7090	. . . . . . . . . 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 43273	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
281	101	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑊 ∈ Mnd)
282		ovexd 7459	. . . . . . . . . 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 7090	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾))
288	24, 30, 112, 76	ply1sclcl 22614	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
289	285, 287, 288	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
290	76, 34	mndcl 18940	. . . . . . . . . . . . 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 2870	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑊))
293	104, 31, 281, 279, 292	mulgnn0cld 19314	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊))
294		fveq2 6890	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
295		2fveq3 6895	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
296	295	oveq2d 7440	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
297	294, 296	oveq12d 7442	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
298	104, 297	gsumsn 20177	. . . . . . . . . 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 5132	. . . . . . . 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 43270	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
303	142, 143, 147	cbvmpt 5206	. . . . . . . . 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 7440	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
306		eqid 2760	. . . . . . . 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 12713	. . . . . . . . 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 12712	. . . . . . . . . . 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 13663	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ∈ ℤ)
321	320	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℤ)
322		elfzle1 13667	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 0 ≤ 𝑘)
323	322	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ≤ 𝑘)
324	321	zred 12810	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℝ)
325	308	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℤ)
326	325	zred 12810	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℝ)
327		1red 11316	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 1 ∈ ℝ)
328	326, 327	readdcld 11345	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ∈ ℝ)
329	319	zred 12810	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℝ)
330		elfzle2 13668	. . . . . . . . . . . . 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 12758	. . . . . . . . . . . . 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 11474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ 𝐴)
336	317, 319, 321, 323, 335	elfzd 13654	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ (0...𝐴))
337	316, 336	ffvelcdmd 7090	. . . . . . . . 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 7090	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾))
346	24, 30, 112, 76	ply1sclcl 22614	. . . . . . . . . . . 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 18940	. . . . . . . . . . 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 2870	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑊))
351	104, 31, 314, 337, 350	mulgnn0cld 19314	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) ∈ (Base‘𝑊))
352	104, 306, 307, 312, 351	gsummptfzsplit 20155	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
353	305, 352	eqtrd 2795	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
354	302, 353	breqtrrd 5132	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
355	10, 14, 18, 22, 135, 354, 93, 2, 3	fzindd 12808	. . . 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 6892	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → (𝑔‘𝑖) = (𝐹‘𝑖))
362	361	oveq1d 7439	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))
363	362	mpteq2dva 5197	. . . 4 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
364	363	oveq2d 7440	. . 3 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
365		nn0ex 12619	. . . . . 6 ⊢ ℕ₀ ∈ V
366	365	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ₀ ∈ V)
367		ovexd 7459	. . . . 5 ⊢ (𝜑 → (0...𝐴) ∈ V)
368	366, 367	elmapd 8867	. . . 4 ⊢ (𝜑 → (𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)) ↔ 𝐹:(0...𝐴)⟶ℕ₀))
369	92, 368	mpbird 260	. . 3 ⊢ (𝜑 → 𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)))
370		ovexd 7459	. . 3 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ∈ V)
371	359, 364, 369, 370	fvmptd 7006	. 2 ⊢ (𝜑 → (𝐺‘𝐹) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
372	357, 371	breqtrrd 5132	1 ⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 Vcvv 3450 {csn 4584 class class class wbr 5102 {copab 5166 ↦ cmpt 5185 ⟶wf 6539 ‘cfv 6543 (class class class)co 7424 ↑_m cmap 8854 0cc0 11207 1c1 11208 + caddc 11210 · cmul 11212 < clt 11350 ≤ cle 11351 / cdiv 11980 ℕcn 12342 ℕ₀cn0 12613 ℤcz 12700 ℤ_≥cuz 12972 ...cfz 13646 ↑cexp 14211 ∥ cdvds 16431 gcd cgcd 16673 ℙcprime 16855 Basecbs 17396 +_gcplusg 17437 0_gc0g 17619 Σ_g cgsu 17620 Mndcmnd 18932 ._gcmg 19286 CMndccmn 20003 mulGrpcmgp 20369 Ringcrg 20468 CRingccrg 20469 RingHom crh 20708 RingIso crs 20709 Fieldcfield 20990 ℤ_ringczring 21761 ℤRHomczrh 21814 chrcchr 21816 algSccascl 22169 var₁cv1 22503 Poly₁cpl1 22504 eval₁ce1 22641 PrimRoots cprimroots 43250

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-pre-sup 11285 ax-addf 11286 ax-mulf 11287

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 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 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7697 df-ofr 7698 df-om 7882 df-1st 8005 df-2nd 8006 df-supp 8184 df-tpos 8250 df-frecs 8306 df-wrecs 8337 df-recs 8386 df-rdg 8425 df-1o 8483 df-2o 8484 df-oadd 8487 df-er 8724 df-map 8856 df-pm 8857 df-ixp 8933 df-en 8981 df-dom 8982 df-sdom 8983 df-fin 8984 df-fsupp 9361 df-sup 9441 df-inf 9442 df-oi 9511 df-dju 9989 df-card 10027 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-div 11981 df-nn 12343 df-2 12412 df-3 12413 df-4 12414 df-5 12415 df-6 12416 df-7 12417 df-8 12418 df-9 12419 df-n0 12614 df-xnn0 12687 df-z 12701 df-dec 12822 df-uz 12973 df-rp 13128 df-fz 13647 df-fzo 13796 df-fl 13939 df-mod 14017 df-seq 14152 df-exp 14212 df-fac 14425 df-bc 14454 df-hash 14482 df-cj 15275 df-re 15276 df-im 15277 df-sqrt 15411 df-abs 15412 df-dvds 16432 df-gcd 16674 df-prm 16856 df-phi 16952 df-struct 17334 df-sets 17351 df-slot 17369 df-ndx 17381 df-base 17397 df-ress 17418 df-plusg 17450 df-mulr 17451 df-starv 17452 df-sca 17453 df-vsca 17454 df-ip 17455 df-tset 17456 df-ple 17457 df-ds 17459 df-unif 17460 df-hom 17461 df-cco 17462 df-0g 17621 df-gsum 17622 df-prds 17627 df-pws 17629 df-mre 17765 df-mrc 17766 df-acs 17768 df-mgm 18825 df-sgrp 18917 df-mnd 18933 df-mhm 18987 df-submnd 18988 df-grp 19156 df-minusg 19157 df-sbg 19158 df-mulg 19287 df-subg 19342 df-ghm 19437 df-cntz 19540 df-od 19751 df-cmn 20005 df-abl 20006 df-mgp 20370 df-rng 20384 df-ur 20417 df-srg 20422 df-ring 20470 df-cring 20471 df-oppr 20576 df-dvdsr 20596 df-unit 20597 df-invr 20627 df-dvr 20640 df-rhm 20711 df-rim 20712 df-subrng 20807 df-subrg 20831 df-drng 20991 df-field 20992 df-lmod 21146 df-lss 21216 df-lsp 21256 df-cnfld 21688 df-zring 21762 df-zrh 21818 df-chr 21820 df-assa 22170 df-asp 22171 df-ascl 22172 df-psr 22226 df-mvr 22227 df-mpl 22228 df-opsr 22230 df-evls 22392 df-evl 22393 df-psr1 22507 df-vr1 22508 df-ply1 22509 df-coe1 22510 df-evl1 22643 df-primroots 43251

This theorem is used by: aks6d1c1rh 43284

W3C validator