Proof of Theorem dgradd2
Step | Hyp | Ref
| Expression |
1 | | plyaddcl 23780 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘𝑓 + 𝐺) ∈
(Poly‘ℂ)) |
2 | 1 | 3adant3 1074 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (𝐹 ∘𝑓 + 𝐺) ∈
(Poly‘ℂ)) |
3 | | dgrcl 23793 |
. . . . 5
⊢ ((𝐹 ∘𝑓 +
𝐺) ∈
(Poly‘ℂ) → (deg‘(𝐹 ∘𝑓 + 𝐺)) ∈
ℕ0) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘𝑓 + 𝐺)) ∈
ℕ0) |
5 | 4 | nn0red 11229 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘𝑓 + 𝐺)) ∈
ℝ) |
6 | | dgradd.2 |
. . . . . . 7
⊢ 𝑁 = (deg‘𝐺) |
7 | | dgrcl 23793 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
8 | 6, 7 | syl5eqel 2692 |
. . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) |
9 | 8 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ∈
ℕ0) |
10 | 9 | nn0red 11229 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ∈ ℝ) |
11 | | dgradd.1 |
. . . . . . 7
⊢ 𝑀 = (deg‘𝐹) |
12 | | dgrcl 23793 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
13 | 11, 12 | syl5eqel 2692 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑀 ∈
ℕ0) |
14 | 13 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ∈
ℕ0) |
15 | 14 | nn0red 11229 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ∈ ℝ) |
16 | 10, 15 | ifcld 4081 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) |
17 | 11, 6 | dgradd 23827 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘𝑓 + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
18 | 17 | 3adant3 1074 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘𝑓 + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
19 | 10 | leidd 10473 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≤ 𝑁) |
20 | | simp3 1056 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁) |
21 | 15, 10, 20 | ltled 10064 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ≤ 𝑁) |
22 | | breq1 4586 |
. . . . 5
⊢ (𝑁 = if(𝑀 ≤ 𝑁, 𝑁, 𝑀) → (𝑁 ≤ 𝑁 ↔ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁)) |
23 | | breq1 4586 |
. . . . 5
⊢ (𝑀 = if(𝑀 ≤ 𝑁, 𝑁, 𝑀) → (𝑀 ≤ 𝑁 ↔ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁)) |
24 | 22, 23 | ifboth 4074 |
. . . 4
⊢ ((𝑁 ≤ 𝑁 ∧ 𝑀 ≤ 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁) |
25 | 19, 21, 24 | syl2anc 691 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁) |
26 | 5, 16, 10, 18, 25 | letrd 10073 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘𝑓 + 𝐺)) ≤ 𝑁) |
27 | | eqid 2610 |
. . . . . . . 8
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
28 | | eqid 2610 |
. . . . . . . 8
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
29 | 27, 28 | coeadd 23811 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘𝑓 + 𝐺)) = ((coeff‘𝐹) ∘𝑓 +
(coeff‘𝐺))) |
30 | 29 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘(𝐹 ∘𝑓 + 𝐺)) = ((coeff‘𝐹) ∘𝑓 +
(coeff‘𝐺))) |
31 | 30 | fveq1d 6105 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘𝑓 + 𝐺))‘𝑁) = (((coeff‘𝐹) ∘𝑓 +
(coeff‘𝐺))‘𝑁)) |
32 | 27 | coef3 23792 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
33 | 32 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐹):ℕ0⟶ℂ) |
34 | | ffn 5958 |
. . . . . . . 8
⊢
((coeff‘𝐹):ℕ0⟶ℂ →
(coeff‘𝐹) Fn
ℕ0) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐹) Fn ℕ0) |
36 | 28 | coef3 23792 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘𝑆) → (coeff‘𝐺):ℕ0⟶ℂ) |
37 | 36 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐺):ℕ0⟶ℂ) |
38 | | ffn 5958 |
. . . . . . . 8
⊢
((coeff‘𝐺):ℕ0⟶ℂ →
(coeff‘𝐺) Fn
ℕ0) |
39 | 37, 38 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐺) Fn ℕ0) |
40 | | nn0ex 11175 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ℕ0 ∈
V) |
42 | | inidm 3784 |
. . . . . . 7
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
43 | 15, 10 | ltnled 10063 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀)) |
44 | 20, 43 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ¬ 𝑁 ≤ 𝑀) |
45 | | simp1 1054 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝐹 ∈ (Poly‘𝑆)) |
46 | 27, 11 | dgrub 23794 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0 ∧
((coeff‘𝐹)‘𝑁) ≠ 0) → 𝑁 ≤ 𝑀) |
47 | 46 | 3expia 1259 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0) →
(((coeff‘𝐹)‘𝑁) ≠ 0 → 𝑁 ≤ 𝑀)) |
48 | 45, 9, 47 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (((coeff‘𝐹)‘𝑁) ≠ 0 → 𝑁 ≤ 𝑀)) |
49 | 48 | necon1bd 2800 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (¬ 𝑁 ≤ 𝑀 → ((coeff‘𝐹)‘𝑁) = 0)) |
50 | 44, 49 | mpd 15 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐹)‘𝑁) = 0) |
51 | 50 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐹)‘𝑁) = 0) |
52 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐺)‘𝑁) = ((coeff‘𝐺)‘𝑁)) |
53 | 35, 39, 41, 41, 42, 51, 52 | ofval 6804 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
(((coeff‘𝐹)
∘𝑓 + (coeff‘𝐺))‘𝑁) = (0 + ((coeff‘𝐺)‘𝑁))) |
54 | 9, 53 | mpdan 699 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (((coeff‘𝐹) ∘𝑓 +
(coeff‘𝐺))‘𝑁) = (0 + ((coeff‘𝐺)‘𝑁))) |
55 | 37, 9 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐺)‘𝑁) ∈ ℂ) |
56 | 55 | addid2d 10116 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (0 + ((coeff‘𝐺)‘𝑁)) = ((coeff‘𝐺)‘𝑁)) |
57 | 31, 54, 56 | 3eqtrd 2648 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘𝑓 + 𝐺))‘𝑁) = ((coeff‘𝐺)‘𝑁)) |
58 | | simp2 1055 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝐺 ∈ (Poly‘𝑆)) |
59 | | 0red 9920 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 ∈ ℝ) |
60 | 14 | nn0ge0d 11231 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 ≤ 𝑀) |
61 | 59, 15, 10, 60, 20 | lelttrd 10074 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 < 𝑁) |
62 | 61 | gt0ne0d 10471 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≠ 0) |
63 | 6, 28 | dgreq0 23825 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘𝑁) = 0)) |
64 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝐺 = 0𝑝 →
(deg‘𝐺) =
(deg‘0𝑝)) |
65 | | dgr0 23822 |
. . . . . . . . 9
⊢
(deg‘0𝑝) = 0 |
66 | 65 | eqcomi 2619 |
. . . . . . . 8
⊢ 0 =
(deg‘0𝑝) |
67 | 64, 6, 66 | 3eqtr4g 2669 |
. . . . . . 7
⊢ (𝐺 = 0𝑝 →
𝑁 = 0) |
68 | 63, 67 | syl6bir 243 |
. . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → (((coeff‘𝐺)‘𝑁) = 0 → 𝑁 = 0)) |
69 | 68 | necon3d 2803 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝑁 ≠ 0 → ((coeff‘𝐺)‘𝑁) ≠ 0)) |
70 | 58, 62, 69 | sylc 63 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐺)‘𝑁) ≠ 0) |
71 | 57, 70 | eqnetrd 2849 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘𝑓 + 𝐺))‘𝑁) ≠ 0) |
72 | | eqid 2610 |
. . . 4
⊢
(coeff‘(𝐹
∘𝑓 + 𝐺)) = (coeff‘(𝐹 ∘𝑓 + 𝐺)) |
73 | | eqid 2610 |
. . . 4
⊢
(deg‘(𝐹
∘𝑓 + 𝐺)) = (deg‘(𝐹 ∘𝑓 + 𝐺)) |
74 | 72, 73 | dgrub 23794 |
. . 3
⊢ (((𝐹 ∘𝑓 +
𝐺) ∈
(Poly‘ℂ) ∧ 𝑁 ∈ ℕ0 ∧
((coeff‘(𝐹
∘𝑓 + 𝐺))‘𝑁) ≠ 0) → 𝑁 ≤ (deg‘(𝐹 ∘𝑓 + 𝐺))) |
75 | 2, 9, 71, 74 | syl3anc 1318 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≤ (deg‘(𝐹 ∘𝑓 + 𝐺))) |
76 | 5, 10 | letri3d 10058 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((deg‘(𝐹 ∘𝑓 + 𝐺)) = 𝑁 ↔ ((deg‘(𝐹 ∘𝑓 + 𝐺)) ≤ 𝑁 ∧ 𝑁 ≤ (deg‘(𝐹 ∘𝑓 + 𝐺))))) |
77 | 26, 75, 76 | mpbir2and 959 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘𝑓 + 𝐺)) = 𝑁) |