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

Metamath Proof Explorer

Theorem chteq0

Description: The first Chebyshev function is zero iff its argument is less than 2 . (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Assertion chteq0 
|- ( A e. RR -> ( ( theta ` A ) = 0 <-> A < 2 ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 lenlt 
 |-  ( ( 2 e. RR /\ A e. RR ) -> ( 2 <_ A <-> -. A < 2 ) )
3 1 2 mpan 
 |-  ( A e. RR -> ( 2 <_ A <-> -. A < 2 ) )
4 chtrpcl 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( theta ` A ) e. RR+ )
5 4 rpne0d 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( theta ` A ) =/= 0 )
6 5 ex 
 |-  ( A e. RR -> ( 2 <_ A -> ( theta ` A ) =/= 0 ) )
7 3 6 sylbird 
 |-  ( A e. RR -> ( -. A < 2 -> ( theta ` A ) =/= 0 ) )
8 7 necon4bd 
 |-  ( A e. RR -> ( ( theta ` A ) = 0 -> A < 2 ) )
9 chtlepsi 
 |-  ( A e. RR -> ( theta ` A ) <_ ( psi ` A ) )
10 9 adantr 
 |-  ( ( A e. RR /\ A < 2 ) -> ( theta ` A ) <_ ( psi ` A ) )
11 chpeq0 
 |-  ( A e. RR -> ( ( psi ` A ) = 0 <-> A < 2 ) )
12 11 biimpar 
 |-  ( ( A e. RR /\ A < 2 ) -> ( psi ` A ) = 0 )
13 10 12 breqtrd 
 |-  ( ( A e. RR /\ A < 2 ) -> ( theta ` A ) <_ 0 )
14 chtge0 
 |-  ( A e. RR -> 0 <_ ( theta ` A ) )
15 14 adantr 
 |-  ( ( A e. RR /\ A < 2 ) -> 0 <_ ( theta ` A ) )
16 chtcl 
 |-  ( A e. RR -> ( theta ` A ) e. RR )
17 16 adantr 
 |-  ( ( A e. RR /\ A < 2 ) -> ( theta ` A ) e. RR )
18 0re 
 |-  0 e. RR
19 letri3 
 |-  ( ( ( theta ` A ) e. RR /\ 0 e. RR ) -> ( ( theta ` A ) = 0 <-> ( ( theta ` A ) <_ 0 /\ 0 <_ ( theta ` A ) ) ) )
20 17 18 19 sylancl 
 |-  ( ( A e. RR /\ A < 2 ) -> ( ( theta ` A ) = 0 <-> ( ( theta ` A ) <_ 0 /\ 0 <_ ( theta ` A ) ) ) )
21 13 15 20 mpbir2and 
 |-  ( ( A e. RR /\ A < 2 ) -> ( theta ` A ) = 0 )
22 21 ex 
 |-  ( A e. RR -> ( A < 2 -> ( theta ` A ) = 0 ) )
23 8 22 impbid 
 |-  ( A e. RR -> ( ( theta ` A ) = 0 <-> A < 2 ) )