aks6d1c2lem4 - Mathbox for metakunt

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

Theorem aks6d1c2lem4 42084

Description: Claim 2 of Theorem 6.1 AKS, Preparation for injectivity proof. (Contributed by metakunt, 1-May-2025.)

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

**Assertion**
Ref	Expression
aks6d1c2lem4	⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ≤ (𝑁↑𝐵))

Distinct variable groups: ∼ ,𝑎 𝐴,𝑎 𝐴,𝑔,𝑖 𝐴,ℎ 𝐴,𝑘,𝑙 𝑥,𝐴 𝐵,𝑎 𝐵,𝑔,𝑖 𝐵,𝑘,𝑙 𝑥,𝐵 𝐸,𝑎 𝑔,𝐸,𝑖 𝑘,𝐸,𝑙 𝑥,𝐸 𝑒,𝐺,𝑓,𝑦 ℎ,𝐺 𝐼,𝑎 𝑔,𝐼,𝑖 𝑘,𝐼,𝑙 𝑥,𝐼 𝐽,𝑎 𝑔,𝐽,𝑖 𝑘,𝐽,𝑙 𝑥,𝐽 𝐾,𝑎 𝑒,𝐾,𝑓,𝑦 𝑔,𝐾,𝑖 ℎ,𝐾 𝑥,𝐾 ℎ,𝑀 𝑦,𝑀 𝑁,𝑎 𝑒,𝑁,𝑓,𝑦 𝑘,𝑁,𝑙 𝑥,𝑁 𝑃,𝑒,𝑓,𝑦 𝑃,𝑘,𝑙 𝑥,𝑃 𝑅,𝑒,𝑓,𝑦 𝑥,𝑅 𝜑,𝑎 𝜑,𝑔,𝑖 𝜑,ℎ 𝜑,𝑘,𝑙 𝜑,𝑥 Allowed substitution hints: 𝜑(𝑦,𝑒,𝑓) 𝐴(𝑦,𝑒,𝑓) 𝐵(𝑦,𝑒,𝑓,ℎ) 𝐶(𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑎,𝑙) 𝑃(𝑔,ℎ,𝑖,𝑎) ∼ (𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑙) 𝑅(𝑔,ℎ,𝑖,𝑘,𝑎,𝑙) 𝑆(𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑎,𝑙) 𝑈(𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑎,𝑙) 𝐸(𝑦,𝑒,𝑓,ℎ) ↑ (𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑎,𝑙) 𝐹(𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑎,𝑙) 𝐺(𝑥,𝑔,𝑖,𝑘,𝑎,𝑙) 𝐻(𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑎,𝑙) 𝐼(𝑦,𝑒,𝑓,ℎ) 𝐽(𝑦,𝑒,𝑓,ℎ) 𝐾(𝑘,𝑙) 𝐿(𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑎,𝑙) 𝑀(𝑥,𝑒,𝑓,𝑔,𝑖,𝑘,𝑎,𝑙) 𝑁(𝑔,ℎ,𝑖) 𝑋(𝑥,𝑦,𝑒,𝑓,𝑔,ℎ,𝑖,𝑘,𝑎,𝑙)

