aks6d1c6lem3 - Mathbox for metakunt

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

Theorem aks6d1c6lem3 42129

Description: Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf TODO, eliminate hypothesis. (Contributed by metakunt, 8-May-2025.)

**Hypotheses**
Ref	Expression
aks6d1c6.1	⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly₁‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘𝑓)‘𝑦)) = (((eval₁‘𝐾)‘𝑓)‘(𝑒(._g‘(mulGrp‘𝐾))𝑦)))}
aks6d1c6.2	⊢ 𝑃 = (chr‘𝐾)
aks6d1c6.3	⊢ (𝜑 → 𝐾 ∈ Field)
aks6d1c6.4	⊢ (𝜑 → 𝑃 ∈ ℙ)
aks6d1c6.5	⊢ (𝜑 → 𝑅 ∈ ℕ)
aks6d1c6.6	⊢ (𝜑 → 𝑁 ∈ ℕ)
aks6d1c6.7	⊢ (𝜑 → 𝑃 ∥ 𝑁)
aks6d1c6.8	⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
aks6d1c6.9	⊢ (𝜑 → 𝐴 < 𝑃)
aks6d1c6.10	⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ ((mulGrp‘(Poly₁‘𝐾)) Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(._g‘(mulGrp‘(Poly₁‘𝐾)))((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
aks6d1c6.11	⊢ (𝜑 → 𝐴 ∈ ℕ₀)
aks6d1c6.12	⊢ 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)))
aks6d1c6.13	⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
aks6d1c6.14	⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
aks6d1c6.15	⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
aks6d1c6.16	⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
aks6d1c6.17	⊢ 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀))
aks6d1c6.18	⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))
aks6d1c6.19	⊢ 𝑆 = {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)}
aks6d1c6lem3.1	⊢ 𝐽 = (𝑗 ∈ (ℕ₀ × ℕ₀) ↦ ((𝐸‘𝑗)(._g‘(mulGrp‘𝐾))𝑀))
aks6d1c6lem3.2	⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))

**Assertion**
Ref	Expression
aks6d1c6lem3	⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))

Distinct variable groups: 𝐴,𝑔,𝑖 𝐴,ℎ,𝑗 𝐴,𝑠,𝑡 𝐷,𝑠 𝑥,𝐸,𝑦 𝑔,𝐺,𝑖 ℎ,𝐺 𝑡,𝐺,𝑖 𝑔,𝐻,𝑖,𝑥,𝑦 𝑗,𝐻 𝑡,𝐻,𝑥,𝑦 𝑔,𝐾,𝑖 ℎ,𝐾,𝑗 𝑡,𝐾 ℎ,𝑀 𝑘,𝑁,𝑙 𝑃,𝑘,𝑙 𝑆,𝑔,𝑖,𝑥,𝑦 𝑆,ℎ,𝑗 𝑡,𝑆 𝜑,𝑔,𝑖,𝑥,𝑦 𝜑,ℎ,𝑗 𝜑,𝑘,𝑥,𝑦,𝑙 𝜑,𝑠,𝑡 ∼ ,𝑎 𝐴,𝑎 𝑥,𝐴 𝑒,𝐸,𝑓,𝑦 𝑗,𝐸 𝑒,𝐺,𝑓,𝑦 𝐻,𝑎 ℎ,𝐻 𝐻,𝑠 𝐾,𝑎 𝑒,𝐾,𝑓,𝑦 𝑥,𝐾 𝑗,𝑀 𝑦,𝑀 𝑁,𝑎 𝑒,𝑁,𝑓 𝑁,𝑠,𝑘,𝑙 𝑥,𝑁 𝑃,𝑒,𝑓 𝑃,𝑠 𝑥,𝑃 𝑅,𝑒,𝑓,𝑦 𝑥,𝑅 𝑆,𝑎 𝑆,𝑠 𝜑,𝑎 Allowed substitution hints: 𝜑(𝑒,𝑓) 𝐴(𝑦,𝑒,𝑓,𝑘,𝑙) 𝐷(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑎,𝑙) 𝑃(𝑦,𝑡,𝑔,ℎ,𝑖,𝑗,𝑎) ∼ (𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑠,𝑙) 𝑅(𝑡,𝑔,ℎ,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙) 𝑆(𝑒,𝑓,𝑘,𝑙) 𝐸(𝑡,𝑔,ℎ,𝑖,𝑘,𝑠,𝑎,𝑙) 𝐺(𝑥,𝑗,𝑘,𝑠,𝑎,𝑙) 𝐻(𝑒,𝑓,𝑘,𝑙) 𝐽(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙) 𝐾(𝑘,𝑠,𝑙) 𝐿(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙) 𝑀(𝑥,𝑡,𝑒,𝑓,𝑔,𝑖,𝑘,𝑠,𝑎,𝑙) 𝑁(𝑦,𝑡,𝑔,ℎ,𝑖,𝑗)

