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