Metamath Proof Explorer

Theorem ppinprm

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

Ref Expression
Assertion ppinprm 
|- ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ppi ` ( A + 1 ) ) = ( ppi ` A ) )

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
2 1 elin1d 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( 2 ... ( A + 1 ) ) )
3 2z 
 |-  2 e. ZZ
4 zcn 
 |-  ( A e. ZZ -> A e. CC )
5 4 adantr 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> A e. CC )
6 ax-1cn 
 |-  1 e. CC
7 pncan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A )
8 5 6 7 sylancl 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( ( A + 1 ) - 1 ) = A )
9 elfzuz2 
 |-  ( x e. ( 2 ... ( A + 1 ) ) -> ( A + 1 ) e. ( ZZ>= ` 2 ) )
10 uz2m1nn 
 |-  ( ( A + 1 ) e. ( ZZ>= ` 2 ) -> ( ( A + 1 ) - 1 ) e. NN )
11 2 9 10 3syl 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( ( A + 1 ) - 1 ) e. NN )
12 8 11 eqeltrrd 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> A e. NN )
13 nnuz 
 |-  NN = ( ZZ>= ` 1 )
14 2m1e1 
 |-  ( 2 - 1 ) = 1
15 14 fveq2i 
 |-  ( ZZ>= ` ( 2 - 1 ) ) = ( ZZ>= ` 1 )
16 13 15 eqtr4i 
 |-  NN = ( ZZ>= ` ( 2 - 1 ) )
17 12 16 eleqtrdi 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> A e. ( ZZ>= ` ( 2 - 1 ) ) )
18 fzsuc2 
 |-  ( ( 2 e. ZZ /\ A e. ( ZZ>= ` ( 2 - 1 ) ) ) -> ( 2 ... ( A + 1 ) ) = ( ( 2 ... A ) u. { ( A + 1 ) } ) )
19 3 17 18 sylancr 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( 2 ... ( A + 1 ) ) = ( ( 2 ... A ) u. { ( A + 1 ) } ) )
20 2 19 eleqtrd 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( ( 2 ... A ) u. { ( A + 1 ) } ) )
21 elun 
 |-  ( x e. ( ( 2 ... A ) u. { ( A + 1 ) } ) <-> ( x e. ( 2 ... A ) \/ x e. { ( A + 1 ) } ) )
22 20 21 sylib 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( x e. ( 2 ... A ) \/ x e. { ( A + 1 ) } ) )
23 1 elin2d 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. Prime )
24 simprl 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> -. ( A + 1 ) e. Prime )
25 nelne2 
 |-  ( ( x e. Prime /\ -. ( A + 1 ) e. Prime ) -> x =/= ( A + 1 ) )
26 23 24 25 syl2anc 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x =/= ( A + 1 ) )
27 velsn 
 |-  ( x e. { ( A + 1 ) } <-> x = ( A + 1 ) )
28 27 necon3bbii 
 |-  ( -. x e. { ( A + 1 ) } <-> x =/= ( A + 1 ) )
29 26 28 sylibr 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> -. x e. { ( A + 1 ) } )
30 22 29 olcnd 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( 2 ... A ) )
31 30 23 elind 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( ( 2 ... A ) i^i Prime ) )
32 31 expr 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) -> x e. ( ( 2 ... A ) i^i Prime ) ) )
33 32 ssrdv 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 2 ... ( A + 1 ) ) i^i Prime ) C_ ( ( 2 ... A ) i^i Prime ) )
34 uzid 
 |-  ( A e. ZZ -> A e. ( ZZ>= ` A ) )
35 34 adantr 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> A e. ( ZZ>= ` A ) )
36 peano2uz 
 |-  ( A e. ( ZZ>= ` A ) -> ( A + 1 ) e. ( ZZ>= ` A ) )
37 fzss2 
 |-  ( ( A + 1 ) e. ( ZZ>= ` A ) -> ( 2 ... A ) C_ ( 2 ... ( A + 1 ) ) )
38 ssrin 
 |-  ( ( 2 ... A ) C_ ( 2 ... ( A + 1 ) ) -> ( ( 2 ... A ) i^i Prime ) C_ ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
39 35 36 37 38 4syl 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 2 ... A ) i^i Prime ) C_ ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
40 33 39 eqssd 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 2 ... ( A + 1 ) ) i^i Prime ) = ( ( 2 ... A ) i^i Prime ) )
41 40 fveq2d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( # ` ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) = ( # ` ( ( 2 ... A ) i^i Prime ) ) )
42 peano2z 
 |-  ( A e. ZZ -> ( A + 1 ) e. ZZ )
43 42 adantr 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( A + 1 ) e. ZZ )
44 ppival2 
 |-  ( ( A + 1 ) e. ZZ -> ( ppi ` ( A + 1 ) ) = ( # ` ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) )
45 43 44 syl 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ppi ` ( A + 1 ) ) = ( # ` ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) )
46 ppival2 
 |-  ( A e. ZZ -> ( ppi ` A ) = ( # ` ( ( 2 ... A ) i^i Prime ) ) )
47 46 adantr 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ppi ` A ) = ( # ` ( ( 2 ... A ) i^i Prime ) ) )
48 41 45 47 3eqtr4d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ppi ` ( A + 1 ) ) = ( ppi ` A ) )