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 ) )