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 42997

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 2765	. . . . . . . . . . . . 13 ⊢ (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
10	2, 3, 4, 5, 6, 7, 8, 9	hashscontpowcl 42945	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ∈ ℕ₀)
11	1, 10	eqeltrid 2869	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
12	11	nn0zd 12631	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
13	12	zcnd 12717	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
14		1cnd 11217	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
15		aks6d1c6.11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
16	15	nn0cnd 12582	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
17	13, 14, 16	nppcan3d 11611	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = (𝐷 + 𝐴))
18	17	eqcomd 2771	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (𝐴 + 1)))
19		hashfz0 14487	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ₀ → (♯‘(0...𝐴)) = (𝐴 + 1))
20	15, 19	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) = (𝐴 + 1))
21	20	eqcomd 2771	. . . . . . . 8 ⊢ (𝜑 → (𝐴 + 1) = (♯‘(0...𝐴)))
22	21	oveq2d 7435	. . . . . . 7 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = ((𝐷 − 1) + (♯‘(0...𝐴))))
23	18, 22	eqtrd 2800	. . . . . 6 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (♯‘(0...𝐴))))
24		1zzd 12640	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
25	12, 24	zsubcld 12721	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℤ)
26		0p1e1 12376	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0 + 1) = 1)
28		fvexd 6900	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘(ℤ/nℤ‘𝑅)) ∈ V)
29	8, 28	eqeltrid 2869	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ V)
30	29	imaexd 7919	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V)
31	15	ne0d 4295	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ₀ ≠ ∅)
32	31, 31	jca 521	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅))
33		xpnz 6158	. . . . . . . . . . . . . . 15 ⊢ ((ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅) ↔ (ℕ₀ × ℕ₀) ≠ ∅)
34	32, 33	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ≠ ∅)
35		ovexd 7454	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑙 ∈ ℕ₀) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
36	35	ralrimiva 3159	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
37	36	ralrimiva 3159	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
38	7	fnmpo 8072	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V → 𝐸 Fn (ℕ₀ × ℕ₀))
39	37, 38	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 Fn (ℕ₀ × ℕ₀))
40		ssidd 3961	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀))
41		fnimaeq0 6672	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 Fn (ℕ₀ × ℕ₀) ∧ (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀)) → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
42	39, 40, 41	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
43	42	necon3bid 3004	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅ ↔ (ℕ₀ × ℕ₀) ≠ ∅))
44	34, 43	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅)
45	5	nnnn0d 12580	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
46	9	zncrng 21744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℕ₀ → (ℤ/nℤ‘𝑅) ∈ CRing)
47	45, 46	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℤ/nℤ‘𝑅) ∈ CRing)
48		crngring 20371	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ CRing → (ℤ/nℤ‘𝑅) ∈ Ring)
49	8	zrhrhm 21711	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)))
50		zringbas 21653	. . . . . . . . . . . . . . . . . 18 ⊢ ℤ = (Base‘ℤ_ring)
51		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑅)) = (Base‘(ℤ/nℤ‘𝑅))
52	50, 51	rhmf 20613	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
53	47, 48, 49, 52	4syl 20	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
54	53	ffnd 6710	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 Fn ℤ)
55	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))))
56		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑘 = 𝑥)
57	56	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → (𝑃↑𝑘) = (𝑃↑𝑥))
58		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑙 = 𝑦)
59	58	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑦))
60	57, 59	oveq12d 7437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
61		simplr 781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑦 ∈ ℕ₀)
63		ovexd 7454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ V)
64	55, 60, 61, 62, 63	ovmpod 7571	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
65	3	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℙ)
66		prmnn 16754	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
67	65, 66	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℕ)
68	67	nnzd 12632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℤ)
69	68, 61	zexpcld 14141	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃↑𝑥) ∈ ℤ)
70	4	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∥ 𝑁)
71	67	nnne0d 12301	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ≠ 0)
72	2	nnzd 12632	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℤ)
73	72	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → 𝑁 ∈ ℤ)
74	73	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑁 ∈ ℤ)
75		dvdsval2 16335	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
76	68, 71, 74, 75	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
77	70, 76	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑁 / 𝑃) ∈ ℤ)
78	77, 62	zexpcld 14141	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑁 / 𝑃)↑𝑦) ∈ ℤ)
79	69, 78	zmulcld 12722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ ℤ)
80	64, 79	eqeltrd 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) ∈ ℤ)
81	80	ralrimiva 3159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
82	81	ralrimiva 3159	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
83	39, 82	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
84		ffnov 7545	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ ↔ (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
85	83, 84	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸:(ℕ₀ × ℕ₀)⟶ℤ)
86		frn 6717	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ → ran 𝐸 ⊆ ℤ)
87	85, 86	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝐸 ⊆ ℤ)
88		fnima 6669	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 Fn (ℕ₀ × ℕ₀) → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
89	39, 88	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
90	89	sseq1d 3969	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ))
91	87, 90	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ)
92		fnimaeq0 6672	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ) → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
93	54, 91, 92	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
94	93	necon3bid 3004	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅))
95	44, 94	mpbird 260	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅)
96		hashge1 14443	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))
97	1	eqcomi 2774	. . . . . . . . . . . . . 14 ⊢ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷
98	97	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷)
99	96, 98	breqtrd 5139	. . . . . . . . . . . 12 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ 𝐷)
100	30, 95, 99	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ 𝐷)
101	27, 100	eqbrtrd 5135	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ≤ 𝐷)
102		0red 11226	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
103		1red 11224	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
104	11	nn0red 12581	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		leaddsub 11705	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
106	102, 103, 104, 105	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
107	101, 106	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 − 1))
108	25, 107	jca 521	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
109		elnn0z 12619	. . . . . . . 8 ⊢ ((𝐷 − 1) ∈ ℕ₀ ↔ ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
110	108, 109	sylibr 237	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ₀)
111		fzfid 14027	. . . . . . . 8 ⊢ (𝜑 → (0...𝐴) ∈ Fin)
112		hashcl 14410	. . . . . . . 8 ⊢ ((0...𝐴) ∈ Fin → (♯‘(0...𝐴)) ∈ ℕ₀)
113	111, 112	syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℕ₀)
114	110, 113	nn0addcld 12584	. . . . . 6 ⊢ (𝜑 → ((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀)
115	23, 114	eqeltrd 2865	. . . . 5 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℕ₀)
116		bccl 14376	. . . . 5 ⊢ (((𝐷 + 𝐴) ∈ ℕ₀ ∧ (𝐷 − 1) ∈ ℤ) → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
117	115, 25, 116	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
118	117	nn0red 12581	. . 3 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ)
119	118	rexrd 11274	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ^*)
120		aks6d1c6.17	. . . . . . 7 ⊢ 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀))
121		ovexd 7454	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
122	121	mptexd 7229	. . . . . . 7 ⊢ (𝜑 → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
123	120, 122	eqeltrid 2869	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ V)
124	123	imaexd 7919	. . . . 5 ⊢ (𝜑 → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V)
125		simprl 783	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)))
126	125	ex 418	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))))
127		simpl 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑤)
128	127	fveq1d 6887	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑤‘𝑡))
129	128	sumeq2dv 15777	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑤 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡))
130	129	breq1d 5121	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))
131	130	elrab 3652	. . . . . . . . . . . 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 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))))
134	133	imim1d 83	. . . . . . . . 9 ⊢ (𝜑 → (((𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)))))
135	126, 134	mpd 16	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))))
136	135	ssrdv 3944	. . . . . . 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 3969	. . . . . . 7 ⊢ (𝜑 → (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) ↔ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴))))
140	136, 139	mpbird 260	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
141		imass2 6106	. . . . . 6 ⊢ (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
142	140, 141	syl 18	. . . . 5 ⊢ (𝜑 → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
143	124, 142	ssexd 5297	. . . 4 ⊢ (𝜑 → (𝐻 “ 𝑆) ∈ V)
144		hashxnn0 14393	. . . 4 ⊢ ((𝐻 “ 𝑆) ∈ V → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
145	143, 144	syl 18	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
146		xnn0xr 12597	. . 3 ⊢ ((♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^* → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
147	145, 146	syl 18	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
148		hashxnn0 14393	. . . 4 ⊢ ((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
149	124, 148	syl 18	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
150		xnn0xr 12597	. . 3 ⊢ ((♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^* → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
151	149, 150	syl 18	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
152	110	nn0cnd 12582	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℂ)
153	113	nn0cnd 12582	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℂ)
154	152, 153	pncand 11585	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))) = (𝐷 − 1))
155	154	eqcomd 2771	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) = (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))))
156	23, 155	oveq12d 7437	. . . . . 6 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
157	15	nn0ge0d 12583	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝐴)
158		0zd 12618	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℤ)
159	15	nn0zd 12631	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
160		eluz 12892	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
161	158, 159, 160	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
162	157, 161	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
163		fzn0 13582	. . . . . . . . . 10 ⊢ ((0...𝐴) ≠ ∅ ↔ 𝐴 ∈ (ℤ_≥‘0))
164	162, 163	sylibr 237	. . . . . . . . 9 ⊢ (𝜑 → (0...𝐴) ≠ ∅)
165	110, 111, 164, 137	sticksstones23 42994	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))))
166	113	nn0zd 12631	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℤ)
167		bccmpl 14363	. . . . . . . . 9 ⊢ ((((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀ ∧ (♯‘(0...𝐴)) ∈ ℤ) → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
168	114, 166, 167	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
169	165, 168	eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
170	169	eqcomd 2771	. . . . . 6 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))) = (♯‘𝑆))
171	156, 170	eqtrd 2800	. . . . 5 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
172	171	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
173	120	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
174		ovexd 7454	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
175	174	mptexd 7229	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
176	173, 175	eqeltrd 2865	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 ∈ V)
177	176	resexd 6029	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆) ∈ V)
178	176	imaexd 7919	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 “ 𝑆) ∈ V)
179		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆))
180		hashf1dmcdm 14499	. . . . 5 ⊢ (((𝐻 ↾ 𝑆) ∈ V ∧ (𝐻 “ 𝑆) ∈ V ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
181	177, 178, 179, 180	syl3anc 1398	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
182	172, 181	eqbrtrd 5135	. . 3 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
183	120	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
184		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ℎ = 𝑗)
185	184	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (𝐺‘ℎ) = (𝐺‘𝑗))
186	185	fveq2d 6889	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ((eval₁‘𝐾)‘(𝐺‘ℎ)) = ((eval₁‘𝐾)‘(𝐺‘𝑗)))
187	186	fveq1d 6887	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
188		simp2 1155	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)) → 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)))
189	188	rabssdv 4029	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴)))
190	137, 189	eqsstrid 3976	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
191	190	sselda 3938	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ (ℕ₀ ↑_m (0...𝐴)))
192		fvexd 6900	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ V)
193	183, 187, 191, 192	fvmptd 7001	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
194		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
195		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
196		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘𝐾)
197		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
198		aks6d1c6.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Field)
199	198	fldcrngd 20892	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ CRing)
200	199	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐾 ∈ CRing)
201		aks6d1c6.16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
202		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
203	202	crngmgp 20367	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
204	199, 203	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
205		eqid 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
206	204, 45, 205	isprimroot 42918	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
207	206	biimpd 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
208	201, 207	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣)))
209	208	simp1d 1160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
210	202, 196	mgpbas 20265	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
211	210	eqcomi 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
212	209, 211	eleqtrdi 2875	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
213	212	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑀 ∈ (Base‘𝐾))
214		aks6d1c6.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = (chr‘𝐾)
215		aks6d1c6.9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝑃)
216		eqid 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
217		eqid 2765	. . . . . . . . . . . . . . . . . . 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 42960	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
220	219	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
221	220, 191	ffvelcdmd 7084	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺‘𝑗) ∈ (Base‘(Poly₁‘𝐾)))
222	194, 195, 196, 197, 200, 213, 221	fveval1fvcl 22543	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ (Base‘𝐾))
223	193, 222	eqeltrd 2865	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) ∈ (Base‘𝐾))
224		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗))
225	223, 224	fmptd 7113	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾))
226		fvexd 6900	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ℎ ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) ∈ V)
227	226, 120	fmptd 7113	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:(ℕ₀ ↑_m (0...𝐴))⟶V)
228	227, 190	feqresmpt 6954	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾ 𝑆) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)))
229	228	feq1d 6691	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) ↔ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾)))
230	225, 229	mpbird 260	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾))
231		ffrn 6723	. . . . . . . . . . . 12 ⊢ ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
232	230, 231	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
233		df-ima 5676	. . . . . . . . . . . . 13 ⊢ (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆)
234	233	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆))
235	234	feq3d 6694	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ↔ (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆)))
236	232, 235	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))
237	236	notnotd 145	. . . . . . . . 9 ⊢ (𝜑 → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))
238	237	a1d 26	. . . . . . . 8 ⊢ (𝜑 → (¬ ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)) → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆)))
239	238	con4d 116	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
240		df-an 402	. . . . . . . . . . . . . 14 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣))
241	240	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣)))
242		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (deg₁‘𝐾) = (deg₁‘𝐾)
243		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
244		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘(Poly₁‘𝐾)) = (0_g‘(Poly₁‘𝐾))
245		fldidom 20925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn)
246	198, 245	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ IDomn)
247	246	ad4antr 745	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ IDomn)
248	195	ply1crng 22408	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
249		crngring 20371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
250		ringgrp 20364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ Ring → (Poly₁‘𝐾) ∈ Grp)
251	199, 248, 249, 250	4syl 20	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Grp)
252	251	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (Poly₁‘𝐾) ∈ Grp)
253	198, 3, 214, 15, 215, 216, 217, 218	aks6d1c5 42964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
254	253	ad4antr 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
255		f1f 6778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
256	254, 255	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
257	137	eleq2i 2857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ 𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
258		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑢)
259	258	fveq1d 6887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑢‘𝑡))
260	259	sumeq2dv 15777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑢 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
261	260	breq1d 5121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑢 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
262	261	elrab 3652	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
263	262	simplbi 502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
264	257, 263	sylbi 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
265	264	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
266	265	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
267	266	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
268	256, 267	ffvelcdmd 7084	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)))
269	137	eleq2i 2857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 ↔ 𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
270		elrabi 3648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
271	269, 270	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
272	271	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
273	272	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
274	256, 273	ffvelcdmd 7084	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)))
275		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
276	197, 275	grpsubcl 19130	. . . . . . . . . . . . . . . . 17 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
277	252, 268, 274, 276	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
278		neqne 2968	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑢 = 𝑣 → 𝑢 ≠ 𝑣)
279	278	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → 𝑢 ≠ 𝑣)
280	279	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
281	267, 273	jca 521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴))))
282		f1fveq 7265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) ∧ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
283	254, 281, 282	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
284	283	bicomd 226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 = 𝑣 ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
285	284	necon3bid 3004	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
286	285	biimpd 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 → (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
287	280, 286	mpd 16	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ≠ (𝐺‘𝑣))
288	197, 244, 275	grpsubeq0 19136	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) = (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
289	288	necon3bid 3004	. . . . . . . . . . . . . . . . . 18 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
290	252, 268, 274, 289	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
291	287, 290	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)))
292	195, 197, 242, 194, 243, 244, 247, 277, 291	fta1g 26378	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
293	242, 195, 197	deg1xrcl 26290	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
294	277, 293	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
295	104	ad4antr 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ)
296		1red 11224	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 1 ∈ ℝ)
297	295, 296	resubcld 11657	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ)
298	297	rexrd 11274	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ^*)
299		simp-4l 795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝜑)
300		fvexd 6900	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
301		cnvexg 7927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
302	300, 301	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
303	302	imaexd 7919	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V)
304		hashxnn0 14393	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^*)
305		xnn0xr 12597	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^* → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
306	299, 303, 304, 305	4syl 20	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
307	242, 195, 197	deg1xrcl 26290	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
308	274, 307	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
309	242, 195, 197	deg1xrcl 26290	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
310	268, 309	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
311	308, 310	ifcld 4536	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ∈ ℝ^*)
312	247	idomringd 20876	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Ring)
313	195, 242, 312, 197, 275, 268, 274	deg1suble 26315	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ≤ if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
314		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
315	314	breq1d 5121	. . . . . . . . . . . . . . . . . . 19 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → (((deg₁‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1) ↔ if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1)))
316		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑢)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
317	316	breq1d 5121	. . . . . . . . . . . . . . . . . . 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 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
320	3	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
321	5	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
322	2	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
323	4	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
324	6	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
325	215	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
326	15	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
327		aks6d1c6.14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
328	327	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
329		aks6d1c6.15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
330	329	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
331	201	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
332		simpllr 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑣 ∈ 𝑆)
333	332, 271	syl 18	. . . . . . . . . . . . . . . . . . . . 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 42995	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
335		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑣)
336	335	fveq1d 6887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑣‘𝑡))
337	336	sumeq2dv 15777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑣 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
338	337	breq1d 5121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑣 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
339	338	elrab 3652	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
340	269, 339	bitri 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝑆 ↔ (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
341	332, 340	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
342	341	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1))
343	334, 342	eqbrtrd 5135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1))
344	198	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
345	3	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
346	5	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
347	2	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
348	4	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
349	6	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
350	215	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
351	15	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
352	327	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
353	329	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
354	201	ad5antr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
355	267	adantr 486	. . . . . . . . . . . . . . . . . . . . 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 42995	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
357		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑢 ∈ 𝑆)
358	257, 262	bitri 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
359	357, 358	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
360	359	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1))
361	356, 360	eqbrtrd 5135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1))
362	315, 317, 343, 361	ifbothda 4528	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1))
363	294, 311, 298, 313, 362	xrletrd 13203	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ≤ (𝐷 − 1))
364	295	rexrd 11274	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ^*)
365	295	ltm1d 12162	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < 𝐷)
366		simpllr 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
367		simplr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
368	299, 366, 367	jca31 524	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆))
369		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣))
370	368, 369	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)))
371	198	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Field)
372	3	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∈ ℙ)
373	5	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑅 ∈ ℕ)
374	2	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑁 ∈ ℕ)
375	4	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∥ 𝑁)
376	6	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑁 gcd 𝑅) = 1)
377	215	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 < 𝑃)
378	15	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 ∈ ℕ₀)
379	327	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
380	329	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
381	201	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
382		simpllr 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
383		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
384		simprl 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣))
385	279	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
386		aks6d1c6lem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (𝑗 ∈ (ℕ₀ × ℕ₀) ↦ ((𝐸‘𝑗)(._g‘(mulGrp‘𝐾))𝑀))
387		aks6d1c6lem3.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))
388	387	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 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 42996	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
390	370, 389	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
391	298, 364, 306, 365, 390	xrltletrd 13202	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
392	294, 298, 306, 363, 391	xrlelttrd 13201	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
393	242, 195, 244, 197	deg1nn0clb 26298	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ Ring ∧ ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
394	312, 277, 393	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
395	291, 394	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀)
396	395	nn0red 12581	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ)
397	396	rexrd 11274	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
398		fvexd 6900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
399	398, 301	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
400	399	imaexd 7919	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V)
401	400, 304	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^*)
402	401, 305	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
403		xrltnle 11291	. . . . . . . . . . . . . . . . 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 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ↔ ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)))))
405	392, 404	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
406	292, 405	pm2.21dd 198	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
407	406	ex 418	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
408	241, 407	sylbird 263	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
409		biidd 265	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 = 𝑣 ↔ 𝑢 = 𝑣))
410	409	necon3abid 2996	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 ≠ 𝑣 ↔ ¬ 𝑢 = 𝑣))
411	410	necon1bbid 2999	. . . . . . . . . . . . . . . 16 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (¬ ¬ 𝑢 = 𝑣 ↔ 𝑢 = 𝑣))
412	411	pm5.74i 274	. . . . . . . . . . . . . . 15 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
413	412	notbii 323	. . . . . . . . . . . . . 14 ⊢ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
414	413	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
415	414	imbi1d 344	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
416	408, 415	mpbid 235	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
417	416	imp 412	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
418		fveqeq2 6894	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦)))
419		equequ1 2058	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 ↔ 𝑢 = 𝑦))
420	418, 419	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑢 → ((((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
421	420	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑢 → (¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
422		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → ((𝐻 ↾ 𝑆)‘𝑦) = ((𝐻 ↾ 𝑆)‘𝑣))
423	422	eqeq2d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣)))
424		equequ2 2059	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → (𝑢 = 𝑦 ↔ 𝑢 = 𝑣))
425	423, 424	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
426	425	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑣 → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
427	421, 426	cbvrex2vw 3250	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
428	427	bilani 510	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
429	417, 428	r19.29vva 3227	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
430	429	ex 418	. . . . . . . 8 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
431		rexnal2 3149	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))
432	431	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
433	432	imbi1d 344	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
434	430, 433	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
435	239, 434	jaod 873	. . . . . 6 ⊢ (𝜑 → ((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
436		ianor 997	. . . . . . . . 9 ⊢ (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
437	436	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
438	437	biimpd 232	. . . . . . 7 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
439	438	imim1d 83	. . . . . 6 ⊢ (𝜑 → (((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
440	435, 439	mpd 16	. . . . 5 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
441		dff13 7257	. . . . . . . . 9 ⊢ ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
442	441	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
443	442	notbid 321	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
444	443	biimpd 232	. . . . . 6 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
445	444	imim1d 83	. . . . 5 ⊢ (𝜑 → ((¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
446	440, 445	mpd 16	. . . 4 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
447	446	imp 412	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
448	182, 447	pm2.61dan 825	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
449		hashss 14463	. . 3 ⊢ (((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V ∧ (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
450	124, 142, 449	syl2anc 596	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
451	119, 147, 151, 448, 450	xrletrd 13203	1 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 {crab 3418 Vcvv 3457 ⊆ wss 3906 ∅c0 4286 ifcif 4489 {csn 4591 class class class wbr 5111 {copab 5175 ↦ cmpt 5194 × cxp 5661 ^◡ccnv 5662 ran crn 5664 ↾ cres 5665 “ cima 5666 Fn wfn 6535 ⟶wf 6536 –1-1→wf1 6537 ‘cfv 6540 (class class class)co 7419 ∈ cmpo 7421 ↑_m cmap 8830 Fincfn 8949 ℝcr 11114 0cc0 11115 1c1 11116 + caddc 11118 · cmul 11120 ℝ^*cxr 11257 < clt 11258 ≤ cle 11259 − cmin 11456 / cdiv 11886 ℕcn 12248 ℕ₀cn0 12519 ℕ₀^*cxnn0 12592 ℤcz 12606 ℤ_≥cuz 12878 ...cfz 13551 ↑cexp 14115 Ccbc 14356 ♯chash 14384 Σcsu 15761 ∥ cdvds 16332 gcd cgcd 16574 ℙcprime 16751 Basecbs 17291 +_gcplusg 17332 0_gc0g 17514 Σ_g cgsu 17515 Grpcgrp 19044 -_gcsg 19046 ._gcmg 19177 CMndccmn 19894 mulGrpcmgp 20260 Ringcrg 20359 CRingccrg 20360 RingHom crh 20597 RingIso crs 20598 IDomncidom 20842 Fieldcfield 20878 ℤ_ringczring 21646 ℤRHomczrh 21699 chrcchr 21701 ℤ/nℤczn 21702 algSccascl 22052 var₁cv1 22386 Poly₁cpl1 22387 eval₁ce1 22524 deg₁cdg1 26262 PrimRoots cprimroots 42916

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192 ax-pre-sup 11193 ax-addf 11194 ax-mulf 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-ofr 7685 df-om 7869 df-1st 7992 df-2nd 7993 df-supp 8163 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-er 8700 df-ec 8702 df-qs 8706 df-map 8832 df-pm 8833 df-ixp 8902 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fsupp 9329 df-sup 9409 df-inf 9410 df-oi 9479 df-dju 9903 df-card 9941 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-div 11887 df-nn 12249 df-2 12318 df-3 12319 df-4 12320 df-5 12321 df-6 12322 df-7 12323 df-8 12324 df-9 12325 df-n0 12520 df-xnn0 12593 df-z 12607 df-dec 12728 df-uz 12879 df-rp 13033 df-ico 13394 df-fz 13552 df-fzo 13700 df-fl 13843 df-mod 13921 df-seq 14056 df-exp 14116 df-fac 14328 df-bc 14357 df-hash 14385 df-cj 15174 df-re 15175 df-im 15176 df-sqrt 15310 df-abs 15311 df-clim 15563 df-sum 15762 df-dvds 16333 df-gcd 16575 df-prm 16752 df-phi 16847 df-struct 17229 df-sets 17246 df-slot 17264 df-ndx 17276 df-base 17292 df-ress 17313 df-plusg 17345 df-mulr 17346 df-starv 17347 df-sca 17348 df-vsca 17349 df-ip 17350 df-tset 17351 df-ple 17352 df-ds 17354 df-unif 17355 df-hom 17356 df-cco 17357 df-0g 17516 df-gsum 17517 df-prds 17522 df-pws 17524 df-imas 17584 df-qus 17585 df-mre 17660 df-mrc 17661 df-acs 17663 df-mgm 18720 df-sgrp 18809 df-mnd 18825 df-mhm 18878 df-submnd 18879 df-grp 19047 df-minusg 19048 df-sbg 19049 df-mulg 19178 df-subg 19233 df-nsg 19234 df-eqg 19235 df-ghm 19328 df-cntz 19431 df-od 19642 df-cmn 19896 df-abl 19897 df-mgp 20261 df-rng 20275 df-ur 20308 df-srg 20313 df-ring 20361 df-cring 20362 df-oppr 20465 df-dvdsr 20485 df-unit 20486 df-invr 20516 df-dvr 20529 df-rhm 20600 df-rim 20601 df-nzr 20660 df-subrng 20695 df-subrg 20719 df-rlreg 20843 df-domn 20844 df-idom 20845 df-drng 20879 df-field 20880 df-lmod 21033 df-lss 21103 df-lsp 21143 df-sra 21344 df-rgmod 21345 df-lidl 21382 df-rsp 21383 df-2idl 21439 df-cnfld 21573 df-zring 21647 df-zrh 21703 df-chr 21705 df-zn 21706 df-assa 22053 df-asp 22054 df-ascl 22055 df-psr 22109 df-mvr 22110 df-mpl 22111 df-opsr 22113 df-evls 22275 df-evl 22276 df-psr1 22390 df-vr1 22391 df-ply1 22392 df-coe1 22393 df-evl1 22526 df-mdeg 26263 df-deg1 26264 df-mon1 26339 df-uc1p 26340 df-q1p 26341 df-r1p 26342 df-primroots 42917

This theorem is used by: aks6d1c6lem4 42998

W3C validator