Metamath Proof Explorer


Theorem ppip1le

Description: The prime-counting function ppi cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion ppip1le
|- ( A e. RR -> ( ppi ` ( A + 1 ) ) <_ ( ( ppi ` A ) + 1 ) )

Proof

Step Hyp Ref Expression
1 flcl
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
2 zre
 |-  ( ( |_ ` A ) e. ZZ -> ( |_ ` A ) e. RR )
3 peano2re
 |-  ( ( |_ ` A ) e. RR -> ( ( |_ ` A ) + 1 ) e. RR )
4 2 3 syl
 |-  ( ( |_ ` A ) e. ZZ -> ( ( |_ ` A ) + 1 ) e. RR )
5 4 adantr
 |-  ( ( ( |_ ` A ) e. ZZ /\ ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ( |_ ` A ) + 1 ) e. RR )
6 ppicl
 |-  ( ( ( |_ ` A ) + 1 ) e. RR -> ( ppi ` ( ( |_ ` A ) + 1 ) ) e. NN0 )
7 5 6 syl
 |-  ( ( ( |_ ` A ) e. ZZ /\ ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ppi ` ( ( |_ ` A ) + 1 ) ) e. NN0 )
8 7 nn0red
 |-  ( ( ( |_ ` A ) e. ZZ /\ ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ppi ` ( ( |_ ` A ) + 1 ) ) e. RR )
9 ppiprm
 |-  ( ( ( |_ ` A ) e. ZZ /\ ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ppi ` ( ( |_ ` A ) + 1 ) ) = ( ( ppi ` ( |_ ` A ) ) + 1 ) )
10 8 9 eqled
 |-  ( ( ( |_ ` A ) e. ZZ /\ ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ppi ` ( ( |_ ` A ) + 1 ) ) <_ ( ( ppi ` ( |_ ` A ) ) + 1 ) )
11 ppinprm
 |-  ( ( ( |_ ` A ) e. ZZ /\ -. ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ppi ` ( ( |_ ` A ) + 1 ) ) = ( ppi ` ( |_ ` A ) ) )
12 ppicl
 |-  ( ( |_ ` A ) e. RR -> ( ppi ` ( |_ ` A ) ) e. NN0 )
13 2 12 syl
 |-  ( ( |_ ` A ) e. ZZ -> ( ppi ` ( |_ ` A ) ) e. NN0 )
14 13 nn0red
 |-  ( ( |_ ` A ) e. ZZ -> ( ppi ` ( |_ ` A ) ) e. RR )
15 14 adantr
 |-  ( ( ( |_ ` A ) e. ZZ /\ -. ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ppi ` ( |_ ` A ) ) e. RR )
16 15 lep1d
 |-  ( ( ( |_ ` A ) e. ZZ /\ -. ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ppi ` ( |_ ` A ) ) <_ ( ( ppi ` ( |_ ` A ) ) + 1 ) )
17 11 16 eqbrtrd
 |-  ( ( ( |_ ` A ) e. ZZ /\ -. ( ( |_ ` A ) + 1 ) e. Prime ) -> ( ppi ` ( ( |_ ` A ) + 1 ) ) <_ ( ( ppi ` ( |_ ` A ) ) + 1 ) )
18 10 17 pm2.61dan
 |-  ( ( |_ ` A ) e. ZZ -> ( ppi ` ( ( |_ ` A ) + 1 ) ) <_ ( ( ppi ` ( |_ ` A ) ) + 1 ) )
19 1 18 syl
 |-  ( A e. RR -> ( ppi ` ( ( |_ ` A ) + 1 ) ) <_ ( ( ppi ` ( |_ ` A ) ) + 1 ) )
20 1z
 |-  1 e. ZZ
21 fladdz
 |-  ( ( A e. RR /\ 1 e. ZZ ) -> ( |_ ` ( A + 1 ) ) = ( ( |_ ` A ) + 1 ) )
22 20 21 mpan2
 |-  ( A e. RR -> ( |_ ` ( A + 1 ) ) = ( ( |_ ` A ) + 1 ) )
23 22 fveq2d
 |-  ( A e. RR -> ( ppi ` ( |_ ` ( A + 1 ) ) ) = ( ppi ` ( ( |_ ` A ) + 1 ) ) )
24 peano2re
 |-  ( A e. RR -> ( A + 1 ) e. RR )
25 ppifl
 |-  ( ( A + 1 ) e. RR -> ( ppi ` ( |_ ` ( A + 1 ) ) ) = ( ppi ` ( A + 1 ) ) )
26 24 25 syl
 |-  ( A e. RR -> ( ppi ` ( |_ ` ( A + 1 ) ) ) = ( ppi ` ( A + 1 ) ) )
27 23 26 eqtr3d
 |-  ( A e. RR -> ( ppi ` ( ( |_ ` A ) + 1 ) ) = ( ppi ` ( A + 1 ) ) )
28 ppifl
 |-  ( A e. RR -> ( ppi ` ( |_ ` A ) ) = ( ppi ` A ) )
29 28 oveq1d
 |-  ( A e. RR -> ( ( ppi ` ( |_ ` A ) ) + 1 ) = ( ( ppi ` A ) + 1 ) )
30 19 27 29 3brtr3d
 |-  ( A e. RR -> ( ppi ` ( A + 1 ) ) <_ ( ( ppi ` A ) + 1 ) )