Metamath Proof Explorer

Theorem ppiltx

Description: The prime-counting function ppi is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 ppicl 
 |-  ( A e. RR -> ( ppi ` A ) e. NN0 )
3 1 2 syl 
 |-  ( A e. RR+ -> ( ppi ` A ) e. NN0 )
4 3 nn0red 
 |-  ( A e. RR+ -> ( ppi ` A ) e. RR )
5 4 adantr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( ppi ` A ) e. RR )
6 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
7 1 6 syl 
 |-  ( A e. RR+ -> ( |_ ` A ) e. RR )
8 7 adantr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( |_ ` A ) e. RR )
9 1 adantr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> A e. RR )
10 fzfi 
 |-  ( 1 ... ( |_ ` A ) ) e. Fin
11 inss1 
 |-  ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( 2 ... ( |_ ` A ) )
12 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
13 fzss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` A ) ) )
14 12 13 mp1i 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( 2 ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` A ) ) )
15 simpr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( |_ ` A ) e. NN )
16 nnuz 
 |-  NN = ( ZZ>= ` 1 )
17 15 16 eleqtrdi 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( |_ ` A ) e. ( ZZ>= ` 1 ) )
18 eluzfz1 
 |-  ( ( |_ ` A ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( |_ ` A ) ) )
19 17 18 syl 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> 1 e. ( 1 ... ( |_ ` A ) ) )
20 1lt2 
 |-  1 < 2
21 1re 
 |-  1 e. RR
22 2re 
 |-  2 e. RR
23 21 22 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
24 20 23 mpbi 
 |-  -. 2 <_ 1
25 elfzle1 
 |-  ( 1 e. ( 2 ... ( |_ ` A ) ) -> 2 <_ 1 )
26 24 25 mto 
 |-  -. 1 e. ( 2 ... ( |_ ` A ) )
27 nelne1 
 |-  ( ( 1 e. ( 1 ... ( |_ ` A ) ) /\ -. 1 e. ( 2 ... ( |_ ` A ) ) ) -> ( 1 ... ( |_ ` A ) ) =/= ( 2 ... ( |_ ` A ) ) )
28 19 26 27 sylancl 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( 1 ... ( |_ ` A ) ) =/= ( 2 ... ( |_ ` A ) ) )
29 28 necomd 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( 2 ... ( |_ ` A ) ) =/= ( 1 ... ( |_ ` A ) ) )
30 df-pss 
 |-  ( ( 2 ... ( |_ ` A ) ) C. ( 1 ... ( |_ ` A ) ) <-> ( ( 2 ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` A ) ) /\ ( 2 ... ( |_ ` A ) ) =/= ( 1 ... ( |_ ` A ) ) ) )
31 14 29 30 sylanbrc 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( 2 ... ( |_ ` A ) ) C. ( 1 ... ( |_ ` A ) ) )
32 sspsstr 
 |-  ( ( ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( 2 ... ( |_ ` A ) ) /\ ( 2 ... ( |_ ` A ) ) C. ( 1 ... ( |_ ` A ) ) ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C. ( 1 ... ( |_ ` A ) ) )
33 11 31 32 sylancr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C. ( 1 ... ( |_ ` A ) ) )
34 php3 
 |-  ( ( ( 1 ... ( |_ ` A ) ) e. Fin /\ ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C. ( 1 ... ( |_ ` A ) ) ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ~< ( 1 ... ( |_ ` A ) ) )
35 10 33 34 sylancr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ~< ( 1 ... ( |_ ` A ) ) )
36 fzfi 
 |-  ( 2 ... ( |_ ` A ) ) e. Fin
37 ssfi 
 |-  ( ( ( 2 ... ( |_ ` A ) ) e. Fin /\ ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( 2 ... ( |_ ` A ) ) ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) e. Fin )
38 36 11 37 mp2an 
 |-  ( ( 2 ... ( |_ ` A ) ) i^i Prime ) e. Fin
39 hashsdom 
 |-  ( ( ( ( 2 ... ( |_ ` A ) ) i^i Prime ) e. Fin /\ ( 1 ... ( |_ ` A ) ) e. Fin ) -> ( ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) < ( # ` ( 1 ... ( |_ ` A ) ) ) <-> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ~< ( 1 ... ( |_ ` A ) ) ) )
