Metamath Proof Explorer

Theorem ppiwordi

Description: The prime-counting function ppi is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014)

Ref Expression
Assertion ppiwordi 
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ppi ` A ) <_ ( ppi ` B ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> B e. RR )
2 ppifi 
 |-  ( B e. RR -> ( ( 0 [,] B ) i^i Prime ) e. Fin )
3 1 2 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( 0 [,] B ) i^i Prime ) e. Fin )
4 0red 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> 0 e. RR )
5 0le0 
 |-  0 <_ 0
6 5 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> 0 <_ 0 )
7 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A <_ B )
8 iccss 
 |-  ( ( ( 0 e. RR /\ B e. RR ) /\ ( 0 <_ 0 /\ A <_ B ) ) -> ( 0 [,] A ) C_ ( 0 [,] B ) )
9 4 1 6 7 8 syl22anc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( 0 [,] A ) C_ ( 0 [,] B ) )
10 9 ssrind 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( 0 [,] A ) i^i Prime ) C_ ( ( 0 [,] B ) i^i Prime ) )
11 ssdomg 
 |-  ( ( ( 0 [,] B ) i^i Prime ) e. Fin -> ( ( ( 0 [,] A ) i^i Prime ) C_ ( ( 0 [,] B ) i^i Prime ) -> ( ( 0 [,] A ) i^i Prime ) ~<_ ( ( 0 [,] B ) i^i Prime ) ) )
12 3 10 11 sylc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( 0 [,] A ) i^i Prime ) ~<_ ( ( 0 [,] B ) i^i Prime ) )
13 ppifi 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
14 13 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
15 hashdom 
 |-  ( ( ( ( 0 [,] A ) i^i Prime ) e. Fin /\ ( ( 0 [,] B ) i^i Prime ) e. Fin ) -> ( ( # ` ( ( 0 [,] A ) i^i Prime ) ) <_ ( # ` ( ( 0 [,] B ) i^i Prime ) ) <-> ( ( 0 [,] A ) i^i Prime ) ~<_ ( ( 0 [,] B ) i^i Prime ) ) )
16 14 3 15 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( # ` ( ( 0 [,] A ) i^i Prime ) ) <_ ( # ` ( ( 0 [,] B ) i^i Prime ) ) <-> ( ( 0 [,] A ) i^i Prime ) ~<_ ( ( 0 [,] B ) i^i Prime ) ) )
17 12 16 mpbird 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( # ` ( ( 0 [,] A ) i^i Prime ) ) <_ ( # ` ( ( 0 [,] B ) i^i Prime ) ) )
18 ppival 
 |-  ( A e. RR -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
19 18 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
20 ppival 
 |-  ( B e. RR -> ( ppi ` B ) = ( # ` ( ( 0 [,] B ) i^i Prime ) ) )
21 1 20 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ppi ` B ) = ( # ` ( ( 0 [,] B ) i^i Prime ) ) )
22 17 19 21 3brtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ppi ` A ) <_ ( ppi ` B ) )