Metamath Proof Explorer

Theorem deg1le1

Description: Dichotomy for a univariate polynomial of degree at most one. (Contributed by Thierry Arnoux, 8-Nov-2026)

Ref Expression
Hypotheses deg1le1.d 
|- D = ( deg1 ` R )
deg1le1.p 
|- P = ( Poly1 ` R )
deg1le1.b 
|- B = ( Base ` P )
deg1le1.f 
|- ( ph -> F e. B )
deg1le1.1 
|- ( ph -> ( D ` F ) <_ 1 )
Assertion deg1le1 
|- ( ph -> ( ( D ` F ) <_ 0 \/ ( D ` F ) = 1 ) )

Proof

Step Hyp Ref Expression
1 deg1le1.d 
 |-  D = ( deg1 ` R )
2 deg1le1.p 
 |-  P = ( Poly1 ` R )
3 deg1le1.b 
 |-  B = ( Base ` P )
4 deg1le1.f 
 |-  ( ph -> F e. B )
5 deg1le1.1 
 |-  ( ph -> ( D ` F ) <_ 1 )
6 simpr 
 |-  ( ( ( ph /\ ( D ` F ) e. NN0 ) /\ ( D ` F ) = 0 ) -> ( D ` F ) = 0 )
7 0le0 
 |-  0 <_ 0
8 6 7 eqbrtrdi 
 |-  ( ( ( ph /\ ( D ` F ) e. NN0 ) /\ ( D ` F ) = 0 ) -> ( D ` F ) <_ 0 )
9 simpr 
 |-  ( ( ( ph /\ ( D ` F ) e. NN0 ) /\ ( D ` F ) = 1 ) -> ( D ` F ) = 1 )
10 simpr 
 |-  ( ( ph /\ ( D ` F ) e. NN0 ) -> ( D ` F ) e. NN0 )
11 1nn0 
 |-  1 e. NN0
12 11 a1i 
 |-  ( ( ph /\ ( D ` F ) e. NN0 ) -> 1 e. NN0 )
13 5 adantr 
 |-  ( ( ph /\ ( D ` F ) e. NN0 ) -> ( D ` F ) <_ 1 )
14 nn0leltp1 
 |-  ( ( ( D ` F ) e. NN0 /\ 1 e. NN0 ) -> ( ( D ` F ) <_ 1 <-> ( D ` F ) < ( 1 + 1 ) ) )
15 14 biimpa 
 |-  ( ( ( ( D ` F ) e. NN0 /\ 1 e. NN0 ) /\ ( D ` F ) <_ 1 ) -> ( D ` F ) < ( 1 + 1 ) )
16 10 12 13 15 syl21anc 
 |-  ( ( ph /\ ( D ` F ) e. NN0 ) -> ( D ` F ) < ( 1 + 1 ) )
17 1p1e2 
 |-  ( 1 + 1 ) = 2
18 16 17 breqtrdi 
 |-  ( ( ph /\ ( D ` F ) e. NN0 ) -> ( D ` F ) < 2 )
19 nn0lt2 
 |-  ( ( ( D ` F ) e. NN0 /\ ( D ` F ) < 2 ) -> ( ( D ` F ) = 0 \/ ( D ` F ) = 1 ) )
20 10 18 19 syl2anc 
 |-  ( ( ph /\ ( D ` F ) e. NN0 ) -> ( ( D ` F ) = 0 \/ ( D ` F ) = 1 ) )
21 8 9 20 orim12da 
 |-  ( ( ph /\ ( D ` F ) e. NN0 ) -> ( ( D ` F ) <_ 0 \/ ( D ` F ) = 1 ) )
22 simpr 
 |-  ( ( ph /\ ( D ` F ) = -oo ) -> ( D ` F ) = -oo )
23 0xr 
 |-  0 e. RR*
24 23 a1i 
 |-  ( ( ph /\ ( D ` F ) = -oo ) -> 0 e. RR* )
25 24 mnfled 
 |-  ( ( ph /\ ( D ` F ) = -oo ) -> -oo <_ 0 )
26 22 25 eqbrtrd 
 |-  ( ( ph /\ ( D ` F ) = -oo ) -> ( D ` F ) <_ 0 )
27 26 orcd 
 |-  ( ( ph /\ ( D ` F ) = -oo ) -> ( ( D ` F ) <_ 0 \/ ( D ` F ) = 1 ) )
28 1 2 3 deg1cl 
 |-  ( F e. B -> ( D ` F ) e. ( NN0 u. { -oo } ) )
29 elunsn 
 |-  ( ( D ` F ) e. ( NN0 u. { -oo } ) -> ( ( D ` F ) e. ( NN0 u. { -oo } ) <-> ( ( D ` F ) e. NN0 \/ ( D ` F ) = -oo ) ) )
30 29 ibi 
 |-  ( ( D ` F ) e. ( NN0 u. { -oo } ) -> ( ( D ` F ) e. NN0 \/ ( D ` F ) = -oo ) )
31 4 28 30 3syl 
 |-  ( ph -> ( ( D ` F ) e. NN0 \/ ( D ` F ) = -oo ) )
32 21 27 31 mpjaodan 
 |-  ( ph -> ( ( D ` F ) <_ 0 \/ ( D ` F ) = 1 ) )