| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aks6d1c6.18 | . . . . . . . . . . . 12
⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) | 
| 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
⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0
↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) | 
| 8 |  | aks6d1c6.13 | . . . . . . . . . . . . 13
⊢ 𝐿 =
(ℤRHom‘(ℤ/nℤ‘𝑅)) | 
| 9 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅) | 
| 10 | 2, 3, 4, 5, 6, 7, 8, 9 | hashscontpowcl 42122 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0) | 
| 11 | 1, 10 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈
ℕ0) | 
| 12 | 11 | nn0zd 12641 | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℤ) | 
| 13 | 12 | zcnd 12725 | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 14 |  | 1cnd 11257 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) | 
| 15 |  | aks6d1c6.11 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℕ0) | 
| 16 | 15 | nn0cnd 12591 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 17 | 13, 14, 16 | nppcan3d 11648 | . . . . . . . 8
⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = (𝐷 + 𝐴)) | 
| 18 | 17 | eqcomd 2742 | . . . . . . 7
⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (𝐴 + 1))) | 
| 19 |  | hashfz0 14472 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℕ0
→ (♯‘(0...𝐴)) = (𝐴 + 1)) | 
| 20 | 15, 19 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (♯‘(0...𝐴)) = (𝐴 + 1)) | 
| 21 | 20 | eqcomd 2742 | . . . . . . . 8
⊢ (𝜑 → (𝐴 + 1) = (♯‘(0...𝐴))) | 
| 22 | 21 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = ((𝐷 − 1) + (♯‘(0...𝐴)))) | 
| 23 | 18, 22 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (♯‘(0...𝐴)))) | 
| 24 |  | 1zzd 12650 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) | 
| 25 | 12, 24 | zsubcld 12729 | . . . . . . . . 9
⊢ (𝜑 → (𝐷 − 1) ∈ ℤ) | 
| 26 |  | 0p1e1 12389 | . . . . . . . . . . . 12
⊢ (0 + 1) =
1 | 
| 27 | 26 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (0 + 1) =
1) | 
| 28 |  | fvexd 6920 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤRHom‘(ℤ/nℤ‘𝑅)) ∈ V) | 
| 29 | 8, 28 | eqeltrid 2844 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ V) | 
| 30 | 29 | imaexd 7939 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ V) | 
| 31 | 15 | ne0d 4341 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℕ0 ≠
∅) | 
| 32 | 31, 31 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℕ0 ≠
∅ ∧ ℕ0 ≠ ∅)) | 
| 33 |  | xpnz 6178 | . . . . . . . . . . . . . . 15
⊢
((ℕ0 ≠ ∅ ∧ ℕ0 ≠
∅) ↔ (ℕ0 × ℕ0) ≠
∅) | 
| 34 | 32, 33 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (ℕ0
× ℕ0) ≠ ∅) | 
| 35 |  | ovexd 7467 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ ℕ0)
→ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V) | 
| 36 | 35 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
∀𝑙 ∈
ℕ0 ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V) | 
| 37 | 36 | ralrimiva 3145 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ∀𝑙 ∈ ℕ0
((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V) | 
| 38 | 7 | fnmpo 8095 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
ℕ0 ∀𝑙 ∈ ℕ0 ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V → 𝐸 Fn (ℕ0 ×
ℕ0)) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 Fn (ℕ0 ×
ℕ0)) | 
| 40 |  | ssidd 4006 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℕ0
× ℕ0) ⊆ (ℕ0 ×
ℕ0)) | 
| 41 |  | fnimaeq0 6700 | . . . . . . . . . . . . . . . 16
⊢ ((𝐸 Fn (ℕ0 ×
ℕ0) ∧ (ℕ0 × ℕ0)
⊆ (ℕ0 × ℕ0)) → ((𝐸 “ (ℕ0
× ℕ0)) = ∅ ↔ (ℕ0 ×
ℕ0) = ∅)) | 
| 42 | 39, 40, 41 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐸 “ (ℕ0 ×
ℕ0)) = ∅ ↔ (ℕ0 ×
ℕ0) = ∅)) | 
| 43 | 42 | necon3bid 2984 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸 “ (ℕ0 ×
ℕ0)) ≠ ∅ ↔ (ℕ0 ×
ℕ0) ≠ ∅)) | 
| 44 | 34, 43 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) ≠ ∅) | 
| 45 | 5 | nnnn0d 12589 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ∈
ℕ0) | 
| 46 | 9 | zncrng 21564 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℕ0
→ (ℤ/nℤ‘𝑅) ∈ CRing) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(ℤ/nℤ‘𝑅) ∈ CRing) | 
| 48 |  | crngring 20243 | . . . . . . . . . . . . . . . . 17
⊢
((ℤ/nℤ‘𝑅) ∈ CRing →
(ℤ/nℤ‘𝑅) ∈ Ring) | 
| 49 | 8 | zrhrhm 21523 | . . . . . . . . . . . . . . . . 17
⊢
((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤring RingHom
(ℤ/nℤ‘𝑅))) | 
| 50 |  | zringbas 21465 | . . . . . . . . . . . . . . . . . 18
⊢ ℤ =
(Base‘ℤring) | 
| 51 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(Base‘(ℤ/nℤ‘𝑅)) =
(Base‘(ℤ/nℤ‘𝑅)) | 
| 52 | 50, 51 | rhmf 20486 | . . . . . . . . . . . . . . . . 17
⊢ (𝐿 ∈ (ℤring
RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅))) | 
| 53 | 47, 48, 49, 52 | 4syl 19 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅))) | 
| 54 | 53 | ffnd 6736 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿 Fn ℤ) | 
| 55 | 7 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝐸 = (𝑘 ∈ ℕ0,
𝑙 ∈
ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)))) | 
| 56 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑘 = 𝑥) | 
| 57 | 56 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → (𝑃↑𝑘) = (𝑃↑𝑥)) | 
| 58 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑙 = 𝑦) | 
| 59 | 58 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑦)) | 
| 60 | 57, 59 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦))) | 
| 61 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝑥 ∈
ℕ0) | 
| 62 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝑦 ∈
ℕ0) | 
| 63 |  | ovexd 7467 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ V) | 
| 64 | 55, 60, 61, 62, 63 | ovmpod 7586 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ (𝑥𝐸𝑦) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦))) | 
| 65 | 3 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝑃 ∈
ℙ) | 
| 66 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 67 | 65, 66 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝑃 ∈
ℕ) | 
| 68 | 67 | nnzd 12642 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝑃 ∈
ℤ) | 
| 69 | 68, 61 | zexpcld 14129 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ (𝑃↑𝑥) ∈
ℤ) | 
| 70 | 4 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝑃 ∥ 𝑁) | 
| 71 | 67 | nnne0d 12317 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝑃 ≠
0) | 
| 72 | 2 | nnzd 12642 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 73 | 72 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝑁 ∈
ℤ) | 
| 74 | 73 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ 𝑁 ∈
ℤ) | 
| 75 |  | dvdsval2 16294 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ)) | 
| 76 | 68, 71, 74, 75 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ)) | 
| 77 | 70, 76 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ (𝑁 / 𝑃) ∈
ℤ) | 
| 78 | 77, 62 | zexpcld 14129 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ ((𝑁 / 𝑃)↑𝑦) ∈ ℤ) | 
| 79 | 69, 78 | zmulcld 12730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ ℤ) | 
| 80 | 64, 79 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0)
→ (𝑥𝐸𝑦) ∈ ℤ) | 
| 81 | 80 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) →
∀𝑦 ∈
ℕ0 (𝑥𝐸𝑦) ∈ ℤ) | 
| 82 | 81 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ∀𝑦 ∈ ℕ0
(𝑥𝐸𝑦) ∈ ℤ) | 
| 83 | 39, 82 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 Fn (ℕ0 ×
ℕ0) ∧ ∀𝑥 ∈ ℕ0 ∀𝑦 ∈ ℕ0
(𝑥𝐸𝑦) ∈ ℤ)) | 
| 84 |  | ffnov 7560 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸:(ℕ0 ×
ℕ0)⟶ℤ ↔ (𝐸 Fn (ℕ0 ×
ℕ0) ∧ ∀𝑥 ∈ ℕ0 ∀𝑦 ∈ ℕ0
(𝑥𝐸𝑦) ∈ ℤ)) | 
| 85 | 83, 84 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸:(ℕ0 ×
ℕ0)⟶ℤ) | 
| 86 |  | frn 6742 | . . . . . . . . . . . . . . . . 17
⊢ (𝐸:(ℕ0 ×
ℕ0)⟶ℤ → ran 𝐸 ⊆ ℤ) | 
| 87 | 85, 86 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran 𝐸 ⊆ ℤ) | 
| 88 |  | fnima 6697 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸 Fn (ℕ0 ×
ℕ0) → (𝐸 “ (ℕ0 ×
ℕ0)) = ran 𝐸) | 
| 89 | 39, 88 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) = ran 𝐸) | 
| 90 | 89 | sseq1d 4014 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ)) | 
| 91 | 87, 90 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ℤ) | 
| 92 |  | fnimaeq0 6700 | . . . . . . . . . . . . . . 15
⊢ ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ0
× ℕ0)) ⊆ ℤ) → ((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) = ∅ ↔ (𝐸 “ (ℕ0 ×
ℕ0)) = ∅)) | 
| 93 | 54, 91, 92 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) = ∅ ↔ (𝐸 “ (ℕ0 ×
ℕ0)) = ∅)) | 
| 94 | 93 | necon3bid 2984 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ≠ ∅ ↔ (𝐸 “ (ℕ0 ×
ℕ0)) ≠ ∅)) | 
| 95 | 44, 94 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ≠ ∅) | 
| 96 |  | hashge1 14429 | . . . . . . . . . . . . 13
⊢ (((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ≠ ∅) → 1 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) | 
| 97 | 1 | eqcomi 2745 | . . . . . . . . . . . . . 14
⊢
(♯‘(𝐿
“ (𝐸 “
(ℕ0 × ℕ0)))) = 𝐷 | 
| 98 | 97 | a1i 11 | . . . . . . . . . . . . 13
⊢ (((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ≠ ∅) → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) = 𝐷) | 
| 99 | 96, 98 | breqtrd 5168 | . . . . . . . . . . . 12
⊢ (((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ≠ ∅) → 1 ≤ 𝐷) | 
| 100 | 30, 95, 99 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ≤ 𝐷) | 
| 101 | 27, 100 | eqbrtrd 5164 | . . . . . . . . . 10
⊢ (𝜑 → (0 + 1) ≤ 𝐷) | 
| 102 |  | 0red 11265 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) | 
| 103 |  | 1red 11263 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) | 
| 104 | 11 | nn0red 12590 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 105 |  | leaddsub 11740 | . . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1))) | 
| 106 | 102, 103,
104, 105 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1))) | 
| 107 | 101, 106 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝐷 − 1)) | 
| 108 | 25, 107 | jca 511 | . . . . . . . 8
⊢ (𝜑 → ((𝐷 − 1) ∈ ℤ ∧ 0 ≤
(𝐷 −
1))) | 
| 109 |  | elnn0z 12628 | . . . . . . . 8
⊢ ((𝐷 − 1) ∈
ℕ0 ↔ ((𝐷 − 1) ∈ ℤ ∧ 0 ≤
(𝐷 −
1))) | 
| 110 | 108, 109 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → (𝐷 − 1) ∈
ℕ0) | 
| 111 |  | fzfid 14015 | . . . . . . . 8
⊢ (𝜑 → (0...𝐴) ∈ Fin) | 
| 112 |  | hashcl 14396 | . . . . . . . 8
⊢
((0...𝐴) ∈ Fin
→ (♯‘(0...𝐴)) ∈
ℕ0) | 
| 113 | 111, 112 | syl 17 | . . . . . . 7
⊢ (𝜑 → (♯‘(0...𝐴)) ∈
ℕ0) | 
| 114 | 110, 113 | nn0addcld 12593 | . . . . . 6
⊢ (𝜑 → ((𝐷 − 1) + (♯‘(0...𝐴))) ∈
ℕ0) | 
| 115 | 23, 114 | eqeltrd 2840 | . . . . 5
⊢ (𝜑 → (𝐷 + 𝐴) ∈
ℕ0) | 
| 116 |  | bccl 14362 | . . . . 5
⊢ (((𝐷 + 𝐴) ∈ ℕ0 ∧ (𝐷 − 1) ∈ ℤ)
→ ((𝐷 + 𝐴)C(𝐷 − 1)) ∈
ℕ0) | 
| 117 | 115, 25, 116 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈
ℕ0) | 
| 118 | 117 | nn0red 12590 | . . 3
⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈
ℝ) | 
| 119 | 118 | rexrd 11312 | . 2
⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈
ℝ*) | 
| 120 |  | aks6d1c6.17 | . . . . . . 7
⊢ 𝐻 = (ℎ ∈ (ℕ0
↑m (0...𝐴))
↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) | 
| 121 |  | ovexd 7467 | . . . . . . . 8
⊢ (𝜑 → (ℕ0
↑m (0...𝐴))
∈ V) | 
| 122 | 121 | mptexd 7245 | . . . . . . 7
⊢ (𝜑 → (ℎ ∈ (ℕ0
↑m (0...𝐴))
↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V) | 
| 123 | 120, 122 | eqeltrid 2844 | . . . . . 6
⊢ (𝜑 → 𝐻 ∈ V) | 
| 124 | 123 | imaexd 7939 | . . . . 5
⊢ (𝜑 → (𝐻 “ (ℕ0
↑m (0...𝐴))) ∈ V) | 
| 125 |  | simprl 770 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))) → 𝑤 ∈ (ℕ0
↑m (0...𝐴))) | 
| 126 | 125 | ex 412 | . . . . . . . . 9
⊢ (𝜑 → ((𝑤 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ0
↑m (0...𝐴)))) | 
| 127 |  | simpl 482 | . . . . . . . . . . . . . . . 16
⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑤) | 
| 128 | 127 | fveq1d 6907 | . . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑤‘𝑡)) | 
| 129 | 128 | sumeq2dv 15739 | . . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑤 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡)) | 
| 130 | 129 | breq1d 5152 | . . . . . . . . . . . . 13
⊢ (𝑠 = 𝑤 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))) | 
| 131 | 130 | elrab 3691 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑤 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))) | 
| 132 | 131 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑤 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))) | 
| 133 | 132 | biimpd 229 | . . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → (𝑤 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))) | 
| 134 | 133 | imim1d 82 | . . . . . . . . 9
⊢ (𝜑 → (((𝑤 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ0
↑m (0...𝐴))) → (𝑤 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ0
↑m (0...𝐴))))) | 
| 135 | 126, 134 | mpd 15 | . . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ0
↑m (0...𝐴)))) | 
| 136 | 135 | ssrdv 3988 | . . . . . . 7
⊢ (𝜑 → {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ0
↑m (0...𝐴))) | 
| 137 |  | aks6d1c6.19 | . . . . . . . . 9
⊢ 𝑆 = {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} | 
| 138 | 137 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 𝑆 = {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)}) | 
| 139 | 138 | sseq1d 4014 | . . . . . . 7
⊢ (𝜑 → (𝑆 ⊆ (ℕ0
↑m (0...𝐴))
↔ {𝑠 ∈
(ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ0
↑m (0...𝐴)))) | 
| 140 | 136, 139 | mpbird 257 | . . . . . 6
⊢ (𝜑 → 𝑆 ⊆ (ℕ0
↑m (0...𝐴))) | 
| 141 |  | imass2 6119 | . . . . . 6
⊢ (𝑆 ⊆ (ℕ0
↑m (0...𝐴))
→ (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ0
↑m (0...𝐴)))) | 
| 142 | 140, 141 | syl 17 | . . . . 5
⊢ (𝜑 → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ0
↑m (0...𝐴)))) | 
| 143 | 124, 142 | ssexd 5323 | . . . 4
⊢ (𝜑 → (𝐻 “ 𝑆) ∈ V) | 
| 144 |  | hashxnn0 14379 | . . . 4
⊢ ((𝐻 “ 𝑆) ∈ V → (♯‘(𝐻 “ 𝑆)) ∈
ℕ0*) | 
| 145 | 143, 144 | syl 17 | . . 3
⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈
ℕ0*) | 
| 146 |  | xnn0xr 12606 | . . 3
⊢
((♯‘(𝐻
“ 𝑆)) ∈
ℕ0* → (♯‘(𝐻 “ 𝑆)) ∈
ℝ*) | 
| 147 | 145, 146 | syl 17 | . 2
⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈
ℝ*) | 
| 148 |  | hashxnn0 14379 | . . . 4
⊢ ((𝐻 “ (ℕ0
↑m (0...𝐴))) ∈ V → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ∈
ℕ0*) | 
| 149 | 124, 148 | syl 17 | . . 3
⊢ (𝜑 → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ∈
ℕ0*) | 
| 150 |  | xnn0xr 12606 | . . 3
⊢
((♯‘(𝐻
“ (ℕ0 ↑m (0...𝐴)))) ∈ ℕ0*
→ (♯‘(𝐻
“ (ℕ0 ↑m (0...𝐴)))) ∈
ℝ*) | 
| 151 | 149, 150 | syl 17 | . 2
⊢ (𝜑 → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ∈
ℝ*) | 
| 152 | 110 | nn0cnd 12591 | . . . . . . . . 9
⊢ (𝜑 → (𝐷 − 1) ∈ ℂ) | 
| 153 | 113 | nn0cnd 12591 | . . . . . . . . 9
⊢ (𝜑 → (♯‘(0...𝐴)) ∈
ℂ) | 
| 154 | 152, 153 | pncand 11622 | . . . . . . . 8
⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴))) −
(♯‘(0...𝐴))) =
(𝐷 −
1)) | 
| 155 | 154 | eqcomd 2742 | . . . . . . 7
⊢ (𝜑 → (𝐷 − 1) = (((𝐷 − 1) + (♯‘(0...𝐴))) −
(♯‘(0...𝐴)))) | 
| 156 | 23, 155 | oveq12d 7450 | . . . . . 6
⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) −
(♯‘(0...𝐴))))) | 
| 157 | 15 | nn0ge0d 12592 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝐴) | 
| 158 |  | 0zd 12627 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℤ) | 
| 159 | 15 | nn0zd 12641 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 160 |  | eluz 12893 | . . . . . . . . . . . 12
⊢ ((0
∈ ℤ ∧ 𝐴
∈ ℤ) → (𝐴
∈ (ℤ≥‘0) ↔ 0 ≤ 𝐴)) | 
| 161 | 158, 159,
160 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ (ℤ≥‘0)
↔ 0 ≤ 𝐴)) | 
| 162 | 157, 161 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘0)) | 
| 163 |  | fzn0 13579 | . . . . . . . . . 10
⊢
((0...𝐴) ≠
∅ ↔ 𝐴 ∈
(ℤ≥‘0)) | 
| 164 | 162, 163 | sylibr 234 | . . . . . . . . 9
⊢ (𝜑 → (0...𝐴) ≠ ∅) | 
| 165 | 110, 111,
164, 137 | sticksstones23 42171 | . . . . . . . 8
⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴)))) | 
| 166 | 113 | nn0zd 12641 | . . . . . . . . 9
⊢ (𝜑 → (♯‘(0...𝐴)) ∈
ℤ) | 
| 167 |  | bccmpl 14349 | . . . . . . . . 9
⊢ ((((𝐷 − 1) +
(♯‘(0...𝐴)))
∈ ℕ0 ∧ (♯‘(0...𝐴)) ∈ ℤ) → (((𝐷 − 1) +
(♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) −
(♯‘(0...𝐴))))) | 
| 168 | 114, 166,
167 | syl2anc 584 | . . . . . . . 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 2742 | . . . . . 6
⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) −
(♯‘(0...𝐴)))) =
(♯‘𝑆)) | 
| 171 | 156, 170 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆)) | 
| 172 | 171 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆)) | 
| 173 | 120 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 = (ℎ ∈ (ℕ0
↑m (0...𝐴))
↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀))) | 
| 174 |  | ovexd 7467 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℕ0
↑m (0...𝐴))
∈ V) | 
| 175 | 174 | mptexd 7245 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℎ ∈ (ℕ0
↑m (0...𝐴))
↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V) | 
| 176 | 173, 175 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 ∈ V) | 
| 177 | 176 | resexd 6045 | . . . . 5
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆) ∈ V) | 
| 178 | 176 | imaexd 7939 | . . . . 5
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 “ 𝑆) ∈ V) | 
| 179 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) | 
| 180 |  | hashf1dmcdm 14484 | . . . . 5
⊢ (((𝐻 ↾ 𝑆) ∈ V ∧ (𝐻 “ 𝑆) ∈ V ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆))) | 
| 181 | 177, 178,
179, 180 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆))) | 
| 182 | 172, 181 | eqbrtrd 5164 | . . 3
⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) | 
| 183 | 120 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐻 = (ℎ ∈ (ℕ0
↑m (0...𝐴))
↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀))) | 
| 184 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ℎ = 𝑗) | 
| 185 | 184 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (𝐺‘ℎ) = (𝐺‘𝑗)) | 
| 186 | 185 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ((eval1‘𝐾)‘(𝐺‘ℎ)) = ((eval1‘𝐾)‘(𝐺‘𝑗))) | 
| 187 | 186 | fveq1d 6907 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀) = (((eval1‘𝐾)‘(𝐺‘𝑗))‘𝑀)) | 
| 188 |  | simp2 1137 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)) → 𝑠 ∈ (ℕ0
↑m (0...𝐴))) | 
| 189 | 188 | rabssdv 4074 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ0
↑m (0...𝐴))) | 
| 190 | 137, 189 | eqsstrid 4021 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ⊆ (ℕ0
↑m (0...𝐴))) | 
| 191 | 190 | sselda 3982 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ (ℕ0
↑m (0...𝐴))) | 
| 192 |  | fvexd 6920 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval1‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ V) | 
| 193 | 183, 187,
191, 192 | fvmptd 7022 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) = (((eval1‘𝐾)‘(𝐺‘𝑗))‘𝑀)) | 
| 194 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(eval1‘𝐾) = (eval1‘𝐾) | 
| 195 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Poly1‘𝐾) = (Poly1‘𝐾) | 
| 196 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 197 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Base‘(Poly1‘𝐾)) =
(Base‘(Poly1‘𝐾)) | 
| 198 |  | aks6d1c6.3 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈ Field) | 
| 199 | 198 | fldcrngd 20743 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ CRing) | 
| 200 | 199 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐾 ∈ CRing) | 
| 201 |  | aks6d1c6.16 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) | 
| 202 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(mulGrp‘𝐾) =
(mulGrp‘𝐾) | 
| 203 | 202 | crngmgp 20239 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐾 ∈ CRing →
(mulGrp‘𝐾) ∈
CMnd) | 
| 204 | 199, 203 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd) | 
| 205 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(.g‘(mulGrp‘𝐾)) =
(.g‘(mulGrp‘𝐾)) | 
| 206 | 204, 45, 205 | isprimroot 42095 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ0
((𝑣(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣)))) | 
| 207 | 206 | biimpd 229 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ0
((𝑣(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣)))) | 
| 208 | 201, 207 | mpd 15 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ0
((𝑣(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))) | 
| 209 | 208 | simp1d 1142 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾))) | 
| 210 | 202, 196 | mgpbas 20143 | . . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝐾) =
(Base‘(mulGrp‘𝐾)) | 
| 211 | 210 | eqcomi 2745 | . . . . . . . . . . . . . . . . . 18
⊢
(Base‘(mulGrp‘𝐾)) = (Base‘𝐾) | 
| 212 | 209, 211 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾)) | 
| 213 | 212 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑀 ∈ (Base‘𝐾)) | 
| 214 |  | aks6d1c6.2 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑃 = (chr‘𝐾) | 
| 215 |  | aks6d1c6.9 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 < 𝑃) | 
| 216 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(var1‘𝐾) = (var1‘𝐾) | 
| 217 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(.g‘(mulGrp‘(Poly1‘𝐾))) =
(.g‘(mulGrp‘(Poly1‘𝐾))) | 
| 218 |  | aks6d1c6.10 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐺 = (𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 219 | 198, 3, 214, 15, 215, 216, 217, 218 | aks6d1c5lem0 42137 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺:(ℕ0 ↑m
(0...𝐴))⟶(Base‘(Poly1‘𝐾))) | 
| 220 | 219 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺:(ℕ0 ↑m
(0...𝐴))⟶(Base‘(Poly1‘𝐾))) | 
| 221 | 220, 191 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺‘𝑗) ∈
(Base‘(Poly1‘𝐾))) | 
| 222 | 194, 195,
196, 197, 200, 213, 221 | fveval1fvcl 22338 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval1‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ (Base‘𝐾)) | 
| 223 | 193, 222 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) ∈ (Base‘𝐾)) | 
| 224 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)) | 
| 225 | 223, 224 | fmptd 7133 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾)) | 
| 226 |  | fvexd 6920 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ℎ ∈ (ℕ0
↑m (0...𝐴))) → (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀) ∈ V) | 
| 227 | 226, 120 | fmptd 7133 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:(ℕ0 ↑m
(0...𝐴))⟶V) | 
| 228 | 227, 190 | feqresmpt 6977 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻 ↾ 𝑆) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗))) | 
| 229 | 228 | feq1d 6719 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) ↔ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾))) | 
| 230 | 225, 229 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾)) | 
| 231 |  | ffrn 6748 | . . . . . . . . . . . 12
⊢ ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆)) | 
| 232 | 230, 231 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆)) | 
| 233 |  | df-ima 5697 | . . . . . . . . . . . . 13
⊢ (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆) | 
| 234 | 233 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆)) | 
| 235 | 234 | feq3d 6722 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ↔ (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))) | 
| 236 | 232, 235 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆)) | 
| 237 | 236 | notnotd 144 | . . . . . . . . 9
⊢ (𝜑 → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆)) | 
| 238 | 237 | a1d 25 | . . . . . . . 8
⊢ (𝜑 → (¬ ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)) → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))) | 
| 239 | 238 | con4d 115 | . . . . . . 7
⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 240 |  | df-an 396 | . . . . . . . . . . . . . 14
⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣)) | 
| 241 | 240 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣))) | 
| 242 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(deg1‘𝐾) = (deg1‘𝐾) | 
| 243 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(0g‘𝐾) = (0g‘𝐾) | 
| 244 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(0g‘(Poly1‘𝐾)) =
(0g‘(Poly1‘𝐾)) | 
| 245 |  | fldidom 20772 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn) | 
| 246 | 198, 245 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ IDomn) | 
| 247 | 246 | ad4antr 732 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ IDomn) | 
| 248 | 195 | ply1crng 22201 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ CRing →
(Poly1‘𝐾)
∈ CRing) | 
| 249 |  | crngring 20243 | . . . . . . . . . . . . . . . . . . 19
⊢
((Poly1‘𝐾) ∈ CRing →
(Poly1‘𝐾)
∈ Ring) | 
| 250 |  | ringgrp 20236 | . . . . . . . . . . . . . . . . . . 19
⊢
((Poly1‘𝐾) ∈ Ring →
(Poly1‘𝐾)
∈ Grp) | 
| 251 | 199, 248,
249, 250 | 4syl 19 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(Poly1‘𝐾)
∈ Grp) | 
| 252 | 251 | ad4antr 732 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (Poly1‘𝐾) ∈ Grp) | 
| 253 | 198, 3, 214, 15, 215, 216, 217, 218 | aks6d1c5 42141 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺:(ℕ0 ↑m
(0...𝐴))–1-1→(Base‘(Poly1‘𝐾))) | 
| 254 | 253 | ad4antr 732 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ0 ↑m
(0...𝐴))–1-1→(Base‘(Poly1‘𝐾))) | 
| 255 |  | f1f 6803 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐺:(ℕ0
↑m (0...𝐴))–1-1→(Base‘(Poly1‘𝐾)) → 𝐺:(ℕ0 ↑m
(0...𝐴))⟶(Base‘(Poly1‘𝐾))) | 
| 256 | 254, 255 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ0 ↑m
(0...𝐴))⟶(Base‘(Poly1‘𝐾))) | 
| 257 | 137 | eleq2i 2832 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ 𝑆 ↔ 𝑢 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)}) | 
| 258 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑢) | 
| 259 | 258 | fveq1d 6907 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑢‘𝑡)) | 
| 260 | 259 | sumeq2dv 15739 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 = 𝑢 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡)) | 
| 261 | 260 | breq1d 5152 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = 𝑢 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1))) | 
| 262 | 261 | elrab 3691 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑢 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1))) | 
| 263 | 262 | simplbi 497 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑢 ∈ (ℕ0
↑m (0...𝐴))) | 
| 264 | 257, 263 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ (ℕ0
↑m (0...𝐴))) | 
| 265 | 264 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ (ℕ0
↑m (0...𝐴))) | 
| 266 | 265 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑢 ∈ (ℕ0
↑m (0...𝐴))) | 
| 267 | 266 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ (ℕ0
↑m (0...𝐴))) | 
| 268 | 256, 267 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ∈
(Base‘(Poly1‘𝐾))) | 
| 269 | 137 | eleq2i 2832 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ 𝑆 ↔ 𝑣 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)}) | 
| 270 |  | elrabi 3686 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑣 ∈ (ℕ0
↑m (0...𝐴))) | 
| 271 | 269, 270 | sylbi 217 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ (ℕ0
↑m (0...𝐴))) | 
| 272 | 271 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ (ℕ0
↑m (0...𝐴))) | 
| 273 | 272 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ (ℕ0
↑m (0...𝐴))) | 
| 274 | 256, 273 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑣) ∈
(Base‘(Poly1‘𝐾))) | 
| 275 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(-g‘(Poly1‘𝐾)) =
(-g‘(Poly1‘𝐾)) | 
| 276 | 197, 275 | grpsubcl 19039 | . . . . . . . . . . . . . . . . 17
⊢
(((Poly1‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈
(Base‘(Poly1‘𝐾)) ∧ (𝐺‘𝑣) ∈
(Base‘(Poly1‘𝐾))) → ((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly1‘𝐾))) | 
| 277 | 252, 268,
274, 276 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly1‘𝐾))) | 
| 278 |  | neqne 2947 | . . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑢 = 𝑣 → 𝑢 ≠ 𝑣) | 
| 279 | 278 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → 𝑢 ≠ 𝑣) | 
| 280 | 279 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣) | 
| 281 | 267, 273 | jca 511 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ∈ (ℕ0
↑m (0...𝐴))
∧ 𝑣 ∈
(ℕ0 ↑m (0...𝐴)))) | 
| 282 |  | f1fveq 7283 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺:(ℕ0
↑m (0...𝐴))–1-1→(Base‘(Poly1‘𝐾)) ∧ (𝑢 ∈ (ℕ0
↑m (0...𝐴))
∧ 𝑣 ∈
(ℕ0 ↑m (0...𝐴)))) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣)) | 
| 283 | 254, 281,
282 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣)) | 
| 284 | 283 | bicomd 223 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 = 𝑣 ↔ (𝐺‘𝑢) = (𝐺‘𝑣))) | 
| 285 | 284 | necon3bid 2984 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣))) | 
| 286 | 285 | biimpd 229 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 → (𝐺‘𝑢) ≠ (𝐺‘𝑣))) | 
| 287 | 280, 286 | mpd 15 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ≠ (𝐺‘𝑣)) | 
| 288 | 197, 244,
275 | grpsubeq0 19045 | . . . . . . . . . . . . . . . . . . 19
⊢
(((Poly1‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈
(Base‘(Poly1‘𝐾)) ∧ (𝐺‘𝑣) ∈
(Base‘(Poly1‘𝐾))) → (((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) =
(0g‘(Poly1‘𝐾)) ↔ (𝐺‘𝑢) = (𝐺‘𝑣))) | 
| 289 | 288 | necon3bid 2984 | . . . . . . . . . . . . . . . . . 18
⊢
(((Poly1‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈
(Base‘(Poly1‘𝐾)) ∧ (𝐺‘𝑣) ∈
(Base‘(Poly1‘𝐾))) → (((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ≠
(0g‘(Poly1‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣))) | 
| 290 | 252, 268,
274, 289 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ≠
(0g‘(Poly1‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣))) | 
| 291 | 287, 290 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ≠
(0g‘(Poly1‘𝐾))) | 
| 292 | 195, 197,
242, 194, 243, 244, 247, 277, 291 | fta1g 26210 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ≤ ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)))) | 
| 293 | 242, 195,
197 | deg1xrcl 26122 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly1‘𝐾)) →
((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ ℝ*) | 
| 294 | 277, 293 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ ℝ*) | 
| 295 | 104 | ad4antr 732 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ) | 
| 296 |  | 1red 11263 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 1 ∈ ℝ) | 
| 297 | 295, 296 | resubcld 11692 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ) | 
| 298 | 297 | rexrd 11312 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈
ℝ*) | 
| 299 |  | simp-4l 782 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝜑) | 
| 300 |  | fvexd 6920 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ V) | 
| 301 |  | cnvexg 7947 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ V → ◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ V) | 
| 302 | 300, 301 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ V) | 
| 303 | 302 | imaexd 7939 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)}) ∈ V) | 
| 304 |  | hashxnn0 14379 | . . . . . . . . . . . . . . . . . 18
⊢ ((◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)}) ∈ V → (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ∈
ℕ0*) | 
| 305 |  | xnn0xr 12606 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ∈ ℕ0* →
(♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ∈ ℝ*) | 
| 306 | 299, 303,
304, 305 | 4syl 19 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ∈ ℝ*) | 
| 307 | 242, 195,
197 | deg1xrcl 26122 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺‘𝑣) ∈
(Base‘(Poly1‘𝐾)) → ((deg1‘𝐾)‘(𝐺‘𝑣)) ∈
ℝ*) | 
| 308 | 274, 307 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘(𝐺‘𝑣)) ∈
ℝ*) | 
| 309 | 242, 195,
197 | deg1xrcl 26122 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺‘𝑢) ∈
(Base‘(Poly1‘𝐾)) → ((deg1‘𝐾)‘(𝐺‘𝑢)) ∈
ℝ*) | 
| 310 | 268, 309 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘(𝐺‘𝑢)) ∈
ℝ*) | 
| 311 | 308, 310 | ifcld 4571 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢))) ∈
ℝ*) | 
| 312 | 247 | idomringd 20729 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Ring) | 
| 313 | 195, 242,
312, 197, 275, 268, 274 | deg1suble 26147 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ≤ if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢)))) | 
| 314 |  | id 22 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((deg1‘𝐾)‘(𝐺‘𝑣)) = if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢))) → ((deg1‘𝐾)‘(𝐺‘𝑣)) = if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢)))) | 
| 315 | 314 | breq1d 5152 | . . . . . . . . . . . . . . . . . . 19
⊢
(((deg1‘𝐾)‘(𝐺‘𝑣)) = if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢))) → (((deg1‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1) ↔
if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1))) | 
| 316 |  | id 22 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((deg1‘𝐾)‘(𝐺‘𝑢)) = if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢))) → ((deg1‘𝐾)‘(𝐺‘𝑢)) = if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢)))) | 
| 317 | 316 | breq1d 5152 | . . . . . . . . . . . . . . . . . . 19
⊢
(((deg1‘𝐾)‘(𝐺‘𝑢)) = if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢))) → (((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1) ↔
if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1))) | 
| 318 |  | aks6d1c6.1 | . . . . . . . . . . . . . . . . . . . . 21
⊢  ∼ =
{〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈
(Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} | 
| 319 | 198 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field) | 
| 320 | 3 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ) | 
| 321 | 5 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ) | 
| 322 | 2 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ) | 
| 323 | 4 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁) | 
| 324 | 6 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1) | 
| 325 | 215 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃) | 
| 326 | 15 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈
ℕ0) | 
| 327 |  | aks6d1c6.14 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼
((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) | 
| 328 | 327 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼
((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) | 
| 329 |  | aks6d1c6.15 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) | 
| 330 | 329 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) | 
| 331 | 201 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) | 
| 332 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑣 ∈ 𝑆) | 
| 333 | 332, 271 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑣 ∈ (ℕ0
↑m (0...𝐴))) | 
| 334 | 318, 214,
319, 320, 321, 322, 323, 324, 325, 218, 326, 7, 8, 328, 330, 331, 120, 1, 137, 333 | aks6d1c6lem1 42172 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → ((deg1‘𝐾)‘(𝐺‘𝑣)) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡)) | 
| 335 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑣) | 
| 336 | 335 | fveq1d 6907 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑣‘𝑡)) | 
| 337 | 336 | sumeq2dv 15739 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 = 𝑣 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡)) | 
| 338 | 337 | breq1d 5152 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = 𝑣 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1))) | 
| 339 | 338 | elrab 3691 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∈ {𝑠 ∈ (ℕ0
↑m (0...𝐴))
∣ Σ𝑡 ∈
(0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑣 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1))) | 
| 340 | 269, 339 | bitri 275 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ 𝑆 ↔ (𝑣 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1))) | 
| 341 | 332, 340 | sylib 218 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → (𝑣 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1))) | 
| 342 | 341 | simprd 495 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)) | 
| 343 | 334, 342 | eqbrtrd 5164 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → ((deg1‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1)) | 
| 344 | 198 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field) | 
| 345 | 3 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ) | 
| 346 | 5 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ) | 
| 347 | 2 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ) | 
| 348 | 4 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁) | 
| 349 | 6 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1) | 
| 350 | 215 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃) | 
| 351 | 15 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈
ℕ0) | 
| 352 | 327 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼
((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) | 
| 353 | 329 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) | 
| 354 | 201 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) | 
| 355 | 267 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑢 ∈ (ℕ0
↑m (0...𝐴))) | 
| 356 | 318, 214,
344, 345, 346, 347, 348, 349, 350, 218, 351, 7, 8, 352, 353, 354, 120, 1, 137, 355 | aks6d1c6lem1 42172 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → ((deg1‘𝐾)‘(𝐺‘𝑢)) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡)) | 
| 357 |  | simp-4r 783 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → 𝑢 ∈ 𝑆) | 
| 358 | 257, 262 | bitri 275 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ 𝑆 ↔ (𝑢 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1))) | 
| 359 | 357, 358 | sylib 218 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → (𝑢 ∈ (ℕ0
↑m (0...𝐴))
∧ Σ𝑡 ∈
(0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1))) | 
| 360 | 359 | simprd 495 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)) | 
| 361 | 356, 360 | eqbrtrd 5164 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣))) → ((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1)) | 
| 362 | 315, 317,
343, 361 | ifbothda 4563 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg1‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑣)), ((deg1‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1)) | 
| 363 | 294, 311,
298, 313, 362 | xrletrd 13205 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ≤ (𝐷 − 1)) | 
| 364 | 295 | rexrd 11312 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈
ℝ*) | 
| 365 | 295 | ltm1d 12201 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < 𝐷) | 
| 366 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆) | 
| 367 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆) | 
| 368 | 299, 366,
367 | jca31 514 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆)) | 
| 369 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) | 
| 370 | 368, 369 | jca 511 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣))) | 
| 371 | 198 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Field) | 
| 372 | 3 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∈ ℙ) | 
| 373 | 5 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑅 ∈ ℕ) | 
| 374 | 2 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑁 ∈ ℕ) | 
| 375 | 4 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∥ 𝑁) | 
| 376 | 6 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑁 gcd 𝑅) = 1) | 
| 377 | 215 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 < 𝑃) | 
| 378 | 15 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 ∈
ℕ0) | 
| 379 | 327 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼
((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) | 
| 380 | 329 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) | 
| 381 | 201 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) | 
| 382 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆) | 
| 383 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆) | 
| 384 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣)) | 
| 385 | 279 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣) | 
| 386 |  | aks6d1c6lem3.1 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝐽 = (𝑗 ∈ (ℕ0 ×
ℕ0) ↦ ((𝐸‘𝑗)(.g‘(mulGrp‘𝐾))𝑀)) | 
| 387 |  | aks6d1c6lem3.2 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 ×
ℕ0)))) | 
| 388 | 387 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 ×
ℕ0)))) | 
| 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 42173 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)}))) | 
| 390 | 370, 389 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)}))) | 
| 391 | 298, 364,
306, 365, 390 | xrltletrd 13204 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)}))) | 
| 392 | 294, 298,
306, 363, 391 | xrlelttrd 13203 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) < (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)}))) | 
| 393 | 242, 195,
244, 197 | deg1nn0clb 26130 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ Ring ∧ ((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly1‘𝐾))) → (((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ≠
(0g‘(Poly1‘𝐾)) ↔ ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ ℕ0)) | 
| 394 | 312, 277,
393 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)) ≠
(0g‘(Poly1‘𝐾)) ↔ ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ ℕ0)) | 
| 395 | 291, 394 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ ℕ0) | 
| 396 | 395 | nn0red 12590 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ ℝ) | 
| 397 | 396 | rexrd 11312 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ ℝ*) | 
| 398 |  | fvexd 6920 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ V) | 
| 399 | 398, 301 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ V) | 
| 400 | 399 | imaexd 7939 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)}) ∈ V) | 
| 401 | 400, 304 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ∈
ℕ0*) | 
| 402 | 401, 305 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ∈ ℝ*) | 
| 403 |  | xrltnle 11329 | . . . . . . . . . . . . . . . . 17
⊢
((((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) ∈ ℝ* ∧
(♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ∈ ℝ*) →
(((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) < (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ↔ ¬ (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ≤ ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))))) | 
| 404 | 397, 402,
403 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) < (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ↔ ¬ (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ≤ ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))))) | 
| 405 | 392, 404 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ¬ (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣))) “ {(0g‘𝐾)})) ≤ ((deg1‘𝐾)‘((𝐺‘𝑢)(-g‘(Poly1‘𝐾))(𝐺‘𝑣)))) | 
| 406 | 292, 405 | pm2.21dd 195 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) | 
| 407 | 406 | ex 412 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 408 | 241, 407 | sylbird 260 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 409 |  | biidd 262 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 = 𝑣 ↔ 𝑢 = 𝑣)) | 
| 410 | 409 | necon3abid 2976 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 ≠ 𝑣 ↔ ¬ 𝑢 = 𝑣)) | 
| 411 | 410 | necon1bbid 2979 | . . . . . . . . . . . . . . . 16
⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (¬ ¬ 𝑢 = 𝑣 ↔ 𝑢 = 𝑣)) | 
| 412 | 411 | pm5.74i 271 | . . . . . . . . . . . . . . 15
⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) | 
| 413 | 412 | notbii 320 | . . . . . . . . . . . . . 14
⊢ (¬
(((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) | 
| 414 | 413 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))) | 
| 415 | 414 | imbi1d 341 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))) | 
| 416 | 408, 415 | mpbid 232 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 417 | 416 | imp 406 | . . . . . . . . . 10
⊢
(((((𝜑 ∧
∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) | 
| 418 |  | fveqeq2 6914 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦))) | 
| 419 |  | equequ1 2023 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 ↔ 𝑢 = 𝑦)) | 
| 420 | 418, 419 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → ((((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦))) | 
| 421 | 420 | notbid 318 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑢 → (¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦))) | 
| 422 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑣 → ((𝐻 ↾ 𝑆)‘𝑦) = ((𝐻 ↾ 𝑆)‘𝑣)) | 
| 423 | 422 | eqeq2d 2747 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑣 → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣))) | 
| 424 |  | equequ2 2024 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑣 → (𝑢 = 𝑦 ↔ 𝑢 = 𝑣)) | 
| 425 | 423, 424 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))) | 
| 426 | 425 | notbid 318 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))) | 
| 427 | 421, 426 | cbvrex2vw 3241 | . . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) | 
| 428 | 427 | biimpi 216 | . . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) | 
| 429 | 428 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) | 
| 430 | 417, 429 | r19.29vva 3215 | . . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) | 
| 431 | 430 | ex 412 | . . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 432 |  | rexnal2 3134 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) | 
| 433 | 432 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))) | 
| 434 | 433 | imbi1d 341 | . . . . . . . 8
⊢ (𝜑 → ((∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))) | 
| 435 | 431, 434 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 436 | 239, 435 | jaod 859 | . . . . . 6
⊢ (𝜑 → ((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 437 |  | ianor 983 | . . . . . . . . 9
⊢ (¬
((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))) | 
| 438 | 437 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))) | 
| 439 | 438 | biimpd 229 | . . . . . . 7
⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))) | 
| 440 | 439 | imim1d 82 | . . . . . 6
⊢ (𝜑 → (((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))) | 
| 441 | 436, 440 | mpd 15 | . . . . 5
⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 442 |  | dff13 7276 | . . . . . . . . 9
⊢ ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))) | 
| 443 | 442 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))) | 
| 444 | 443 | notbid 318 | . . . . . . 7
⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))) | 
| 445 | 444 | biimpd 229 | . . . . . 6
⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))) | 
| 446 | 445 | imim1d 82 | . . . . 5
⊢ (𝜑 → ((¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))) | 
| 447 | 441, 446 | mpd 15 | . . . 4
⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))) | 
| 448 | 447 | imp 406 | . . 3
⊢ ((𝜑 ∧ ¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) | 
| 449 | 182, 448 | pm2.61dan 812 | . 2
⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) | 
| 450 |  | hashss 14449 | . . 3
⊢ (((𝐻 “ (ℕ0
↑m (0...𝐴))) ∈ V ∧ (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ0
↑m (0...𝐴)))) → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴))))) | 
| 451 | 124, 142,
450 | syl2anc 584 | . 2
⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴))))) | 
| 452 | 119, 147,
151, 449, 451 | xrletrd 13205 | 1
⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴))))) |