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 e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ppi ` ( A + 1 ) ) = ( ( ppi ` A ) + 1 ) )

Proof

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