Proof of Theorem dgradd2
Step | Hyp | Ref
| Expression |
1 | | plyaddcl 25391 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) ∈
(Poly‘ℂ)) |
2 | 1 | 3adant3 1131 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (𝐹 ∘f + 𝐺) ∈
(Poly‘ℂ)) |
3 | | dgrcl 25404 |
. . . . 5
⊢ ((𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ)
→ (deg‘(𝐹
∘f + 𝐺))
∈ ℕ0) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) ∈
ℕ0) |
5 | 4 | nn0red 12304 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) ∈ ℝ) |
6 | | dgradd.2 |
. . . . . . 7
⊢ 𝑁 = (deg‘𝐺) |
7 | | dgrcl 25404 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
8 | 6, 7 | eqeltrid 2843 |
. . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) |
9 | 8 | 3ad2ant2 1133 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ∈
ℕ0) |
10 | 9 | nn0red 12304 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ∈ ℝ) |
11 | | dgradd.1 |
. . . . . . 7
⊢ 𝑀 = (deg‘𝐹) |
12 | | dgrcl 25404 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
13 | 11, 12 | eqeltrid 2843 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑀 ∈
ℕ0) |
14 | 13 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ∈
ℕ0) |
15 | 14 | nn0red 12304 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ∈ ℝ) |
16 | 10, 15 | ifcld 4505 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) |
17 | 11, 6 | dgradd 25438 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
18 | 17 | 3adant3 1131 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
19 | 10 | leidd 11551 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≤ 𝑁) |
20 | | simp3 1137 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁) |
21 | 15, 10, 20 | ltled 11133 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ≤ 𝑁) |
22 | | breq1 5076 |
. . . . 5
⊢ (𝑁 = if(𝑀 ≤ 𝑁, 𝑁, 𝑀) → (𝑁 ≤ 𝑁 ↔ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁)) |
23 | | breq1 5076 |
. . . . 5
⊢ (𝑀 = if(𝑀 ≤ 𝑁, 𝑁, 𝑀) → (𝑀 ≤ 𝑁 ↔ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁)) |
24 | 22, 23 | ifboth 4498 |
. . . 4
⊢ ((𝑁 ≤ 𝑁 ∧ 𝑀 ≤ 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁) |
25 | 19, 21, 24 | syl2anc 584 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁) |
26 | 5, 16, 10, 18, 25 | letrd 11142 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) ≤ 𝑁) |
27 | | eqid 2738 |
. . . . . . . 8
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
28 | | eqid 2738 |
. . . . . . . 8
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
29 | 27, 28 | coeadd 25422 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘f + 𝐺)) = ((coeff‘𝐹) ∘f + (coeff‘𝐺))) |
30 | 29 | 3adant3 1131 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘(𝐹 ∘f + 𝐺)) = ((coeff‘𝐹) ∘f + (coeff‘𝐺))) |
31 | 30 | fveq1d 6768 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘f + 𝐺))‘𝑁) = (((coeff‘𝐹) ∘f + (coeff‘𝐺))‘𝑁)) |
32 | 27 | coef3 25403 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
33 | 32 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐹):ℕ0⟶ℂ) |
34 | 33 | ffnd 6593 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐹) Fn ℕ0) |
35 | 28 | coef3 25403 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘𝑆) → (coeff‘𝐺):ℕ0⟶ℂ) |
36 | 35 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐺):ℕ0⟶ℂ) |
37 | 36 | ffnd 6593 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐺) Fn ℕ0) |
38 | | nn0ex 12249 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ℕ0 ∈
V) |
40 | | inidm 4152 |
. . . . . . 7
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
41 | 15, 10 | ltnled 11132 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀)) |
42 | 20, 41 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ¬ 𝑁 ≤ 𝑀) |
43 | | simp1 1135 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝐹 ∈ (Poly‘𝑆)) |
44 | 27, 11 | dgrub 25405 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0 ∧
((coeff‘𝐹)‘𝑁) ≠ 0) → 𝑁 ≤ 𝑀) |
45 | 44 | 3expia 1120 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0) →
(((coeff‘𝐹)‘𝑁) ≠ 0 → 𝑁 ≤ 𝑀)) |
46 | 43, 9, 45 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (((coeff‘𝐹)‘𝑁) ≠ 0 → 𝑁 ≤ 𝑀)) |
47 | 46 | necon1bd 2961 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (¬ 𝑁 ≤ 𝑀 → ((coeff‘𝐹)‘𝑁) = 0)) |
48 | 42, 47 | mpd 15 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐹)‘𝑁) = 0) |
49 | 48 | adantr 481 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐹)‘𝑁) = 0) |
50 | | eqidd 2739 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐺)‘𝑁) = ((coeff‘𝐺)‘𝑁)) |
51 | 34, 37, 39, 39, 40, 49, 50 | ofval 7534 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
(((coeff‘𝐹)
∘f + (coeff‘𝐺))‘𝑁) = (0 + ((coeff‘𝐺)‘𝑁))) |
52 | 9, 51 | mpdan 684 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (((coeff‘𝐹) ∘f + (coeff‘𝐺))‘𝑁) = (0 + ((coeff‘𝐺)‘𝑁))) |
53 | 36, 9 | ffvelrnd 6954 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐺)‘𝑁) ∈ ℂ) |
54 | 53 | addid2d 11186 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (0 + ((coeff‘𝐺)‘𝑁)) = ((coeff‘𝐺)‘𝑁)) |
55 | 31, 52, 54 | 3eqtrd 2782 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘f + 𝐺))‘𝑁) = ((coeff‘𝐺)‘𝑁)) |
56 | | simp2 1136 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝐺 ∈ (Poly‘𝑆)) |
57 | | 0red 10988 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 ∈ ℝ) |
58 | 14 | nn0ge0d 12306 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 ≤ 𝑀) |
59 | 57, 15, 10, 58, 20 | lelttrd 11143 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 < 𝑁) |
60 | 59 | gt0ne0d 11549 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≠ 0) |
61 | 6, 28 | dgreq0 25436 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘𝑁) = 0)) |
62 | | fveq2 6766 |
. . . . . . . 8
⊢ (𝐺 = 0𝑝 →
(deg‘𝐺) =
(deg‘0𝑝)) |
63 | | dgr0 25433 |
. . . . . . . . 9
⊢
(deg‘0𝑝) = 0 |
64 | 63 | eqcomi 2747 |
. . . . . . . 8
⊢ 0 =
(deg‘0𝑝) |
65 | 62, 6, 64 | 3eqtr4g 2803 |
. . . . . . 7
⊢ (𝐺 = 0𝑝 →
𝑁 = 0) |
66 | 61, 65 | syl6bir 253 |
. . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → (((coeff‘𝐺)‘𝑁) = 0 → 𝑁 = 0)) |
67 | 66 | necon3d 2964 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝑁 ≠ 0 → ((coeff‘𝐺)‘𝑁) ≠ 0)) |
68 | 56, 60, 67 | sylc 65 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐺)‘𝑁) ≠ 0) |
69 | 55, 68 | eqnetrd 3011 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘f + 𝐺))‘𝑁) ≠ 0) |
70 | | eqid 2738 |
. . . 4
⊢
(coeff‘(𝐹
∘f + 𝐺)) =
(coeff‘(𝐹
∘f + 𝐺)) |
71 | | eqid 2738 |
. . . 4
⊢
(deg‘(𝐹
∘f + 𝐺)) =
(deg‘(𝐹
∘f + 𝐺)) |
72 | 70, 71 | dgrub 25405 |
. . 3
⊢ (((𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ)
∧ 𝑁 ∈
ℕ0 ∧ ((coeff‘(𝐹 ∘f + 𝐺))‘𝑁) ≠ 0) → 𝑁 ≤ (deg‘(𝐹 ∘f + 𝐺))) |
73 | 2, 9, 69, 72 | syl3anc 1370 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≤ (deg‘(𝐹 ∘f + 𝐺))) |
74 | 5, 10 | letri3d 11127 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((deg‘(𝐹 ∘f + 𝐺)) = 𝑁 ↔ ((deg‘(𝐹 ∘f + 𝐺)) ≤ 𝑁 ∧ 𝑁 ≤ (deg‘(𝐹 ∘f + 𝐺))))) |
75 | 26, 73, 74 | mpbir2and 710 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) = 𝑁) |