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