Metamath Proof Explorer


Theorem ppiprm

Description: The prime-counting function ppi at a prime. (Contributed by Mario Carneiro, 19-Sep-2014)

Ref Expression
Assertion ppiprm A A + 1 π _ A + 1 = π _ A + 1

Proof

Step Hyp Ref Expression
1 fzfid A A + 1 2 A Fin
2 inss1 2 A 2 A
3 ssfi 2 A Fin 2 A 2 A 2 A Fin
4 1 2 3 sylancl A A + 1 2 A Fin
5 zre A A
6 5 adantr A A + 1 A
7 6 ltp1d A A + 1 A < A + 1
8 peano2z A A + 1
9 8 adantr A A + 1 A + 1
10 9 zred A A + 1 A + 1
11 6 10 ltnled A A + 1 A < A + 1 ¬ A + 1 A
12 7 11 mpbid A A + 1 ¬ A + 1 A
13 elinel1 A + 1 2 A A + 1 2 A
14 elfzle2 A + 1 2 A A + 1 A
15 13 14 syl A + 1 2 A A + 1 A
16 12 15 nsyl A A + 1 ¬ A + 1 2 A
17 ovex A + 1 V
18 hashunsng A + 1 V 2 A Fin ¬ A + 1 2 A 2 A A + 1 = 2 A + 1
19 17 18 ax-mp 2 A Fin ¬ A + 1 2 A 2 A A + 1 = 2 A + 1
20 4 16 19 syl2anc A A + 1 2 A A + 1 = 2 A + 1
21 ppival2 A + 1 π _ A + 1 = 2 A + 1
22 9 21 syl A A + 1 π _ A + 1 = 2 A + 1
23 2z 2
24 zcn A A
25 24 adantr A A + 1 A
26 ax-1cn 1
27 pncan A 1 A + 1 - 1 = A
28 25 26 27 sylancl A A + 1 A + 1 - 1 = A
29 prmuz2 A + 1 A + 1 2
30 29 adantl A A + 1 A + 1 2
31 uz2m1nn A + 1 2 A + 1 - 1
32 30 31 syl A A + 1 A + 1 - 1
33 28 32 eqeltrrd A A + 1 A
34 nnuz = 1
35 2m1e1 2 1 = 1
36 35 fveq2i 2 1 = 1
37 34 36 eqtr4i = 2 1
38 33 37 eleqtrdi A A + 1 A 2 1
39 fzsuc2 2 A 2 1 2 A + 1 = 2 A A + 1
40 23 38 39 sylancr A A + 1 2 A + 1 = 2 A A + 1
41 40 ineq1d A A + 1 2 A + 1 = 2 A A + 1
42 indir 2 A A + 1 = 2 A A + 1
43 41 42 eqtrdi A A + 1 2 A + 1 = 2 A A + 1
44 simpr A A + 1 A + 1
45 44 snssd A A + 1 A + 1
46 df-ss A + 1 A + 1 = A + 1
47 45 46 sylib A A + 1 A + 1 = A + 1
48 47 uneq2d A A + 1 2 A A + 1 = 2 A A + 1
49 43 48 eqtrd A A + 1 2 A + 1 = 2 A A + 1
50 49 fveq2d A A + 1 2 A + 1 = 2 A A + 1
51 22 50 eqtrd A A + 1 π _ A + 1 = 2 A A + 1
52 ppival2 A π _ A = 2 A
53 52 adantr A A + 1 π _ A = 2 A
54 53 oveq1d A A + 1 π _ A + 1 = 2 A + 1
55 20 51 54 3eqtr4d A A + 1 π _ A + 1 = π _ A + 1