Metamath Proof Explorer

Theorem chtnprm

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

Ref Expression
Assertion chtnprm 
|- ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = ( theta ` 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 elin2d 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. Prime )
3 simprl 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> -. ( A + 1 ) e. Prime )
4 nelne2 
 |-  ( ( x e. Prime /\ -. ( A + 1 ) e. Prime ) -> x =/= ( A + 1 ) )
5 2 3 4 syl2anc 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x =/= ( A + 1 ) )
6 velsn 
 |-  ( x e. { ( A + 1 ) } <-> x = ( A + 1 ) )
7 6 necon3bbii 
 |-  ( -. x e. { ( A + 1 ) } <-> x =/= ( A + 1 ) )
8 5 7 sylibr 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> -. x e. { ( A + 1 ) } )
9 1 elin1d 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( 2 ... ( A + 1 ) ) )
10 2z 
 |-  2 e. ZZ
11 zcn 
 |-  ( A e. ZZ -> A e. CC )
12 11 adantr 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> A e. CC )
13 ax-1cn 
 |-  1 e. CC
14 pncan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A )
15 12 13 14 sylancl 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( ( A + 1 ) - 1 ) = A )
16 elfzuz2 
 |-  ( x e. ( 2 ... ( A + 1 ) ) -> ( A + 1 ) e. ( ZZ>= ` 2 ) )
17 uz2m1nn 
 |-  ( ( A + 1 ) e. ( ZZ>= ` 2 ) -> ( ( A + 1 ) - 1 ) e. NN )
18 9 16 17 3syl 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( ( A + 1 ) - 1 ) e. NN )
19 15 18 eqeltrrd 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> A e. NN )
20 nnuz 
 |-  NN = ( ZZ>= ` 1 )
21 2m1e1 
 |-  ( 2 - 1 ) = 1
22 21 fveq2i 
 |-  ( ZZ>= ` ( 2 - 1 ) ) = ( ZZ>= ` 1 )
23 20 22 eqtr4i 
 |-  NN = ( ZZ>= ` ( 2 - 1 ) )
24 19 23 eleqtrdi 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> A e. ( ZZ>= ` ( 2 - 1 ) ) )
25 fzsuc2 
 |-  ( ( 2 e. ZZ /\ A e. ( ZZ>= ` ( 2 - 1 ) ) ) -> ( 2 ... ( A + 1 ) ) = ( ( 2 ... A ) u. { ( A + 1 ) } ) )
26 10 24 25 sylancr 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( 2 ... ( A + 1 ) ) = ( ( 2 ... A ) u. { ( A + 1 ) } ) )
27 9 26 eleqtrd 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( ( 2 ... A ) u. { ( A + 1 ) } ) )
28 elun 
 |-  ( x e. ( ( 2 ... A ) u. { ( A + 1 ) } ) <-> ( x e. ( 2 ... A ) \/ x e. { ( A + 1 ) } ) )
29 27 28 sylib 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( x e. ( 2 ... A ) \/ x e. { ( A + 1 ) } ) )
30 29 ord 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> ( -. x e. ( 2 ... A ) -> x e. { ( A + 1 ) } ) )
31 8 30 mt3d 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( 2 ... A ) )
32 31 2 elind 
 |-  ( ( A e. ZZ /\ ( -. ( A + 1 ) e. Prime /\ x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) ) -> x e. ( ( 2 ... A ) i^i Prime ) )
33 32 expr 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( x e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) -> x e. ( ( 2 ... A ) i^i Prime ) ) )
34 33 ssrdv 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 2 ... ( A + 1 ) ) i^i Prime ) C_ ( ( 2 ... A ) i^i Prime ) )
35 uzid 
 |-  ( A e. ZZ -> A e. ( ZZ>= ` A ) )
36 35 adantr 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> A e. ( ZZ>= ` A ) )
37 peano2uz 
 |-  ( A e. ( ZZ>= ` A ) -> ( A + 1 ) e. ( ZZ>= ` A ) )
38 fzss2 
 |-  ( ( A + 1 ) e. ( ZZ>= ` A ) -> ( 2 ... A ) C_ ( 2 ... ( A + 1 ) ) )
39 ssrin 
 |-  ( ( 2 ... A ) C_ ( 2 ... ( A + 1 ) ) -> ( ( 2 ... A ) i^i Prime ) C_ ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
40 36 37 38 39 4syl 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 2 ... A ) i^i Prime ) C_ ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
41 34 40 eqssd 
 |-  ( ( 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 flid 
 |-  ( ( A + 1 ) e. ZZ -> ( |_ ` ( A + 1 ) ) = ( A + 1 ) )
45 43 44 syl 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( |_ ` ( A + 1 ) ) = ( A + 1 ) )
46 45 oveq2d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( 2 ... ( |_ ` ( A + 1 ) ) ) = ( 2 ... ( A + 1 ) ) )
47 46 ineq1d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 2 ... ( |_ ` ( A + 1 ) ) ) i^i Prime ) = ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
48 flid 
 |-  ( A e. ZZ -> ( |_ ` A ) = A )
49 48 adantr 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( |_ ` A ) = A )
50 49 oveq2d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( 2 ... ( |_ ` A ) ) = ( 2 ... A ) )
51 50 ineq1d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) = ( ( 2 ... A ) i^i Prime ) )
52 41 47 51 3eqtr4d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 2 ... ( |_ ` ( A + 1 ) ) ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
53 zre 
 |-  ( A e. ZZ -> A e. RR )
54 53 adantr 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> A e. RR )
55 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
56 ppisval 
 |-  ( ( A + 1 ) e. RR -> ( ( 0 [,] ( A + 1 ) ) i^i Prime ) = ( ( 2 ... ( |_ ` ( A + 1 ) ) ) i^i Prime ) )
57 54 55 56 3syl 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 0 [,] ( A + 1 ) ) i^i Prime ) = ( ( 2 ... ( |_ ` ( A + 1 ) ) ) i^i Prime ) )
58 ppisval 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
59 54 58 syl 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
60 52 57 59 3eqtr4d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( ( 0 [,] ( A + 1 ) ) i^i Prime ) = ( ( 0 [,] A ) i^i Prime ) )
61 60 sumeq1d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> sum_ p e. ( ( 0 [,] ( A + 1 ) ) i^i Prime ) ( log ` p ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
62 chtval 
 |-  ( ( A + 1 ) e. RR -> ( theta ` ( A + 1 ) ) = sum_ p e. ( ( 0 [,] ( A + 1 ) ) i^i Prime ) ( log ` p ) )
63 54 55 62 3syl 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = sum_ p e. ( ( 0 [,] ( A + 1 ) ) i^i Prime ) ( log ` p ) )
64 chtval 
 |-  ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
65 54 64 syl 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
66 61 63 65 3eqtr4d 
 |-  ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = ( theta ` A ) )