| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simprl 771 | . . . 4
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → 𝐴 ∈ ℂ) | 
| 2 |  | eldifsn 4786 | . . . . . . 7
⊢ (𝑃 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ↔ (𝑃 ∈ (Poly‘ℚ) ∧ 𝑃 ≠
0𝑝)) | 
| 3 | 2 | biimpri 228 | . . . . . 6
⊢ ((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) → 𝑃 ∈ ((Poly‘ℚ) ∖
{0𝑝})) | 
| 4 | 3 | adantr 480 | . . . . 5
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → 𝑃 ∈ ((Poly‘ℚ) ∖
{0𝑝})) | 
| 5 |  | simprr 773 | . . . . 5
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (𝑃‘𝐴) = 0) | 
| 6 |  | fveq1 6905 | . . . . . . 7
⊢ (𝑎 = 𝑃 → (𝑎‘𝐴) = (𝑃‘𝐴)) | 
| 7 | 6 | eqeq1d 2739 | . . . . . 6
⊢ (𝑎 = 𝑃 → ((𝑎‘𝐴) = 0 ↔ (𝑃‘𝐴) = 0)) | 
| 8 | 7 | rspcev 3622 | . . . . 5
⊢ ((𝑃 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑃‘𝐴) = 0) → ∃𝑎 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑎‘𝐴) = 0) | 
| 9 | 4, 5, 8 | syl2anc 584 | . . . 4
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → ∃𝑎 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑎‘𝐴) = 0) | 
| 10 |  | elqaa 26364 | . . . 4
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑎 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑎‘𝐴) = 0)) | 
| 11 | 1, 9, 10 | sylanbrc 583 | . . 3
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → 𝐴 ∈ 𝔸) | 
| 12 |  | dgraaval 43156 | . . 3
⊢ (𝐴 ∈ 𝔸 →
(degAA‘𝐴)
= inf({𝑎 ∈ ℕ
∣ ∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}, ℝ, < )) | 
| 13 | 11, 12 | syl 17 | . 2
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (degAA‘𝐴) = inf({𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}, ℝ, < )) | 
| 14 |  | ssrab2 4080 | . . . 4
⊢ {𝑎 ∈ ℕ ∣
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)} ⊆ ℕ | 
| 15 |  | nnuz 12921 | . . . 4
⊢ ℕ =
(ℤ≥‘1) | 
| 16 | 14, 15 | sseqtri 4032 | . . 3
⊢ {𝑎 ∈ ℕ ∣
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)} ⊆
(ℤ≥‘1) | 
| 17 |  | dgrnznn 26286 | . . . 4
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (deg‘𝑃) ∈ ℕ) | 
| 18 |  | eqid 2737 | . . . . . 6
⊢
(deg‘𝑃) =
(deg‘𝑃) | 
| 19 | 5, 18 | jctil 519 | . . . . 5
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → ((deg‘𝑃) = (deg‘𝑃) ∧ (𝑃‘𝐴) = 0)) | 
| 20 |  | fveqeq2 6915 | . . . . . . 7
⊢ (𝑏 = 𝑃 → ((deg‘𝑏) = (deg‘𝑃) ↔ (deg‘𝑃) = (deg‘𝑃))) | 
| 21 |  | fveq1 6905 | . . . . . . . 8
⊢ (𝑏 = 𝑃 → (𝑏‘𝐴) = (𝑃‘𝐴)) | 
| 22 | 21 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑏 = 𝑃 → ((𝑏‘𝐴) = 0 ↔ (𝑃‘𝐴) = 0)) | 
| 23 | 20, 22 | anbi12d 632 | . . . . . 6
⊢ (𝑏 = 𝑃 → (((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0) ↔ ((deg‘𝑃) = (deg‘𝑃) ∧ (𝑃‘𝐴) = 0))) | 
| 24 | 23 | rspcev 3622 | . . . . 5
⊢ ((𝑃 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ ((deg‘𝑃) = (deg‘𝑃) ∧ (𝑃‘𝐴) = 0)) → ∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0)) | 
| 25 | 4, 19, 24 | syl2anc 584 | . . . 4
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → ∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0)) | 
| 26 |  | eqeq2 2749 | . . . . . . 7
⊢ (𝑎 = (deg‘𝑃) → ((deg‘𝑏) = 𝑎 ↔ (deg‘𝑏) = (deg‘𝑃))) | 
| 27 | 26 | anbi1d 631 | . . . . . 6
⊢ (𝑎 = (deg‘𝑃) → (((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0) ↔ ((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0))) | 
| 28 | 27 | rexbidv 3179 | . . . . 5
⊢ (𝑎 = (deg‘𝑃) → (∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0) ↔ ∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0))) | 
| 29 | 28 | elrab 3692 | . . . 4
⊢
((deg‘𝑃)
∈ {𝑎 ∈ ℕ
∣ ∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)} ↔ ((deg‘𝑃) ∈ ℕ ∧ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0))) | 
| 30 | 17, 25, 29 | sylanbrc 583 | . . 3
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (deg‘𝑃) ∈ {𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}) | 
| 31 |  | infssuzle 12973 | . . 3
⊢ (({𝑎 ∈ ℕ ∣
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)} ⊆
(ℤ≥‘1) ∧ (deg‘𝑃) ∈ {𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}) → inf({𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}, ℝ, < ) ≤
(deg‘𝑃)) | 
| 32 | 16, 30, 31 | sylancr 587 | . 2
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → inf({𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}, ℝ, < ) ≤
(deg‘𝑃)) | 
| 33 | 13, 32 | eqbrtrd 5165 | 1
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (degAA‘𝐴) ≤ (deg‘𝑃)) |