Proof of Theorem aks6d1c2lem4 Dummy variables 𝑜 𝑝 𝑞 𝑟 𝑠 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvexd 6935	. . . . . . . 8 ⊢ (𝜑 → ((eval₁‘𝐾)‘𝑆) ∈ V)
2		cnvexg 7964	. . . . . . . 8 ⊢ (((eval₁‘𝐾)‘𝑆) ∈ V → ^◡((eval₁‘𝐾)‘𝑆) ∈ V)
3	1, 2	syl 17	. . . . . . 7 ⊢ (𝜑 → ^◡((eval₁‘𝐾)‘𝑆) ∈ V)
4	3	imaexd 7956	. . . . . 6 ⊢ (𝜑 → (^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}) ∈ V)
5		nfv 1913	. . . . . . 7 ⊢ Ⅎ𝑠𝜑
6		fvexd 6935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ℎ ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) ∈ V)
7		aks6d1c2.17	. . . . . . . . . 10 ⊢ 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀))
8	6, 7	fmptd 7148	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:(ℕ₀ ↑_m (0...𝐴))⟶V)
9	8	ffnd 6748	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Fn (ℕ₀ ↑_m (0...𝐴)))
10	9	fnfund 6680	. . . . . . 7 ⊢ (𝜑 → Fun 𝐻)
11		aks6d1c2.25	. . . . . . . . . . . . 13 ⊢ 𝑆 = ((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋))
12	11	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑆 = ((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)))
13	12	fveq2d 6924	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((eval₁‘𝐾)‘𝑆) = ((eval₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋))))
14	13	fveq1d 6922	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) = (((eval₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)))‘(𝐻‘𝑠)))
15		eqid 2740	. . . . . . . . . . . . 13 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
16		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
17		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Base‘𝐾) = (Base‘𝐾)
18		eqid 2740	. . . . . . . . . . . . 13 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
19		aks6d1c2.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Field)
20	19	fldcrngd 20764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
21	20	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝐾 ∈ CRing)
22	7	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
23		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ ℎ = 𝑠) → ℎ = 𝑠)
24	23	fveq2d 6924	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ ℎ = 𝑠) → (𝐺‘ℎ) = (𝐺‘𝑠))
25	24	fveq2d 6924	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ ℎ = 𝑠) → ((eval₁‘𝐾)‘(𝐺‘ℎ)) = ((eval₁‘𝐾)‘(𝐺‘𝑠)))
26	25	fveq1d 6922	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ ℎ = 𝑠) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) = (((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀))
27		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)))
28		fvexd 6935	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀) ∈ V)
29	22, 26, 27, 28	fvmptd 7036	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐻‘𝑠) = (((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀))
30		aks6d1c2.16	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
31		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
32	31	crngmgp 20268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
33	20, 32	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
34		aks6d1c2.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑅 ∈ ℕ)
35	34	nnnn0d 12613	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
36		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
37	33, 35, 36	isprimroot 42050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
38	37	biimpd 229	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
39	30, 38	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣)))
40	39	simp1d 1142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
41	31, 17	mgpbas 20167	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
42	40, 41	eleqtrrdi 2855	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
43	42	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑀 ∈ (Base‘𝐾))
44		aks6d1c2.1	. . . . . . . . . . . . . . . . 17 ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly₁‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘𝑓)‘𝑦)) = (((eval₁‘𝐾)‘𝑓)‘(𝑒(._g‘(mulGrp‘𝐾))𝑦)))}
45		aks6d1c2.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑃 = (chr‘𝐾)
46	19	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝐾 ∈ Field)
47		aks6d1c2.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ ℙ)
48	47	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑃 ∈ ℙ)
49	34	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑅 ∈ ℕ)
50		aks6d1c2.6	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℕ)
51	50	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑁 ∈ ℕ)
52		aks6d1c2.7	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
53	52	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑃 ∥ 𝑁)
54		aks6d1c2.8	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
55	54	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝑁 gcd 𝑅) = 1)
56		elmapi 8907	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) → 𝑠:(0...𝐴)⟶ℕ₀)
57	56	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑠:(0...𝐴)⟶ℕ₀)
58		aks6d1c2.10	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ ((mulGrp‘(Poly₁‘𝐾)) Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(._g‘(mulGrp‘(Poly₁‘𝐾)))((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
59		aks6d1c2.11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
60	59	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝐴 ∈ ℕ₀)
61		0nn0 12568	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
62	61	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 0 ∈ ℕ₀)
63		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃↑0) · ((𝑁 / 𝑃)↑0)) = ((𝑃↑0) · ((𝑁 / 𝑃)↑0))
64		aks6d1c2.14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
65	64	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
66		aks6d1c2.15	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
67	66	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
68	44, 45, 46, 48, 49, 51, 53, 55, 57, 58, 60, 62, 62, 63, 65, 67	aks6d1c1rh 42082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((𝑃↑0) · ((𝑁 / 𝑃)↑0)) ∼ (𝐺‘𝑠))
69	44, 68	aks6d1c1p1rcl 42065	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((𝑃↑0) · ((𝑁 / 𝑃)↑0)) ∈ ℕ ∧ (𝐺‘𝑠) ∈ (Base‘(Poly₁‘𝐾))))
70	69	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐺‘𝑠) ∈ (Base‘(Poly₁‘𝐾)))
71	15, 16, 17, 18, 21, 43, 70	fveval1fvcl 22358	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀) ∈ (Base‘𝐾))
72	29, 71	eqeltrd 2844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐻‘𝑠) ∈ (Base‘𝐾))
73		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(mulGrp‘(Poly₁‘𝐾))) = (Base‘(mulGrp‘(Poly₁‘𝐾)))
74		aks6d1c2.23	. . . . . . . . . . . . . . . . 17 ⊢ ↑ = (._g‘(mulGrp‘(Poly₁‘𝐾)))
75	16	ply1crng 22221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
76	20, 75	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ CRing)
77		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (mulGrp‘(Poly₁‘𝐾)) = (mulGrp‘(Poly₁‘𝐾))
78	77	crngmgp 20268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ CRing → (mulGrp‘(Poly₁‘𝐾)) ∈ CMnd)
79	76, 78	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (mulGrp‘(Poly₁‘𝐾)) ∈ CMnd)
80	79	cmnmndd 19846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
81		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) → 𝐽 = (𝑟𝐸𝑜))
82		aks6d1c2.12	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)))
83	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))))
84		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ (𝑘 = 𝑟 ∧ 𝑙 = 𝑜)) → 𝑘 = 𝑟)
85	84	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ (𝑘 = 𝑟 ∧ 𝑙 = 𝑜)) → (𝑃↑𝑘) = (𝑃↑𝑟))
86		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ (𝑘 = 𝑟 ∧ 𝑙 = 𝑜)) → 𝑙 = 𝑜)
87	86	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ (𝑘 = 𝑟 ∧ 𝑙 = 𝑜)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑜))
88	85, 87	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ (𝑘 = 𝑟 ∧ 𝑙 = 𝑜)) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑟) · ((𝑁 / 𝑃)↑𝑜)))
89		fz0ssnn0 13679	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0...𝐵) ⊆ ℕ₀
90	89	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (0...𝐵) ⊆ ℕ₀)
91	90	sselda 4008	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 𝑟 ∈ ℕ₀)
92	91	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝑟 ∈ ℕ₀)
93	89	sseli 4004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑜 ∈ (0...𝐵) → 𝑜 ∈ ℕ₀)
94	93	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝑜 ∈ ℕ₀)
95		ovexd 7483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃↑𝑟) · ((𝑁 / 𝑃)↑𝑜)) ∈ V)
96	83, 88, 92, 94, 95	ovmpod 7602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑟𝐸𝑜) = ((𝑃↑𝑟) · ((𝑁 / 𝑃)↑𝑜)))
97		prmnn 16721	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
98	47, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑃 ∈ ℕ)
99	98	nnnn0d 12613	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
100	99	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 𝑃 ∈ ℕ₀)
101	100	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝑃 ∈ ℕ₀)
102	101, 92	nn0expcld 14295	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑃↑𝑟) ∈ ℕ₀)
103	99	nn0zd 12665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑃 ∈ ℤ)
104	98	nnne0d 12343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑃 ≠ 0)
105	50	nnnn0d 12613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
106	105	nn0zd 12665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑁 ∈ ℤ)
107		dvdsval2 16305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
108	103, 104, 106, 107	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
109	52, 108	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℤ)
110	50	nnred 12308	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℝ)
111	98	nnrpd 13097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑃 ∈ ℝ⁺)
112	105	nn0ge0d 12616	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 ≤ 𝑁)
113	110, 111, 112	divge0d 13139	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 0 ≤ (𝑁 / 𝑃))
114	109, 113	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 0 ≤ (𝑁 / 𝑃)))
115		elnn0z 12652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 / 𝑃) ∈ ℕ₀ ↔ ((𝑁 / 𝑃) ∈ ℤ ∧ 0 ≤ (𝑁 / 𝑃)))
116	114, 115	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℕ₀)
117	116	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → (𝑁 / 𝑃) ∈ ℕ₀)
118	117	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑁 / 𝑃) ∈ ℕ₀)
119	118, 94	nn0expcld 14295	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑁 / 𝑃)↑𝑜) ∈ ℕ₀)
120	102, 119	nn0mulcld 12618	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃↑𝑟) · ((𝑁 / 𝑃)↑𝑜)) ∈ ℕ₀)
121	96, 120	eqeltrd 2844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑟𝐸𝑜) ∈ ℕ₀)
122	121	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) → (𝑟𝐸𝑜) ∈ ℕ₀)
123	81, 122	eqeltrd 2844	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) → 𝐽 ∈ ℕ₀)
124		aks6d1c2.21	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ 𝐶)
125		aks6d1c2.19	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵)))
126	125	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵))))
127	124, 126	eleqtrd 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ (𝐸 “ ((0...𝐵) × (0...𝐵))))
128	50, 47, 52, 82	aks6d1c2p1 42075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸:(ℕ₀ × ℕ₀)⟶ℕ)
129	128	ffnd 6748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 Fn (ℕ₀ × ℕ₀))
130	90, 90	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((0...𝐵) ⊆ ℕ₀ ∧ (0...𝐵) ⊆ ℕ₀))
131		aks6d1c2.18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))))
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))))
133		aks6d1c2.13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
134		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
135	50, 47, 52, 34, 54, 82, 133, 134	hashscontpowcl 42077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ∈ ℕ₀)
136	135	nn0red 12614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ∈ ℝ)
137	135	nn0ge0d 12616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))
138	136, 137	resqrtcld 15466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))) ∈ ℝ)
139	138	flcld 13849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))) ∈ ℤ)
140	136, 137	sqrtge0d 15469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))))
141		0zd 12651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 0 ∈ ℤ)
142		flge 13856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))) ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))) ↔ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))))))
143	138, 141, 142	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))) ↔ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))))))
144	140, 143	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))))
145	139, 144	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))) ∈ ℤ ∧ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))))))
146		elnn0z 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))) ∈ ℕ₀ ↔ ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))) ∈ ℤ ∧ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))))))
147	145, 146	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))) ∈ ℕ₀)
148	132, 147	eqeltrd 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ∈ ℕ₀)
149		elnn0z 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐵 ∈ ℕ₀ ↔ (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵))
150	148, 149	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵))
151		0z 12650	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℤ
152		eluz1 12907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 ∈ ℤ → (𝐵 ∈ (ℤ_≥‘0) ↔ (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵)))
153	151, 152	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 ∈ (ℤ_≥‘0) ↔ (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵))
154	150, 153	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘0))
155		fzn0 13598	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0...𝐵) ≠ ∅ ↔ 𝐵 ∈ (ℤ_≥‘0))
156	154, 155	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (0...𝐵) ≠ ∅)
157	156, 156	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅))
158		xpnz 6190	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅) ↔ ((0...𝐵) × (0...𝐵)) ≠ ∅)
159	157, 158	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((0...𝐵) × (0...𝐵)) ≠ ∅)
160		ssxpb 6205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((0...𝐵) × (0...𝐵)) ≠ ∅ → (((0...𝐵) × (0...𝐵)) ⊆ (ℕ₀ × ℕ₀) ↔ ((0...𝐵) ⊆ ℕ₀ ∧ (0...𝐵) ⊆ ℕ₀)))
161	159, 160	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((0...𝐵) × (0...𝐵)) ⊆ (ℕ₀ × ℕ₀) ↔ ((0...𝐵) ⊆ ℕ₀ ∧ (0...𝐵) ⊆ ℕ₀)))
162	130, 161	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((0...𝐵) × (0...𝐵)) ⊆ (ℕ₀ × ℕ₀))
163		ovelimab 7628	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 Fn (ℕ₀ × ℕ₀) ∧ ((0...𝐵) × (0...𝐵)) ⊆ (ℕ₀ × ℕ₀)) → (𝐽 ∈ (𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ ∃𝑟 ∈ (0...𝐵)∃𝑜 ∈ (0...𝐵)𝐽 = (𝑟𝐸𝑜)))
164	129, 162, 163	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 ∈ (𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ ∃𝑟 ∈ (0...𝐵)∃𝑜 ∈ (0...𝐵)𝐽 = (𝑟𝐸𝑜)))
165	127, 164	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑟 ∈ (0...𝐵)∃𝑜 ∈ (0...𝐵)𝐽 = (𝑟𝐸𝑜))
166	123, 165	r19.29vva 3222	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
167	20	crngringd 20273	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Ring)
168		aks6d1c2.24	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑋 = (var₁‘𝐾)
169	168, 16, 18	vr1cl 22240	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ Ring → 𝑋 ∈ (Base‘(Poly₁‘𝐾)))
170	167, 169	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ (Base‘(Poly₁‘𝐾)))
171	77, 18	mgpbas 20167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(mulGrp‘(Poly₁‘𝐾)))
172	171	eqcomi 2749	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘(mulGrp‘(Poly₁‘𝐾))) = (Base‘(Poly₁‘𝐾))
173	172	eleq2i 2836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ (Base‘(mulGrp‘(Poly₁‘𝐾))) ↔ 𝑋 ∈ (Base‘(Poly₁‘𝐾)))
174	170, 173	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ (Base‘(mulGrp‘(Poly₁‘𝐾))))
175	73, 74, 80, 166, 174	mulgnn0cld 19135	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐽 ↑ 𝑋) ∈ (Base‘(mulGrp‘(Poly₁‘𝐾))))
176	175, 171	eleqtrrdi 2855	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐽 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)))
177	176	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐽 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)))
178	170	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝑋 ∈ (Base‘(Poly₁‘𝐾)))
179	15, 168, 17, 16, 18, 21, 72	evl1vard 22362	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝑋 ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘𝑋)‘(𝐻‘𝑠)) = (𝐻‘𝑠)))
180	179	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘𝑋)‘(𝐻‘𝑠)) = (𝐻‘𝑠))
181	178, 180	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝑋 ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘𝑋)‘(𝐻‘𝑠)) = (𝐻‘𝑠)))
182	166	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝐽 ∈ ℕ₀)
183	15, 16, 17, 18, 21, 72, 181, 74, 36, 182	evl1expd 22370	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((𝐽 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(𝐽 ↑ 𝑋))‘(𝐻‘𝑠)) = (𝐽(._g‘(mulGrp‘𝐾))(𝐻‘𝑠))))
184	183	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐽 ↑ 𝑋))‘(𝐻‘𝑠)) = (𝐽(._g‘(mulGrp‘𝐾))(𝐻‘𝑠)))
185	29	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐽(._g‘(mulGrp‘𝐾))(𝐻‘𝑠)) = (𝐽(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀)))
186	19	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐾 ∈ Field)
187	47	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑃 ∈ ℙ)
188	34	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑅 ∈ ℕ)
189	50	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑁 ∈ ℕ)
190	52	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑃 ∥ 𝑁)
191	54	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → (𝑁 gcd 𝑅) = 1)
192		aks6d1c2.9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ₀)
193	192	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐹:(0...𝐴)⟶ℕ₀)
194	59	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐴 ∈ ℕ₀)
195	64	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
196	66	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
197	30	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
198		aks6d1c2.20	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐼 ∈ 𝐶)
199	198	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐼 ∈ 𝐶)
200	124	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐽 ∈ 𝐶)
201		aks6d1c2.22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐼 < 𝐽)
202	201	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐼 < 𝐽)
203		aks6d1c2.26	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑈 ∈ ℕ)
204	203	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑈 ∈ ℕ)
205		aks6d1c2.27	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 = (𝐼 + (𝑈 · 𝑅)))
206	205	ad7antr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐽 = (𝐼 + (𝑈 · 𝑅)))
207	27	ad6antr 735	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)))
208		simp-6r 787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑟 ∈ (0...𝐵))
209		simp-5r 785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑜 ∈ (0...𝐵))
210		simp-4r 783	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐽 = (𝑟𝐸𝑜))
211		simpllr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑝 ∈ (0...𝐵))
212		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑞 ∈ (0...𝐵))
213		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐼 = (𝑝𝐸𝑞))
214		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐼 = (𝑝𝐸𝑞))
215	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))))
216		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) ∧ (𝑘 = 𝑝 ∧ 𝑙 = 𝑞)) → 𝑘 = 𝑝)
217	216	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) ∧ (𝑘 = 𝑝 ∧ 𝑙 = 𝑞)) → (𝑃↑𝑘) = (𝑃↑𝑝))
218		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) ∧ (𝑘 = 𝑝 ∧ 𝑙 = 𝑞)) → 𝑙 = 𝑞)
219	218	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) ∧ (𝑘 = 𝑝 ∧ 𝑙 = 𝑞)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑞))
220	217, 219	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) ∧ (𝑘 = 𝑝 ∧ 𝑙 = 𝑞)) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑝) · ((𝑁 / 𝑃)↑𝑞)))
221	90	sselda 4008	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑝 ∈ (0...𝐵)) → 𝑝 ∈ ℕ₀)
222	221	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) → 𝑝 ∈ ℕ₀)
223	222	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑝 ∈ ℕ₀)
224	89	sseli 4004	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑞 ∈ (0...𝐵) → 𝑞 ∈ ℕ₀)
225	224	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) → 𝑞 ∈ ℕ₀)
226	225	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑞 ∈ ℕ₀)
227		ovexd 7483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → ((𝑃↑𝑝) · ((𝑁 / 𝑃)↑𝑞)) ∈ V)
228	215, 220, 223, 226, 227	ovmpod 7602	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → (𝑝𝐸𝑞) = ((𝑃↑𝑝) · ((𝑁 / 𝑃)↑𝑞)))
229	214, 228	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐼 = ((𝑃↑𝑝) · ((𝑁 / 𝑃)↑𝑞)))
230	99	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝑃 ∈ ℕ₀)
231	230, 223	nn0expcld 14295	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → (𝑃↑𝑝) ∈ ℕ₀)
232	116	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) → (𝑁 / 𝑃) ∈ ℕ₀)
233	232	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → (𝑁 / 𝑃) ∈ ℕ₀)
234	233, 226	nn0expcld 14295	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → ((𝑁 / 𝑃)↑𝑞) ∈ ℕ₀)
235	231, 234	nn0mulcld 12618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → ((𝑃↑𝑝) · ((𝑁 / 𝑃)↑𝑞)) ∈ ℕ₀)
236	229, 235	eqeltrd 2844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐼 ∈ ℕ₀)
237	198, 126	eleqtrd 2846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐼 ∈ (𝐸 “ ((0...𝐵) × (0...𝐵))))
238		ovelimab 7628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐸 Fn (ℕ₀ × ℕ₀) ∧ ((0...𝐵) × (0...𝐵)) ⊆ (ℕ₀ × ℕ₀)) → (𝐼 ∈ (𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ ∃𝑝 ∈ (0...𝐵)∃𝑞 ∈ (0...𝐵)𝐼 = (𝑝𝐸𝑞)))
239	129, 162, 238	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐼 ∈ (𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ ∃𝑝 ∈ (0...𝐵)∃𝑞 ∈ (0...𝐵)𝐼 = (𝑝𝐸𝑞)))
240	237, 239	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∃𝑝 ∈ (0...𝐵)∃𝑞 ∈ (0...𝐵)𝐼 = (𝑝𝐸𝑞))
241	236, 240	r19.29vva 3222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐼 ∈ ℕ₀)
242	241	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝐼 ∈ ℕ₀)
243	242	ad6antr 735	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → 𝐼 ∈ ℕ₀)
244	44, 45, 186, 187, 188, 189, 190, 191, 193, 58, 194, 82, 133, 195, 196, 197, 7, 131, 125, 199, 200, 202, 74, 168, 11, 204, 206, 207, 208, 209, 210, 211, 212, 213, 243	aks6d1c2lem3 42083	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) ∧ 𝑝 ∈ (0...𝐵)) ∧ 𝑞 ∈ (0...𝐵)) ∧ 𝐼 = (𝑝𝐸𝑞)) → (𝐽(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀)) = (𝐼(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀)))
245	240	ad4antr 731	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) → ∃𝑝 ∈ (0...𝐵)∃𝑞 ∈ (0...𝐵)𝐼 = (𝑝𝐸𝑞))
246	244, 245	r19.29vva 3222	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) → (𝐽(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀)) = (𝐼(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀)))
247	165	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ∃𝑟 ∈ (0...𝐵)∃𝑜 ∈ (0...𝐵)𝐽 = (𝑟𝐸𝑜))
248	246, 247	r19.29vva 3222	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐽(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀)) = (𝐼(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀)))
249	29	eqcomd 2746	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀) = (𝐻‘𝑠))
250	249	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐼(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘(𝐺‘𝑠))‘𝑀)) = (𝐼(._g‘(mulGrp‘𝐾))(𝐻‘𝑠)))
251	185, 248, 250	3eqtrd 2784	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐽(._g‘(mulGrp‘𝐾))(𝐻‘𝑠)) = (𝐼(._g‘(mulGrp‘𝐾))(𝐻‘𝑠)))
252	15, 16, 17, 18, 21, 72, 181, 74, 36, 242	evl1expd 22370	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((𝐼 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)) = (𝐼(._g‘(mulGrp‘𝐾))(𝐻‘𝑠))))
253	252	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)) = (𝐼(._g‘(mulGrp‘𝐾))(𝐻‘𝑠)))
254	253	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐼(._g‘(mulGrp‘𝐾))(𝐻‘𝑠)) = (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)))
255	184, 251, 254	3eqtrd 2784	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐽 ↑ 𝑋))‘(𝐻‘𝑠)) = (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)))
256	177, 255	jca 511	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((𝐽 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(𝐽 ↑ 𝑋))‘(𝐻‘𝑠)) = (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))))
257	73, 74, 80, 241, 174	mulgnn0cld 19135	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 ↑ 𝑋) ∈ (Base‘(mulGrp‘(Poly₁‘𝐾))))
258	171	eleq2i 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)) ↔ (𝐼 ↑ 𝑋) ∈ (Base‘(mulGrp‘(Poly₁‘𝐾))))
259	257, 258	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)))
260	259	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐼 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)))
261		eqidd 2741	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)) = (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)))
262	260, 261	jca 511	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((𝐼 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)) = (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))))
263		eqid 2740	. . . . . . . . . . . . 13 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
264		eqid 2740	. . . . . . . . . . . . 13 ⊢ (-_g‘𝐾) = (-_g‘𝐾)
265	15, 16, 17, 18, 21, 72, 256, 262, 263, 264	evl1subd 22367	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)))‘(𝐻‘𝑠)) = ((((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))(-_g‘𝐾)(((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)))))
266	265	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)))‘(𝐻‘𝑠)) = ((((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))(-_g‘𝐾)(((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))))
267	21	crnggrpd 20274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → 𝐾 ∈ Grp)
268	15, 16, 17, 18, 21, 72, 260	fveval1fvcl 22358	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)) ∈ (Base‘𝐾))
269		eqid 2740	. . . . . . . . . . . . 13 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
270	17, 269, 264	grpsubid 19064	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Grp ∧ (((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠)) ∈ (Base‘𝐾)) → ((((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))(-_g‘𝐾)(((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))) = (0_g‘𝐾))
271	267, 268, 270	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))(-_g‘𝐾)(((eval₁‘𝐾)‘(𝐼 ↑ 𝑋))‘(𝐻‘𝑠))) = (0_g‘𝐾))
272	266, 271	eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)))‘(𝐻‘𝑠)) = (0_g‘𝐾))
273	14, 272	eqtrd 2780	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) = (0_g‘𝐾))
274		fvexd 6935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) ∈ V)
275		elsng 4662	. . . . . . . . . 10 ⊢ ((((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) ∈ V → ((((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) ∈ {(0_g‘𝐾)} ↔ (((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) = (0_g‘𝐾)))
276	274, 275	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) ∈ {(0_g‘𝐾)} ↔ (((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) = (0_g‘𝐾)))
277	273, 276	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) ∈ {(0_g‘𝐾)})
278	76	crnggrpd 20274	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Grp)
279	18, 263	grpsubcl 19060	. . . . . . . . . . . . . . . . 17 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐽 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐼 ↑ 𝑋) ∈ (Base‘(Poly₁‘𝐾))) → ((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)) ∈ (Base‘(Poly₁‘𝐾)))
280	278, 176, 259, 279	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)) ∈ (Base‘(Poly₁‘𝐾)))
281	11, 280	eqeltrid 2848	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (Base‘(Poly₁‘𝐾)))
282		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ↑_s (Base‘𝐾)) = (𝐾 ↑_s (Base‘𝐾))
283	15, 16, 282, 17	evl1rhm 22357	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (eval₁‘𝐾) ∈ ((Poly₁‘𝐾) RingHom (𝐾 ↑_s (Base‘𝐾))))
284	20, 283	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (eval₁‘𝐾) ∈ ((Poly₁‘𝐾) RingHom (𝐾 ↑_s (Base‘𝐾))))
285		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘(𝐾 ↑_s (Base‘𝐾))) = (Base‘(𝐾 ↑_s (Base‘𝐾)))
286	18, 285	rhmf 20511	. . . . . . . . . . . . . . . . . 18 ⊢ ((eval₁‘𝐾) ∈ ((Poly₁‘𝐾) RingHom (𝐾 ↑_s (Base‘𝐾))) → (eval₁‘𝐾):(Base‘(Poly₁‘𝐾))⟶(Base‘(𝐾 ↑_s (Base‘𝐾))))
287	284, 286	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (eval₁‘𝐾):(Base‘(Poly₁‘𝐾))⟶(Base‘(𝐾 ↑_s (Base‘𝐾))))
288	287	ffvelcdmda 7118	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 ∈ (Base‘(Poly₁‘𝐾))) → ((eval₁‘𝐾)‘𝑆) ∈ (Base‘(𝐾 ↑_s (Base‘𝐾))))
289	288	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ∈ (Base‘(Poly₁‘𝐾)) → ((eval₁‘𝐾)‘𝑆) ∈ (Base‘(𝐾 ↑_s (Base‘𝐾)))))
290	281, 289	mpd 15	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((eval₁‘𝐾)‘𝑆) ∈ (Base‘(𝐾 ↑_s (Base‘𝐾))))
291		fvexd 6935	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘𝐾) ∈ V)
292	282, 17	pwsbas 17547	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Field ∧ (Base‘𝐾) ∈ V) → ((Base‘𝐾) ↑_m (Base‘𝐾)) = (Base‘(𝐾 ↑_s (Base‘𝐾))))
293	19, 291, 292	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((Base‘𝐾) ↑_m (Base‘𝐾)) = (Base‘(𝐾 ↑_s (Base‘𝐾))))
294	290, 293	eleqtrrd 2847	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((eval₁‘𝐾)‘𝑆) ∈ ((Base‘𝐾) ↑_m (Base‘𝐾)))
295	291, 291	elmapd 8898	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((eval₁‘𝐾)‘𝑆) ∈ ((Base‘𝐾) ↑_m (Base‘𝐾)) ↔ ((eval₁‘𝐾)‘𝑆):(Base‘𝐾)⟶(Base‘𝐾)))
296	294, 295	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → ((eval₁‘𝐾)‘𝑆):(Base‘𝐾)⟶(Base‘𝐾))
297		ffn 6747	. . . . . . . . . . . 12 ⊢ (((eval₁‘𝐾)‘𝑆):(Base‘𝐾)⟶(Base‘𝐾) → ((eval₁‘𝐾)‘𝑆) Fn (Base‘𝐾))
298	296, 297	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((eval₁‘𝐾)‘𝑆) Fn (Base‘𝐾))
299	298	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((eval₁‘𝐾)‘𝑆) Fn (Base‘𝐾))
300		fnfun 6679	. . . . . . . . . 10 ⊢ (((eval₁‘𝐾)‘𝑆) Fn (Base‘𝐾) → Fun ((eval₁‘𝐾)‘𝑆))
301	299, 300	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → Fun ((eval₁‘𝐾)‘𝑆))
302		fndm 6682	. . . . . . . . . . . 12 ⊢ (((eval₁‘𝐾)‘𝑆) Fn (Base‘𝐾) → dom ((eval₁‘𝐾)‘𝑆) = (Base‘𝐾))
303	298, 302	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom ((eval₁‘𝐾)‘𝑆) = (Base‘𝐾))
304	303	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → dom ((eval₁‘𝐾)‘𝑆) = (Base‘𝐾))
305	72, 304	eleqtrrd 2847	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐻‘𝑠) ∈ dom ((eval₁‘𝐾)‘𝑆))
306		fvimacnv 7086	. . . . . . . . 9 ⊢ ((Fun ((eval₁‘𝐾)‘𝑆) ∧ (𝐻‘𝑠) ∈ dom ((eval₁‘𝐾)‘𝑆)) → ((((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) ∈ {(0_g‘𝐾)} ↔ (𝐻‘𝑠) ∈ (^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})))
307	301, 305, 306	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → ((((eval₁‘𝐾)‘𝑆)‘(𝐻‘𝑠)) ∈ {(0_g‘𝐾)} ↔ (𝐻‘𝑠) ∈ (^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})))
308	277, 307	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝐻‘𝑠) ∈ (^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}))
309	5, 10, 308	funimassd 6988	. . . . . 6 ⊢ (𝜑 → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ⊆ (^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}))
310	4, 309	ssexd 5342	. . . . 5 ⊢ (𝜑 → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V)
311	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 = ((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋)))
312	311	fveq2d 6924	. . . . . . . . . 10 ⊢ (𝜑 → ((deg₁‘𝐾)‘𝑆) = ((deg₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋))))
313		eqid 2740	. . . . . . . . . . 11 ⊢ (deg₁‘𝐾) = (deg₁‘𝐾)
314		isfld 20762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field ↔ (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing))
315	314	biimpi 216	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Field → (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing))
316	315	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Field → 𝐾 ∈ DivRing)
317		drngnzr 20770	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
318	316, 317	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Field → 𝐾 ∈ NzRing)
319	19, 318	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ NzRing)
320	313, 16, 168, 77, 74	deg1pw 26180	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ NzRing ∧ 𝐼 ∈ ℕ₀) → ((deg₁‘𝐾)‘(𝐼 ↑ 𝑋)) = 𝐼)
321	319, 241, 320	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg₁‘𝐾)‘(𝐼 ↑ 𝑋)) = 𝐼)
322	321	eqcomd 2746	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 = ((deg₁‘𝐾)‘(𝐼 ↑ 𝑋)))
323	313, 16, 168, 77, 74	deg1pw 26180	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ NzRing ∧ 𝐽 ∈ ℕ₀) → ((deg₁‘𝐾)‘(𝐽 ↑ 𝑋)) = 𝐽)
324	319, 166, 323	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg₁‘𝐾)‘(𝐽 ↑ 𝑋)) = 𝐽)
325	324	eqcomd 2746	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 = ((deg₁‘𝐾)‘(𝐽 ↑ 𝑋)))
326	201, 322, 325	3brtr3d 5197	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg₁‘𝐾)‘(𝐼 ↑ 𝑋)) < ((deg₁‘𝐾)‘(𝐽 ↑ 𝑋)))
327	16, 313, 167, 18, 263, 176, 259, 326	deg1sub 26167	. . . . . . . . . 10 ⊢ (𝜑 → ((deg₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋))) = ((deg₁‘𝐾)‘(𝐽 ↑ 𝑋)))
328	312, 327	eqtrd 2780	. . . . . . . . 9 ⊢ (𝜑 → ((deg₁‘𝐾)‘𝑆) = ((deg₁‘𝐾)‘(𝐽 ↑ 𝑋)))
329	328, 324	eqtrd 2780	. . . . . . . 8 ⊢ (𝜑 → ((deg₁‘𝐾)‘𝑆) = 𝐽)
330	329, 166	eqeltrd 2844	. . . . . . 7 ⊢ (𝜑 → ((deg₁‘𝐾)‘𝑆) ∈ ℕ₀)
331		eqid 2740	. . . . . . . 8 ⊢ (0_g‘(Poly₁‘𝐾)) = (0_g‘(Poly₁‘𝐾))
332		fldidom 20793	. . . . . . . . 9 ⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn)
333	19, 332	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ IDomn)
334	313, 16, 331, 18	deg1nn0clb 26149	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Ring ∧ 𝑆 ∈ (Base‘(Poly₁‘𝐾))) → (𝑆 ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘𝑆) ∈ ℕ₀))
335	167, 281, 334	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘𝑆) ∈ ℕ₀))
336	330, 335	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ≠ (0_g‘(Poly₁‘𝐾)))
337	16, 18, 313, 15, 269, 331, 333, 281, 336	fta1g 26229	. . . . . . 7 ⊢ (𝜑 → (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘𝑆))
338		hashbnd 14385	. . . . . . 7 ⊢ (((^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}) ∈ V ∧ ((deg₁‘𝐾)‘𝑆) ∈ ℕ₀ ∧ (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘𝑆)) → (^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}) ∈ Fin)
339	4, 330, 337, 338	syl3anc 1371	. . . . . 6 ⊢ (𝜑 → (^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}) ∈ Fin)
340		hashcl 14405	. . . . . 6 ⊢ ((^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}) ∈ Fin → (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})) ∈ ℕ₀)
341	339, 340	syl 17	. . . . 5 ⊢ (𝜑 → (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})) ∈ ℕ₀)
342		hashss 14458	. . . . . 6 ⊢ (((^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}) ∈ V ∧ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ⊆ (^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})) → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ≤ (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})))
343	4, 309, 342	syl2anc 583	. . . . 5 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ≤ (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})))
344		hashbnd 14385	. . . . 5 ⊢ (((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V ∧ (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})) ∈ ℕ₀ ∧ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ≤ (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)}))) → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ Fin)
345	310, 341, 343, 344	syl3anc 1371	. . . 4 ⊢ (𝜑 → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ Fin)
346		hashcl 14405	. . . 4 ⊢ ((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ Fin → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀)
347	345, 346	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀)
348	347	nn0red 12614	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ)
349	341	nn0red 12614	. 2 ⊢ (𝜑 → (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})) ∈ ℝ)
350	105, 148	nn0expcld 14295	. . 3 ⊢ (𝜑 → (𝑁↑𝐵) ∈ ℕ₀)
351	350	nn0red 12614	. 2 ⊢ (𝜑 → (𝑁↑𝐵) ∈ ℝ)
352	166	nn0red 12614	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ ℝ)
353	324, 352	eqeltrd 2844	. . . . 5 ⊢ (𝜑 → ((deg₁‘𝐾)‘(𝐽 ↑ 𝑋)) ∈ ℝ)
354	327, 353	eqeltrd 2844	. . . 4 ⊢ (𝜑 → ((deg₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋))) ∈ ℝ)
355	312, 354	eqeltrd 2844	. . 3 ⊢ (𝜑 → ((deg₁‘𝐾)‘𝑆) ∈ ℝ)
356	97	nnred 12308	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
357	47, 356	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℝ)
358	357	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 𝑃 ∈ ℝ)
359	358	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝑃 ∈ ℝ)
360	359, 92	reexpcld 14213	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑃↑𝑟) ∈ ℝ)
361	110, 357, 104	redivcld 12122	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℝ)
362	361	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → (𝑁 / 𝑃) ∈ ℝ)
363	362	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑁 / 𝑃) ∈ ℝ)
364	363, 94	reexpcld 14213	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑁 / 𝑃)↑𝑜) ∈ ℝ)
365	360, 364	remulcld 11320	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃↑𝑟) · ((𝑁 / 𝑃)↑𝑜)) ∈ ℝ)
366	357, 148	reexpcld 14213	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃↑𝐵) ∈ ℝ)
367	366	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → (𝑃↑𝐵) ∈ ℝ)
368	361, 148	reexpcld 14213	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 𝑃)↑𝐵) ∈ ℝ)
369	368	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → ((𝑁 / 𝑃)↑𝐵) ∈ ℝ)
370	367, 369	remulcld 11320	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → ((𝑃↑𝐵) · ((𝑁 / 𝑃)↑𝐵)) ∈ ℝ)
371	370	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃↑𝐵) · ((𝑁 / 𝑃)↑𝐵)) ∈ ℝ)
372	110, 148	reexpcld 14213	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁↑𝐵) ∈ ℝ)
373	372	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → (𝑁↑𝐵) ∈ ℝ)
374	373	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑁↑𝐵) ∈ ℝ)
375	367	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑃↑𝐵) ∈ ℝ)
376	369	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑁 / 𝑃)↑𝐵) ∈ ℝ)
377		0red 11293	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℝ)
378		1red 11291	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ)
379		0le1 11813	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 1
380	379	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ 1)
381		prmgt1 16744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
382	47, 381	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 < 𝑃)
383	378, 357, 382	ltled 11438	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ 𝑃)
384	377, 378, 357, 380, 383	letrd 11447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ≤ 𝑃)
385	384	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 0 ≤ 𝑃)
386	385	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 0 ≤ 𝑃)
387	359, 92, 386	expge0d 14214	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 0 ≤ (𝑃↑𝑟))
388	113	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 0 ≤ (𝑁 / 𝑃))
389	388	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 0 ≤ (𝑁 / 𝑃))
390	363, 94, 389	expge0d 14214	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 0 ≤ ((𝑁 / 𝑃)↑𝑜))
391	98	nnge1d 12341	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ≤ 𝑃)
392	391	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 1 ≤ 𝑃)
393	392	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 1 ≤ 𝑃)
394		elfzuz3 13581	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ (0...𝐵) → 𝐵 ∈ (ℤ_≥‘𝑟))
395	394	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 𝐵 ∈ (ℤ_≥‘𝑟))
396	395	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝐵 ∈ (ℤ_≥‘𝑟))
397	359, 393, 396	leexp2ad 14303	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑃↑𝑟) ≤ (𝑃↑𝐵))
398	357	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℂ)
399	398	mullidd 11308	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 · 𝑃) = 𝑃)
400	98	nnzd 12666	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ ℤ)
401		dvdsle 16358	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑃 ∥ 𝑁 → 𝑃 ≤ 𝑁))
402	400, 50, 401	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 ∥ 𝑁 → 𝑃 ≤ 𝑁))
403	52, 402	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ≤ 𝑁)
404	399, 403	eqbrtrd 5188	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · 𝑃) ≤ 𝑁)
405	378, 110, 111	lemuldivd 13148	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 · 𝑃) ≤ 𝑁 ↔ 1 ≤ (𝑁 / 𝑃)))
406	404, 405	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ≤ (𝑁 / 𝑃))
407	406	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 1 ≤ (𝑁 / 𝑃))
408	407	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 1 ≤ (𝑁 / 𝑃))
409		elfzuz3 13581	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∈ (0...𝐵) → 𝐵 ∈ (ℤ_≥‘𝑜))
410	409	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝐵 ∈ (ℤ_≥‘𝑜))
411	363, 408, 410	leexp2ad 14303	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑁 / 𝑃)↑𝑜) ≤ ((𝑁 / 𝑃)↑𝐵))
412	360, 375, 364, 376, 387, 390, 397, 411	lemul12ad 12237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃↑𝑟) · ((𝑁 / 𝑃)↑𝑜)) ≤ ((𝑃↑𝐵) · ((𝑁 / 𝑃)↑𝐵)))
413	110	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℂ)
414	413, 398, 104	divcan2d 12072	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 · (𝑁 / 𝑃)) = 𝑁)
415	414	eqcomd 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 = (𝑃 · (𝑁 / 𝑃)))
416	415	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ (0...𝐵)) → 𝑁 = (𝑃 · (𝑁 / 𝑃)))
417	416	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝑁 = (𝑃 · (𝑁 / 𝑃)))
418	417	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑁↑𝐵) = ((𝑃 · (𝑁 / 𝑃))↑𝐵))
419	359	recnd 11318	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝑃 ∈ ℂ)
420	363	recnd 11318	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑁 / 𝑃) ∈ ℂ)
421	148	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → 𝐵 ∈ ℕ₀)
422	419, 420, 421	mulexpd 14211	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃 · (𝑁 / 𝑃))↑𝐵) = ((𝑃↑𝐵) · ((𝑁 / 𝑃)↑𝐵)))
423	418, 422	eqtr2d 2781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃↑𝐵) · ((𝑁 / 𝑃)↑𝐵)) = (𝑁↑𝐵))
424	374	leidd 11856	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑁↑𝐵) ≤ (𝑁↑𝐵))
425	423, 424	eqbrtrd 5188	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃↑𝐵) · ((𝑁 / 𝑃)↑𝐵)) ≤ (𝑁↑𝐵))
426	365, 371, 374, 412, 425	letrd 11447	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → ((𝑃↑𝑟) · ((𝑁 / 𝑃)↑𝑜)) ≤ (𝑁↑𝐵))
427	96, 426	eqbrtrd 5188	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) → (𝑟𝐸𝑜) ≤ (𝑁↑𝐵))
428	427	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) → (𝑟𝐸𝑜) ≤ (𝑁↑𝐵))
429	81, 428	eqbrtrd 5188	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0...𝐵)) ∧ 𝑜 ∈ (0...𝐵)) ∧ 𝐽 = (𝑟𝐸𝑜)) → 𝐽 ≤ (𝑁↑𝐵))
430	429, 165	r19.29vva 3222	. . . . . 6 ⊢ (𝜑 → 𝐽 ≤ (𝑁↑𝐵))
431	324, 430	eqbrtrd 5188	. . . . 5 ⊢ (𝜑 → ((deg₁‘𝐾)‘(𝐽 ↑ 𝑋)) ≤ (𝑁↑𝐵))
432	327, 431	eqbrtrd 5188	. . . 4 ⊢ (𝜑 → ((deg₁‘𝐾)‘((𝐽 ↑ 𝑋)(-_g‘(Poly₁‘𝐾))(𝐼 ↑ 𝑋))) ≤ (𝑁↑𝐵))
433	312, 432	eqbrtrd 5188	. . 3 ⊢ (𝜑 → ((deg₁‘𝐾)‘𝑆) ≤ (𝑁↑𝐵))
434	349, 355, 351, 337, 433	letrd 11447	. 2 ⊢ (𝜑 → (♯‘(^◡((eval₁‘𝐾)‘𝑆) “ {(0_g‘𝐾)})) ≤ (𝑁↑𝐵))
435	348, 349, 351, 343, 434	letrd 11447	1 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ≤ (𝑁↑𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 Vcvv 3488 ⊆ wss 3976 ∅c0 4352 {csn 4648 class class class wbr 5166 {copab 5228 ↦ cmpt 5249 × cxp 5698 ^◡ccnv 5699 dom cdm 5700 “ cima 5703 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 ∈ cmpo 7450 ↑_m cmap 8884 Fincfn 9003 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 < clt 11324 ≤ cle 11325 / cdiv 11947 ℕcn 12293 ℕ₀cn0 12553 ℤcz 12639 ℤ_≥cuz 12903 ...cfz 13567 ⌊cfl 13841 ↑cexp 14112 ♯chash 14379 √csqrt 15282 ∥ cdvds 16302 gcd cgcd 16540 ℙcprime 16718 Basecbs 17258 +_gcplusg 17311 0_gc0g 17499 Σ_g cgsu 17500 ↑_s cpws 17506 Grpcgrp 18973 -_gcsg 18975 ._gcmg 19107 CMndccmn 19822 mulGrpcmgp 20161 Ringcrg 20260 CRingccrg 20261 RingHom crh 20495 RingIso crs 20496 NzRingcnzr 20538 IDomncidom 20715 DivRingcdr 20751 Fieldcfield 20752 ℤRHomczrh 21533 chrcchr 21535 ℤ/nℤczn 21536 algSccascl 21895 var₁cv1 22198 Poly₁cpl1 22199 eval₁ce1 22339 deg₁cdg1 26113 PrimRoots cprimroots 42048

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262 ax-addf 11263 ax-mulf 11264

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-ofr 7715 df-om 7904 df-1st 8030 df-2nd 8031 df-supp 8202 df-tpos 8267 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-oadd 8526 df-er 8763 df-ec 8765 df-qs 8769 df-map 8886 df-pm 8887 df-ixp 8956 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fsupp 9432 df-sup 9511 df-inf 9512 df-oi 9579 df-dju 9970 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-xnn0 12626 df-z 12640 df-dec 12759 df-uz 12904 df-rp 13058 df-fz 13568 df-fzo 13712 df-fl 13843 df-mod 13921 df-seq 14053 df-exp 14113 df-fac 14323 df-bc 14352 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-dvds 16303 df-gcd 16541 df-prm 16719 df-phi 16813 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-hom 17335 df-cco 17336 df-0g 17501 df-gsum 17502 df-prds 17507 df-pws 17509 df-imas 17568 df-qus 17569 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-mhm 18818 df-submnd 18819 df-grp 18976 df-minusg 18977 df-sbg 18978 df-mulg 19108 df-subg 19163 df-nsg 19164 df-eqg 19165 df-ghm 19253 df-cntz 19357 df-od 19570 df-cmn 19824 df-abl 19825 df-mgp 20162 df-rng 20180 df-ur 20209 df-srg 20214 df-ring 20262 df-cring 20263 df-oppr 20360 df-dvdsr 20383 df-unit 20384 df-invr 20414 df-dvr 20427 df-rhm 20498 df-rim 20499 df-nzr 20539 df-subrng 20572 df-subrg 20597 df-rlreg 20716 df-domn 20717 df-idom 20718 df-drng 20753 df-field 20754 df-lmod 20882 df-lss 20953 df-lsp 20993 df-sra 21195 df-rgmod 21196 df-lidl 21241 df-rsp 21242 df-2idl 21283 df-cnfld 21388 df-zring 21481 df-zrh 21537 df-chr 21539 df-zn 21540 df-assa 21896 df-asp 21897 df-ascl 21898 df-psr 21952 df-mvr 21953 df-mpl 21954 df-opsr 21956 df-evls 22121 df-evl 22122 df-psr1 22202 df-vr1 22203 df-ply1 22204 df-coe1 22205 df-evl1 22341 df-mdeg 26114 df-deg1 26115 df-mon1 26190 df-uc1p 26191 df-q1p 26192 df-r1p 26193 df-primroots 42049

This theorem is referenced by: aks6d1c2 42087

W3C validator