# Metamath Proof Explorer

## 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( A e. RR /\ A < 2 ) -> ( ppi ` A ) e. NN0 )`
` |-  ( ( ppi ` A ) e. NN0 -> ( ( ppi ` A ) <_ 0 <-> ( ppi ` A ) = 0 ) )`
` |-  ( ( A e. RR /\ A < 2 ) -> ( ( ppi ` A ) <_ 0 <-> ( ppi ` A ) = 0 ) )`
` |-  ( ( A e. RR /\ A < 2 ) -> ( ppi ` A ) = 0 )`
` |-  ( A e. RR -> ( A < 2 -> ( ppi ` A ) = 0 ) )`
` |-  ( A e. RR -> ( ( ppi ` A ) = 0 <-> A < 2 ) )`