Metamath Proof Explorer

Theorem dgradd2

Description: The degree of a sum of polynomials of unequal degrees is the degree of the larger polynomial. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgradd.1 ⊢ 𝑀 = ( deg ‘ 𝐹 )
dgradd.2 ⊢ 𝑁 = ( deg ‘ 𝐺 )
Assertion dgradd2 ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 dgradd.1 ⊢ 𝑀 = ( deg ‘ 𝐹 )
2 dgradd.2 ⊢ 𝑁 = ( deg ‘ 𝐺 )
3 plyaddcl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( Poly ‘ ℂ ) )
4 3 3adant3 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( Poly ‘ ℂ ) )
5 dgrcl ⊢ ( ( 𝐹 ∘f + 𝐺 ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ∈ ℕ0 )
6 4 5 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ∈ ℕ0 )
7 6 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ∈ ℝ )
8 dgrcl ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
9 2 8 eqeltrid ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
10 9 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑁 ∈ ℕ0 )
11 10 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑁 ∈ ℝ )
12 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
13 1 12 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑀 ∈ ℕ0 )
14 13 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑀 ∈ ℕ0 )
15 14 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑀 ∈ ℝ )
16 11 15 ifcld ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℝ )
17 1 2 dgradd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
18 17 3adant3 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
19 11 leidd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑁 ≤ 𝑁 )
20 simp3 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑀 < 𝑁 )
21 15 11 20 ltled ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑀 ≤ 𝑁 )
22 breq1 ⊢ ( 𝑁 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) → ( 𝑁 ≤ 𝑁 ↔ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ≤ 𝑁 ) )
23 breq1 ⊢ ( 𝑀 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) → ( 𝑀 ≤ 𝑁 ↔ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ≤ 𝑁 ) )
24 22 23 ifboth ⊢ ( ( 𝑁 ≤ 𝑁 ∧ 𝑀 ≤ 𝑁 ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ≤ 𝑁 )
25 19 21 24 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ≤ 𝑁 )
26 7 16 11 18 25 letrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ 𝑁 )
27 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
28 eqid ⊢ ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 )
29 27 28 coeadd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( coeff ‘ 𝐹 ) ∘f + ( coeff ‘ 𝐺 ) ) )
30 29 3adant3 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( coeff ‘ 𝐹 ) ∘f + ( coeff ‘ 𝐺 ) ) )
31 30 fveq1d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) ‘ 𝑁 ) = ( ( ( coeff ‘ 𝐹 ) ∘f + ( coeff ‘ 𝐺 ) ) ‘ 𝑁 ) )
32 27 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
33 32 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
34 33 ffnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( coeff ‘ 𝐹 ) Fn ℕ0 )
35 28 coef3 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
36 35 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
37 36 ffnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( coeff ‘ 𝐺 ) Fn ℕ0 )
38 nn0ex ⊢ ℕ0 ∈ V
39 38 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ℕ0 ∈ V )
40 inidm ⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
41 15 11 ltnled ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( 𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀 ) )
42 20 41 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ¬ 𝑁 ≤ 𝑀 )
43 simp1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
44 27 1 dgrub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 ) → 𝑁 ≤ 𝑀 )
45 44 3expia ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 → 𝑁 ≤ 𝑀 ) )
46 43 10 45 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 → 𝑁 ≤ 𝑀 ) )
47 46 necon1bd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ¬ 𝑁 ≤ 𝑀 → ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = 0 ) )
48 42 47 mpd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = 0 )
49 48 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = 0 )
50 eqidd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) )
51 34 37 39 39 40 49 50 ofval ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( coeff ‘ 𝐹 ) ∘f + ( coeff ‘ 𝐺 ) ) ‘ 𝑁 ) = ( 0 + ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) )
52 10 51 mpdan ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( ( coeff ‘ 𝐹 ) ∘f + ( coeff ‘ 𝐺 ) ) ‘ 𝑁 ) = ( 0 + ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) )
53 36 10 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ∈ ℂ )
54 53 addlidd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( 0 + ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) )
55 31 52 54 3eqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) )
56 simp2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
57 0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 0 ∈ ℝ )
58 14 nn0ge0d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 0 ≤ 𝑀 )
59 57 15 11 58 20 lelttrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 0 < 𝑁 )
60 59 gt0ne0d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑁 ≠ 0 )
61 2 28 dgreq0 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( 𝐺 = 0𝑝 ↔ ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) = 0 ) )
62 fveq2 ⊢ ( 𝐺 = 0𝑝 → ( deg ‘ 𝐺 ) = ( deg ‘ 0𝑝 ) )
63 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
64 63 eqcomi ⊢ 0 = ( deg ‘ 0𝑝 )
65 62 2 64 3eqtr4g ⊢ ( 𝐺 = 0𝑝 → 𝑁 = 0 )
66 61 65 biimtrrdi ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) = 0 → 𝑁 = 0 ) )
67 66 necon3d ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( 𝑁 ≠ 0 → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 ) )
68 56 60 67 sylc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 )
69 55 68 eqnetrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) ‘ 𝑁 ) ≠ 0 )
70 eqid ⊢ ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) )
71 eqid ⊢ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( deg ‘ ( 𝐹 ∘f + 𝐺 ) )
72 70 71 dgrub ⊢ ( ( ( 𝐹 ∘f + 𝐺 ) ∈ ( Poly ‘ ℂ ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) ‘ 𝑁 ) ≠ 0 ) → 𝑁 ≤ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) )
73 4 10 69 72 syl3anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → 𝑁 ≤ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) )
74 7 11 letri3d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) = 𝑁 ↔ ( ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ 𝑁 ∧ 𝑁 ≤ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ) ) )
75 26 73 74 mpbir2and ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 < 𝑁 ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) = 𝑁 )