40 38 10 39 mp2an 
 |-  ( ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) < ( # ` ( 1 ... ( |_ ` A ) ) ) <-> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ~< ( 1 ... ( |_ ` A ) ) )
41 35 40 sylibr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) < ( # ` ( 1 ... ( |_ ` A ) ) ) )
42 1 flcld 
 |-  ( A e. RR+ -> ( |_ ` A ) e. ZZ )
43 ppival2 
 |-  ( ( |_ ` A ) e. ZZ -> ( ppi ` ( |_ ` A ) ) = ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) )
44 42 43 syl 
 |-  ( A e. RR+ -> ( ppi ` ( |_ ` A ) ) = ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) )
45 ppifl 
 |-  ( A e. RR -> ( ppi ` ( |_ ` A ) ) = ( ppi ` A ) )
46 1 45 syl 
 |-  ( A e. RR+ -> ( ppi ` ( |_ ` A ) ) = ( ppi ` A ) )
47 44 46 eqtr3d 
 |-  ( A e. RR+ -> ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) = ( ppi ` A ) )
48 47 adantr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) = ( ppi ` A ) )
49 rpge0 
 |-  ( A e. RR+ -> 0 <_ A )
50 flge0nn0 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )
51 1 49 50 syl2anc 
 |-  ( A e. RR+ -> ( |_ ` A ) e. NN0 )
52 hashfz1 
 |-  ( ( |_ ` A ) e. NN0 -> ( # ` ( 1 ... ( |_ ` A ) ) ) = ( |_ ` A ) )
53 51 52 syl 
 |-  ( A e. RR+ -> ( # ` ( 1 ... ( |_ ` A ) ) ) = ( |_ ` A ) )
54 53 adantr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( # ` ( 1 ... ( |_ ` A ) ) ) = ( |_ ` A ) )
55 41 48 54 3brtr3d 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( ppi ` A ) < ( |_ ` A ) )
56 flle 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
57 9 56 syl 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( |_ ` A ) <_ A )
58 5 8 9 55 57 ltletrd 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) e. NN ) -> ( ppi ` A ) < A )
59 46 adantr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) = 0 ) -> ( ppi ` ( |_ ` A ) ) = ( ppi ` A ) )
60 simpr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) = 0 ) -> ( |_ ` A ) = 0 )
61 60 fveq2d 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) = 0 ) -> ( ppi ` ( |_ ` A ) ) = ( ppi ` 0 ) )
62 2pos 
 |-  0 < 2
63 0re 
 |-  0 e. RR
64 ppieq0 
 |-  ( 0 e. RR -> ( ( ppi ` 0 ) = 0 <-> 0 < 2 ) )
65 63 64 ax-mp 
 |-  ( ( ppi ` 0 ) = 0 <-> 0 < 2 )
66 62 65 mpbir 
 |-  ( ppi ` 0 ) = 0
67 61 66 eqtrdi 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) = 0 ) -> ( ppi ` ( |_ ` A ) ) = 0 )
68 59 67 eqtr3d 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) = 0 ) -> ( ppi ` A ) = 0 )
69 rpgt0 
 |-  ( A e. RR+ -> 0 < A )
70 69 adantr 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) = 0 ) -> 0 < A )
71 68 70 eqbrtrd 
 |-  ( ( A e. RR+ /\ ( |_ ` A ) = 0 ) -> ( ppi ` A ) < A )
72 elnn0 
 |-  ( ( |_ ` A ) e. NN0 <-> ( ( |_ ` A ) e. NN \/ ( |_ ` A ) = 0 ) )
73 51 72 sylib 
 |-  ( A e. RR+ -> ( ( |_ ` A ) e. NN \/ ( |_ ` A ) = 0 ) )
74 58 71 73 mpjaodan 
 |-  ( A e. RR+ -> ( ppi ` A ) < A )