Step | Hyp | Ref
| Expression |
1 | | peano2z 11295 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 + 1) ∈
ℤ) |
2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(𝐴 + 1) ∈
ℤ) |
3 | | zre 11258 |
. . . . 5
⊢ ((𝐴 + 1) ∈ ℤ →
(𝐴 + 1) ∈
ℝ) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(𝐴 + 1) ∈
ℝ) |
5 | | chtval 24636 |
. . . 4
⊢ ((𝐴 + 1) ∈ ℝ →
(θ‘(𝐴 + 1)) =
Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(θ‘(𝐴 + 1)) =
Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
7 | | ppisval 24630 |
. . . . . 6
⊢ ((𝐴 + 1) ∈ ℝ →
((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(⌊‘(𝐴 + 1))) ∩ ℙ)) |
8 | 4, 7 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(⌊‘(𝐴 + 1))) ∩ ℙ)) |
9 | | flid 12471 |
. . . . . . . 8
⊢ ((𝐴 + 1) ∈ ℤ →
(⌊‘(𝐴 + 1)) =
(𝐴 + 1)) |
10 | 2, 9 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(⌊‘(𝐴 + 1)) =
(𝐴 + 1)) |
11 | 10 | oveq2d 6565 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(2...(⌊‘(𝐴 +
1))) = (2...(𝐴 +
1))) |
12 | 11 | ineq1d 3775 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((2...(⌊‘(𝐴 +
1))) ∩ ℙ) = ((2...(𝐴 + 1)) ∩ ℙ)) |
13 | 8, 12 | eqtrd 2644 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(𝐴 + 1))
∩ ℙ)) |
14 | 13 | sumeq1d 14279 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝) =
Σ𝑝 ∈
((2...(𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
15 | 6, 14 | eqtrd 2644 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(θ‘(𝐴 + 1)) =
Σ𝑝 ∈
((2...(𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
16 | | zre 11258 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
𝐴 ∈
ℝ) |
18 | 17 | ltp1d 10833 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
𝐴 < (𝐴 + 1)) |
19 | 17, 4 | ltnled 10063 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(𝐴 < (𝐴 + 1) ↔ ¬ (𝐴 + 1) ≤ 𝐴)) |
20 | 18, 19 | mpbid 221 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
¬ (𝐴 + 1) ≤ 𝐴) |
21 | | inss1 3795 |
. . . . . . 7
⊢
((2...𝐴) ∩
ℙ) ⊆ (2...𝐴) |
22 | 21 | sseli 3564 |
. . . . . 6
⊢ ((𝐴 + 1) ∈ ((2...𝐴) ∩ ℙ) → (𝐴 + 1) ∈ (2...𝐴)) |
23 | | elfzle2 12216 |
. . . . . 6
⊢ ((𝐴 + 1) ∈ (2...𝐴) → (𝐴 + 1) ≤ 𝐴) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝐴 + 1) ∈ ((2...𝐴) ∩ ℙ) → (𝐴 + 1) ≤ 𝐴) |
25 | 20, 24 | nsyl 134 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
¬ (𝐴 + 1) ∈
((2...𝐴) ∩
ℙ)) |
26 | | disjsn 4192 |
. . . 4
⊢
((((2...𝐴) ∩
ℙ) ∩ {(𝐴 + 1)}) =
∅ ↔ ¬ (𝐴 +
1) ∈ ((2...𝐴) ∩
ℙ)) |
27 | 25, 26 | sylibr 223 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(((2...𝐴) ∩ ℙ)
∩ {(𝐴 + 1)}) =
∅) |
28 | | 2z 11286 |
. . . . . . 7
⊢ 2 ∈
ℤ |
29 | | zcn 11259 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
30 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
𝐴 ∈
ℂ) |
31 | | ax-1cn 9873 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
32 | | pncan 10166 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
33 | 30, 31, 32 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((𝐴 + 1) − 1) = 𝐴) |
34 | | prmuz2 15246 |
. . . . . . . . . . 11
⊢ ((𝐴 + 1) ∈ ℙ →
(𝐴 + 1) ∈
(ℤ≥‘2)) |
35 | 34 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(𝐴 + 1) ∈
(ℤ≥‘2)) |
36 | | uz2m1nn 11639 |
. . . . . . . . . 10
⊢ ((𝐴 + 1) ∈
(ℤ≥‘2) → ((𝐴 + 1) − 1) ∈
ℕ) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((𝐴 + 1) − 1) ∈
ℕ) |
38 | 33, 37 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
𝐴 ∈
ℕ) |
39 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
40 | | 2m1e1 11012 |
. . . . . . . . . 10
⊢ (2
− 1) = 1 |
41 | 40 | fveq2i 6106 |
. . . . . . . . 9
⊢
(ℤ≥‘(2 − 1)) =
(ℤ≥‘1) |
42 | 39, 41 | eqtr4i 2635 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘(2 − 1)) |
43 | 38, 42 | syl6eleq 2698 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
𝐴 ∈
(ℤ≥‘(2 − 1))) |
44 | | fzsuc2 12268 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝐴
∈ (ℤ≥‘(2 − 1))) → (2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
45 | 28, 43, 44 | sylancr 694 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
46 | 45 | ineq1d 3775 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((2...(𝐴 + 1)) ∩
ℙ) = (((2...𝐴) ∪
{(𝐴 + 1)}) ∩
ℙ)) |
47 | | indir 3834 |
. . . . 5
⊢
(((2...𝐴) ∪
{(𝐴 + 1)}) ∩ ℙ) =
(((2...𝐴) ∩ ℙ)
∪ ({(𝐴 + 1)} ∩
ℙ)) |
48 | 46, 47 | syl6eq 2660 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((2...(𝐴 + 1)) ∩
ℙ) = (((2...𝐴) ∩
ℙ) ∪ ({(𝐴 + 1)}
∩ ℙ))) |
49 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(𝐴 + 1) ∈
ℙ) |
50 | 49 | snssd 4281 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
{(𝐴 + 1)} ⊆
ℙ) |
51 | | df-ss 3554 |
. . . . . 6
⊢ ({(𝐴 + 1)} ⊆ ℙ ↔
({(𝐴 + 1)} ∩ ℙ) =
{(𝐴 + 1)}) |
52 | 50, 51 | sylib 207 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
({(𝐴 + 1)} ∩ ℙ) =
{(𝐴 + 1)}) |
53 | 52 | uneq2d 3729 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(((2...𝐴) ∩ ℙ)
∪ ({(𝐴 + 1)} ∩
ℙ)) = (((2...𝐴) ∩
ℙ) ∪ {(𝐴 +
1)})) |
54 | 48, 53 | eqtrd 2644 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((2...(𝐴 + 1)) ∩
ℙ) = (((2...𝐴) ∩
ℙ) ∪ {(𝐴 +
1)})) |
55 | | fzfid 12634 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(2...(𝐴 + 1)) ∈
Fin) |
56 | | inss1 3795 |
. . . 4
⊢
((2...(𝐴 + 1)) ∩
ℙ) ⊆ (2...(𝐴 +
1)) |
57 | | ssfi 8065 |
. . . 4
⊢
(((2...(𝐴 + 1))
∈ Fin ∧ ((2...(𝐴 +
1)) ∩ ℙ) ⊆ (2...(𝐴 + 1))) → ((2...(𝐴 + 1)) ∩ ℙ) ∈
Fin) |
58 | 55, 56, 57 | sylancl 693 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((2...(𝐴 + 1)) ∩
ℙ) ∈ Fin) |
59 | | inss2 3796 |
. . . . . . . 8
⊢
((2...(𝐴 + 1)) ∩
ℙ) ⊆ ℙ |
60 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) ∧
𝑝 ∈ ((2...(𝐴 + 1)) ∩ ℙ)) →
𝑝 ∈ ((2...(𝐴 + 1)) ∩
ℙ)) |
61 | 59, 60 | sseldi 3566 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) ∧
𝑝 ∈ ((2...(𝐴 + 1)) ∩ ℙ)) →
𝑝 ∈
ℙ) |
62 | | prmnn 15226 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
63 | 61, 62 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) ∧
𝑝 ∈ ((2...(𝐴 + 1)) ∩ ℙ)) →
𝑝 ∈
ℕ) |
64 | 63 | nnrpd 11746 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) ∧
𝑝 ∈ ((2...(𝐴 + 1)) ∩ ℙ)) →
𝑝 ∈
ℝ+) |
65 | 64 | relogcld 24173 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) ∧
𝑝 ∈ ((2...(𝐴 + 1)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ) |
66 | 65 | recnd 9947 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) ∧
𝑝 ∈ ((2...(𝐴 + 1)) ∩ ℙ)) →
(log‘𝑝) ∈
ℂ) |
67 | 27, 54, 58, 66 | fsumsplit 14318 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
Σ𝑝 ∈
((2...(𝐴 + 1)) ∩
ℙ)(log‘𝑝) =
(Σ𝑝 ∈
((2...𝐴) ∩
ℙ)(log‘𝑝) +
Σ𝑝 ∈ {(𝐴 + 1)} (log‘𝑝))) |
68 | | chtval 24636 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
69 | 17, 68 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
70 | | ppisval 24630 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
71 | 17, 70 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((0[,]𝐴) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
72 | | flid 12471 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
73 | 72 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(⌊‘𝐴) = 𝐴) |
74 | 73 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(2...(⌊‘𝐴)) =
(2...𝐴)) |
75 | 74 | ineq1d 3775 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((2...(⌊‘𝐴))
∩ ℙ) = ((2...𝐴)
∩ ℙ)) |
76 | 71, 75 | eqtrd 2644 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
((0[,]𝐴) ∩ ℙ) =
((2...𝐴) ∩
ℙ)) |
77 | 76 | sumeq1d 14279 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝) = Σ𝑝 ∈ ((2...𝐴) ∩ ℙ)(log‘𝑝)) |
78 | 69, 77 | eqtr2d 2645 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
Σ𝑝 ∈ ((2...𝐴) ∩ ℙ)(log‘𝑝) = (θ‘𝐴)) |
79 | | prmnn 15226 |
. . . . 5
⊢ ((𝐴 + 1) ∈ ℙ →
(𝐴 + 1) ∈
ℕ) |
80 | 79 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(𝐴 + 1) ∈
ℕ) |
81 | 80 | nnrpd 11746 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(𝐴 + 1) ∈
ℝ+) |
82 | 81 | relogcld 24173 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(log‘(𝐴 + 1)) ∈
ℝ) |
83 | 82 | recnd 9947 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(log‘(𝐴 + 1)) ∈
ℂ) |
84 | | fveq2 6103 |
. . . . 5
⊢ (𝑝 = (𝐴 + 1) → (log‘𝑝) = (log‘(𝐴 + 1))) |
85 | 84 | sumsn 14319 |
. . . 4
⊢ (((𝐴 + 1) ∈ ℕ ∧
(log‘(𝐴 + 1)) ∈
ℂ) → Σ𝑝
∈ {(𝐴 + 1)}
(log‘𝑝) =
(log‘(𝐴 +
1))) |
86 | 80, 83, 85 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
Σ𝑝 ∈ {(𝐴 + 1)} (log‘𝑝) = (log‘(𝐴 + 1))) |
87 | 78, 86 | oveq12d 6567 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(Σ𝑝 ∈
((2...𝐴) ∩
ℙ)(log‘𝑝) +
Σ𝑝 ∈ {(𝐴 + 1)} (log‘𝑝)) = ((θ‘𝐴) + (log‘(𝐴 + 1)))) |
88 | 15, 67, 87 | 3eqtrd 2648 |
1
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 + 1) ∈ ℙ) →
(θ‘(𝐴 + 1)) =
((θ‘𝐴) +
(log‘(𝐴 +
1)))) |