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

Metamath Proof Explorer

Theorem chpeq0

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

Ref Expression
Assertion chpeq0 
|- ( A e. RR -> ( ( psi ` 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 chprpcl 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( psi ` A ) e. RR+ )
5 4 rpne0d 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( psi ` A ) =/= 0 )
6 5 ex 
 |-  ( A e. RR -> ( 2 <_ A -> ( psi ` A ) =/= 0 ) )
7 3 6 sylbird 
 |-  ( A e. RR -> ( -. A < 2 -> ( psi ` A ) =/= 0 ) )
8 7 necon4bd 
 |-  ( A e. RR -> ( ( psi ` A ) = 0 -> A < 2 ) )
9 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
10 9 adantr 
 |-  ( ( A e. RR /\ A < 2 ) -> ( |_ ` A ) e. RR )
11 1red 
 |-  ( ( A e. RR /\ A < 2 ) -> 1 e. RR )
12 2z 
 |-  2 e. ZZ
13 fllt 
 |-  ( ( A e. RR /\ 2 e. ZZ ) -> ( A < 2 <-> ( |_ ` A ) < 2 ) )
14 12 13 mpan2 
 |-  ( A e. RR -> ( A < 2 <-> ( |_ ` A ) < 2 ) )
15 14 biimpa 
 |-  ( ( A e. RR /\ A < 2 ) -> ( |_ ` A ) < 2 )
16 df-2 
 |-  2 = ( 1 + 1 )
17 15 16 breqtrdi 
 |-  ( ( A e. RR /\ A < 2 ) -> ( |_ ` A ) < ( 1 + 1 ) )
18 flcl 
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
19 18 adantr 
 |-  ( ( A e. RR /\ A < 2 ) -> ( |_ ` A ) e. ZZ )
20 1z 
 |-  1 e. ZZ
21 zleltp1 
 |-  ( ( ( |_ ` A ) e. ZZ /\ 1 e. ZZ ) -> ( ( |_ ` A ) <_ 1 <-> ( |_ ` A ) < ( 1 + 1 ) ) )
22 19 20 21 sylancl 
 |-  ( ( A e. RR /\ A < 2 ) -> ( ( |_ ` A ) <_ 1 <-> ( |_ ` A ) < ( 1 + 1 ) ) )
23 17 22 mpbird 
 |-  ( ( A e. RR /\ A < 2 ) -> ( |_ ` A ) <_ 1 )
24 chpwordi 
 |-  ( ( ( |_ ` A ) e. RR /\ 1 e. RR /\ ( |_ ` A ) <_ 1 ) -> ( psi ` ( |_ ` A ) ) <_ ( psi ` 1 ) )
25 10 11 23 24 syl3anc 
 |-  ( ( A e. RR /\ A < 2 ) -> ( psi ` ( |_ ` A ) ) <_ ( psi ` 1 ) )
26 chpfl 
 |-  ( A e. RR -> ( psi ` ( |_ ` A ) ) = ( psi ` A ) )
27 26 adantr 
 |-  ( ( A e. RR /\ A < 2 ) -> ( psi ` ( |_ ` A ) ) = ( psi ` A ) )
28 chp1 
 |-  ( psi ` 1 ) = 0
29 28 a1i 
 |-  ( ( A e. RR /\ A < 2 ) -> ( psi ` 1 ) = 0 )
30 25 27 29 3brtr3d 
 |-  ( ( A e. RR /\ A < 2 ) -> ( psi ` A ) <_ 0 )
31 chpge0 
 |-  ( A e. RR -> 0 <_ ( psi ` A ) )
32 31 adantr 
 |-  ( ( A e. RR /\ A < 2 ) -> 0 <_ ( psi ` A ) )
33 chpcl 
 |-  ( A e. RR -> ( psi ` A ) e. RR )
34 33 adantr 
 |-  ( ( A e. RR /\ A < 2 ) -> ( psi ` A ) e. RR )
35 0re 
 |-  0 e. RR
36 letri3 
 |-  ( ( ( psi ` A ) e. RR /\ 0 e. RR ) -> ( ( psi ` A ) = 0 <-> ( ( psi ` A ) <_ 0 /\ 0 <_ ( psi ` A ) ) ) )
37 34 35 36 sylancl 
 |-  ( ( A e. RR /\ A < 2 ) -> ( ( psi ` A ) = 0 <-> ( ( psi ` A ) <_ 0 /\ 0 <_ ( psi ` A ) ) ) )
38 30 32 37 mpbir2and 
 |-  ( ( A e. RR /\ A < 2 ) -> ( psi ` A ) = 0 )
39 38 ex 
 |-  ( A e. RR -> ( A < 2 -> ( psi ` A ) = 0 ) )
40 8 39 impbid 
 |-  ( A e. RR -> ( ( psi ` A ) = 0 <-> A < 2 ) )