| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dgraaval 43156 | . . 3
⊢ (𝐴 ∈ 𝔸 →
(degAA‘𝐴)
= inf({𝑎 ∈ ℕ
∣ ∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}, ℝ, < )) | 
| 2 |  | ssrab2 4080 | . . . . 5
⊢ {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ⊆ ℕ | 
| 3 |  | nnuz 12921 | . . . . 5
⊢ ℕ =
(ℤ≥‘1) | 
| 4 | 2, 3 | sseqtri 4032 | . . . 4
⊢ {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ⊆
(ℤ≥‘1) | 
| 5 |  | eldifsn 4786 | . . . . . . . . . . . 12
⊢ (𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ↔ (𝑏 ∈ (Poly‘ℚ) ∧ 𝑏 ≠
0𝑝)) | 
| 6 | 5 | biimpi 216 | . . . . . . . . . . 11
⊢ (𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) → (𝑏 ∈ (Poly‘ℚ) ∧ 𝑏 ≠
0𝑝)) | 
| 7 | 6 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → (𝑏 ∈ (Poly‘ℚ) ∧ 𝑏 ≠
0𝑝)) | 
| 8 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ℂ) | 
| 9 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → (𝑏‘𝐴) = 0) | 
| 10 |  | dgrnznn 26286 | . . . . . . . . . 10
⊢ (((𝑏 ∈ (Poly‘ℚ)
∧ 𝑏 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑏‘𝐴) = 0)) → (deg‘𝑏) ∈ ℕ) | 
| 11 | 7, 8, 9, 10 | syl12anc 837 | . . . . . . . . 9
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → (deg‘𝑏) ∈
ℕ) | 
| 12 |  | simpll 767 | . . . . . . . . 9
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → 𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})) | 
| 13 |  | eqid 2737 | . . . . . . . . . 10
⊢
(deg‘𝑏) =
(deg‘𝑏) | 
| 14 | 9, 13 | jctil 519 | . . . . . . . . 9
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → ((deg‘𝑏) = (deg‘𝑏) ∧ (𝑏‘𝐴) = 0)) | 
| 15 |  | eqeq2 2749 | . . . . . . . . . . 11
⊢ (𝑎 = (deg‘𝑏) → ((deg‘𝑝) = 𝑎 ↔ (deg‘𝑝) = (deg‘𝑏))) | 
| 16 | 15 | anbi1d 631 | . . . . . . . . . 10
⊢ (𝑎 = (deg‘𝑏) → (((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0) ↔ ((deg‘𝑝) = (deg‘𝑏) ∧ (𝑝‘𝐴) = 0))) | 
| 17 |  | fveqeq2 6915 | . . . . . . . . . . 11
⊢ (𝑝 = 𝑏 → ((deg‘𝑝) = (deg‘𝑏) ↔ (deg‘𝑏) = (deg‘𝑏))) | 
| 18 |  | fveq1 6905 | . . . . . . . . . . . 12
⊢ (𝑝 = 𝑏 → (𝑝‘𝐴) = (𝑏‘𝐴)) | 
| 19 | 18 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (𝑝 = 𝑏 → ((𝑝‘𝐴) = 0 ↔ (𝑏‘𝐴) = 0)) | 
| 20 | 17, 19 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑝 = 𝑏 → (((deg‘𝑝) = (deg‘𝑏) ∧ (𝑝‘𝐴) = 0) ↔ ((deg‘𝑏) = (deg‘𝑏) ∧ (𝑏‘𝐴) = 0))) | 
| 21 | 16, 20 | rspc2ev 3635 | . . . . . . . . 9
⊢
(((deg‘𝑏)
∈ ℕ ∧ 𝑏
∈ ((Poly‘ℚ) ∖ {0𝑝}) ∧
((deg‘𝑏) =
(deg‘𝑏) ∧ (𝑏‘𝐴) = 0)) → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)) | 
| 22 | 11, 12, 14, 21 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)) | 
| 23 | 22 | ex 412 | . . . . . . 7
⊢ ((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) → (𝐴 ∈ ℂ → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0))) | 
| 24 | 23 | rexlimiva 3147 | . . . . . 6
⊢
(∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑏‘𝐴) = 0 → (𝐴 ∈ ℂ → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0))) | 
| 25 | 24 | impcom 407 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑏‘𝐴) = 0) → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)) | 
| 26 |  | elqaa 26364 | . . . . 5
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑏‘𝐴) = 0)) | 
| 27 |  | rabn0 4389 | . . . . 5
⊢ ({𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ≠ ∅ ↔ ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)) | 
| 28 | 25, 26, 27 | 3imtr4i 292 | . . . 4
⊢ (𝐴 ∈ 𝔸 → {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ≠ ∅) | 
| 29 |  | infssuzcl 12974 | . . . 4
⊢ (({𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ⊆
(ℤ≥‘1) ∧ {𝑎 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ≠ ∅) → inf({𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}, ℝ, < ) ∈ {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}) | 
| 30 | 4, 28, 29 | sylancr 587 | . . 3
⊢ (𝐴 ∈ 𝔸 →
inf({𝑎 ∈ ℕ
∣ ∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}, ℝ, < ) ∈ {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}) | 
| 31 | 1, 30 | eqeltrd 2841 | . 2
⊢ (𝐴 ∈ 𝔸 →
(degAA‘𝐴)
∈ {𝑎 ∈ ℕ
∣ ∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}) | 
| 32 |  | eqeq2 2749 | . . . . 5
⊢ (𝑎 = (degAA‘𝐴) → ((deg‘𝑝) = 𝑎 ↔ (deg‘𝑝) = (degAA‘𝐴))) | 
| 33 | 32 | anbi1d 631 | . . . 4
⊢ (𝑎 = (degAA‘𝐴) → (((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0) ↔ ((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) | 
| 34 | 33 | rexbidv 3179 | . . 3
⊢ (𝑎 = (degAA‘𝐴) → (∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0) ↔ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) | 
| 35 | 34 | elrab 3692 | . 2
⊢
((degAA‘𝐴) ∈ {𝑎 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ↔
((degAA‘𝐴)
∈ ℕ ∧ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) | 
| 36 | 31, 35 | sylib 218 | 1
⊢ (𝐴 ∈ 𝔸 →
((degAA‘𝐴)
∈ ℕ ∧ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) |