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 42111

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 12562	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1	nn0ge0d 12513	. . . 4 ⊢ (𝜑 → 0 ≤ 𝐴)
4	1	nn0red 12511	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	4	leidd 11751	. . . 4 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
6	2, 3, 5	3jca 1128	. . 3 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴))
7		oveq2 7398	. . . . . . . 8 ⊢ (ℎ = 0 → (0...ℎ) = (0...0))
8	7	mpteq1d 5200	. . . . . . 7 ⊢ (ℎ = 0 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
9	8	oveq2d 7406	. . . . . 6 ⊢ (ℎ = 0 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
10	9	breq2d 5122	. . . . 5 ⊢ (ℎ = 0 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
11		oveq2 7398	. . . . . . . 8 ⊢ (ℎ = 𝑗 → (0...ℎ) = (0...𝑗))
12	11	mpteq1d 5200	. . . . . . 7 ⊢ (ℎ = 𝑗 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
13	12	oveq2d 7406	. . . . . 6 ⊢ (ℎ = 𝑗 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
14	13	breq2d 5122	. . . . 5 ⊢ (ℎ = 𝑗 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
15		oveq2 7398	. . . . . . . 8 ⊢ (ℎ = (𝑗 + 1) → (0...ℎ) = (0...(𝑗 + 1)))
16	15	mpteq1d 5200	. . . . . . 7 ⊢ (ℎ = (𝑗 + 1) → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
17	16	oveq2d 7406	. . . . . 6 ⊢ (ℎ = (𝑗 + 1) → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
18	17	breq2d 5122	. . . . 5 ⊢ (ℎ = (𝑗 + 1) → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
19		oveq2 7398	. . . . . . . 8 ⊢ (ℎ = 𝐴 → (0...ℎ) = (0...𝐴))
20	19	mpteq1d 5200	. . . . . . 7 ⊢ (ℎ = 𝐴 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
21	20	oveq2d 7406	. . . . . 6 ⊢ (ℎ = 𝐴 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
22	21	breq2d 5122	. . . . 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 16651	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
43	36, 42	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℕ)
44		aks6d1c1.22	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℕ₀)
45	43, 44	nnexpcld 14217	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃↑𝑈) ∈ ℕ)
46	43	nnzd 12563	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℤ)
47	43	nnne0d 12243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ≠ 0)
48	38	nnzd 12563	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℤ)
49		dvdsval2 16232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
50	46, 47, 48, 49	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
51	39, 50	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℤ)
52	38	nnred 12208	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53	43	nnred 12208	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
54	38	nngt0d 12242	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑁)
55	43	nngt0d 12242	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑃)
56	52, 53, 54, 55	divgt0d 12125	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < (𝑁 / 𝑃))
57	51, 56	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
58		elnnz 12546	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 / 𝑃) ∈ ℕ ↔ ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
59	57, 58	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℕ)
60		aks6d1c1.23	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℕ₀)
61	59, 60	nnexpcld 14217	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 / 𝑃)↑𝐿) ∈ ℕ)
62	45, 61	nnmulcld 12246	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∈ ℕ)
63	41, 62	eqeltrid 2833	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℕ)
64	23, 24, 25, 26, 28, 29, 32, 33, 35, 36, 37, 38, 39, 40, 63	aks6d1c1p7 42108	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∼ 𝑋)
65	35	fldcrngd 20658	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
66	24	ply1crng 22090	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing)
67	65, 66	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ CRing)
68		crngring 20161	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
69		ringcmn 20198	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
70	68, 69	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ CMnd)
71	67, 70	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ CMnd)
72		cmnmnd 19734	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ CMnd → 𝑆 ∈ Mnd)
73	71, 72	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Mnd)
74		crngring 20161	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
75	65, 74	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
76		eqid 2730	. . . . . . . . . . . . 13 ⊢ (Base‘𝑆) = (Base‘𝑆)
77	26, 24, 76	vr1cl 22109	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑋 ∈ (Base‘𝑆))
78	75, 77	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆))
79		eqid 2730	. . . . . . . . . . . 12 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
80	76, 34, 79	mndrid 18689	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆)) → (𝑋 + (0_g‘𝑆)) = 𝑋)
81	73, 78, 80	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (0_g‘𝑆)) = 𝑋)
82	64, 81	breqtrrd 5138	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (0_g‘𝑆)))
83		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
84		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
85	83, 84	zrh0 21430	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
86	75, 85	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
87	86	fveq2d 6865	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (𝐶‘(0_g‘𝐾)))
88	24, 30, 84, 79, 75	ply1ascl0 22146	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(0_g‘𝐾)) = (0_g‘𝑆))
89	87, 88	eqtrd 2765	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (0_g‘𝑆))
90	89	oveq2d 7406	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) = (𝑋 + (0_g‘𝑆)))
91	82, 90	breqtrrd 5138	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
92		aks6d1c1.19	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ₀)
93		0zd 12548	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℤ)
94		0red 11184	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
95	94	leidd 11751	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 0)
96	93, 2, 93, 95, 3	elfzd 13483	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝐴))
97	92, 96	ffvelcdmd 7060	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
98	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 91, 97	aks6d1c1p6 42109	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∼ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
99	27	crngmgp 20157	. . . . . . . . . 10 ⊢ (𝑆 ∈ CRing → 𝑊 ∈ CMnd)
100	67, 99	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ CMnd)
101	100	cmnmndd 19741	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Mnd)
102		0z 12547	. . . . . . . . 9 ⊢ 0 ∈ ℤ
103	102	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
104		eqid 2730	. . . . . . . . 9 ⊢ (Base‘𝑊) = (Base‘𝑊)
105		0le0 12294	. . . . . . . . . . . 12 ⊢ 0 ≤ 0
106	105	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 0)
107	103, 2, 103, 106, 3	elfzd 13483	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (0...𝐴))
108	92, 107	ffvelcdmd 7060	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
109	83	zrhrhm 21428	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
110	75, 109	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
111		zringbas 21370	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤ_ring)
112		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐾) = (Base‘𝐾)
113	111, 112	rhmf 20401	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
114	110, 113	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
115	114, 93	ffvelcdmd 7060	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾))
116	24, 30, 112, 76	ply1sclcl 22179	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
117	75, 115, 116	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
118	76, 34	mndcl 18676	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
119	73, 78, 117, 118	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
120	27, 76	mgpbas 20061	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑊)
121	119, 120	eleqtrdi 2839	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑊))
122	104, 31, 101, 108, 121	mulgnn0cld 19034	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊))
123		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝐹‘𝑖) = (𝐹‘0))
124		2fveq3 6866	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
125	124	oveq2d 7406	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
126	123, 125	oveq12d 7408	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
127	104, 126	gsumsn 19891	. . . . . . . 8 ⊢ ((𝑊 ∈ Mnd ∧ 0 ∈ ℤ ∧ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊)) → (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
128	101, 103, 122, 127	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
129	98, 128	breqtrrd 5138	. . . . . 6 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
130		fzsn 13534	. . . . . . . . . 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 5200	. . . . . . 7 ⊢ (𝜑 → (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
134	133	oveq2d 7406	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
135	129, 134	breqtrrd 5138	. . . . 5 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
136	35	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Field)
137	36	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∈ ℙ)
138	37	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑅 ∈ ℕ)
139	40	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑁 gcd 𝑅) = 1)
140	39	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∥ 𝑁)
141		simp3 1138	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
142		nfcv 2892	. . . . . . . . . . 11 ⊢ Ⅎ𝑘((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))
143		nfcv 2892	. . . . . . . . . . 11 ⊢ Ⅎ𝑖((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
144		fveq2 6861	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹‘𝑖) = (𝐹‘𝑘))
145		2fveq3 6866	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘𝑘)))
146	145	oveq2d 7406	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
147	144, 146	oveq12d 7408	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
148	142, 143, 147	cbvmpt 5212	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
149	148	oveq2i 7401	. . . . . . . . 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 5136	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
152	35	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Field)
153	36	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∈ ℙ)
154	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑅 ∈ ℕ)
155	38	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∈ ℕ)
156	39	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∥ 𝑁)
157	40	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 gcd 𝑅) = 1)
158	41	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)))
159	37	nnzd 12563	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ ℤ)
160	51, 159, 60	3jca 1128	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀))
161	159, 51, 48	3jca 1128	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ))
162	48, 159	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ))
163		gcdcom 16490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
165		eqeq1 2734	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 gcd 𝑅) = (𝑅 gcd 𝑁) → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1))
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1))
167	166	pm5.74i 271	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 → (𝑁 gcd 𝑅) = 1) ↔ (𝜑 → (𝑅 gcd 𝑁) = 1))
168	40, 167	mpbi 230	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd 𝑁) = 1)
169	52	recnd 11209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℂ)
170	53	recnd 11209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℂ)
171	94, 54	gtned 11316	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ≠ 0)
172	169, 169, 170, 171, 47	divdiv2d 11997	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) = ((𝑁 · 𝑃) / 𝑁))
173	169, 170	mulcomd 11202	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 · 𝑃) = (𝑃 · 𝑁))
174	173	oveq1d 7405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = ((𝑃 · 𝑁) / 𝑁))
175	170, 169, 169, 171, 171	divdiv2d 11997	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = ((𝑃 · 𝑁) / 𝑁))
176	175	eqcomd 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑃 · 𝑁) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
177	174, 176	eqtrd 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
178	169, 171	dividd 11963	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
179	178	oveq2d 7406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = (𝑃 / 1))
180	170	div1d 11957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / 1) = 𝑃)
181	179, 180	eqtrd 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = 𝑃)
182	181, 46	eqeltrd 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) ∈ ℤ)
183	177, 182	eqeltrd 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) ∈ ℤ)
184	172, 183	eqeltrd 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)
185	94, 56	gtned 11316	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / 𝑃) ≠ 0)
186		dvdsval2 16232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ (𝑁 / 𝑃) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ))
187	51, 185, 48, 186	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ))
188	184, 187	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 / 𝑃) ∥ 𝑁)
189	168, 188	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁))
190		rpdvds 16637	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) → (𝑅 gcd (𝑁 / 𝑃)) = 1)
191	161, 189, 190	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1)
192	159, 51	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ))
193		gcdcom 16490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ) → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
194	192, 193	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
195		eqeq1 2734	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅) → ((𝑅 gcd (𝑁 / 𝑃)) = 1 ↔ ((𝑁 / 𝑃) gcd 𝑅) = 1))
196	194, 195	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd (𝑁 / 𝑃)) = 1 ↔ ((𝑁 / 𝑃) gcd 𝑅) = 1))
197	196	pm5.74i 271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1) ↔ (𝜑 → ((𝑁 / 𝑃) gcd 𝑅) = 1))
198	191, 197	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃) gcd 𝑅) = 1)
199		rpexp1i 16700	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀) → (((𝑁 / 𝑃) gcd 𝑅) = 1 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1))
200	199	imp 406	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀) ∧ ((𝑁 / 𝑃) gcd 𝑅) = 1) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
201	160, 198, 200	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
202	201	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
203		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
204		simpr1 1195	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℤ)
205	204	peano2zd 12648	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ ℤ)
206	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205	aks6d1c1p2 42104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
207	44	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑈 ∈ ℕ₀)
208	159, 46, 48	3jca 1128	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ))
209	168, 39	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁))
210		rpdvds 16637	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) → (𝑅 gcd 𝑃) = 1)
211	208, 209, 210	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd 𝑃) = 1)
212	159, 46	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ))
213		gcdcom 16490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
214	212, 213	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
215		eqeq1 2734	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 gcd 𝑃) = (𝑃 gcd 𝑅) → ((𝑅 gcd 𝑃) = 1 ↔ (𝑃 gcd 𝑅) = 1))
216	214, 215	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑃) = 1 ↔ (𝑃 gcd 𝑅) = 1))
217	216	pm5.74i 271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 → (𝑅 gcd 𝑃) = 1) ↔ (𝜑 → (𝑃 gcd 𝑅) = 1))
218	211, 217	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 gcd 𝑅) = 1)
219	218	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃 gcd 𝑅) = 1)
220	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 155, 156, 157, 206, 207, 219	aks6d1c1p8 42110	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃↑𝑈) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
221		2fveq3 6866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
222	221	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
223	222	breq2d 5122	. . . . . . . . . . . . . . 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 42108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∼ 𝑋)
226	225, 81	breqtrrd 5138	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (0_g‘𝑆)))
227	226, 90	breqtrrd 5138	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
228	227	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
229		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑎 = 0)
230	229	fveq2d 6865	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑎 = 0) → ((ℤRHom‘𝐾)‘𝑎) = ((ℤRHom‘𝐾)‘0))
231	230	fveq2d 6865	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
232	231	oveq2d 7406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
233	228, 232	breqtrrd 5138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
234	233	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
235	234	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
236		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
237		1cnd 11176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 1 ∈ ℂ)
238	237	addlidd 11382	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (0 + 1) = 1)
239	238	oveq1d 7405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((0 + 1)...𝐴) = (1...𝐴))
240	239	eleq2d 2815	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ ((0 + 1)...𝐴) ↔ 𝑎 ∈ (1...𝐴)))
241	240	imbi1d 341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 ∈ ((0 + 1)...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) ↔ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
242	236, 241	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ ((0 + 1)...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
243	235, 242	jaod 859	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
244	2, 3	jca 511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
245		eluz1 12804	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ ℤ → (𝐴 ∈ (ℤ_≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)))
246	93, 245	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)))
247	244, 246	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
248	247	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 𝐴 ∈ (ℤ_≥‘0))
249		elfzp12 13571	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (ℤ_≥‘0) → (𝑎 ∈ (0...𝐴) ↔ (𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴))))
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (0...𝐴) ↔ (𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴))))
251	250	imbi1d 341	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) ↔ ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
252	243, 251	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
253	252	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
254	253	ralimdv2 3143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
255	224, 254	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
256	255	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
257		0zd 12548	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ∈ ℤ)
258	2	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐴 ∈ ℤ)
259	204	zred 12645	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℝ)
260		1red 11182	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 1 ∈ ℝ)
261		simpr2 1196	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 𝑗)
262		0le1 11708	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 1
263	262	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 1)
264	259, 260, 261, 263	addge0d 11761	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ (𝑗 + 1))
265		simpr3 1197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 < 𝐴)
266	204, 258	zltp1led 41974	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴))
267	265, 266	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ≤ 𝐴)
268	257, 258, 205, 264, 267	elfzd 13483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ (0...𝐴))
269	223, 256, 268	rspcdva 3592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
270		aks6d1c1.26	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾))
271	270	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾))
272	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205, 269, 271	aks6d1c1p3 42105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 / 𝑃) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
273	60	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐿 ∈ ℕ₀)
274	198	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃) gcd 𝑅) = 1)
275	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 155, 156, 157, 272, 273, 274	aks6d1c1p8 42110	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃)↑𝐿) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
276	23, 24, 25, 26, 27, 28, 29, 30, 32, 33, 34, 152, 153, 154, 202, 156, 220, 275	aks6d1c1p5 42107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
277	158, 276	eqbrtrd 5132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
278	92	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐹:(0...𝐴)⟶ℕ₀)
279	278, 268	ffvelcdmd 7060	. . . . . . . . . 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 42109	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
281	101	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑊 ∈ Mnd)
282		ovexd 7425	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ V)
283	73	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑆 ∈ Mnd)
284	78	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑋 ∈ (Base‘𝑆))
285	75	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Ring)
286	114	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
287	286, 205	ffvelcdmd 7060	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾))
288	24, 30, 112, 76	ply1sclcl 22179	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
289	285, 287, 288	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
290	76, 34	mndcl 18676	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆))
291	283, 284, 289, 290	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆))
292	291, 120	eleqtrdi 2839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑊))
293	104, 31, 281, 279, 292	mulgnn0cld 19034	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊))
294		fveq2 6861	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
295		2fveq3 6866	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
296	295	oveq2d 7406	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
297	294, 296	oveq12d 7408	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
298	104, 297	gsumsn 19891	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ (𝑗 + 1) ∈ V ∧ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊)) → (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
299	281, 282, 293, 298	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
300	280, 299	breqtrrd 5138	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
301	300	3adant3 1132	. . . . . . 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 42106	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
303	142, 143, 147	cbvmpt 5212	. . . . . . . . 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 7406	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
306		eqid 2730	. . . . . . . 8 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
307	100	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ CMnd)
308		simp21 1207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℤ)
309		simp22 1208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 0 ≤ 𝑗)
310	308, 309	jca 511	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
311		elnn0z 12549	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ₀ ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
312	310, 311	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℕ₀)
313	281	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ Mnd)
314	313	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑊 ∈ Mnd)
315	92	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐹:(0...𝐴)⟶ℕ₀)
316	315	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐹:(0...𝐴)⟶ℕ₀)
317		0zd 12548	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ∈ ℤ)
318	2	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐴 ∈ ℤ)
319	318	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℤ)
320		elfzelz 13492	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ∈ ℤ)
321	320	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℤ)
322		elfzle1 13495	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 0 ≤ 𝑘)
323	322	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ≤ 𝑘)
324	321	zred 12645	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℝ)
325	308	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℤ)
326	325	zred 12645	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℝ)
327		1red 11182	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 1 ∈ ℝ)
328	326, 327	readdcld 11210	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ∈ ℝ)
329	319	zred 12645	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℝ)
330		elfzle2 13496	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ≤ (𝑗 + 1))
331	330	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ (𝑗 + 1))
332		simpl23 1254	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 < 𝐴)
333	325, 319	zltp1led 41974	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴))
334	332, 333	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ≤ 𝐴)
335	324, 328, 329, 331, 334	letrd 11338	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ 𝐴)
336	317, 319, 321, 323, 335	elfzd 13483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ (0...𝐴))
337	316, 336	ffvelcdmd 7060	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℕ₀)
338	283	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑆 ∈ Mnd)
339	338	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑆 ∈ Mnd)
340	284	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑋 ∈ (Base‘𝑆))
341	340	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑋 ∈ (Base‘𝑆))
342	285	3adant3 1132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Ring)
343	342	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐾 ∈ Ring)
344	343, 109, 113	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
345	344, 321	ffvelcdmd 7060	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾))
346	24, 30, 112, 76	ply1sclcl 22179	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆))
347	343, 345, 346	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆))
348	76, 34	mndcl 18676	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆))
349	339, 341, 347, 348	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆))
350	349, 120	eleqtrdi 2839	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑊))
351	104, 31, 314, 337, 350	mulgnn0cld 19034	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) ∈ (Base‘𝑊))
352	104, 306, 307, 312, 351	gsummptfzsplit 19869	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
353	305, 352	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
354	302, 353	breqtrrd 5138	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
355	10, 14, 18, 22, 135, 354, 93, 2, 3	fzindd 12643	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴)) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
356	355	ex 412	. . 3 ⊢ (𝜑 → ((𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
357	6, 356	mpd 15	. 2 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
358		aks6d1c1.20	. . . 4 ⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
359	358	a1i 11	. . 3 ⊢ (𝜑 → 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
360		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → 𝑔 = 𝐹)
361	360	fveq1d 6863	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → (𝑔‘𝑖) = (𝐹‘𝑖))
362	361	oveq1d 7405	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))
363	362	mpteq2dva 5203	. . . 4 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
364	363	oveq2d 7406	. . 3 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
365		nn0ex 12455	. . . . . 6 ⊢ ℕ₀ ∈ V
366	365	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ₀ ∈ V)
367		ovexd 7425	. . . . 5 ⊢ (𝜑 → (0...𝐴) ∈ V)
368	366, 367	elmapd 8816	. . . 4 ⊢ (𝜑 → (𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)) ↔ 𝐹:(0...𝐴)⟶ℕ₀))
369	92, 368	mpbird 257	. . 3 ⊢ (𝜑 → 𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)))
370		ovexd 7425	. . 3 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ∈ V)
371	359, 364, 369, 370	fvmptd 6978	. 2 ⊢ (𝜑 → (𝐺‘𝐹) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
372	357, 371	breqtrrd 5138	1 ⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 Vcvv 3450 {csn 4592 class class class wbr 5110 {copab 5172 ↦ cmpt 5191 ⟶wf 6510 ‘cfv 6514 (class class class)co 7390 ↑_m cmap 8802 0cc0 11075 1c1 11076 + caddc 11078 · cmul 11080 < clt 11215 ≤ cle 11216 / cdiv 11842 ℕcn 12193 ℕ₀cn0 12449 ℤcz 12536 ℤ_≥cuz 12800 ...cfz 13475 ↑cexp 14033 ∥ cdvds 16229 gcd cgcd 16471 ℙcprime 16648 Basecbs 17186 +_gcplusg 17227 0_gc0g 17409 Σ_g cgsu 17410 Mndcmnd 18668 ._gcmg 19006 CMndccmn 19717 mulGrpcmgp 20056 Ringcrg 20149 CRingccrg 20150 RingHom crh 20385 RingIso crs 20386 Fieldcfield 20646 ℤ_ringczring 21363 ℤRHomczrh 21416 chrcchr 21418 algSccascl 21768 var₁cv1 22067 Poly₁cpl1 22068 eval₁ce1 22208 PrimRoots cprimroots 42086

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153 ax-addf 11154 ax-mulf 11155

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-iin 4961 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-ofr 7657 df-om 7846 df-1st 7971 df-2nd 7972 df-supp 8143 df-tpos 8208 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8674 df-map 8804 df-pm 8805 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9320 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9861 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-xnn0 12523 df-z 12537 df-dec 12657 df-uz 12801 df-rp 12959 df-fz 13476 df-fzo 13623 df-fl 13761 df-mod 13839 df-seq 13974 df-exp 14034 df-fac 14246 df-bc 14275 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-dvds 16230 df-gcd 16472 df-prm 16649 df-phi 16743 df-struct 17124 df-sets 17141 df-slot 17159 df-ndx 17171 df-base 17187 df-ress 17208 df-plusg 17240 df-mulr 17241 df-starv 17242 df-sca 17243 df-vsca 17244 df-ip 17245 df-tset 17246 df-ple 17247 df-ds 17249 df-unif 17250 df-hom 17251 df-cco 17252 df-0g 17411 df-gsum 17412 df-prds 17417 df-pws 17419 df-mre 17554 df-mrc 17555 df-acs 17557 df-mgm 18574 df-sgrp 18653 df-mnd 18669 df-mhm 18717 df-submnd 18718 df-grp 18875 df-minusg 18876 df-sbg 18877 df-mulg 19007 df-subg 19062 df-ghm 19152 df-cntz 19256 df-od 19465 df-cmn 19719 df-abl 19720 df-mgp 20057 df-rng 20069 df-ur 20098 df-srg 20103 df-ring 20151 df-cring 20152 df-oppr 20253 df-dvdsr 20273 df-unit 20274 df-invr 20304 df-dvr 20317 df-rhm 20388 df-rim 20389 df-subrng 20462 df-subrg 20486 df-drng 20647 df-field 20648 df-lmod 20775 df-lss 20845 df-lsp 20885 df-cnfld 21272 df-zring 21364 df-zrh 21420 df-chr 21422 df-assa 21769 df-asp 21770 df-ascl 21771 df-psr 21825 df-mvr 21826 df-mpl 21827 df-opsr 21829 df-evls 21988 df-evl 21989 df-psr1 22071 df-vr1 22072 df-ply1 22073 df-coe1 22074 df-evl1 22210 df-primroots 42087

This theorem is referenced by: aks6d1c1rh 42120

W3C validator