Proof of Theorem dgradd2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | plyaddcl 26259 | . . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) ∈
(Poly‘ℂ)) | 
| 2 | 1 | 3adant3 1133 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (𝐹 ∘f + 𝐺) ∈
(Poly‘ℂ)) | 
| 3 |  | dgrcl 26272 | . . . . 5
⊢ ((𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ)
→ (deg‘(𝐹
∘f + 𝐺))
∈ ℕ0) | 
| 4 | 2, 3 | syl 17 | . . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) ∈
ℕ0) | 
| 5 | 4 | nn0red 12588 | . . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) ∈ ℝ) | 
| 6 |  | dgradd.2 | . . . . . . 7
⊢ 𝑁 = (deg‘𝐺) | 
| 7 |  | dgrcl 26272 | . . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) | 
| 8 | 6, 7 | eqeltrid 2845 | . . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) | 
| 9 | 8 | 3ad2ant2 1135 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ∈
ℕ0) | 
| 10 | 9 | nn0red 12588 | . . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ∈ ℝ) | 
| 11 |  | dgradd.1 | . . . . . . 7
⊢ 𝑀 = (deg‘𝐹) | 
| 12 |  | dgrcl 26272 | . . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) | 
| 13 | 11, 12 | eqeltrid 2845 | . . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑀 ∈
ℕ0) | 
| 14 | 13 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ∈
ℕ0) | 
| 15 | 14 | nn0red 12588 | . . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ∈ ℝ) | 
| 16 | 10, 15 | ifcld 4572 | . . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) | 
| 17 | 11, 6 | dgradd 26307 | . . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) | 
| 18 | 17 | 3adant3 1133 | . . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) | 
| 19 | 10 | leidd 11829 | . . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≤ 𝑁) | 
| 20 |  | simp3 1139 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁) | 
| 21 | 15, 10, 20 | ltled 11409 | . . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑀 ≤ 𝑁) | 
| 22 |  | breq1 5146 | . . . . 5
⊢ (𝑁 = if(𝑀 ≤ 𝑁, 𝑁, 𝑀) → (𝑁 ≤ 𝑁 ↔ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁)) | 
| 23 |  | breq1 5146 | . . . . 5
⊢ (𝑀 = if(𝑀 ≤ 𝑁, 𝑁, 𝑀) → (𝑀 ≤ 𝑁 ↔ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁)) | 
| 24 | 22, 23 | ifboth 4565 | . . . 4
⊢ ((𝑁 ≤ 𝑁 ∧ 𝑀 ≤ 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁) | 
| 25 | 19, 21, 24 | syl2anc 584 | . . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ≤ 𝑁) | 
| 26 | 5, 16, 10, 18, 25 | letrd 11418 | . 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) ≤ 𝑁) | 
| 27 |  | eqid 2737 | . . . . . . . 8
⊢
(coeff‘𝐹) =
(coeff‘𝐹) | 
| 28 |  | eqid 2737 | . . . . . . . 8
⊢
(coeff‘𝐺) =
(coeff‘𝐺) | 
| 29 | 27, 28 | coeadd 26290 | . . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘f + 𝐺)) = ((coeff‘𝐹) ∘f + (coeff‘𝐺))) | 
| 30 | 29 | 3adant3 1133 | . . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘(𝐹 ∘f + 𝐺)) = ((coeff‘𝐹) ∘f + (coeff‘𝐺))) | 
| 31 | 30 | fveq1d 6908 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘f + 𝐺))‘𝑁) = (((coeff‘𝐹) ∘f + (coeff‘𝐺))‘𝑁)) | 
| 32 | 27 | coef3 26271 | . . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) | 
| 33 | 32 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐹):ℕ0⟶ℂ) | 
| 34 | 33 | ffnd 6737 | . . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐹) Fn ℕ0) | 
| 35 | 28 | coef3 26271 | . . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘𝑆) → (coeff‘𝐺):ℕ0⟶ℂ) | 
| 36 | 35 | 3ad2ant2 1135 | . . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐺):ℕ0⟶ℂ) | 
| 37 | 36 | ffnd 6737 | . . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (coeff‘𝐺) Fn ℕ0) | 
| 38 |  | nn0ex 12532 | . . . . . . . 8
⊢
ℕ0 ∈ V | 
| 39 | 38 | a1i 11 | . . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ℕ0 ∈
V) | 
| 40 |  | inidm 4227 | . . . . . . 7
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 | 
| 41 | 15, 10 | ltnled 11408 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀)) | 
| 42 | 20, 41 | mpbid 232 | . . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ¬ 𝑁 ≤ 𝑀) | 
| 43 |  | simp1 1137 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝐹 ∈ (Poly‘𝑆)) | 
| 44 | 27, 11 | dgrub 26273 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0 ∧
((coeff‘𝐹)‘𝑁) ≠ 0) → 𝑁 ≤ 𝑀) | 
| 45 | 44 | 3expia 1122 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0) →
(((coeff‘𝐹)‘𝑁) ≠ 0 → 𝑁 ≤ 𝑀)) | 
| 46 | 43, 9, 45 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (((coeff‘𝐹)‘𝑁) ≠ 0 → 𝑁 ≤ 𝑀)) | 
| 47 | 46 | necon1bd 2958 | . . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (¬ 𝑁 ≤ 𝑀 → ((coeff‘𝐹)‘𝑁) = 0)) | 
| 48 | 42, 47 | mpd 15 | . . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐹)‘𝑁) = 0) | 
| 49 | 48 | adantr 480 | . . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐹)‘𝑁) = 0) | 
| 50 |  | eqidd 2738 | . . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐺)‘𝑁) = ((coeff‘𝐺)‘𝑁)) | 
| 51 | 34, 37, 39, 39, 40, 49, 50 | ofval 7708 | . . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) ∧ 𝑁 ∈ ℕ0) →
(((coeff‘𝐹)
∘f + (coeff‘𝐺))‘𝑁) = (0 + ((coeff‘𝐺)‘𝑁))) | 
| 52 | 9, 51 | mpdan 687 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (((coeff‘𝐹) ∘f + (coeff‘𝐺))‘𝑁) = (0 + ((coeff‘𝐺)‘𝑁))) | 
| 53 | 36, 9 | ffvelcdmd 7105 | . . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐺)‘𝑁) ∈ ℂ) | 
| 54 | 53 | addlidd 11462 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (0 + ((coeff‘𝐺)‘𝑁)) = ((coeff‘𝐺)‘𝑁)) | 
| 55 | 31, 52, 54 | 3eqtrd 2781 | . . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘f + 𝐺))‘𝑁) = ((coeff‘𝐺)‘𝑁)) | 
| 56 |  | simp2 1138 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝐺 ∈ (Poly‘𝑆)) | 
| 57 |  | 0red 11264 | . . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 ∈ ℝ) | 
| 58 | 14 | nn0ge0d 12590 | . . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 ≤ 𝑀) | 
| 59 | 57, 15, 10, 58, 20 | lelttrd 11419 | . . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 0 < 𝑁) | 
| 60 | 59 | gt0ne0d 11827 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≠ 0) | 
| 61 | 6, 28 | dgreq0 26305 | . . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘𝑁) = 0)) | 
| 62 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝐺 = 0𝑝 →
(deg‘𝐺) =
(deg‘0𝑝)) | 
| 63 |  | dgr0 26302 | . . . . . . . . 9
⊢
(deg‘0𝑝) = 0 | 
| 64 | 63 | eqcomi 2746 | . . . . . . . 8
⊢ 0 =
(deg‘0𝑝) | 
| 65 | 62, 6, 64 | 3eqtr4g 2802 | . . . . . . 7
⊢ (𝐺 = 0𝑝 →
𝑁 = 0) | 
| 66 | 61, 65 | biimtrrdi 254 | . . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → (((coeff‘𝐺)‘𝑁) = 0 → 𝑁 = 0)) | 
| 67 | 66 | necon3d 2961 | . . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝑁 ≠ 0 → ((coeff‘𝐺)‘𝑁) ≠ 0)) | 
| 68 | 56, 60, 67 | sylc 65 | . . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘𝐺)‘𝑁) ≠ 0) | 
| 69 | 55, 68 | eqnetrd 3008 | . . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((coeff‘(𝐹 ∘f + 𝐺))‘𝑁) ≠ 0) | 
| 70 |  | eqid 2737 | . . . 4
⊢
(coeff‘(𝐹
∘f + 𝐺)) =
(coeff‘(𝐹
∘f + 𝐺)) | 
| 71 |  | eqid 2737 | . . . 4
⊢
(deg‘(𝐹
∘f + 𝐺)) =
(deg‘(𝐹
∘f + 𝐺)) | 
| 72 | 70, 71 | dgrub 26273 | . . 3
⊢ (((𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ)
∧ 𝑁 ∈
ℕ0 ∧ ((coeff‘(𝐹 ∘f + 𝐺))‘𝑁) ≠ 0) → 𝑁 ≤ (deg‘(𝐹 ∘f + 𝐺))) | 
| 73 | 2, 9, 69, 72 | syl3anc 1373 | . 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → 𝑁 ≤ (deg‘(𝐹 ∘f + 𝐺))) | 
| 74 | 5, 10 | letri3d 11403 | . 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → ((deg‘(𝐹 ∘f + 𝐺)) = 𝑁 ↔ ((deg‘(𝐹 ∘f + 𝐺)) ≤ 𝑁 ∧ 𝑁 ≤ (deg‘(𝐹 ∘f + 𝐺))))) | 
| 75 | 26, 73, 74 | mpbir2and 713 | 1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝑀 < 𝑁) → (deg‘(𝐹 ∘f + 𝐺)) = 𝑁) |