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 42740

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 12604	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1	nn0ge0d 12556	. . . 4 ⊢ (𝜑 → 0 ≤ 𝐴)
4	1	nn0red 12554	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	4	leidd 11768	. . . 4 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
6	2, 3, 5	3jca 1144	. . 3 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴))
7		oveq2 7408	. . . . . . . 8 ⊢ (ℎ = 0 → (0...ℎ) = (0...0))
8	7	mpteq1d 5194	. . . . . . 7 ⊢ (ℎ = 0 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
9	8	oveq2d 7416	. . . . . 6 ⊢ (ℎ = 0 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
10	9	breq2d 5116	. . . . 5 ⊢ (ℎ = 0 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
11		oveq2 7408	. . . . . . . 8 ⊢ (ℎ = 𝑗 → (0...ℎ) = (0...𝑗))
12	11	mpteq1d 5194	. . . . . . 7 ⊢ (ℎ = 𝑗 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
13	12	oveq2d 7416	. . . . . 6 ⊢ (ℎ = 𝑗 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
14	13	breq2d 5116	. . . . 5 ⊢ (ℎ = 𝑗 → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
15		oveq2 7408	. . . . . . . 8 ⊢ (ℎ = (𝑗 + 1) → (0...ℎ) = (0...(𝑗 + 1)))
16	15	mpteq1d 5194	. . . . . . 7 ⊢ (ℎ = (𝑗 + 1) → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
17	16	oveq2d 7416	. . . . . 6 ⊢ (ℎ = (𝑗 + 1) → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
18	17	breq2d 5116	. . . . 5 ⊢ (ℎ = (𝑗 + 1) → (𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))))
19		oveq2 7408	. . . . . . . 8 ⊢ (ℎ = 𝐴 → (0...ℎ) = (0...𝐴))
20	19	mpteq1d 5194	. . . . . . 7 ⊢ (ℎ = 𝐴 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
21	20	oveq2d 7416	. . . . . 6 ⊢ (ℎ = 𝐴 → (𝑊 Σ_g (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
22	21	breq2d 5116	. . . . 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 16720	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
43	36, 42	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℕ)
44		aks6d1c1.22	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℕ₀)
45	43, 44	nnexpcld 14269	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃↑𝑈) ∈ ℕ)
46	43	nnzd 12605	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℤ)
47	43	nnne0d 12274	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ≠ 0)
48	38	nnzd 12605	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℤ)
49		dvdsval2 16301	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
50	46, 47, 48, 49	syl3anc 1394	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
51	39, 50	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℤ)
52	38	nnred 12236	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53	43	nnred 12236	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
54	38	nngt0d 12273	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑁)
55	43	nngt0d 12273	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑃)
56	52, 53, 54, 55	divgt0d 12138	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < (𝑁 / 𝑃))
57	51, 56	jca 520	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
58		elnnz 12589	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 / 𝑃) ∈ ℕ ↔ ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃)))
59	57, 58	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℕ)
60		aks6d1c1.23	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℕ₀)
61	59, 60	nnexpcld 14269	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 / 𝑃)↑𝐿) ∈ ℕ)
62	45, 61	nnmulcld 12277	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∈ ℕ)
63	41, 62	eqeltrid 2869	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℕ)
64	23, 24, 25, 26, 28, 29, 32, 33, 35, 36, 37, 38, 39, 40, 63	aks6d1c1p7 42737	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∼ 𝑋)
65	35	fldcrngd 20814	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
66	24	ply1crng 22315	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing)
67	65, 66	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ CRing)
68		crngring 20315	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
69		ringcmn 20353	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
70	68, 69	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ CMnd)
71	67, 70	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ CMnd)
72		cmnmnd 19855	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ CMnd → 𝑆 ∈ Mnd)
73	71, 72	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Mnd)
74		crngring 20315	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
75	65, 74	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
76		eqid 2765	. . . . . . . . . . . . 13 ⊢ (Base‘𝑆) = (Base‘𝑆)
77	26, 24, 76	vr1cl 22334	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑋 ∈ (Base‘𝑆))
78	75, 77	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆))
79		eqid 2765	. . . . . . . . . . . 12 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
80	76, 34, 79	mndrid 18801	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆)) → (𝑋 + (0_g‘𝑆)) = 𝑋)
81	73, 78, 80	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (0_g‘𝑆)) = 𝑋)
82	64, 81	breqtrrd 5132	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (0_g‘𝑆)))
83		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
84		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
85	83, 84	zrh0 21620	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Ring → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
86	75, 85	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) = (0_g‘𝐾))
87	86	fveq2d 6875	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (𝐶‘(0_g‘𝐾)))
88	24, 30, 84, 79, 75	ply1ascl0 22371	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(0_g‘𝐾)) = (0_g‘𝑆))
89	87, 88	eqtrd 2800	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (0_g‘𝑆))
90	89	oveq2d 7416	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) = (𝑋 + (0_g‘𝑆)))
91	82, 90	breqtrrd 5132	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
92		aks6d1c1.19	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ₀)
93		0zd 12591	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℤ)
94		0red 11199	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
95	94	leidd 11768	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 0)
96	93, 2, 93, 95, 3	elfzd 13531	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝐴))
97	92, 96	ffvelcdmd 7070	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
98	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 91, 97	aks6d1c1p6 42738	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∼ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
99	27	crngmgp 20311	. . . . . . . . . 10 ⊢ (𝑆 ∈ CRing → 𝑊 ∈ CMnd)
100	67, 99	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ CMnd)
101	100	cmnmndd 19862	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Mnd)
102		0z 12590	. . . . . . . . 9 ⊢ 0 ∈ ℤ
103	102	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
104		eqid 2765	. . . . . . . . 9 ⊢ (Base‘𝑊) = (Base‘𝑊)
105		0le0 12330	. . . . . . . . . . . 12 ⊢ 0 ≤ 0
106	105	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 0)
107	103, 2, 103, 106, 3	elfzd 13531	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ (0...𝐴))
108	92, 107	ffvelcdmd 7070	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) ∈ ℕ₀)
109	83	zrhrhm 21618	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
110	75, 109	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
111		zringbas 21560	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤ_ring)
112		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐾) = (Base‘𝐾)
113	111, 112	rhmf 20554	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
114	110, 113	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
115	114, 93	ffvelcdmd 7070	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾))
116	24, 30, 112, 76	ply1sclcl 22404	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
117	75, 115, 116	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆))
118	76, 34	mndcl 18788	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
119	73, 78, 117, 118	syl3anc 1394	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆))
120	27, 76	mgpbas 20209	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑊)
121	119, 120	eleqtrdi 2875	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑊))
122	104, 31, 101, 108, 121	mulgnn0cld 19149	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊))
123		fveq2 6871	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝐹‘𝑖) = (𝐹‘0))
124		2fveq3 6876	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
125	124	oveq2d 7416	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
126	123, 125	oveq12d 7418	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
127	104, 126	gsumsn 20012	. . . . . . . 8 ⊢ ((𝑊 ∈ Mnd ∧ 0 ∈ ℤ ∧ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊)) → (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
128	101, 103, 122, 127	syl3anc 1394	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))))
129	98, 128	breqtrrd 5132	. . . . . 6 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
130		fzsn 13582	. . . . . . . . . 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 7416	. . . . . 6 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
135	129, 134	breqtrrd 5132	. . . . 5 ⊢ (𝜑 → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
136	35	3ad2ant1 1149	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Field)
137	36	3ad2ant1 1149	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∈ ℙ)
138	37	3ad2ant1 1149	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑅 ∈ ℕ)
139	40	3ad2ant1 1149	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑁 gcd 𝑅) = 1)
140	39	3ad2ant1 1149	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∥ 𝑁)
141		simp3 1154	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
142		nfcv 2927	. . . . . . . . . . 11 ⊢ Ⅎ𝑘((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))
143		nfcv 2927	. . . . . . . . . . 11 ⊢ Ⅎ𝑖((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
144		fveq2 6871	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹‘𝑖) = (𝐹‘𝑘))
145		2fveq3 6876	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘𝑘)))
146	145	oveq2d 7416	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))
147	144, 146	oveq12d 7418	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
148	142, 143, 147	cbvmpt 5206	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))
149	148	oveq2i 7411	. . . . . . . . 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 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Field)
153	36	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∈ ℙ)
154	37	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑅 ∈ ℕ)
155	38	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∈ ℕ)
156	39	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∥ 𝑁)
157	40	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 gcd 𝑅) = 1)
158	41	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)))
159	37	nnzd 12605	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ ℤ)
160	51, 159, 60	3jca 1144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀))
161	159, 51, 48	3jca 1144	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ))
162	48, 159	jca 520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ))
163		gcdcom 16559	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
164	162, 163	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁))
165		eqeq1 2769	. . . . . . . . . . . . . . . . . . . 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 11225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℂ)
170	53	recnd 11225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℂ)
171	94, 54	gtned 11333	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ≠ 0)
172	169, 169, 170, 171, 47	divdiv2d 12011	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) = ((𝑁 · 𝑃) / 𝑁))
173	169, 170	mulcomd 11218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 · 𝑃) = (𝑃 · 𝑁))
174	173	oveq1d 7415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = ((𝑃 · 𝑁) / 𝑁))
175	170, 169, 169, 171, 171	divdiv2d 12011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = ((𝑃 · 𝑁) / 𝑁))
176	175	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑃 · 𝑁) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
177	174, 176	eqtrd 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = (𝑃 / (𝑁 / 𝑁)))
178	169, 171	dividd 11977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
179	178	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = (𝑃 / 1))
180	170	div1d 11971	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 / 1) = 𝑃)
181	179, 180	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = 𝑃)
182	181, 46	eqeltrd 2865	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) ∈ ℤ)
183	177, 182	eqeltrd 2865	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) ∈ ℤ)
184	172, 183	eqeltrd 2865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)
185	94, 56	gtned 11333	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 / 𝑃) ≠ 0)
186		dvdsval2 16301	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ (𝑁 / 𝑃) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ))
187	51, 185, 48, 186	syl3anc 1394	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ))
188	184, 187	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 / 𝑃) ∥ 𝑁)
189	168, 188	jca 520	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁))
190		rpdvds 16706	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) → (𝑅 gcd (𝑁 / 𝑃)) = 1)
191	161, 189, 190	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1)
192	159, 51	jca 520	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ))
193		gcdcom 16559	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ) → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
194	192, 193	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅))
195		eqeq1 2769	. . . . . . . . . . . . . . . . 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 16770	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀) → (((𝑁 / 𝑃) gcd 𝑅) = 1 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1))
200	199	imp 411	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ₀) ∧ ((𝑁 / 𝑃) gcd 𝑅) = 1) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
201	160, 198, 200	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
202	201	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)
203		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
204		simpr1 1211	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℤ)
205	204	peano2zd 12691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ ℤ)
206	23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205	aks6d1c1p2 42733	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
207	44	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑈 ∈ ℕ₀)
208	159, 46, 48	3jca 1144	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ))
209	168, 39	jca 520	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁))
210		rpdvds 16706	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) → (𝑅 gcd 𝑃) = 1)
211	208, 209, 210	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 gcd 𝑃) = 1)
212	159, 46	jca 520	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ))
213		gcdcom 16559	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
214	212, 213	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅))
215		eqeq1 2769	. . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . 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 42739	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃↑𝑈) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
221		2fveq3 6876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
222	221	oveq2d 7416	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
223	222	breq2d 5116	. . . . . . . . . . . . . . 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 42737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∼ 𝑋)
226	225, 81	breqtrrd 5132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (0_g‘𝑆)))
227	226, 90	breqtrrd 5132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
228	227	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
229		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑎 = 0)
230	229	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑎 = 0) → ((ℤRHom‘𝐾)‘𝑎) = ((ℤRHom‘𝐾)‘0))
231	230	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘0)))
232	231	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 = 0) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))
233	228, 232	breqtrrd 5132	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
234	233	ex 417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
235	234	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
236		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
237		1cnd 11190	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 1 ∈ ℂ)
238	237	addlidd 11399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (0 + 1) = 1)
239	238	oveq1d 7415	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((0 + 1)...𝐴) = (1...𝐴))
240	239	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . . 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 872	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
244	2, 3	jca 520	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
245		eluz1 12854	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ ℤ → (𝐴 ∈ (ℤ_≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)))
246	93, 245	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)))
247	244, 246	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
248	247	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 𝐴 ∈ (ℤ_≥‘0))
249		elfzp12 13619	. . . . . . . . . . . . . . . . . . . . . 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 417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))))
254	253	ralimdv2 3174	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))
255	224, 254	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
256	255	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))
257		0zd 12591	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ∈ ℤ)
258	2	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐴 ∈ ℤ)
259	204	zred 12688	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℝ)
260		1red 11197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 1 ∈ ℝ)
261		simpr2 1212	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 𝑗)
262		0le1 11725	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 1
263	262	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 1)
264	259, 260, 261, 263	addge0d 11778	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ (𝑗 + 1))
265		simpr3 1213	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 < 𝐴)
266	204, 258	zltp1led 12637	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴))
267	265, 266	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ≤ 𝐴)
268	257, 258, 205, 264, 267	elfzd 13531	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ (0...𝐴))
269	223, 256, 268	rspcdva 3585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
270		aks6d1c1.26	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾))
271	270	adantr 485	. . . . . . . . . . . . . 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 42734	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 / 𝑃) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
273	60	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐿 ∈ ℕ₀)
274	198	adantr 485	. . . . . . . . . . . . 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 42739	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃)↑𝐿) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
276	23, 24, 25, 26, 27, 28, 29, 30, 32, 33, 34, 152, 153, 154, 202, 156, 220, 275	aks6d1c1p5 42736	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
277	158, 276	eqbrtrd 5126	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
278	92	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐹:(0...𝐴)⟶ℕ₀)
279	278, 268	ffvelcdmd 7070	. . . . . . . . . 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 42738	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
281	101	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑊 ∈ Mnd)
282		ovexd 7435	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ V)
283	73	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑆 ∈ Mnd)
284	78	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑋 ∈ (Base‘𝑆))
285	75	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Ring)
286	114	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
287	286, 205	ffvelcdmd 7070	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾))
288	24, 30, 112, 76	ply1sclcl 22404	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
289	285, 287, 288	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆))
290	76, 34	mndcl 18788	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆))
291	283, 284, 289, 290	syl3anc 1394	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆))
292	291, 120	eleqtrdi 2875	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑊))
293	104, 31, 281, 279, 292	mulgnn0cld 19149	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊))
294		fveq2 6871	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1)))
295		2fveq3 6876	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))
296	295	oveq2d 7416	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))
297	294, 296	oveq12d 7418	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
298	104, 297	gsumsn 20012	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ (𝑗 + 1) ∈ V ∧ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊)) → (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
299	281, 282, 293, 298	syl3anc 1394	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))))
300	280, 299	breqtrrd 5132	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
301	300	3adant3 1148	. . . . . . 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 42735	. . . . . 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 7416	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))
306		eqid 2765	. . . . . . . 8 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
307	100	3ad2ant1 1149	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ CMnd)
308		simp21 1223	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℤ)
309		simp22 1224	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 0 ≤ 𝑗)
310	308, 309	jca 520	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
311		elnn0z 12592	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ₀ ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
312	310, 311	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℕ₀)
313	281	3adant3 1148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ Mnd)
314	313	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑊 ∈ Mnd)
315	92	3ad2ant1 1149	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐹:(0...𝐴)⟶ℕ₀)
316	315	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐹:(0...𝐴)⟶ℕ₀)
317		0zd 12591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ∈ ℤ)
318	2	3ad2ant1 1149	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐴 ∈ ℤ)
319	318	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℤ)
320		elfzelz 13540	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ∈ ℤ)
321	320	adantl 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℤ)
322		elfzle1 13543	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 0 ≤ 𝑘)
323	322	adantl 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ≤ 𝑘)
324	321	zred 12688	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℝ)
325	308	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℤ)
326	325	zred 12688	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℝ)
327		1red 11197	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 1 ∈ ℝ)
328	326, 327	readdcld 11226	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ∈ ℝ)
329	319	zred 12688	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℝ)
330		elfzle2 13544	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ≤ (𝑗 + 1))
331	330	adantl 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ (𝑗 + 1))
332		simpl23 1270	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 < 𝐴)
333	325, 319	zltp1led 12637	. . . . . . . . . . . . 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 11355	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ 𝐴)
336	317, 319, 321, 323, 335	elfzd 13531	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ (0...𝐴))
337	316, 336	ffvelcdmd 7070	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℕ₀)
338	283	3adant3 1148	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑆 ∈ Mnd)
339	338	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑆 ∈ Mnd)
340	284	3adant3 1148	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑋 ∈ (Base‘𝑆))
341	340	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑋 ∈ (Base‘𝑆))
342	285	3adant3 1148	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Ring)
343	342	adantr 485	. . . . . . . . . . . 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 7070	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾))
346	24, 30, 112, 76	ply1sclcl 22404	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆))
347	343, 345, 346	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆))
348	76, 34	mndcl 18788	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆))
349	339, 341, 347, 348	syl3anc 1394	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆))
350	349, 120	eleqtrdi 2875	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑊))
351	104, 31, 314, 337, 350	mulgnn0cld 19149	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) ∈ (Base‘𝑊))
352	104, 306, 307, 312, 351	gsummptfzsplit 19990	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σ_g (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝑊 Σ_g (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+_g‘𝑊)(𝑊 Σ_g (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))))
353	305, 352	eqtrd 2800	. . . . . 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 12686	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴)) → 𝐸 ∼ (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
356	355	ex 417	. . 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 780	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → 𝑔 = 𝐹)
361	360	fveq1d 6873	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → (𝑔‘𝑖) = (𝐹‘𝑖))
362	361	oveq1d 7415	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))
363	362	mpteq2dva 5197	. . . 4 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))
364	363	oveq2d 7416	. . 3 ⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
365		nn0ex 12498	. . . . . 6 ⊢ ℕ₀ ∈ V
366	365	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ₀ ∈ V)
367		ovexd 7435	. . . . 5 ⊢ (𝜑 → (0...𝐴) ∈ V)
368	366, 367	elmapd 8825	. . . 4 ⊢ (𝜑 → (𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)) ↔ 𝐹:(0...𝐴)⟶ℕ₀))
369	92, 368	mpbird 260	. . 3 ⊢ (𝜑 → 𝐹 ∈ (ℕ₀ ↑_m (0...𝐴)))
370		ovexd 7435	. . 3 ⊢ (𝜑 → (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ∈ V)
371	359, 364, 369, 370	fvmptd 6987	. 2 ⊢ (𝜑 → (𝐺‘𝐹) = (𝑊 Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))
372	357, 371	breqtrrd 5132	1 ⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∀wral 3079 Vcvv 3457 {csn 4585 class class class wbr 5104 {copab 5166 ↦ cmpt 5185 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ↑_m cmap 8812 0cc0 11088 1c1 11089 + caddc 11091 · cmul 11093 < clt 11231 ≤ cle 11232 / cdiv 11859 ℕcn 12221 ℕ₀cn0 12492 ℤcz 12579 ℤ_≥cuz 12850 ...cfz 13523 ↑cexp 14085 ∥ cdvds 16298 gcd cgcd 16540 ℙcprime 16717 Basecbs 17257 +_gcplusg 17298 0_gc0g 17480 Σ_g cgsu 17481 Mndcmnd 18780 ._gcmg 19121 CMndccmn 19838 mulGrpcmgp 20204 Ringcrg 20303 CRingccrg 20304 RingHom crh 20539 RingIso crs 20540 Fieldcfield 20802 ℤ_ringczring 21553 ℤRHomczrh 21606 chrcchr 21608 algSccascl 21959 var₁cv1 22293 Poly₁cpl1 22294 eval₁ce1 22431 PrimRoots cprimroots 42715

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166 ax-addf 11167 ax-mulf 11168

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5105 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 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7664 df-ofr 7665 df-om 7851 df-1st 7974 df-2nd 7975 df-supp 8145 df-tpos 8210 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-oadd 8445 df-er 8682 df-map 8814 df-pm 8815 df-ixp 8884 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fsupp 9310 df-sup 9390 df-inf 9391 df-oi 9460 df-dju 9875 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12222 df-2 12291 df-3 12292 df-4 12293 df-5 12294 df-6 12295 df-7 12296 df-8 12297 df-9 12298 df-n0 12493 df-xnn0 12566 df-z 12580 df-dec 12700 df-uz 12851 df-rp 13005 df-fz 13524 df-fzo 13671 df-fl 13813 df-mod 13891 df-seq 14026 df-exp 14086 df-fac 14298 df-bc 14327 df-hash 14355 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-dvds 16299 df-gcd 16541 df-prm 16718 df-phi 16813 df-struct 17195 df-sets 17212 df-slot 17230 df-ndx 17242 df-base 17258 df-ress 17279 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-0g 17482 df-gsum 17483 df-prds 17488 df-pws 17490 df-mre 17626 df-mrc 17627 df-acs 17629 df-mgm 18686 df-sgrp 18765 df-mnd 18781 df-mhm 18829 df-submnd 18830 df-grp 18991 df-minusg 18992 df-sbg 18993 df-mulg 19122 df-subg 19177 df-ghm 19272 df-cntz 19375 df-od 19586 df-cmn 19840 df-abl 19841 df-mgp 20205 df-rng 20219 df-ur 20252 df-srg 20257 df-ring 20305 df-cring 20306 df-oppr 20407 df-dvdsr 20427 df-unit 20428 df-invr 20458 df-dvr 20471 df-rhm 20542 df-rim 20543 df-subrng 20619 df-subrg 20643 df-drng 20803 df-field 20804 df-lmod 20949 df-lss 21019 df-lsp 21059 df-cnfld 21480 df-zring 21554 df-zrh 21610 df-chr 21612 df-assa 21960 df-asp 21961 df-ascl 21962 df-psr 22016 df-mvr 22017 df-mpl 22018 df-opsr 22020 df-evls 22182 df-evl 22183 df-psr1 22297 df-vr1 22298 df-ply1 22299 df-coe1 22300 df-evl1 22433 df-primroots 42716

This theorem is referenced by: aks6d1c1rh 42749

W3C validator