Step | Hyp | Ref
| Expression |
1 | | simprl 771 |
. . . 4
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → 𝐴 ∈ ℂ) |
2 | | eldifsn 4672 |
. . . . . . 7
⊢ (𝑃 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ↔ (𝑃 ∈ (Poly‘ℚ) ∧ 𝑃 ≠
0𝑝)) |
3 | 2 | biimpri 231 |
. . . . . 6
⊢ ((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) → 𝑃 ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
4 | 3 | adantr 484 |
. . . . 5
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → 𝑃 ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
5 | | simprr 773 |
. . . . 5
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (𝑃‘𝐴) = 0) |
6 | | fveq1 6667 |
. . . . . . 7
⊢ (𝑎 = 𝑃 → (𝑎‘𝐴) = (𝑃‘𝐴)) |
7 | 6 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑎 = 𝑃 → ((𝑎‘𝐴) = 0 ↔ (𝑃‘𝐴) = 0)) |
8 | 7 | rspcev 3524 |
. . . . 5
⊢ ((𝑃 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑃‘𝐴) = 0) → ∃𝑎 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑎‘𝐴) = 0) |
9 | 4, 5, 8 | syl2anc 587 |
. . . 4
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → ∃𝑎 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑎‘𝐴) = 0) |
10 | | elqaa 25062 |
. . . 4
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑎 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑎‘𝐴) = 0)) |
11 | 1, 9, 10 | sylanbrc 586 |
. . 3
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → 𝐴 ∈ 𝔸) |
12 | | dgraaval 40525 |
. . 3
⊢ (𝐴 ∈ 𝔸 →
(degAA‘𝐴)
= inf({𝑎 ∈ ℕ
∣ ∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}, ℝ, < )) |
13 | 11, 12 | syl 17 |
. 2
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (degAA‘𝐴) = inf({𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}, ℝ, < )) |
14 | | ssrab2 3967 |
. . . 4
⊢ {𝑎 ∈ ℕ ∣
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)} ⊆ ℕ |
15 | | nnuz 12356 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
16 | 14, 15 | sseqtri 3911 |
. . 3
⊢ {𝑎 ∈ ℕ ∣
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)} ⊆
(ℤ≥‘1) |
17 | | dgrnznn 24988 |
. . . 4
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (deg‘𝑃) ∈ ℕ) |
18 | | eqid 2738 |
. . . . . 6
⊢
(deg‘𝑃) =
(deg‘𝑃) |
19 | 5, 18 | jctil 523 |
. . . . 5
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → ((deg‘𝑃) = (deg‘𝑃) ∧ (𝑃‘𝐴) = 0)) |
20 | | fveqeq2 6677 |
. . . . . . 7
⊢ (𝑏 = 𝑃 → ((deg‘𝑏) = (deg‘𝑃) ↔ (deg‘𝑃) = (deg‘𝑃))) |
21 | | fveq1 6667 |
. . . . . . . 8
⊢ (𝑏 = 𝑃 → (𝑏‘𝐴) = (𝑃‘𝐴)) |
22 | 21 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑏 = 𝑃 → ((𝑏‘𝐴) = 0 ↔ (𝑃‘𝐴) = 0)) |
23 | 20, 22 | anbi12d 634 |
. . . . . 6
⊢ (𝑏 = 𝑃 → (((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0) ↔ ((deg‘𝑃) = (deg‘𝑃) ∧ (𝑃‘𝐴) = 0))) |
24 | 23 | rspcev 3524 |
. . . . 5
⊢ ((𝑃 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ ((deg‘𝑃) = (deg‘𝑃) ∧ (𝑃‘𝐴) = 0)) → ∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0)) |
25 | 4, 19, 24 | syl2anc 587 |
. . . 4
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → ∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0)) |
26 | | eqeq2 2750 |
. . . . . . 7
⊢ (𝑎 = (deg‘𝑃) → ((deg‘𝑏) = 𝑎 ↔ (deg‘𝑏) = (deg‘𝑃))) |
27 | 26 | anbi1d 633 |
. . . . . 6
⊢ (𝑎 = (deg‘𝑃) → (((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0) ↔ ((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0))) |
28 | 27 | rexbidv 3206 |
. . . . 5
⊢ (𝑎 = (deg‘𝑃) → (∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0) ↔ ∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0))) |
29 | 28 | elrab 3585 |
. . . 4
⊢
((deg‘𝑃)
∈ {𝑎 ∈ ℕ
∣ ∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)} ↔ ((deg‘𝑃) ∈ ℕ ∧ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = (deg‘𝑃) ∧ (𝑏‘𝐴) = 0))) |
30 | 17, 25, 29 | sylanbrc 586 |
. . 3
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (deg‘𝑃) ∈ {𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}) |
31 | | infssuzle 12406 |
. . 3
⊢ (({𝑎 ∈ ℕ ∣
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)} ⊆
(ℤ≥‘1) ∧ (deg‘𝑃) ∈ {𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}) → inf({𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}, ℝ, < ) ≤
(deg‘𝑃)) |
32 | 16, 30, 31 | sylancr 590 |
. 2
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → inf({𝑎 ∈ ℕ ∣ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑏) = 𝑎 ∧ (𝑏‘𝐴) = 0)}, ℝ, < ) ≤
(deg‘𝑃)) |
33 | 13, 32 | eqbrtrd 5049 |
1
⊢ (((𝑃 ∈ (Poly‘ℚ)
∧ 𝑃 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (degAA‘𝐴) ≤ (deg‘𝑃)) |