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 
|- M = ( deg ` F )
dgradd.2 
|- N = ( deg ` G )
Assertion dgradd2 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( deg ` ( F oF + G ) ) = N )

Proof

Step Hyp Ref Expression
1 dgradd.1 
 |-  M = ( deg ` F )
2 dgradd.2 
 |-  N = ( deg ` G )
3 plyaddcl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF + G ) e. ( Poly ` CC ) )
4 3 3adant3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( F oF + G ) e. ( Poly ` CC ) )
5 dgrcl 
 |-  ( ( F oF + G ) e. ( Poly ` CC ) -> ( deg ` ( F oF + G ) ) e. NN0 )
6 4 5 syl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( deg ` ( F oF + G ) ) e. NN0 )
7 6 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( deg ` ( F oF + G ) ) e. RR )
8 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
9 2 8 eqeltrid 
 |-  ( G e. ( Poly ` S ) -> N e. NN0 )
10 9 3ad2ant2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> N e. NN0 )
11 10 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> N e. RR )
12 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
13 1 12 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> M e. NN0 )
14 13 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> M e. NN0 )
15 14 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> M e. RR )
16 11 15 ifcld 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> if ( M <_ N , N , M ) e. RR )
17 1 2 dgradd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF + G ) ) <_ if ( M <_ N , N , M ) )
18 17 3adant3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( deg ` ( F oF + G ) ) <_ if ( M <_ N , N , M ) )
19 11 leidd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> N <_ N )
20 simp3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> M < N )
21 15 11 20 ltled 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> M <_ N )
22 breq1 
 |-  ( N = if ( M <_ N , N , M ) -> ( N <_ N <-> if ( M <_ N , N , M ) <_ N ) )
23 breq1 
 |-  ( M = if ( M <_ N , N , M ) -> ( M <_ N <-> if ( M <_ N , N , M ) <_ N ) )
24 22 23 ifboth 
 |-  ( ( N <_ N /\ M <_ N ) -> if ( M <_ N , N , M ) <_ N )
25 19 21 24 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> if ( M <_ N , N , M ) <_ N )
26 7 16 11 18 25 letrd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( deg ` ( F oF + G ) ) <_ N )
27 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
28 eqid 
 |-  ( coeff ` G ) = ( coeff ` G )
29 27 28 coeadd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF + G ) ) = ( ( coeff ` F ) oF + ( coeff ` G ) ) )
30 29 3adant3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( coeff ` ( F oF + G ) ) = ( ( coeff ` F ) oF + ( coeff ` G ) ) )
31 30 fveq1d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( coeff ` ( F oF + G ) ) ` N ) = ( ( ( coeff ` F ) oF + ( coeff ` G ) ) ` N ) )
32 27 coef3 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
33 32 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( coeff ` F ) : NN0 --> CC )
34 33 ffnd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( coeff ` F ) Fn NN0 )
35 28 coef3 
 |-  ( G e. ( Poly ` S ) -> ( coeff ` G ) : NN0 --> CC )
36 35 3ad2ant2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( coeff ` G ) : NN0 --> CC )
37 36 ffnd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( coeff ` G ) Fn NN0 )
38 nn0ex 
 |-  NN0 e. _V
39 38 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> NN0 e. _V )
40 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
41 15 11 ltnled 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( M < N <-> -. N <_ M ) )
42 20 41 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> -. N <_ M )
43 simp1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> F e. ( Poly ` S ) )
44 27 1 dgrub 
 |-  ( ( F e. ( Poly ` S ) /\ N e. NN0 /\ ( ( coeff ` F ) ` N ) =/= 0 ) -> N <_ M )
45 44 3expia 
 |-  ( ( F e. ( Poly ` S ) /\ N e. NN0 ) -> ( ( ( coeff ` F ) ` N ) =/= 0 -> N <_ M ) )
46 43 10 45 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( ( coeff ` F ) ` N ) =/= 0 -> N <_ M ) )
47 46 necon1bd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( -. N <_ M -> ( ( coeff ` F ) ` N ) = 0 ) )
48 42 47 mpd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( coeff ` F ) ` N ) = 0 )
49 48 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) /\ N e. NN0 ) -> ( ( coeff ` F ) ` N ) = 0 )
50 eqidd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) /\ N e. NN0 ) -> ( ( coeff ` G ) ` N ) = ( ( coeff ` G ) ` N ) )
51 34 37 39 39 40 49 50 ofval 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) /\ N e. NN0 ) -> ( ( ( coeff ` F ) oF + ( coeff ` G ) ) ` N ) = ( 0 + ( ( coeff ` G ) ` N ) ) )
52 10 51 mpdan 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( ( coeff ` F ) oF + ( coeff ` G ) ) ` N ) = ( 0 + ( ( coeff ` G ) ` N ) ) )
53 36 10 ffvelrnd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( coeff ` G ) ` N ) e. CC )
54 53 addid2d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( 0 + ( ( coeff ` G ) ` N ) ) = ( ( coeff ` G ) ` N ) )
55 31 52 54 3eqtrd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( coeff ` ( F oF + G ) ) ` N ) = ( ( coeff ` G ) ` N ) )
56 simp2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> G e. ( Poly ` S ) )
57 0red 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> 0 e. RR )
58 14 nn0ge0d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> 0 <_ M )
59 57 15 11 58 20 lelttrd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> 0 < N )
60 59 gt0ne0d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> N =/= 0 )
61 2 28 dgreq0 
 |-  ( G e. ( Poly ` S ) -> ( G = 0p <-> ( ( coeff ` G ) ` N ) = 0 ) )
62 fveq2 
 |-  ( G = 0p -> ( deg ` G ) = ( deg ` 0p ) )
63 dgr0 
 |-  ( deg ` 0p ) = 0
64 63 eqcomi 
 |-  0 = ( deg ` 0p )
65 62 2 64 3eqtr4g 
 |-  ( G = 0p -> N = 0 )
66 61 65 syl6bir 
 |-  ( G e. ( Poly ` S ) -> ( ( ( coeff ` G ) ` N ) = 0 -> N = 0 ) )
67 66 necon3d 
 |-  ( G e. ( Poly ` S ) -> ( N =/= 0 -> ( ( coeff ` G ) ` N ) =/= 0 ) )
68 56 60 67 sylc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( coeff ` G ) ` N ) =/= 0 )
69 55 68 eqnetrd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( coeff ` ( F oF + G ) ) ` N ) =/= 0 )
70 eqid 
 |-  ( coeff ` ( F oF + G ) ) = ( coeff ` ( F oF + G ) )
71 eqid 
 |-  ( deg ` ( F oF + G ) ) = ( deg ` ( F oF + G ) )
72 70 71 dgrub 
 |-  ( ( ( F oF + G ) e. ( Poly ` CC ) /\ N e. NN0 /\ ( ( coeff ` ( F oF + G ) ) ` N ) =/= 0 ) -> N <_ ( deg ` ( F oF + G ) ) )
73 4 10 69 72 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> N <_ ( deg ` ( F oF + G ) ) )
74 7 11 letri3d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( ( deg ` ( F oF + G ) ) = N <-> ( ( deg ` ( F oF + G ) ) <_ N /\ N <_ ( deg ` ( F oF + G ) ) ) ) )
75 26 73 74 mpbir2and 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ M < N ) -> ( deg ` ( F oF + G ) ) = N )