Proof of Theorem ply1degltel
Step | Hyp | Ref
| Expression |
1 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → 𝐹 = (0g‘𝑃)) |
2 | | ply1degltlss.d |
. . . . . . . . . 10
⊢ 𝐷 = ( deg1
‘𝑅) |
3 | | ply1degltlss.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
4 | | ply1degltel.1 |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑃) |
5 | 2, 3, 4 | deg1xrf 26004 |
. . . . . . . . 9
⊢ 𝐷:𝐵⟶ℝ* |
6 | 5 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐷:𝐵⟶ℝ*) |
7 | 6 | ffnd 6717 |
. . . . . . 7
⊢ (𝜑 → 𝐷 Fn 𝐵) |
8 | | ply1degltlss.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
9 | 3 | ply1ring 22153 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
10 | | eqid 2727 |
. . . . . . . . 9
⊢
(0g‘𝑃) = (0g‘𝑃) |
11 | 4, 10 | ring0cl 20192 |
. . . . . . . 8
⊢ (𝑃 ∈ Ring →
(0g‘𝑃)
∈ 𝐵) |
12 | 8, 9, 11 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑃) ∈ 𝐵) |
13 | 2, 3, 10 | deg1z 26010 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (𝐷‘(0g‘𝑃)) = -∞) |
14 | 8, 13 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) = -∞) |
15 | | mnfxr 11293 |
. . . . . . . . . 10
⊢ -∞
∈ ℝ* |
16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -∞ ∈
ℝ*) |
17 | | ply1degltlss.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
18 | 17 | nn0red 12555 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) |
19 | 18 | rexrd 11286 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
20 | 16 | xrleidd 13155 |
. . . . . . . . 9
⊢ (𝜑 → -∞ ≤
-∞) |
21 | 18 | mnfltd 13128 |
. . . . . . . . 9
⊢ (𝜑 → -∞ < 𝑁) |
22 | 16, 19, 16, 20, 21 | elicod 13398 |
. . . . . . . 8
⊢ (𝜑 → -∞ ∈
(-∞[,)𝑁)) |
23 | 14, 22 | eqeltrd 2828 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) ∈ (-∞[,)𝑁)) |
24 | 7, 12, 23 | elpreimad 7062 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑃) ∈ (◡𝐷 “ (-∞[,)𝑁))) |
25 | | ply1degltlss.1 |
. . . . . 6
⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) |
26 | 24, 25 | eleqtrrdi 2839 |
. . . . 5
⊢ (𝜑 → (0g‘𝑃) ∈ 𝑆) |
27 | 26 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → (0g‘𝑃) ∈ 𝑆) |
28 | 1, 27 | eqeltrd 2828 |
. . 3
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → 𝐹 ∈ 𝑆) |
29 | | cnvimass 6079 |
. . . . . 6
⊢ (◡𝐷 “ (-∞[,)𝑁)) ⊆ dom 𝐷 |
30 | 25, 29 | eqsstri 4012 |
. . . . 5
⊢ 𝑆 ⊆ dom 𝐷 |
31 | 5 | fdmi 6728 |
. . . . 5
⊢ dom 𝐷 = 𝐵 |
32 | 30, 31 | sseqtri 4014 |
. . . 4
⊢ 𝑆 ⊆ 𝐵 |
33 | 32, 28 | sselid 3976 |
. . 3
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → 𝐹 ∈ 𝐵) |
34 | 1 | fveq2d 6895 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → (𝐷‘𝐹) = (𝐷‘(0g‘𝑃))) |
35 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → (𝐷‘(0g‘𝑃)) = -∞) |
36 | 34, 35 | eqtrd 2767 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → (𝐷‘𝐹) = -∞) |
37 | | 1red 11237 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
38 | 18, 37 | resubcld 11664 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
39 | 38 | rexrd 11286 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈
ℝ*) |
40 | 39 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → (𝑁 − 1) ∈
ℝ*) |
41 | 40 | mnfled 13139 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → -∞ ≤ (𝑁 − 1)) |
42 | 36, 41 | eqbrtrd 5164 |
. . 3
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → (𝐷‘𝐹) ≤ (𝑁 − 1)) |
43 | | pm5.1 823 |
. . 3
⊢ ((𝐹 ∈ 𝑆 ∧ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1))) → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1)))) |
44 | 28, 33, 42, 43 | syl12anc 836 |
. 2
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑃)) → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1)))) |
45 | 25 | eleq2i 2820 |
. . . 4
⊢ (𝐹 ∈ 𝑆 ↔ 𝐹 ∈ (◡𝐷 “ (-∞[,)𝑁))) |
46 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) → 𝐷 Fn 𝐵) |
47 | | elpreima 7061 |
. . . . 5
⊢ (𝐷 Fn 𝐵 → (𝐹 ∈ (◡𝐷 “ (-∞[,)𝑁)) ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ∈ (-∞[,)𝑁)))) |
48 | 46, 47 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) → (𝐹 ∈ (◡𝐷 “ (-∞[,)𝑁)) ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ∈ (-∞[,)𝑁)))) |
49 | 45, 48 | bitrid 283 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ∈ (-∞[,)𝑁)))) |
50 | 15 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → -∞ ∈
ℝ*) |
51 | 19 | ad2antrr 725 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → 𝑁 ∈
ℝ*) |
52 | | elico1 13391 |
. . . . . . 7
⊢
((-∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ*) → ((𝐷‘𝐹) ∈ (-∞[,)𝑁) ↔ ((𝐷‘𝐹) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝐹) ∧ (𝐷‘𝐹) < 𝑁))) |
53 | 50, 51, 52 | syl2anc 583 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) ∈ (-∞[,)𝑁) ↔ ((𝐷‘𝐹) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝐹) ∧ (𝐷‘𝐹) < 𝑁))) |
54 | | df-3an 1087 |
. . . . . 6
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝐹) ∧ (𝐷‘𝐹) < 𝑁) ↔ (((𝐷‘𝐹) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝐹)) ∧ (𝐷‘𝐹) < 𝑁)) |
55 | 53, 54 | bitrdi 287 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) ∈ (-∞[,)𝑁) ↔ (((𝐷‘𝐹) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝐹)) ∧ (𝐷‘𝐹) < 𝑁))) |
56 | 8 | ad2antrr 725 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → 𝑅 ∈ Ring) |
57 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
58 | | simplr 768 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → 𝐹 ≠ (0g‘𝑃)) |
59 | 2, 3, 10, 4 | deg1nn0cl 26011 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ (0g‘𝑃)) → (𝐷‘𝐹) ∈
ℕ0) |
60 | 56, 57, 58, 59 | syl3anc 1369 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → (𝐷‘𝐹) ∈
ℕ0) |
61 | 60 | nn0red 12555 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → (𝐷‘𝐹) ∈ ℝ) |
62 | 61 | rexrd 11286 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → (𝐷‘𝐹) ∈
ℝ*) |
63 | 62 | mnfled 13139 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → -∞ ≤ (𝐷‘𝐹)) |
64 | 62, 63 | jca 511 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝐹))) |
65 | 64 | biantrurd 532 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) < 𝑁 ↔ (((𝐷‘𝐹) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝐹)) ∧ (𝐷‘𝐹) < 𝑁))) |
66 | 60 | nn0zd 12606 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → (𝐷‘𝐹) ∈ ℤ) |
67 | 17 | nn0zd 12606 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) |
68 | 67 | ad2antrr 725 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → 𝑁 ∈ ℤ) |
69 | | zltlem1 12637 |
. . . . . 6
⊢ (((𝐷‘𝐹) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐷‘𝐹) < 𝑁 ↔ (𝐷‘𝐹) ≤ (𝑁 − 1))) |
70 | 66, 68, 69 | syl2anc 583 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) < 𝑁 ↔ (𝐷‘𝐹) ≤ (𝑁 − 1))) |
71 | 55, 65, 70 | 3bitr2d 307 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) ∈ (-∞[,)𝑁) ↔ (𝐷‘𝐹) ≤ (𝑁 − 1))) |
72 | 71 | pm5.32da 578 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) → ((𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ∈ (-∞[,)𝑁)) ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1)))) |
73 | 49, 72 | bitrd 279 |
. 2
⊢ ((𝜑 ∧ 𝐹 ≠ (0g‘𝑃)) → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1)))) |
74 | 44, 73 | pm2.61dane 3024 |
1
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1)))) |