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 42670

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 2741	. . . . . . . . . . . . 13 ⊢ (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
10	2, 3, 4, 5, 6, 7, 8, 9	hashscontpowcl 42618	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ∈ ℕ₀)
11	1, 10	eqeltrid 2845	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
12	11	nn0zd 12544	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
13	12	zcnd 12629	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
14		1cnd 11135	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
15		aks6d1c6.11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
16	15	nn0cnd 12495	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
17	13, 14, 16	nppcan3d 11528	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = (𝐷 + 𝐴))
18	17	eqcomd 2747	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (𝐴 + 1)))
19		hashfz0 14389	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ₀ → (♯‘(0...𝐴)) = (𝐴 + 1))
20	15, 19	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) = (𝐴 + 1))
21	20	eqcomd 2747	. . . . . . . 8 ⊢ (𝜑 → (𝐴 + 1) = (♯‘(0...𝐴)))
22	21	oveq2d 7375	. . . . . . 7 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = ((𝐷 − 1) + (♯‘(0...𝐴))))
23	18, 22	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (♯‘(0...𝐴))))
24		1zzd 12553	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
25	12, 24	zsubcld 12633	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℤ)
26		0p1e1 12293	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0 + 1) = 1)
28		fvexd 6845	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘(ℤ/nℤ‘𝑅)) ∈ V)
29	8, 28	eqeltrid 2845	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ V)
30	29	imaexd 7860	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V)
31	15	ne0d 4272	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ₀ ≠ ∅)
32	31, 31	jca 517	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅))
33		xpnz 6113	. . . . . . . . . . . . . . 15 ⊢ ((ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅) ↔ (ℕ₀ × ℕ₀) ≠ ∅)
34	32, 33	sylib 220	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ≠ ∅)
35		ovexd 7394	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑙 ∈ ℕ₀) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
36	35	ralrimiva 3133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
37	36	ralrimiva 3133	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
38	7	fnmpo 8013	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V → 𝐸 Fn (ℕ₀ × ℕ₀))
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 Fn (ℕ₀ × ℕ₀))
40		ssidd 3939	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀))
41		fnimaeq0 6621	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 Fn (ℕ₀ × ℕ₀) ∧ (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀)) → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
42	39, 40, 41	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
43	42	necon3bid 2980	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅ ↔ (ℕ₀ × ℕ₀) ≠ ∅))
44	34, 43	mpbird 259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅)
45	5	nnnn0d 12493	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
46	9	zncrng 21522	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℕ₀ → (ℤ/nℤ‘𝑅) ∈ CRing)
47	45, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℤ/nℤ‘𝑅) ∈ CRing)
48		crngring 20220	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ CRing → (ℤ/nℤ‘𝑅) ∈ Ring)
49	8	zrhrhm 21489	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)))
50		zringbas 21431	. . . . . . . . . . . . . . . . . 18 ⊢ ℤ = (Base‘ℤ_ring)
51		eqid 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑅)) = (Base‘(ℤ/nℤ‘𝑅))
52	50, 51	rhmf 20458	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
53	47, 48, 49, 52	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
54	53	ffnd 6659	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 Fn ℤ)
55	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))))
56		simprl 777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑘 = 𝑥)
57	56	oveq2d 7375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → (𝑃↑𝑘) = (𝑃↑𝑥))
58		simprr 779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑙 = 𝑦)
59	58	oveq2d 7375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑦))
60	57, 59	oveq12d 7377	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
61		simplr 775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62		simpr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑦 ∈ ℕ₀)
63		ovexd 7394	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ V)
64	55, 60, 61, 62, 63	ovmpod 7511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
65	3	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℙ)
66		prmnn 16638	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
67	65, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℕ)
68	67	nnzd 12545	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℤ)
69	68, 61	zexpcld 14044	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃↑𝑥) ∈ ℤ)
70	4	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∥ 𝑁)
71	67	nnne0d 12222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ≠ 0)
72	2	nnzd 12545	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℤ)
73	72	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → 𝑁 ∈ ℤ)
74	73	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑁 ∈ ℤ)
75		dvdsval2 16219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
76	68, 71, 74, 75	syl3anc 1380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
77	70, 76	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑁 / 𝑃) ∈ ℤ)
78	77, 62	zexpcld 14044	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑁 / 𝑃)↑𝑦) ∈ ℤ)
79	69, 78	zmulcld 12634	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ ℤ)
80	64, 79	eqeltrd 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) ∈ ℤ)
81	80	ralrimiva 3133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
82	81	ralrimiva 3133	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
83	39, 82	jca 517	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
84		ffnov 7485	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ ↔ (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
85	83, 84	sylibr 236	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸:(ℕ₀ × ℕ₀)⟶ℤ)
86		frn 6665	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ → ran 𝐸 ⊆ ℤ)
87	85, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝐸 ⊆ ℤ)
88		fnima 6618	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 Fn (ℕ₀ × ℕ₀) → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
89	39, 88	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
90	89	sseq1d 3947	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ))
91	87, 90	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ)
92		fnimaeq0 6621	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ) → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
93	54, 91, 92	syl2anc 591	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
94	93	necon3bid 2980	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅))
95	44, 94	mpbird 259	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅)
96		hashge1 14346	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))
97	1	eqcomi 2750	. . . . . . . . . . . . . 14 ⊢ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷
98	97	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷)
99	96, 98	breqtrd 5100	. . . . . . . . . . . 12 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ 𝐷)
100	30, 95, 99	syl2anc 591	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ 𝐷)
101	27, 100	eqbrtrd 5096	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ≤ 𝐷)
102		0red 11143	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
103		1red 11141	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
104	11	nn0red 12494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		leaddsub 11622	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
106	102, 103, 104, 105	syl3anc 1380	. . . . . . . . . 10 ⊢ (𝜑 → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
107	101, 106	mpbid 234	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 − 1))
108	25, 107	jca 517	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
109		elnn0z 12532	. . . . . . . 8 ⊢ ((𝐷 − 1) ∈ ℕ₀ ↔ ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
110	108, 109	sylibr 236	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ₀)
111		fzfid 13930	. . . . . . . 8 ⊢ (𝜑 → (0...𝐴) ∈ Fin)
112		hashcl 14313	. . . . . . . 8 ⊢ ((0...𝐴) ∈ Fin → (♯‘(0...𝐴)) ∈ ℕ₀)
113	111, 112	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℕ₀)
114	110, 113	nn0addcld 12497	. . . . . 6 ⊢ (𝜑 → ((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀)
115	23, 114	eqeltrd 2841	. . . . 5 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℕ₀)
116		bccl 14279	. . . . 5 ⊢ (((𝐷 + 𝐴) ∈ ℕ₀ ∧ (𝐷 − 1) ∈ ℤ) → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
117	115, 25, 116	syl2anc 591	. . . 4 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
118	117	nn0red 12494	. . 3 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ)
119	118	rexrd 11191	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ^*)
120		aks6d1c6.17	. . . . . . 7 ⊢ 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀))
121		ovexd 7394	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
122	121	mptexd 7171	. . . . . . 7 ⊢ (𝜑 → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
123	120, 122	eqeltrid 2845	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ V)
124	123	imaexd 7860	. . . . 5 ⊢ (𝜑 → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V)
125		simprl 777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)))
126	125	ex 414	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))))
127		simpl 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑤)
128	127	fveq1d 6832	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑤‘𝑡))
129	128	sumeq2dv 15659	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑤 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡))
130	129	breq1d 5084	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))
131	130	elrab 3630	. . . . . . . . . . . 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 231	. . . . . . . . . 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 3922	. . . . . . 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 3947	. . . . . . 7 ⊢ (𝜑 → (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) ↔ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴))))
140	136, 139	mpbird 259	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
141		imass2 6060	. . . . . 6 ⊢ (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
142	140, 141	syl 17	. . . . 5 ⊢ (𝜑 → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
143	124, 142	ssexd 5254	. . . 4 ⊢ (𝜑 → (𝐻 “ 𝑆) ∈ V)
144		hashxnn0 14296	. . . 4 ⊢ ((𝐻 “ 𝑆) ∈ V → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
145	143, 144	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
146		xnn0xr 12510	. . 3 ⊢ ((♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^* → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
147	145, 146	syl 17	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
148		hashxnn0 14296	. . . 4 ⊢ ((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
149	124, 148	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
150		xnn0xr 12510	. . 3 ⊢ ((♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^* → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
151	149, 150	syl 17	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
152	110	nn0cnd 12495	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℂ)
153	113	nn0cnd 12495	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℂ)
154	152, 153	pncand 11502	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))) = (𝐷 − 1))
155	154	eqcomd 2747	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) = (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))))
156	23, 155	oveq12d 7377	. . . . . 6 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
157	15	nn0ge0d 12496	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝐴)
158		0zd 12531	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℤ)
159	15	nn0zd 12544	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
160		eluz 12797	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
161	158, 159, 160	syl2anc 591	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
162	157, 161	mpbird 259	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
163		fzn0 13487	. . . . . . . . . 10 ⊢ ((0...𝐴) ≠ ∅ ↔ 𝐴 ∈ (ℤ_≥‘0))
164	162, 163	sylibr 236	. . . . . . . . 9 ⊢ (𝜑 → (0...𝐴) ≠ ∅)
165	110, 111, 164, 137	sticksstones23 42667	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))))
166	113	nn0zd 12544	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℤ)
167		bccmpl 14266	. . . . . . . . 9 ⊢ ((((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀ ∧ (♯‘(0...𝐴)) ∈ ℤ) → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
168	114, 166, 167	syl2anc 591	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
169	165, 168	eqtrd 2776	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
170	169	eqcomd 2747	. . . . . 6 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))) = (♯‘𝑆))
171	156, 170	eqtrd 2776	. . . . 5 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
172	171	adantr 482	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
173	120	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
174		ovexd 7394	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
175	174	mptexd 7171	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
176	173, 175	eqeltrd 2841	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 ∈ V)
177	176	resexd 5986	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆) ∈ V)
178	176	imaexd 7860	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 “ 𝑆) ∈ V)
179		simpr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆))
180		hashf1dmcdm 14401	. . . . 5 ⊢ (((𝐻 ↾ 𝑆) ∈ V ∧ (𝐻 “ 𝑆) ∈ V ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
181	177, 178, 179, 180	syl3anc 1380	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
182	172, 181	eqbrtrd 5096	. . 3 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
183	120	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
184		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ℎ = 𝑗)
185	184	fveq2d 6834	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (𝐺‘ℎ) = (𝐺‘𝑗))
186	185	fveq2d 6834	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ((eval₁‘𝐾)‘(𝐺‘ℎ)) = ((eval₁‘𝐾)‘(𝐺‘𝑗)))
187	186	fveq1d 6832	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
188		simp2 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)) → 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)))
189	188	rabssdv 4007	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴)))
190	137, 189	eqsstrid 3954	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
191	190	sselda 3916	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ (ℕ₀ ↑_m (0...𝐴)))
192		fvexd 6845	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ V)
193	183, 187, 191, 192	fvmptd 6946	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
194		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
195		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
196		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘𝐾)
197		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
198		aks6d1c6.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Field)
199	198	fldcrngd 20717	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ CRing)
200	199	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐾 ∈ CRing)
201		aks6d1c6.16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
202		eqid 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
203	202	crngmgp 20216	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
204	199, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
205		eqid 2741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
206	204, 45, 205	isprimroot 42591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
207	206	biimpd 231	. . . . . . . . . . . . . . . . . . . 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 1149	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
210	202, 196	mgpbas 20120	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
211	210	eqcomi 2750	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
212	209, 211	eleqtrdi 2851	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
213	212	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑀 ∈ (Base‘𝐾))
214		aks6d1c6.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = (chr‘𝐾)
215		aks6d1c6.9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝑃)
216		eqid 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
217		eqid 2741	. . . . . . . . . . . . . . . . . . 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 42633	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
220	219	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
221	220, 191	ffvelcdmd 7029	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺‘𝑗) ∈ (Base‘(Poly₁‘𝐾)))
222	194, 195, 196, 197, 200, 213, 221	fveval1fvcl 22322	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ (Base‘𝐾))
223	193, 222	eqeltrd 2841	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) ∈ (Base‘𝐾))
224		eqid 2741	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗))
225	223, 224	fmptd 7058	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾))
226		fvexd 6845	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ℎ ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) ∈ V)
227	226, 120	fmptd 7058	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:(ℕ₀ ↑_m (0...𝐴))⟶V)
228	227, 190	feqresmpt 6899	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾ 𝑆) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)))
229	228	feq1d 6640	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) ↔ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾)))
230	225, 229	mpbird 259	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾))
231		ffrn 6671	. . . . . . . . . . . 12 ⊢ ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
232	230, 231	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
233		df-ima 5633	. . . . . . . . . . . . 13 ⊢ (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆)
234	233	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆))
235	234	feq3d 6643	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ↔ (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆)))
236	232, 235	mpbird 259	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))
237	236	notnotd 144	. . . . . . . . 9 ⊢ (𝜑 → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))
238	237	a1d 25	. . . . . . . 8 ⊢ (𝜑 → (¬ ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)) → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆)))
239	238	con4d 115	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
240		df-an 398	. . . . . . . . . . . . . 14 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣))
241	240	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣)))
242		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (deg₁‘𝐾) = (deg₁‘𝐾)
243		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
244		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘(Poly₁‘𝐾)) = (0_g‘(Poly₁‘𝐾))
245		fldidom 20746	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn)
246	198, 245	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ IDomn)
247	246	ad4antr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ IDomn)
248	195	ply1crng 22186	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
249		crngring 20220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
250		ringgrp 20213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ Ring → (Poly₁‘𝐾) ∈ Grp)
251	199, 248, 249, 250	4syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Grp)
252	251	ad4antr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (Poly₁‘𝐾) ∈ Grp)
253	198, 3, 214, 15, 215, 216, 217, 218	aks6d1c5 42637	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
254	253	ad4antr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
255		f1f 6726	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
256	254, 255	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
257	137	eleq2i 2833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ 𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
258		simpl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑢)
259	258	fveq1d 6832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑢‘𝑡))
260	259	sumeq2dv 15659	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑢 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
261	260	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑢 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
262	261	elrab 3630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
263	262	simplbi 498	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
264	257, 263	sylbi 219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
265	264	adantl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
266	265	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
267	266	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
268	256, 267	ffvelcdmd 7029	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)))
269	137	eleq2i 2833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 ↔ 𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
270		elrabi 3626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
271	269, 270	sylbi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
272	271	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
273	272	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
274	256, 273	ffvelcdmd 7029	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)))
275		eqid 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
276	197, 275	grpsubcl 18991	. . . . . . . . . . . . . . . . 17 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
277	252, 268, 274, 276	syl3anc 1380	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
278		neqne 2944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑢 = 𝑣 → 𝑢 ≠ 𝑣)
279	278	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → 𝑢 ≠ 𝑣)
280	279	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
281	267, 273	jca 517	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴))))
282		f1fveq 7209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) ∧ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
283	254, 281, 282	syl2anc 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
284	283	bicomd 225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 = 𝑣 ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
285	284	necon3bid 2980	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
286	285	biimpd 231	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 → (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
287	280, 286	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ≠ (𝐺‘𝑣))
288	197, 244, 275	grpsubeq0 18997	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) = (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
289	288	necon3bid 2980	. . . . . . . . . . . . . . . . . 18 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
290	252, 268, 274, 289	syl3anc 1380	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
291	287, 290	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)))
292	195, 197, 242, 194, 243, 244, 247, 277, 291	fta1g 26156	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
293	242, 195, 197	deg1xrcl 26068	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
294	277, 293	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
295	104	ad4antr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ)
296		1red 11141	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 1 ∈ ℝ)
297	295, 296	resubcld 11574	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ)
298	297	rexrd 11191	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ^*)
299		simp-4l 789	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝜑)
300		fvexd 6845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
301		cnvexg 7868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
302	300, 301	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
303	302	imaexd 7860	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V)
304		hashxnn0 14296	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^*)
305		xnn0xr 12510	. . . . . . . . . . . . . . . . . 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 26068	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
308	274, 307	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
309	242, 195, 197	deg1xrcl 26068	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
310	268, 309	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
311	308, 310	ifcld 4503	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ∈ ℝ^*)
312	247	idomringd 20703	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Ring)
313	195, 242, 312, 197, 275, 268, 274	deg1suble 26093	. . . . . . . . . . . . . . . . . 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 5084	. . . . . . . . . . . . . . . . . . 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 5084	. . . . . . . . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
320	3	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
321	5	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
322	2	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
323	4	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
324	6	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
325	215	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
326	15	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
327		aks6d1c6.14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
328	327	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
329		aks6d1c6.15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
330	329	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
331	201	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
332		simpllr 782	. . . . . . . . . . . . . . . . . . . . . 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 42668	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
335		simpl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑣)
336	335	fveq1d 6832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑣‘𝑡))
337	336	sumeq2dv 15659	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑣 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
338	337	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑣 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
339	338	elrab 3630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
340	269, 339	bitri 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝑆 ↔ (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
341	332, 340	sylib 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
342	341	simprd 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1))
343	334, 342	eqbrtrd 5096	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1))
344	198	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
345	3	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
346	5	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
347	2	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
348	4	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
349	6	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
350	215	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
351	15	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
352	327	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
353	329	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
354	201	ad5antr 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
355	267	adantr 482	. . . . . . . . . . . . . . . . . . . . 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 42668	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
357		simp-4r 790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑢 ∈ 𝑆)
358	257, 262	bitri 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
359	357, 358	sylib 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
360	359	simprd 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1))
361	356, 360	eqbrtrd 5096	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1))
362	315, 317, 343, 361	ifbothda 4495	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1))
363	294, 311, 298, 313, 362	xrletrd 13108	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ≤ (𝐷 − 1))
364	295	rexrd 11191	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ^*)
365	295	ltm1d 12083	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < 𝐷)
366		simpllr 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
367		simplr 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
368	299, 366, 367	jca31 520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆))
369		simpr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣))
370	368, 369	jca 517	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)))
371	198	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Field)
372	3	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∈ ℙ)
373	5	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑅 ∈ ℕ)
374	2	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑁 ∈ ℕ)
375	4	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∥ 𝑁)
376	6	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑁 gcd 𝑅) = 1)
377	215	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 < 𝑃)
378	15	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 ∈ ℕ₀)
379	327	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
380	329	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
381	201	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
382		simpllr 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
383		simplr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
384		simprl 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣))
385	279	adantl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
386		aks6d1c6lem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (𝑗 ∈ (ℕ₀ × ℕ₀) ↦ ((𝐸‘𝑗)(._g‘(mulGrp‘𝐾))𝑀))
387		aks6d1c6lem3.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))
388	387	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . 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 42669	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
390	370, 389	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
391	298, 364, 306, 365, 390	xrltletrd 13107	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
392	294, 298, 306, 363, 391	xrlelttrd 13106	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
393	242, 195, 244, 197	deg1nn0clb 26076	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ Ring ∧ ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
394	312, 277, 393	syl2anc 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
395	291, 394	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀)
396	395	nn0red 12494	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ)
397	396	rexrd 11191	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
398		fvexd 6845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
399	398, 301	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
400	399	imaexd 7860	. . . . . . . . . . . . . . . . . . 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 11208	. . . . . . . . . . . . . . . . 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 591	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ↔ ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)))))
405	392, 404	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
406	292, 405	pm2.21dd 197	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
407	406	ex 414	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
408	241, 407	sylbird 262	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
409		biidd 264	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 = 𝑣 ↔ 𝑢 = 𝑣))
410	409	necon3abid 2972	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 ≠ 𝑣 ↔ ¬ 𝑢 = 𝑣))
411	410	necon1bbid 2975	. . . . . . . . . . . . . . . 16 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (¬ ¬ 𝑢 = 𝑣 ↔ 𝑢 = 𝑣))
412	411	pm5.74i 273	. . . . . . . . . . . . . . 15 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
413	412	notbii 322	. . . . . . . . . . . . . 14 ⊢ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
414	413	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
415	414	imbi1d 343	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
416	408, 415	mpbid 234	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
417	416	imp 408	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
418		fveqeq2 6839	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦)))
419		equequ1 2033	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 ↔ 𝑢 = 𝑦))
420	418, 419	imbi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑢 → ((((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
421	420	notbid 320	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
422		fveq2 6830	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → ((𝐻 ↾ 𝑆)‘𝑦) = ((𝐻 ↾ 𝑆)‘𝑣))
423	422	eqeq2d 2752	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣)))
424		equequ2 2034	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → (𝑢 = 𝑦 ↔ 𝑢 = 𝑣))
425	423, 424	imbi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
426	425	notbid 320	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
427	421, 426	cbvrex2vw 3224	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
428	427	bilani 506	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
429	417, 428	r19.29vva 3201	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
430	429	ex 414	. . . . . . . 8 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
431		rexnal2 3123	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))
432	431	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
433	432	imbi1d 343	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
434	430, 433	mpbid 234	. . . . . . 7 ⊢ (𝜑 → (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
435	239, 434	jaod 866	. . . . . 6 ⊢ (𝜑 → ((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
436		ianor 990	. . . . . . . . 9 ⊢ (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
437	436	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
438	437	biimpd 231	. . . . . . 7 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
439	438	imim1d 82	. . . . . 6 ⊢ (𝜑 → (((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
440	435, 439	mpd 15	. . . . 5 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
441		dff13 7201	. . . . . . . . 9 ⊢ ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
442	441	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
443	442	notbid 320	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
444	443	biimpd 231	. . . . . 6 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
445	444	imim1d 82	. . . . 5 ⊢ (𝜑 → ((¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
446	440, 445	mpd 15	. . . 4 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
447	446	imp 408	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
448	182, 447	pm2.61dan 819	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
449		hashss 14366	. . 3 ⊢ (((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V ∧ (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
450	124, 142, 449	syl2anc 591	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
451	119, 147, 151, 448, 450	xrletrd 13108	1 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 397 ∨ wo 854 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∀wral 3055 ∃wrex 3065 {crab 3393 Vcvv 3433 ⊆ wss 3884 ∅c0 4263 ifcif 4456 {csn 4557 class class class wbr 5074 {copab 5136 ↦ cmpt 5155 × cxp 5618 ^◡ccnv 5619 ran crn 5621 ↾ cres 5622 “ cima 5623 Fn wfn 6483 ⟶wf 6484 –1-1→wf1 6485 ‘cfv 6488 (class class class)co 7359 ∈ cmpo 7361 ↑_m cmap 8767 Fincfn 8887 ℝcr 11033 0cc0 11034 1c1 11035 + caddc 11037 · cmul 11039 ℝ^*cxr 11174 < clt 11175 ≤ cle 11176 − cmin 11373 / cdiv 11803 ℕcn 12169 ℕ₀cn0 12432 ℕ₀^*cxnn0 12505 ℤcz 12519 ℤ_≥cuz 12783 ...cfz 13456 ↑cexp 14018 Ccbc 14259 ♯chash 14287 Σcsu 15643 ∥ cdvds 16216 gcd cgcd 16458 ℙcprime 16635 Basecbs 17174 +_gcplusg 17215 0_gc0g 17397 Σ_g cgsu 17398 Grpcgrp 18904 -_gcsg 18906 ._gcmg 19038 CMndccmn 19749 mulGrpcmgp 20115 Ringcrg 20208 CRingccrg 20209 RingHom crh 20443 RingIso crs 20444 IDomncidom 20668 Fieldcfield 20705 ℤ_ringczring 21424 ℤRHomczrh 21477 chrcchr 21479 ℤ/nℤczn 21480 algSccascl 21830 var₁cv1 22164 Poly₁cpl1 22165 eval₁ce1 22303 deg₁cdg1 26040 PrimRoots cprimroots 42589

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7681 ax-inf2 9557 ax-cnex 11090 ax-resscn 11091 ax-1cn 11092 ax-icn 11093 ax-addcl 11094 ax-addrcl 11095 ax-mulcl 11096 ax-mulrcl 11097 ax-mulcom 11098 ax-addass 11099 ax-mulass 11100 ax-distr 11101 ax-i2m1 11102 ax-1ne0 11103 ax-1rid 11104 ax-rnegex 11105 ax-rrecex 11106 ax-cnre 11107 ax-pre-lttri 11108 ax-pre-lttrn 11109 ax-pre-ltadd 11110 ax-pre-mulgt0 11111 ax-pre-sup 11112 ax-addf 11113 ax-mulf 11114

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3725 df-csb 3833 df-dif 3887 df-un 3889 df-in 3891 df-ss 3901 df-pss 3904 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4841 df-int 4880 df-iun 4925 df-iin 4926 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-se 5574 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7316 df-ov 7362 df-oprab 7363 df-mpo 7364 df-of 7623 df-ofr 7624 df-om 7810 df-1st 7933 df-2nd 7934 df-supp 8103 df-tpos 8168 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8343 df-1o 8399 df-2o 8400 df-oadd 8403 df-er 8637 df-ec 8639 df-qs 8643 df-map 8769 df-pm 8770 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-sup 9349 df-inf 9350 df-oi 9419 df-dju 9820 df-card 9858 df-pnf 11177 df-mnf 11178 df-xr 11179 df-ltxr 11180 df-le 11181 df-sub 11375 df-neg 11376 df-div 11804 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-7 12244 df-8 12245 df-9 12246 df-n0 12433 df-xnn0 12506 df-z 12520 df-dec 12640 df-uz 12784 df-rp 12938 df-ico 13299 df-fz 13457 df-fzo 13604 df-fl 13746 df-mod 13824 df-seq 13959 df-exp 14019 df-fac 14231 df-bc 14260 df-hash 14288 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-clim 15445 df-sum 15644 df-dvds 16217 df-gcd 16459 df-prm 16636 df-phi 16731 df-struct 17112 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-starv 17230 df-sca 17231 df-vsca 17232 df-ip 17233 df-tset 17234 df-ple 17235 df-ds 17237 df-unif 17238 df-hom 17239 df-cco 17240 df-0g 17399 df-gsum 17400 df-prds 17405 df-pws 17407 df-imas 17467 df-qus 17468 df-mre 17543 df-mrc 17544 df-acs 17546 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-mhm 18746 df-submnd 18747 df-grp 18907 df-minusg 18908 df-sbg 18909 df-mulg 19039 df-subg 19094 df-nsg 19095 df-eqg 19096 df-ghm 19183 df-cntz 19286 df-od 19497 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-srg 20162 df-ring 20210 df-cring 20211 df-oppr 20311 df-dvdsr 20331 df-unit 20332 df-invr 20362 df-dvr 20375 df-rhm 20446 df-rim 20447 df-nzr 20488 df-subrng 20521 df-subrg 20545 df-rlreg 20669 df-domn 20670 df-idom 20671 df-drng 20706 df-field 20707 df-lmod 20855 df-lss 20925 df-lsp 20965 df-sra 21166 df-rgmod 21167 df-lidl 21204 df-rsp 21205 df-2idl 21246 df-cnfld 21351 df-zring 21425 df-zrh 21481 df-chr 21483 df-zn 21484 df-assa 21831 df-asp 21832 df-ascl 21833 df-psr 21887 df-mvr 21888 df-mpl 21889 df-opsr 21891 df-evls 22053 df-evl 22054 df-psr1 22168 df-vr1 22169 df-ply1 22170 df-coe1 22171 df-evl1 22305 df-mdeg 26041 df-deg1 26042 df-mon1 26117 df-uc1p 26118 df-q1p 26119 df-r1p 26120 df-primroots 42590

This theorem is referenced by: aks6d1c6lem4 42671

W3C validator