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 + π _ A < A

Proof

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