Metamath Proof Explorer

Theorem chtprm

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

Ref Expression
Assertion chtprm ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ ( 𝐴 + 1 ) ) = ( ( θ ‘ 𝐴 ) + ( log ‘ ( 𝐴 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 peano2z ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℤ )
3 zre ⊢ ( ( 𝐴 + 1 ) ∈ ℤ → ( 𝐴 + 1 ) ∈ ℝ )
4 2 3 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℝ )
5 chtval ⊢ ( ( 𝐴 + 1 ) ∈ ℝ → ( θ ‘ ( 𝐴 + 1 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
6 4 5 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ ( 𝐴 + 1 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
7 ppisval ⊢ ( ( 𝐴 + 1 ) ∈ ℝ → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) )
8 4 7 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) )
9 flid ⊢ ( ( 𝐴 + 1 ) ∈ ℤ → ( ⌊ ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
10 2 9 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ⌊ ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
11 10 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) = ( 2 ... ( 𝐴 + 1 ) ) )
12 11 ineq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) = ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) )
13 8 12 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) )
14 13 sumeq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
15 6 14 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ ( 𝐴 + 1 ) ) = Σ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
16 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
17 16 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℝ )
18 17 ltp1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 < ( 𝐴 + 1 ) )
19 17 4 ltnled ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 < ( 𝐴 + 1 ) ↔ ¬ ( 𝐴 + 1 ) ≤ 𝐴 ) )
20 18 19 mpbid ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ¬ ( 𝐴 + 1 ) ≤ 𝐴 )
21 elinel1 ⊢ ( ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) → ( 𝐴 + 1 ) ∈ ( 2 ... 𝐴 ) )
22 elfzle2 ⊢ ( ( 𝐴 + 1 ) ∈ ( 2 ... 𝐴 ) → ( 𝐴 + 1 ) ≤ 𝐴 )
23 21 22 syl ⊢ ( ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) → ( 𝐴 + 1 ) ≤ 𝐴 )
24 20 23 nsyl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ¬ ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) )
25 disjsn ⊢ ( ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∩ { ( 𝐴 + 1 ) } ) = ∅ ↔ ¬ ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) )
26 24 25 sylibr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∩ { ( 𝐴 + 1 ) } ) = ∅ )
27 2z ⊢ 2 ∈ ℤ
28 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
29 28 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℂ )
30 ax-1cn ⊢ 1 ∈ ℂ
31 pncan ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
32 29 30 31 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
33 prmuz2 ⊢ ( ( 𝐴 + 1 ) ∈ ℙ → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
34 33 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
35 uz2m1nn ⊢ ( ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ )
36 34 35 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ )
37 32 36 eqeltrrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℕ )
38 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
39 2m1e1 ⊢ ( 2 − 1 ) = 1
40 39 fveq2i ⊢ ( ℤ≥ ‘ ( 2 − 1 ) ) = ( ℤ≥ ‘ 1 )
41 38 40 eqtr4i ⊢ ℕ = ( ℤ≥ ‘ ( 2 − 1 ) )
42 37 41 eleqtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) )
43 fzsuc2 ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) )
44 27 42 43 sylancr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) )
45 44 ineq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ∩ ℙ ) )
46 indir ⊢ ( ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) )
47 45 46 eqtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) ) )
48 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℙ )
49 48 snssd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → { ( 𝐴 + 1 ) } ⊆ ℙ )
50 dfss2 ⊢ ( { ( 𝐴 + 1 ) } ⊆ ℙ ↔ ( { ( 𝐴 + 1 ) } ∩ ℙ ) = { ( 𝐴 + 1 ) } )
51 49 50 sylib ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( { ( 𝐴 + 1 ) } ∩ ℙ ) = { ( 𝐴 + 1 ) } )
52 51 uneq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) )
53 47 52 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) )
54 fzfid ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( 𝐴 + 1 ) ) ∈ Fin )
55 inss1 ⊢ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ⊆ ( 2 ... ( 𝐴 + 1 ) )
56 ssfi ⊢ ( ( ( 2 ... ( 𝐴 + 1 ) ) ∈ Fin ∧ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ⊆ ( 2 ... ( 𝐴 + 1 ) ) ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ∈ Fin )
57 54 55 56 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ∈ Fin )
58 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) )
59 58 elin2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
60 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
61 59 60 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
62 61 nnrpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
63 62 relogcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
64 63 recnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
65 26 53 57 64 fsumsplit ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → Σ 𝑝 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) = ( Σ 𝑝 ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) + Σ 𝑝 ∈ { ( 𝐴 + 1 ) } ( log ‘ 𝑝 ) ) )
66 chtval ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
67 17 66 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
68 ppisval ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
69 17 68 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
70 flid ⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
71 70 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ⌊ ‘ 𝐴 ) = 𝐴 )
72 71 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) = ( 2 ... 𝐴 ) )
73 72 ineq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... 𝐴 ) ∩ ℙ ) )
74 69 73 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... 𝐴 ) ∩ ℙ ) )
75 74 sumeq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
76 67 75 eqtr2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → Σ 𝑝 ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) = ( θ ‘ 𝐴 ) )
77 prmnn ⊢ ( ( 𝐴 + 1 ) ∈ ℙ → ( 𝐴 + 1 ) ∈ ℕ )
78 77 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℕ )
79 78 nnrpd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℝ+ )
80 79 relogcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( log ‘ ( 𝐴 + 1 ) ) ∈ ℝ )
81 80 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( log ‘ ( 𝐴 + 1 ) ) ∈ ℂ )
82 fveq2 ⊢ ( 𝑝 = ( 𝐴 + 1 ) → ( log ‘ 𝑝 ) = ( log ‘ ( 𝐴 + 1 ) ) )
83 82 sumsn ⊢ ( ( ( 𝐴 + 1 ) ∈ ℕ ∧ ( log ‘ ( 𝐴 + 1 ) ) ∈ ℂ ) → Σ 𝑝 ∈ { ( 𝐴 + 1 ) } ( log ‘ 𝑝 ) = ( log ‘ ( 𝐴 + 1 ) ) )
84 78 81 83 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → Σ 𝑝 ∈ { ( 𝐴 + 1 ) } ( log ‘ 𝑝 ) = ( log ‘ ( 𝐴 + 1 ) ) )
85 76 84 oveq12d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( Σ 𝑝 ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) + Σ 𝑝 ∈ { ( 𝐴 + 1 ) } ( log ‘ 𝑝 ) ) = ( ( θ ‘ 𝐴 ) + ( log ‘ ( 𝐴 + 1 ) ) ) )
86 15 65 85 3eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ ( 𝐴 + 1 ) ) = ( ( θ ‘ 𝐴 ) + ( log ‘ ( 𝐴 + 1 ) ) ) )