Theorem ppieq0

Description: The prime-counting function ppi is zero iff its argument is less than 2 . (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	ppieq0	|- ( A e. RR -> ( ( ppi ` 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		ppinncl	|- ( ( A e. RR /\ 2 <_ A ) -> ( ppi ` A ) e. NN )
5	4	nnne0d	|- ( ( A e. RR /\ 2 <_ A ) -> ( ppi ` A ) =/= 0 )
6	5	ex	|- ( A e. RR -> ( 2 <_ A -> ( ppi ` A ) =/= 0 ) )
7	3 6	sylbird	|- ( A e. RR -> ( -. A < 2 -> ( ppi ` A ) =/= 0 ) )
8	7	necon4bd	|- ( A e. RR -> ( ( ppi ` 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		ppiwordi	|- ( ( ( |_ ` A ) e. RR /\ 1 e. RR /\ ( |_ ` A ) <_ 1 ) -> ( ppi ` ( |_ ` A ) ) <_ ( ppi ` 1 ) )
25	10 11 23 24	syl3anc	|- ( ( A e. RR /\ A < 2 ) -> ( ppi ` ( |_ ` A ) ) <_ ( ppi ` 1 ) )
26		ppifl	|- ( A e. RR -> ( ppi ` ( |_ ` A ) ) = ( ppi ` A ) )
27	26	adantr	|- ( ( A e. RR /\ A < 2 ) -> ( ppi ` ( |_ ` A ) ) = ( ppi ` A ) )
28		ppi1	|- ( ppi ` 1 ) = 0
29	28	a1i	|- ( ( A e. RR /\ A < 2 ) -> ( ppi ` 1 ) = 0 )
30	25 27 29	3brtr3d	|- ( ( A e. RR /\ A < 2 ) -> ( ppi ` A ) <_ 0 )
31		ppicl	|- ( A e. RR -> ( ppi ` A ) e. NN0 )
32	31	adantr	|- ( ( A e. RR /\ A < 2 ) -> ( ppi ` A ) e. NN0 )
33		nn0le0eq0	|- ( ( ppi ` A ) e. NN0 -> ( ( ppi ` A ) <_ 0 <-> ( ppi ` A ) = 0 ) )
34	32 33	syl	|- ( ( A e. RR /\ A < 2 ) -> ( ( ppi ` A ) <_ 0 <-> ( ppi ` A ) = 0 ) )
35	30 34	mpbid	|- ( ( A e. RR /\ A < 2 ) -> ( ppi ` A ) = 0 )
36	35	ex	|- ( A e. RR -> ( A < 2 -> ( ppi ` A ) = 0 ) )
37	8 36	impbid	|- ( A e. RR -> ( ( ppi ` A ) = 0 <-> A < 2 ) )