This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem deg1lt

Description: If the degree of a univariate polynomial is less than some index, then that coefficient must be zero. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1leb.d 
|- D = ( deg1 ` R )
deg1leb.p 
|- P = ( Poly1 ` R )
deg1leb.b 
|- B = ( Base ` P )
deg1leb.y 
|- .0. = ( 0g ` R )
deg1leb.a 
|- A = ( coe1 ` F )
Assertion deg1lt 
|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( A ` G ) = .0. )

Proof

Step Hyp Ref Expression
1 deg1leb.d 
 |-  D = ( deg1 ` R )
2 deg1leb.p 
 |-  P = ( Poly1 ` R )
3 deg1leb.b 
 |-  B = ( Base ` P )
4 deg1leb.y 
 |-  .0. = ( 0g ` R )
5 deg1leb.a 
 |-  A = ( coe1 ` F )
6 simp3 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( D ` F ) < G )
7 breq2 
 |-  ( x = G -> ( ( D ` F ) < x <-> ( D ` F ) < G ) )
8 fveqeq2 
 |-  ( x = G -> ( ( A ` x ) = .0. <-> ( A ` G ) = .0. ) )
9 7 8 imbi12d 
 |-  ( x = G -> ( ( ( D ` F ) < x -> ( A ` x ) = .0. ) <-> ( ( D ` F ) < G -> ( A ` G ) = .0. ) ) )
10 1 2 3 deg1xrcl 
 |-  ( F e. B -> ( D ` F ) e. RR* )
11 10 3ad2ant1 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( D ` F ) e. RR* )
12 11 xrleidd 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( D ` F ) <_ ( D ` F ) )
13 simp1 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> F e. B )
14 1 2 3 4 5 deg1leb 
 |-  ( ( F e. B /\ ( D ` F ) e. RR* ) -> ( ( D ` F ) <_ ( D ` F ) <-> A. x e. NN0 ( ( D ` F ) < x -> ( A ` x ) = .0. ) ) )
15 13 10 14 syl2anc2 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( ( D ` F ) <_ ( D ` F ) <-> A. x e. NN0 ( ( D ` F ) < x -> ( A ` x ) = .0. ) ) )
16 12 15 mpbid 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> A. x e. NN0 ( ( D ` F ) < x -> ( A ` x ) = .0. ) )
17 simp2 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> G e. NN0 )
18 9 16 17 rspcdva 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( ( D ` F ) < G -> ( A ` G ) = .0. ) )
19 6 18 mpd 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( A ` G ) = .0. )