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 42542

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 2737	. . . . . . . . . . . . 13 ⊢ (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
10	2, 3, 4, 5, 6, 7, 8, 9	hashscontpowcl 42490	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ∈ ℕ₀)
11	1, 10	eqeltrid 2841	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
12	11	nn0zd 12525	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
13	12	zcnd 12609	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
14		1cnd 11139	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
15		aks6d1c6.11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
16	15	nn0cnd 12476	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
17	13, 14, 16	nppcan3d 11531	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = (𝐷 + 𝐴))
18	17	eqcomd 2743	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (𝐴 + 1)))
19		hashfz0 14367	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ₀ → (♯‘(0...𝐴)) = (𝐴 + 1))
20	15, 19	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) = (𝐴 + 1))
21	20	eqcomd 2743	. . . . . . . 8 ⊢ (𝜑 → (𝐴 + 1) = (♯‘(0...𝐴)))
22	21	oveq2d 7384	. . . . . . 7 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = ((𝐷 − 1) + (♯‘(0...𝐴))))
23	18, 22	eqtrd 2772	. . . . . 6 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (♯‘(0...𝐴))))
24		1zzd 12534	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
25	12, 24	zsubcld 12613	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℤ)
26		0p1e1 12274	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0 + 1) = 1)
28		fvexd 6857	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘(ℤ/nℤ‘𝑅)) ∈ V)
29	8, 28	eqeltrid 2841	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ V)
30	29	imaexd 7868	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V)
31	15	ne0d 4296	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ₀ ≠ ∅)
32	31, 31	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅))
33		xpnz 6125	. . . . . . . . . . . . . . 15 ⊢ ((ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅) ↔ (ℕ₀ × ℕ₀) ≠ ∅)
34	32, 33	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ≠ ∅)
35		ovexd 7403	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑙 ∈ ℕ₀) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
36	35	ralrimiva 3130	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
37	36	ralrimiva 3130	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
38	7	fnmpo 8023	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V → 𝐸 Fn (ℕ₀ × ℕ₀))
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 Fn (ℕ₀ × ℕ₀))
40		ssidd 3959	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀))
41		fnimaeq0 6633	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 Fn (ℕ₀ × ℕ₀) ∧ (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀)) → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
42	39, 40, 41	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
43	42	necon3bid 2977	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅ ↔ (ℕ₀ × ℕ₀) ≠ ∅))
44	34, 43	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅)
45	5	nnnn0d 12474	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
46	9	zncrng 21511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℕ₀ → (ℤ/nℤ‘𝑅) ∈ CRing)
47	45, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℤ/nℤ‘𝑅) ∈ CRing)
48		crngring 20192	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ CRing → (ℤ/nℤ‘𝑅) ∈ Ring)
49	8	zrhrhm 21478	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)))
50		zringbas 21420	. . . . . . . . . . . . . . . . . 18 ⊢ ℤ = (Base‘ℤ_ring)
51		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑅)) = (Base‘(ℤ/nℤ‘𝑅))
52	50, 51	rhmf 20432	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
53	47, 48, 49, 52	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
54	53	ffnd 6671	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 Fn ℤ)
55	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))))
56		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑘 = 𝑥)
57	56	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → (𝑃↑𝑘) = (𝑃↑𝑥))
58		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑙 = 𝑦)
59	58	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑦))
60	57, 59	oveq12d 7386	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
61		simplr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑦 ∈ ℕ₀)
63		ovexd 7403	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ V)
64	55, 60, 61, 62, 63	ovmpod 7520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
65	3	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℙ)
66		prmnn 16613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
67	65, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℕ)
68	67	nnzd 12526	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℤ)
69	68, 61	zexpcld 14022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃↑𝑥) ∈ ℤ)
70	4	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∥ 𝑁)
71	67	nnne0d 12207	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ≠ 0)
72	2	nnzd 12526	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℤ)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → 𝑁 ∈ ℤ)
74	73	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑁 ∈ ℤ)
75		dvdsval2 16194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
76	68, 71, 74, 75	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
77	70, 76	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑁 / 𝑃) ∈ ℤ)
78	77, 62	zexpcld 14022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑁 / 𝑃)↑𝑦) ∈ ℤ)
79	69, 78	zmulcld 12614	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ ℤ)
80	64, 79	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) ∈ ℤ)
81	80	ralrimiva 3130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
82	81	ralrimiva 3130	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
83	39, 82	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
84		ffnov 7494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ ↔ (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
85	83, 84	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸:(ℕ₀ × ℕ₀)⟶ℤ)
86		frn 6677	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ → ran 𝐸 ⊆ ℤ)
87	85, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝐸 ⊆ ℤ)
88		fnima 6630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 Fn (ℕ₀ × ℕ₀) → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
89	39, 88	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
90	89	sseq1d 3967	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ))
91	87, 90	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ)
92		fnimaeq0 6633	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ) → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
93	54, 91, 92	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
94	93	necon3bid 2977	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅))
95	44, 94	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅)
96		hashge1 14324	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))
97	1	eqcomi 2746	. . . . . . . . . . . . . 14 ⊢ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷
98	97	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷)
99	96, 98	breqtrd 5126	. . . . . . . . . . . 12 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ 𝐷)
100	30, 95, 99	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ 𝐷)
101	27, 100	eqbrtrd 5122	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ≤ 𝐷)
102		0red 11147	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
103		1red 11145	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
104	11	nn0red 12475	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		leaddsub 11625	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
106	102, 103, 104, 105	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
107	101, 106	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 − 1))
108	25, 107	jca 511	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
109		elnn0z 12513	. . . . . . . 8 ⊢ ((𝐷 − 1) ∈ ℕ₀ ↔ ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
110	108, 109	sylibr 234	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ₀)
111		fzfid 13908	. . . . . . . 8 ⊢ (𝜑 → (0...𝐴) ∈ Fin)
112		hashcl 14291	. . . . . . . 8 ⊢ ((0...𝐴) ∈ Fin → (♯‘(0...𝐴)) ∈ ℕ₀)
113	111, 112	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℕ₀)
114	110, 113	nn0addcld 12478	. . . . . 6 ⊢ (𝜑 → ((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀)
115	23, 114	eqeltrd 2837	. . . . 5 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℕ₀)
116		bccl 14257	. . . . 5 ⊢ (((𝐷 + 𝐴) ∈ ℕ₀ ∧ (𝐷 − 1) ∈ ℤ) → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
117	115, 25, 116	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
118	117	nn0red 12475	. . 3 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ)
119	118	rexrd 11194	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ^*)
120		aks6d1c6.17	. . . . . . 7 ⊢ 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀))
121		ovexd 7403	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
122	121	mptexd 7180	. . . . . . 7 ⊢ (𝜑 → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
123	120, 122	eqeltrid 2841	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ V)
124	123	imaexd 7868	. . . . 5 ⊢ (𝜑 → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V)
125		simprl 771	. . . . . . . . . 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 6844	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑤‘𝑡))
129	128	sumeq2dv 15637	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑤 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡))
130	129	breq1d 5110	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))
131	130	elrab 3648	. . . . . . . . . . . 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 3941	. . . . . . 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 3967	. . . . . . 7 ⊢ (𝜑 → (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) ↔ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴))))
140	136, 139	mpbird 257	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
141		imass2 6069	. . . . . 6 ⊢ (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
142	140, 141	syl 17	. . . . 5 ⊢ (𝜑 → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
143	124, 142	ssexd 5271	. . . 4 ⊢ (𝜑 → (𝐻 “ 𝑆) ∈ V)
144		hashxnn0 14274	. . . 4 ⊢ ((𝐻 “ 𝑆) ∈ V → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
145	143, 144	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
146		xnn0xr 12491	. . 3 ⊢ ((♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^* → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
147	145, 146	syl 17	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
148		hashxnn0 14274	. . . 4 ⊢ ((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
149	124, 148	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
150		xnn0xr 12491	. . 3 ⊢ ((♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^* → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
151	149, 150	syl 17	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
152	110	nn0cnd 12476	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℂ)
153	113	nn0cnd 12476	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℂ)
154	152, 153	pncand 11505	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))) = (𝐷 − 1))
155	154	eqcomd 2743	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) = (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))))
156	23, 155	oveq12d 7386	. . . . . 6 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
157	15	nn0ge0d 12477	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝐴)
158		0zd 12512	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℤ)
159	15	nn0zd 12525	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
160		eluz 12777	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
161	158, 159, 160	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
162	157, 161	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
163		fzn0 13466	. . . . . . . . . 10 ⊢ ((0...𝐴) ≠ ∅ ↔ 𝐴 ∈ (ℤ_≥‘0))
164	162, 163	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → (0...𝐴) ≠ ∅)
165	110, 111, 164, 137	sticksstones23 42539	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))))
166	113	nn0zd 12525	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℤ)
167		bccmpl 14244	. . . . . . . . 9 ⊢ ((((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀ ∧ (♯‘(0...𝐴)) ∈ ℤ) → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
168	114, 166, 167	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
169	165, 168	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
170	169	eqcomd 2743	. . . . . 6 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))) = (♯‘𝑆))
171	156, 170	eqtrd 2772	. . . . 5 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
172	171	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
173	120	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
174		ovexd 7403	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
175	174	mptexd 7180	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
176	173, 175	eqeltrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 ∈ V)
177	176	resexd 5995	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆) ∈ V)
178	176	imaexd 7868	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 “ 𝑆) ∈ V)
179		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆))
180		hashf1dmcdm 14379	. . . . 5 ⊢ (((𝐻 ↾ 𝑆) ∈ V ∧ (𝐻 “ 𝑆) ∈ V ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
181	177, 178, 179, 180	syl3anc 1374	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
182	172, 181	eqbrtrd 5122	. . 3 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
183	120	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
184		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ℎ = 𝑗)
185	184	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (𝐺‘ℎ) = (𝐺‘𝑗))
186	185	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ((eval₁‘𝐾)‘(𝐺‘ℎ)) = ((eval₁‘𝐾)‘(𝐺‘𝑗)))
187	186	fveq1d 6844	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
188		simp2 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)) → 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)))
189	188	rabssdv 4028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴)))
190	137, 189	eqsstrid 3974	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
191	190	sselda 3935	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ (ℕ₀ ↑_m (0...𝐴)))
192		fvexd 6857	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ V)
193	183, 187, 191, 192	fvmptd 6957	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
194		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
195		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
196		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘𝐾)
197		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
198		aks6d1c6.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Field)
199	198	fldcrngd 20687	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ CRing)
200	199	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐾 ∈ CRing)
201		aks6d1c6.16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
202		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
203	202	crngmgp 20188	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
204	199, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
205		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
206	204, 45, 205	isprimroot 42463	. . . . . . . . . . . . . . . . . . . . 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 1143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
210	202, 196	mgpbas 20092	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
211	210	eqcomi 2746	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
212	209, 211	eleqtrdi 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
213	212	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑀 ∈ (Base‘𝐾))
214		aks6d1c6.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = (chr‘𝐾)
215		aks6d1c6.9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝑃)
216		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
217		eqid 2737	. . . . . . . . . . . . . . . . . . 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 42505	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
220	219	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
221	220, 191	ffvelcdmd 7039	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺‘𝑗) ∈ (Base‘(Poly₁‘𝐾)))
222	194, 195, 196, 197, 200, 213, 221	fveval1fvcl 22289	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ (Base‘𝐾))
223	193, 222	eqeltrd 2837	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) ∈ (Base‘𝐾))
224		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗))
225	223, 224	fmptd 7068	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾))
226		fvexd 6857	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ℎ ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) ∈ V)
227	226, 120	fmptd 7068	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:(ℕ₀ ↑_m (0...𝐴))⟶V)
228	227, 190	feqresmpt 6911	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾ 𝑆) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)))
229	228	feq1d 6652	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) ↔ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾)))
230	225, 229	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾))
231		ffrn 6683	. . . . . . . . . . . 12 ⊢ ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
232	230, 231	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
233		df-ima 5645	. . . . . . . . . . . . 13 ⊢ (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆)
234	233	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆))
235	234	feq3d 6655	. . . . . . . . . . 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 2737	. . . . . . . . . . . . . . . 16 ⊢ (deg₁‘𝐾) = (deg₁‘𝐾)
243		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
244		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘(Poly₁‘𝐾)) = (0_g‘(Poly₁‘𝐾))
245		fldidom 20716	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn)
246	198, 245	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ IDomn)
247	246	ad4antr 733	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ IDomn)
248	195	ply1crng 22151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
249		crngring 20192	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
250		ringgrp 20185	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ Ring → (Poly₁‘𝐾) ∈ Grp)
251	199, 248, 249, 250	4syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Grp)
252	251	ad4antr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (Poly₁‘𝐾) ∈ Grp)
253	198, 3, 214, 15, 215, 216, 217, 218	aks6d1c5 42509	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
254	253	ad4antr 733	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
255		f1f 6738	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
256	254, 255	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
257	137	eleq2i 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ 𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
258		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑢)
259	258	fveq1d 6844	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑢‘𝑡))
260	259	sumeq2dv 15637	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑢 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
261	260	breq1d 5110	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑢 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
262	261	elrab 3648	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
263	262	simplbi 496	. . . . . . . . . . . . . . . . . . . . . 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 7039	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)))
269	137	eleq2i 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 ↔ 𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
270		elrabi 3644	. . . . . . . . . . . . . . . . . . . . 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 7039	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)))
275		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
276	197, 275	grpsubcl 18962	. . . . . . . . . . . . . . . . 17 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
277	252, 268, 274, 276	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
278		neqne 2941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑢 = 𝑣 → 𝑢 ≠ 𝑣)
279	278	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → 𝑢 ≠ 𝑣)
280	279	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
281	267, 273	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴))))
282		f1fveq 7218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) ∧ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
283	254, 281, 282	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
284	283	bicomd 223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 = 𝑣 ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
285	284	necon3bid 2977	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
286	285	biimpd 229	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 → (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
287	280, 286	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ≠ (𝐺‘𝑣))
288	197, 244, 275	grpsubeq0 18968	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) = (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
289	288	necon3bid 2977	. . . . . . . . . . . . . . . . . 18 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
290	252, 268, 274, 289	syl3anc 1374	. . . . . . . . . . . . . . . . 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 26143	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
293	242, 195, 197	deg1xrcl 26055	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
294	277, 293	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
295	104	ad4antr 733	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ)
296		1red 11145	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 1 ∈ ℝ)
297	295, 296	resubcld 11577	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ)
298	297	rexrd 11194	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ^*)
299		simp-4l 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝜑)
300		fvexd 6857	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
301		cnvexg 7876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
302	300, 301	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
303	302	imaexd 7868	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V)
304		hashxnn0 14274	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^*)
305		xnn0xr 12491	. . . . . . . . . . . . . . . . . 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 26055	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
308	274, 307	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
309	242, 195, 197	deg1xrcl 26055	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
310	268, 309	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
311	308, 310	ifcld 4528	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ∈ ℝ^*)
312	247	idomringd 20673	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Ring)
313	195, 242, 312, 197, 275, 268, 274	deg1suble 26080	. . . . . . . . . . . . . . . . . 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 5110	. . . . . . . . . . . . . . . . . . 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 5110	. . . . . . . . . . . . . . . . . . 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 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
320	3	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
321	5	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
322	2	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
323	4	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
324	6	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
325	215	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
326	15	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
327		aks6d1c6.14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
328	327	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
329		aks6d1c6.15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
330	329	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
331	201	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
332		simpllr 776	. . . . . . . . . . . . . . . . . . . . . 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 42540	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
335		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑣)
336	335	fveq1d 6844	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑣‘𝑡))
337	336	sumeq2dv 15637	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑣 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
338	337	breq1d 5110	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑣 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
339	338	elrab 3648	. . . . . . . . . . . . . . . . . . . . . . 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 5122	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1))
344	198	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
345	3	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
346	5	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
347	2	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
348	4	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
349	6	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
350	215	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
351	15	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
352	327	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
353	329	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
354	201	ad5antr 735	. . . . . . . . . . . . . . . . . . . . 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 42540	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
357		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . 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 5122	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1))
362	315, 317, 343, 361	ifbothda 4520	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1))
363	294, 311, 298, 313, 362	xrletrd 13088	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ≤ (𝐷 − 1))
364	295	rexrd 11194	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ^*)
365	295	ltm1d 12086	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < 𝐷)
366		simpllr 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
367		simplr 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
368	299, 366, 367	jca31 514	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆))
369		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣))
370	368, 369	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)))
371	198	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Field)
372	3	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∈ ℙ)
373	5	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑅 ∈ ℕ)
374	2	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑁 ∈ ℕ)
375	4	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∥ 𝑁)
376	6	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑁 gcd 𝑅) = 1)
377	215	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 < 𝑃)
378	15	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 ∈ ℕ₀)
379	327	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
380	329	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
381	201	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
382		simpllr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
383		simplr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
384		simprl 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣))
385	279	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
386		aks6d1c6lem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (𝑗 ∈ (ℕ₀ × ℕ₀) ↦ ((𝐸‘𝑗)(._g‘(mulGrp‘𝐾))𝑀))
387		aks6d1c6lem3.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))
388	387	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 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 42541	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
390	370, 389	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
391	298, 364, 306, 365, 390	xrltletrd 13087	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
392	294, 298, 306, 363, 391	xrlelttrd 13086	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
393	242, 195, 244, 197	deg1nn0clb 26063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ Ring ∧ ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
394	312, 277, 393	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
395	291, 394	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀)
396	395	nn0red 12475	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ)
397	396	rexrd 11194	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
398		fvexd 6857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
399	398, 301	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
400	399	imaexd 7868	. . . . . . . . . . . . . . . . . . 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 11211	. . . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . . 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 2969	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 ≠ 𝑣 ↔ ¬ 𝑢 = 𝑣))
411	410	necon1bbid 2972	. . . . . . . . . . . . . . . 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 6851	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦)))
419		equequ1 2027	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 ↔ 𝑢 = 𝑦))
420	418, 419	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → ((((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
421	420	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑢 → (¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
422		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → ((𝐻 ↾ 𝑆)‘𝑦) = ((𝐻 ↾ 𝑆)‘𝑣))
423	422	eqeq2d 2748	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣)))
424		equequ2 2028	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (𝑢 = 𝑦 ↔ 𝑢 = 𝑣))
425	423, 424	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
426	425	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
427	421, 426	cbvrex2vw 3221	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
428	427	biimpi 216	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
429	428	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
430	417, 429	r19.29vva 3198	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
431	430	ex 412	. . . . . . . 8 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
432		rexnal2 3120	. . . . . . . . . 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 860	. . . . . 6 ⊢ (𝜑 → ((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
437		ianor 984	. . . . . . . . 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 7210	. . . . . . . . 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 813	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
450		hashss 14344	. . 3 ⊢ (((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V ∧ (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
451	124, 142, 450	syl2anc 585	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
452	119, 147, 151, 449, 451	xrletrd 13088	1 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3401 Vcvv 3442 ⊆ wss 3903 ∅c0 4287 ifcif 4481 {csn 4582 class class class wbr 5100 {copab 5162 ↦ cmpt 5181 × cxp 5630 ^◡ccnv 5631 ran crn 5633 ↾ cres 5634 “ cima 5635 Fn wfn 6495 ⟶wf 6496 –1-1→wf1 6497 ‘cfv 6500 (class class class)co 7368 ∈ cmpo 7370 ↑_m cmap 8775 Fincfn 8895 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 ℝ^*cxr 11177 < clt 11178 ≤ cle 11179 − cmin 11376 / cdiv 11806 ℕcn 12157 ℕ₀cn0 12413 ℕ₀^*cxnn0 12486 ℤcz 12500 ℤ_≥cuz 12763 ...cfz 13435 ↑cexp 13996 Ccbc 14237 ♯chash 14265 Σcsu 15621 ∥ cdvds 16191 gcd cgcd 16433 ℙcprime 16610 Basecbs 17148 +_gcplusg 17189 0_gc0g 17371 Σ_g cgsu 17372 Grpcgrp 18875 -_gcsg 18877 ._gcmg 19009 CMndccmn 19721 mulGrpcmgp 20087 Ringcrg 20180 CRingccrg 20181 RingHom crh 20417 RingIso crs 20418 IDomncidom 20638 Fieldcfield 20675 ℤ_ringczring 21413 ℤRHomczrh 21466 chrcchr 21468 ℤ/nℤczn 21469 algSccascl 21819 var₁cv1 22128 Poly₁cpl1 22129 eval₁ce1 22270 deg₁cdg1 26027 PrimRoots cprimroots 42461

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117 ax-mulf 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-ofr 7633 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-tpos 8178 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-oadd 8411 df-er 8645 df-ec 8647 df-qs 8651 df-map 8777 df-pm 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-sup 9357 df-inf 9358 df-oi 9427 df-dju 9825 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-xnn0 12487 df-z 12501 df-dec 12620 df-uz 12764 df-rp 12918 df-ico 13279 df-fz 13436 df-fzo 13583 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-fac 14209 df-bc 14238 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-clim 15423 df-sum 15622 df-dvds 16192 df-gcd 16434 df-prm 16611 df-phi 16705 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-hom 17213 df-cco 17214 df-0g 17373 df-gsum 17374 df-prds 17379 df-pws 17381 df-imas 17441 df-qus 17442 df-mre 17517 df-mrc 17518 df-acs 17520 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-mhm 18720 df-submnd 18721 df-grp 18878 df-minusg 18879 df-sbg 18880 df-mulg 19010 df-subg 19065 df-nsg 19066 df-eqg 19067 df-ghm 19154 df-cntz 19258 df-od 19469 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100 df-ur 20129 df-srg 20134 df-ring 20182 df-cring 20183 df-oppr 20285 df-dvdsr 20305 df-unit 20306 df-invr 20336 df-dvr 20349 df-rhm 20420 df-rim 20421 df-nzr 20458 df-subrng 20491 df-subrg 20515 df-rlreg 20639 df-domn 20640 df-idom 20641 df-drng 20676 df-field 20677 df-lmod 20825 df-lss 20895 df-lsp 20935 df-sra 21137 df-rgmod 21138 df-lidl 21175 df-rsp 21176 df-2idl 21217 df-cnfld 21322 df-zring 21414 df-zrh 21470 df-chr 21472 df-zn 21473 df-assa 21820 df-asp 21821 df-ascl 21822 df-psr 21877 df-mvr 21878 df-mpl 21879 df-opsr 21881 df-evls 22041 df-evl 22042 df-psr1 22132 df-vr1 22133 df-ply1 22134 df-coe1 22135 df-evl1 22272 df-mdeg 26028 df-deg1 26029 df-mon1 26104 df-uc1p 26105 df-q1p 26106 df-r1p 26107 df-primroots 42462

This theorem is referenced by: aks6d1c6lem4 42543

W3C validator