Step | Hyp | Ref
| Expression |
1 | | dgraaval 36733 |
. . 3
⊢ (𝐴 ∈ 𝔸 →
(degAA‘𝐴)
= inf({𝑎 ∈ ℕ
∣ ∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}, ℝ, < )) |
2 | | ssrab2 3650 |
. . . . 5
⊢ {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ⊆ ℕ |
3 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
4 | 2, 3 | sseqtri 3600 |
. . . 4
⊢ {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ⊆
(ℤ≥‘1) |
5 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ↔ (𝑏 ∈ (Poly‘ℚ) ∧ 𝑏 ≠
0𝑝)) |
6 | 5 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) → (𝑏 ∈ (Poly‘ℚ) ∧ 𝑏 ≠
0𝑝)) |
7 | 6 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → (𝑏 ∈ (Poly‘ℚ) ∧ 𝑏 ≠
0𝑝)) |
8 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ℂ) |
9 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → (𝑏‘𝐴) = 0) |
10 | | dgrnznn 23807 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ (Poly‘ℚ)
∧ 𝑏 ≠
0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑏‘𝐴) = 0)) → (deg‘𝑏) ∈ ℕ) |
11 | 7, 8, 9, 10 | syl12anc 1316 |
. . . . . . . . 9
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → (deg‘𝑏) ∈
ℕ) |
12 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → 𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
13 | | eqid 2610 |
. . . . . . . . . 10
⊢
(deg‘𝑏) =
(deg‘𝑏) |
14 | 9, 13 | jctil 558 |
. . . . . . . . 9
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → ((deg‘𝑏) = (deg‘𝑏) ∧ (𝑏‘𝐴) = 0)) |
15 | | eqeq2 2621 |
. . . . . . . . . . 11
⊢ (𝑎 = (deg‘𝑏) → ((deg‘𝑝) = 𝑎 ↔ (deg‘𝑝) = (deg‘𝑏))) |
16 | 15 | anbi1d 737 |
. . . . . . . . . 10
⊢ (𝑎 = (deg‘𝑏) → (((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0) ↔ ((deg‘𝑝) = (deg‘𝑏) ∧ (𝑝‘𝐴) = 0))) |
17 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑏 → (deg‘𝑝) = (deg‘𝑏)) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑏 → ((deg‘𝑝) = (deg‘𝑏) ↔ (deg‘𝑏) = (deg‘𝑏))) |
19 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑏 → (𝑝‘𝐴) = (𝑏‘𝐴)) |
20 | 19 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑏 → ((𝑝‘𝐴) = 0 ↔ (𝑏‘𝐴) = 0)) |
21 | 18, 20 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑏 → (((deg‘𝑝) = (deg‘𝑏) ∧ (𝑝‘𝐴) = 0) ↔ ((deg‘𝑏) = (deg‘𝑏) ∧ (𝑏‘𝐴) = 0))) |
22 | 16, 21 | rspc2ev 3295 |
. . . . . . . . 9
⊢
(((deg‘𝑏)
∈ ℕ ∧ 𝑏
∈ ((Poly‘ℚ) ∖ {0𝑝}) ∧
((deg‘𝑏) =
(deg‘𝑏) ∧ (𝑏‘𝐴) = 0)) → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)) |
23 | 11, 12, 14, 22 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) ∧ 𝐴 ∈ ℂ) → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)) |
24 | 23 | ex 449 |
. . . . . . 7
⊢ ((𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝐴) = 0) → (𝐴 ∈ ℂ → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0))) |
25 | 24 | rexlimiva 3010 |
. . . . . 6
⊢
(∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑏‘𝐴) = 0 → (𝐴 ∈ ℂ → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0))) |
26 | 25 | impcom 445 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑏‘𝐴) = 0) → ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)) |
27 | | elqaa 23881 |
. . . . 5
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑏‘𝐴) = 0)) |
28 | | rabn0 3912 |
. . . . 5
⊢ ({𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ≠ ∅ ↔ ∃𝑎 ∈ ℕ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)) |
29 | 26, 27, 28 | 3imtr4i 280 |
. . . 4
⊢ (𝐴 ∈ 𝔸 → {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ≠ ∅) |
30 | | infssuzcl 11648 |
. . . 4
⊢ (({𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ⊆
(ℤ≥‘1) ∧ {𝑎 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ≠ ∅) → inf({𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}, ℝ, < ) ∈ {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}) |
31 | 4, 29, 30 | sylancr 694 |
. . 3
⊢ (𝐴 ∈ 𝔸 →
inf({𝑎 ∈ ℕ
∣ ∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}, ℝ, < ) ∈ {𝑎 ∈ ℕ ∣
∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}) |
32 | 1, 31 | eqeltrd 2688 |
. 2
⊢ (𝐴 ∈ 𝔸 →
(degAA‘𝐴)
∈ {𝑎 ∈ ℕ
∣ ∃𝑝 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)}) |
33 | | eqeq2 2621 |
. . . . 5
⊢ (𝑎 = (degAA‘𝐴) → ((deg‘𝑝) = 𝑎 ↔ (deg‘𝑝) = (degAA‘𝐴))) |
34 | 33 | anbi1d 737 |
. . . 4
⊢ (𝑎 = (degAA‘𝐴) → (((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0) ↔ ((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) |
35 | 34 | rexbidv 3034 |
. . 3
⊢ (𝑎 = (degAA‘𝐴) → (∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0) ↔ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) |
36 | 35 | elrab 3331 |
. 2
⊢
((degAA‘𝐴) ∈ {𝑎 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ)
∖ {0𝑝})((deg‘𝑝) = 𝑎 ∧ (𝑝‘𝐴) = 0)} ↔
((degAA‘𝐴)
∈ ℕ ∧ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) |
37 | 32, 36 | sylib 207 |
1
⊢ (𝐴 ∈ 𝔸 →
((degAA‘𝐴)
∈ ℕ ∧ ∃𝑝 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) |