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