Proof of Theorem aks6d1c6lem3 Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aks6d1c6.18	. . . . . . . . . . . 12 ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))
2		aks6d1c6.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3		aks6d1c6.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℙ)
4		aks6d1c6.7	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
5		aks6d1c6.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ℕ)
6		aks6d1c6.8	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
7		aks6d1c6.12	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)))
8		aks6d1c6.13	. . . . . . . . . . . . 13 ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
9		eqid 2740	. . . . . . . . . . . . 13 ⊢ (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
10	2, 3, 4, 5, 6, 7, 8, 9	hashscontpowcl 42077	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ∈ ℕ₀)
11	1, 10	eqeltrid 2848	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
12	11	nn0zd 12665	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
13	12	zcnd 12748	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
14		1cnd 11285	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
15		aks6d1c6.11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
16	15	nn0cnd 12615	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
17	13, 14, 16	nppcan3d 11674	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = (𝐷 + 𝐴))
18	17	eqcomd 2746	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (𝐴 + 1)))
19		hashfz0 14481	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ₀ → (♯‘(0...𝐴)) = (𝐴 + 1))
20	15, 19	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) = (𝐴 + 1))
21	20	eqcomd 2746	. . . . . . . 8 ⊢ (𝜑 → (𝐴 + 1) = (♯‘(0...𝐴)))
22	21	oveq2d 7464	. . . . . . 7 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = ((𝐷 − 1) + (♯‘(0...𝐴))))
23	18, 22	eqtrd 2780	. . . . . 6 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (♯‘(0...𝐴))))
24		1zzd 12674	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
25	12, 24	zsubcld 12752	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℤ)
26		0p1e1 12415	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0 + 1) = 1)
28		fvexd 6935	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘(ℤ/nℤ‘𝑅)) ∈ V)
29	8, 28	eqeltrid 2848	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ V)
30	29	imaexd 7956	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V)
31	15	ne0d 4365	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ₀ ≠ ∅)
32	31, 31	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅))
33		xpnz 6190	. . . . . . . . . . . . . . 15 ⊢ ((ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅) ↔ (ℕ₀ × ℕ₀) ≠ ∅)
34	32, 33	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ≠ ∅)
35		ovexd 7483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑙 ∈ ℕ₀) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
36	35	ralrimiva 3152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
37	36	ralrimiva 3152	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
38	7	fnmpo 8110	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V → 𝐸 Fn (ℕ₀ × ℕ₀))
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 Fn (ℕ₀ × ℕ₀))
40		ssidd 4032	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀))
41		fnimaeq0 6713	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 Fn (ℕ₀ × ℕ₀) ∧ (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀)) → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
42	39, 40, 41	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
43	42	necon3bid 2991	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅ ↔ (ℕ₀ × ℕ₀) ≠ ∅))
44	34, 43	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅)
45	5	nnnn0d 12613	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
46	9	zncrng 21586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℕ₀ → (ℤ/nℤ‘𝑅) ∈ CRing)
47	45, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℤ/nℤ‘𝑅) ∈ CRing)
48		crngring 20272	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ CRing → (ℤ/nℤ‘𝑅) ∈ Ring)
49	8	zrhrhm 21545	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)))
50		zringbas 21487	. . . . . . . . . . . . . . . . . 18 ⊢ ℤ = (Base‘ℤ_ring)
51		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑅)) = (Base‘(ℤ/nℤ‘𝑅))
52	50, 51	rhmf 20511	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
53	47, 48, 49, 52	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
54	53	ffnd 6748	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 Fn ℤ)
55	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))))
56		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑘 = 𝑥)
57	56	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → (𝑃↑𝑘) = (𝑃↑𝑥))
58		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑙 = 𝑦)
59	58	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑦))
60	57, 59	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
61		simplr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑦 ∈ ℕ₀)
63		ovexd 7483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ V)
64	55, 60, 61, 62, 63	ovmpod 7602	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
65	3	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℙ)
66		prmnn 16721	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
67	65, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℕ)
68	67	nnzd 12666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℤ)
69	68, 61	zexpcld 14138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃↑𝑥) ∈ ℤ)
70	4	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∥ 𝑁)
71	67	nnne0d 12343	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ≠ 0)
72	2	nnzd 12666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℤ)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → 𝑁 ∈ ℤ)
74	73	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑁 ∈ ℤ)
75		dvdsval2 16305	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
76	68, 71, 74, 75	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
77	70, 76	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑁 / 𝑃) ∈ ℤ)
78	77, 62	zexpcld 14138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑁 / 𝑃)↑𝑦) ∈ ℤ)
79	69, 78	zmulcld 12753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ ℤ)
80	64, 79	eqeltrd 2844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) ∈ ℤ)
81	80	ralrimiva 3152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
82	81	ralrimiva 3152	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
83	39, 82	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
84		ffnov 7576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ ↔ (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
85	83, 84	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸:(ℕ₀ × ℕ₀)⟶ℤ)
86		frn 6754	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ → ran 𝐸 ⊆ ℤ)
87	85, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝐸 ⊆ ℤ)
88		fnima 6710	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 Fn (ℕ₀ × ℕ₀) → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
89	39, 88	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
90	89	sseq1d 4040	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ))
91	87, 90	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ)
92		fnimaeq0 6713	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ) → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
93	54, 91, 92	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
94	93	necon3bid 2991	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅))
95	44, 94	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅)
96		hashge1 14438	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))
97	1	eqcomi 2749	. . . . . . . . . . . . . 14 ⊢ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷
98	97	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷)
99	96, 98	breqtrd 5192	. . . . . . . . . . . 12 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ 𝐷)
100	30, 95, 99	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ 𝐷)
101	27, 100	eqbrtrd 5188	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ≤ 𝐷)
102		0red 11293	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
103		1red 11291	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
104	11	nn0red 12614	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		leaddsub 11766	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
106	102, 103, 104, 105	syl3anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
107	101, 106	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 − 1))
108	25, 107	jca 511	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
109		elnn0z 12652	. . . . . . . 8 ⊢ ((𝐷 − 1) ∈ ℕ₀ ↔ ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
110	108, 109	sylibr 234	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ₀)
111		fzfid 14024	. . . . . . . 8 ⊢ (𝜑 → (0...𝐴) ∈ Fin)
112		hashcl 14405	. . . . . . . 8 ⊢ ((0...𝐴) ∈ Fin → (♯‘(0...𝐴)) ∈ ℕ₀)
113	111, 112	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℕ₀)
114	110, 113	nn0addcld 12617	. . . . . 6 ⊢ (𝜑 → ((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀)
115	23, 114	eqeltrd 2844	. . . . 5 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℕ₀)
116		bccl 14371	. . . . 5 ⊢ (((𝐷 + 𝐴) ∈ ℕ₀ ∧ (𝐷 − 1) ∈ ℤ) → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
117	115, 25, 116	syl2anc 583	. . . 4 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
118	117	nn0red 12614	. . 3 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ)
119	118	rexrd 11340	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ^*)
120		aks6d1c6.17	. . . . . . 7 ⊢ 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀))
121		ovexd 7483	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
122	121	mptexd 7261	. . . . . . 7 ⊢ (𝜑 → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
123	120, 122	eqeltrid 2848	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ V)
124	123	imaexd 7956	. . . . 5 ⊢ (𝜑 → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V)
125		simprl 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)))
126	125	ex 412	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))))
127		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑤)
128	127	fveq1d 6922	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑤‘𝑡))
129	128	sumeq2dv 15750	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑤 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡))
130	129	breq1d 5176	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))
131	130	elrab 3708	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))
132	131	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))))
133	132	biimpd 229	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))))
134	133	imim1d 82	. . . . . . . . 9 ⊢ (𝜑 → (((𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)))))
135	126, 134	mpd 15	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))))
136	135	ssrdv 4014	. . . . . . 7 ⊢ (𝜑 → {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴)))
137		aks6d1c6.19	. . . . . . . . 9 ⊢ 𝑆 = {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)}
138	137	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
139	138	sseq1d 4040	. . . . . . 7 ⊢ (𝜑 → (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) ↔ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴))))
140	136, 139	mpbird 257	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
141		imass2 6132	. . . . . 6 ⊢ (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
142	140, 141	syl 17	. . . . 5 ⊢ (𝜑 → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
143	124, 142	ssexd 5342	. . . 4 ⊢ (𝜑 → (𝐻 “ 𝑆) ∈ V)
144		hashxnn0 14388	. . . 4 ⊢ ((𝐻 “ 𝑆) ∈ V → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
145	143, 144	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
146		xnn0xr 12630	. . 3 ⊢ ((♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^* → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
147	145, 146	syl 17	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
148		hashxnn0 14388	. . . 4 ⊢ ((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
149	124, 148	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
150		xnn0xr 12630	. . 3 ⊢ ((♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^* → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
151	149, 150	syl 17	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
152	110	nn0cnd 12615	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℂ)
153	113	nn0cnd 12615	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℂ)
154	152, 153	pncand 11648	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))) = (𝐷 − 1))
155	154	eqcomd 2746	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) = (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))))
156	23, 155	oveq12d 7466	. . . . . 6 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
157	15	nn0ge0d 12616	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝐴)
158		0zd 12651	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℤ)
159	15	nn0zd 12665	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
160		eluz 12917	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
161	158, 159, 160	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
162	157, 161	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
163		fzn0 13598	. . . . . . . . . 10 ⊢ ((0...𝐴) ≠ ∅ ↔ 𝐴 ∈ (ℤ_≥‘0))
164	162, 163	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → (0...𝐴) ≠ ∅)
165	110, 111, 164, 137	sticksstones23 42126	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))))
166	113	nn0zd 12665	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℤ)
167		bccmpl 14358	. . . . . . . . 9 ⊢ ((((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀ ∧ (♯‘(0...𝐴)) ∈ ℤ) → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
168	114, 166, 167	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
169	165, 168	eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
170	169	eqcomd 2746	. . . . . 6 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))) = (♯‘𝑆))
171	156, 170	eqtrd 2780	. . . . 5 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
172	171	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
173	120	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
174		ovexd 7483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
175	174	mptexd 7261	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
176	173, 175	eqeltrd 2844	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 ∈ V)
177	176	resexd 6057	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆) ∈ V)
178	176	imaexd 7956	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 “ 𝑆) ∈ V)
179		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆))
180		hashf1dmcdm 14493	. . . . 5 ⊢ (((𝐻 ↾ 𝑆) ∈ V ∧ (𝐻 “ 𝑆) ∈ V ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
181	177, 178, 179, 180	syl3anc 1371	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
182	172, 181	eqbrtrd 5188	. . 3 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
183	120	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
184		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ℎ = 𝑗)
185	184	fveq2d 6924	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (𝐺‘ℎ) = (𝐺‘𝑗))
186	185	fveq2d 6924	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ((eval₁‘𝐾)‘(𝐺‘ℎ)) = ((eval₁‘𝐾)‘(𝐺‘𝑗)))
187	186	fveq1d 6922	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
188		simp2 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)) → 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)))
189	188	rabssdv 4098	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴)))
190	137, 189	eqsstrid 4057	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
191	190	sselda 4008	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ (ℕ₀ ↑_m (0...𝐴)))
192		fvexd 6935	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ V)
193	183, 187, 191, 192	fvmptd 7036	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
194		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
195		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
196		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘𝐾)
197		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
198		aks6d1c6.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Field)
199	198	fldcrngd 20764	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ CRing)
200	199	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐾 ∈ CRing)
201		aks6d1c6.16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
202		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
203	202	crngmgp 20268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
204	199, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
205		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
206	204, 45, 205	isprimroot 42050	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
207	206	biimpd 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
208	201, 207	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣)))
209	208	simp1d 1142	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
210	202, 196	mgpbas 20167	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
211	210	eqcomi 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
212	209, 211	eleqtrdi 2854	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
213	212	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑀 ∈ (Base‘𝐾))
214		aks6d1c6.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = (chr‘𝐾)
215		aks6d1c6.9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝑃)
216		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
217		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (._g‘(mulGrp‘(Poly₁‘𝐾))) = (._g‘(mulGrp‘(Poly₁‘𝐾)))
218		aks6d1c6.10	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ ((mulGrp‘(Poly₁‘𝐾)) Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(._g‘(mulGrp‘(Poly₁‘𝐾)))((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
219	198, 3, 214, 15, 215, 216, 217, 218	aks6d1c5lem0 42092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
220	219	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
221	220, 191	ffvelcdmd 7119	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺‘𝑗) ∈ (Base‘(Poly₁‘𝐾)))
222	194, 195, 196, 197, 200, 213, 221	fveval1fvcl 22358	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ (Base‘𝐾))
223	193, 222	eqeltrd 2844	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) ∈ (Base‘𝐾))
224		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗))
225	223, 224	fmptd 7148	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾))
226		fvexd 6935	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ℎ ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) ∈ V)
227	226, 120	fmptd 7148	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:(ℕ₀ ↑_m (0...𝐴))⟶V)
228	227, 190	feqresmpt 6991	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾ 𝑆) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)))
229	228	feq1d 6732	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) ↔ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾)))
230	225, 229	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾))
231		ffrn 6760	. . . . . . . . . . . 12 ⊢ ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
232	230, 231	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
233		df-ima 5713	. . . . . . . . . . . . 13 ⊢ (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆)
234	233	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆))
235	234	feq3d 6734	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ↔ (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆)))
236	232, 235	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))
237	236	notnotd 144	. . . . . . . . 9 ⊢ (𝜑 → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))
238	237	a1d 25	. . . . . . . 8 ⊢ (𝜑 → (¬ ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)) → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆)))
239	238	con4d 115	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
240		df-an 396	. . . . . . . . . . . . . 14 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣))
241	240	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣)))
242		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (deg₁‘𝐾) = (deg₁‘𝐾)
243		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
244		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘(Poly₁‘𝐾)) = (0_g‘(Poly₁‘𝐾))
245		fldidom 20793	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn)
246	198, 245	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ IDomn)
247	246	ad4antr 731	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ IDomn)
248	195	ply1crng 22221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
249		crngring 20272	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
250		ringgrp 20265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ Ring → (Poly₁‘𝐾) ∈ Grp)
251	199, 248, 249, 250	4syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Grp)
252	251	ad4antr 731	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (Poly₁‘𝐾) ∈ Grp)
253	198, 3, 214, 15, 215, 216, 217, 218	aks6d1c5 42096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
254	253	ad4antr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
255		f1f 6817	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
256	254, 255	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
257	137	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ 𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
258		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑢)
259	258	fveq1d 6922	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑢‘𝑡))
260	259	sumeq2dv 15750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑢 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
261	260	breq1d 5176	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑢 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
262	261	elrab 3708	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
263	262	simplbi 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
264	257, 263	sylbi 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
265	264	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
266	265	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
267	266	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
268	256, 267	ffvelcdmd 7119	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)))
269	137	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 ↔ 𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
270		elrabi 3703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
271	269, 270	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
272	271	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
273	272	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
274	256, 273	ffvelcdmd 7119	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)))
275		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
276	197, 275	grpsubcl 19060	. . . . . . . . . . . . . . . . 17 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
277	252, 268, 274, 276	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
278		neqne 2954	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑢 = 𝑣 → 𝑢 ≠ 𝑣)
279	278	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → 𝑢 ≠ 𝑣)
280	279	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
281	267, 273	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴))))
282		f1fveq 7299	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) ∧ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
283	254, 281, 282	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
284	283	bicomd 223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 = 𝑣 ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
285	284	necon3bid 2991	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
286	285	biimpd 229	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 → (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
287	280, 286	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ≠ (𝐺‘𝑣))
288	197, 244, 275	grpsubeq0 19066	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) = (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
289	288	necon3bid 2991	. . . . . . . . . . . . . . . . . 18 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
290	252, 268, 274, 289	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
291	287, 290	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)))
292	195, 197, 242, 194, 243, 244, 247, 277, 291	fta1g 26229	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
293	242, 195, 197	deg1xrcl 26141	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
294	277, 293	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
295	104	ad4antr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ)
296		1red 11291	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 1 ∈ ℝ)
297	295, 296	resubcld 11718	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ)
298	297	rexrd 11340	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ^*)
299		simp-4l 782	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝜑)
300		fvexd 6935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
301		cnvexg 7964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
302	300, 301	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
303	302	imaexd 7956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V)
304		hashxnn0 14388	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^*)
305		xnn0xr 12630	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^* → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
306	299, 303, 304, 305	4syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
307	242, 195, 197	deg1xrcl 26141	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
308	274, 307	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
309	242, 195, 197	deg1xrcl 26141	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
310	268, 309	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
311	308, 310	ifcld 4594	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ∈ ℝ^*)
312	247	idomringd 20750	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Ring)
313	195, 242, 312, 197, 275, 268, 274	deg1suble 26166	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ≤ if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
314		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
315	314	breq1d 5176	. . . . . . . . . . . . . . . . . . 19 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → (((deg₁‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1) ↔ if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1)))
316		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑢)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
317	316	breq1d 5176	. . . . . . . . . . . . . . . . . . 19 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑢)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → (((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1) ↔ if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1)))
318		aks6d1c6.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly₁‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘𝑓)‘𝑦)) = (((eval₁‘𝐾)‘𝑓)‘(𝑒(._g‘(mulGrp‘𝐾))𝑦)))}
319	198	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
320	3	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
321	5	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
322	2	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
323	4	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
324	6	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
325	215	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
326	15	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
327		aks6d1c6.14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
328	327	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
329		aks6d1c6.15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
330	329	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
331	201	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
332		simpllr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑣 ∈ 𝑆)
333	332, 271	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
334	318, 214, 319, 320, 321, 322, 323, 324, 325, 218, 326, 7, 8, 328, 330, 331, 120, 1, 137, 333	aks6d1c6lem1 42127	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
335		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑣)
336	335	fveq1d 6922	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑣‘𝑡))
337	336	sumeq2dv 15750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑣 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
338	337	breq1d 5176	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑣 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
339	338	elrab 3708	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
340	269, 339	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝑆 ↔ (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
341	332, 340	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
342	341	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1))
343	334, 342	eqbrtrd 5188	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1))
344	198	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
345	3	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
346	5	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
347	2	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
348	4	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
349	6	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
350	215	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
351	15	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
352	327	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
353	329	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
354	201	ad5antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
355	267	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
356	318, 214, 344, 345, 346, 347, 348, 349, 350, 218, 351, 7, 8, 352, 353, 354, 120, 1, 137, 355	aks6d1c6lem1 42127	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
357		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑢 ∈ 𝑆)
358	257, 262	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
359	357, 358	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
360	359	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1))
361	356, 360	eqbrtrd 5188	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1))
362	315, 317, 343, 361	ifbothda 4586	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1))
363	294, 311, 298, 313, 362	xrletrd 13224	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ≤ (𝐷 − 1))
364	295	rexrd 11340	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ^*)
365	295	ltm1d 12227	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < 𝐷)
366		simpllr 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
367		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
368	299, 366, 367	jca31 514	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆))
369		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣))
370	368, 369	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)))
371	198	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Field)
372	3	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∈ ℙ)
373	5	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑅 ∈ ℕ)
374	2	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑁 ∈ ℕ)
375	4	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∥ 𝑁)
376	6	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑁 gcd 𝑅) = 1)
377	215	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 < 𝑃)
378	15	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 ∈ ℕ₀)
379	327	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
380	329	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
381	201	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
382		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
383		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
384		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣))
385	279	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
386		aks6d1c6lem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (𝑗 ∈ (ℕ₀ × ℕ₀) ↦ ((𝐸‘𝑗)(._g‘(mulGrp‘𝐾))𝑀))
387		aks6d1c6lem3.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))
388	387	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))
389	318, 214, 371, 372, 373, 374, 375, 376, 377, 218, 378, 7, 8, 379, 380, 381, 120, 1, 137, 382, 383, 384, 385, 386, 388	aks6d1c6lem2 42128	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
390	370, 389	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
391	298, 364, 306, 365, 390	xrltletrd 13223	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
392	294, 298, 306, 363, 391	xrlelttrd 13222	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
393	242, 195, 244, 197	deg1nn0clb 26149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ Ring ∧ ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
394	312, 277, 393	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
395	291, 394	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀)
396	395	nn0red 12614	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ)
397	396	rexrd 11340	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
398		fvexd 6935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
399	398, 301	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
400	399	imaexd 7956	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V)
401	400, 304	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^*)
402	401, 305	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
403		xrltnle 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^* ∧ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*) → (((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ↔ ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)))))
404	397, 402, 403	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ↔ ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)))))
405	392, 404	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
406	292, 405	pm2.21dd 195	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
407	406	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
408	241, 407	sylbird 260	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
409		biidd 262	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 = 𝑣 ↔ 𝑢 = 𝑣))
410	409	necon3abid 2983	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 ≠ 𝑣 ↔ ¬ 𝑢 = 𝑣))
411	410	necon1bbid 2986	. . . . . . . . . . . . . . . 16 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (¬ ¬ 𝑢 = 𝑣 ↔ 𝑢 = 𝑣))
412	411	pm5.74i 271	. . . . . . . . . . . . . . 15 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
413	412	notbii 320	. . . . . . . . . . . . . 14 ⊢ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
414	413	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
415	414	imbi1d 341	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
416	408, 415	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
417	416	imp 406	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
418		fveqeq2 6929	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦)))
419		equequ1 2024	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 ↔ 𝑢 = 𝑦))
420	418, 419	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → ((((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
421	420	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑢 → (¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
422		fveq2 6920	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → ((𝐻 ↾ 𝑆)‘𝑦) = ((𝐻 ↾ 𝑆)‘𝑣))
423	422	eqeq2d 2751	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣)))
424		equequ2 2025	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (𝑢 = 𝑦 ↔ 𝑢 = 𝑣))
425	423, 424	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
426	425	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
427	421, 426	cbvrex2vw 3248	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
428	427	biimpi 216	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
429	428	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
430	417, 429	r19.29vva 3222	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
431	430	ex 412	. . . . . . . 8 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
432		rexnal2 3141	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))
433	432	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
434	433	imbi1d 341	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
435	431, 434	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
436	239, 435	jaod 858	. . . . . 6 ⊢ (𝜑 → ((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
437		ianor 982	. . . . . . . . 9 ⊢ (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
438	437	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
439	438	biimpd 229	. . . . . . 7 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
440	439	imim1d 82	. . . . . 6 ⊢ (𝜑 → (((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
441	436, 440	mpd 15	. . . . 5 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
442		dff13 7292	. . . . . . . . 9 ⊢ ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
443	442	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
444	443	notbid 318	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
445	444	biimpd 229	. . . . . 6 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
446	445	imim1d 82	. . . . 5 ⊢ (𝜑 → ((¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
447	441, 446	mpd 15	. . . 4 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
448	447	imp 406	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
449	182, 448	pm2.61dan 812	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
450		hashss 14458	. . 3 ⊢ (((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V ∧ (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
451	124, 142, 450	syl2anc 583	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
452	119, 147, 151, 449, 451	xrletrd 13224	1 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 {crab 3443 Vcvv 3488 ⊆ wss 3976 ∅c0 4352 ifcif 4548 {csn 4648 class class class wbr 5166 {copab 5228 ↦ cmpt 5249 × cxp 5698 ^◡ccnv 5699 ran crn 5701 ↾ cres 5702 “ cima 5703 Fn wfn 6568 ⟶wf 6569 –1-1→wf1 6570 ‘cfv 6573 (class class class)co 7448 ∈ cmpo 7450 ↑_m cmap 8884 Fincfn 9003 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11520 / cdiv 11947 ℕcn 12293 ℕ₀cn0 12553 ℕ₀^*cxnn0 12625 ℤcz 12639 ℤ_≥cuz 12903 ...cfz 13567 ↑cexp 14112 Ccbc 14351 ♯chash 14379 Σcsu 15734 ∥ cdvds 16302 gcd cgcd 16540 ℙcprime 16718 Basecbs 17258 +_gcplusg 17311 0_gc0g 17499 Σ_g cgsu 17500 Grpcgrp 18973 -_gcsg 18975 ._gcmg 19107 CMndccmn 19822 mulGrpcmgp 20161 Ringcrg 20260 CRingccrg 20261 RingHom crh 20495 RingIso crs 20496 IDomncidom 20715 Fieldcfield 20752 ℤ_ringczring 21480 ℤ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-inf2 9710 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-ico 13413 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-clim 15534 df-sum 15735 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: aks6d1c6lem4 42130

W3C validator