Metamath Proof Explorer

Theorem dgrlt

Description: Two ways to say that the degree of F is strictly less than N . (Contributed by Mario Carneiro, 25-Jul-2014)

Ref Expression
Hypotheses dgreq0.1 
|- N = ( deg ` F )
dgreq0.2 
|- A = ( coeff ` F )
Assertion dgrlt 
|- ( ( F e. ( Poly ` S ) /\ M e. NN0 ) -> ( ( F = 0p \/ N < M ) <-> ( N <_ M /\ ( A ` M ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 dgreq0.1 
 |-  N = ( deg ` F )
2 dgreq0.2 
 |-  A = ( coeff ` F )
3 simpr 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> F = 0p )
4 3 fveq2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> ( deg ` F ) = ( deg ` 0p ) )
5 dgr0 
 |-  ( deg ` 0p ) = 0
6 5 eqcomi 
 |-  0 = ( deg ` 0p )
7 4 1 6 3eqtr4g 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> N = 0 )
8 nn0ge0 
 |-  ( M e. NN0 -> 0 <_ M )
9 8 ad2antlr 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> 0 <_ M )
10 7 9 eqbrtrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> N <_ M )
11 3 fveq2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> ( coeff ` F ) = ( coeff ` 0p ) )
12 coe0 
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
13 12 eqcomi 
 |-  ( NN0 X. { 0 } ) = ( coeff ` 0p )
14 11 2 13 3eqtr4g 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> A = ( NN0 X. { 0 } ) )
15 14 fveq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> ( A ` M ) = ( ( NN0 X. { 0 } ) ` M ) )
16 c0ex 
 |-  0 e. _V
17 16 fvconst2 
 |-  ( M e. NN0 -> ( ( NN0 X. { 0 } ) ` M ) = 0 )
18 17 ad2antlr 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> ( ( NN0 X. { 0 } ) ` M ) = 0 )
19 15 18 eqtrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> ( A ` M ) = 0 )
20 10 19 jca 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ F = 0p ) -> ( N <_ M /\ ( A ` M ) = 0 ) )
21 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
22 1 21 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> N e. NN0 )
23 22 nn0red 
 |-  ( F e. ( Poly ` S ) -> N e. RR )
24 nn0re 
 |-  ( M e. NN0 -> M e. RR )
25 ltle 
 |-  ( ( N e. RR /\ M e. RR ) -> ( N < M -> N <_ M ) )
26 23 24 25 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 ) -> ( N < M -> N <_ M ) )
27 26 imp 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ N < M ) -> N <_ M )
28 2 1 dgrub 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> M <_ N )
29 28 3expia 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 ) -> ( ( A ` M ) =/= 0 -> M <_ N ) )
30 lenlt 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> -. N < M ) )
31 24 23 30 syl2anr 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 ) -> ( M <_ N <-> -. N < M ) )
32 29 31 sylibd 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 ) -> ( ( A ` M ) =/= 0 -> -. N < M ) )
33 32 necon4ad 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 ) -> ( N < M -> ( A ` M ) = 0 ) )
34 33 imp 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ N < M ) -> ( A ` M ) = 0 )
35 27 34 jca 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ N < M ) -> ( N <_ M /\ ( A ` M ) = 0 ) )
36 20 35 jaodan 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( F = 0p \/ N < M ) ) -> ( N <_ M /\ ( A ` M ) = 0 ) )
37 leloe 
 |-  ( ( N e. RR /\ M e. RR ) -> ( N <_ M <-> ( N < M \/ N = M ) ) )
38 23 24 37 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 ) -> ( N <_ M <-> ( N < M \/ N = M ) ) )
39 38 biimpa 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ N <_ M ) -> ( N < M \/ N = M ) )
40 39 adantrr 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( N < M \/ N = M ) )
41 fveq2 
 |-  ( N = M -> ( A ` N ) = ( A ` M ) )
42 1 2 dgreq0 
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` N ) = 0 ) )
43 42 ad2antrr 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( F = 0p <-> ( A ` N ) = 0 ) )
44 simprr 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( A ` M ) = 0 )
45 44 eqeq2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( ( A ` N ) = ( A ` M ) <-> ( A ` N ) = 0 ) )
46 43 45 bitr4d 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( F = 0p <-> ( A ` N ) = ( A ` M ) ) )
47 41 46 syl5ibr 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( N = M -> F = 0p ) )
48 47 orim2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( ( N < M \/ N = M ) -> ( N < M \/ F = 0p ) ) )
49 40 48 mpd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( N < M \/ F = 0p ) )
50 49 orcomd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 ) /\ ( N <_ M /\ ( A ` M ) = 0 ) ) -> ( F = 0p \/ N < M ) )
51 36 50 impbida 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 ) -> ( ( F = 0p \/ N < M ) <-> ( N <_ M /\ ( A ` M ) = 0 ) ) )