Step | Hyp | Ref
| Expression |
1 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...(𝐴 + 1)) ∩
ℙ)) |
2 | 1 | elin2d 4089 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈
ℙ) |
3 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
¬ (𝐴 + 1) ∈
ℙ) |
4 | | nelne2 3031 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℙ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝑥 ≠ (𝐴 + 1)) |
5 | 2, 3, 4 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ≠ (𝐴 + 1)) |
6 | | velsn 4532 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {(𝐴 + 1)} ↔ 𝑥 = (𝐴 + 1)) |
7 | 6 | necon3bbii 2981 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ {(𝐴 + 1)} ↔ 𝑥 ≠ (𝐴 + 1)) |
8 | 5, 7 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
¬ 𝑥 ∈ {(𝐴 + 1)}) |
9 | 1 | elin1d 4088 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ (2...(𝐴 + 1))) |
10 | | 2z 12097 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
11 | | zcn 12069 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
12 | 11 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
ℂ) |
13 | | ax-1cn 10675 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
14 | | pncan 10972 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
15 | 12, 13, 14 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
((𝐴 + 1) − 1) = 𝐴) |
16 | | elfzuz2 13005 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (2...(𝐴 + 1)) → (𝐴 + 1) ∈
(ℤ≥‘2)) |
17 | | uz2m1nn 12407 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 + 1) ∈
(ℤ≥‘2) → ((𝐴 + 1) − 1) ∈
ℕ) |
18 | 9, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
((𝐴 + 1) − 1) ∈
ℕ) |
19 | 15, 18 | eqeltrrd 2834 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
ℕ) |
20 | | nnuz 12365 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
21 | | 2m1e1 11844 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
22 | 21 | fveq2i 6679 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘(2 − 1)) =
(ℤ≥‘1) |
23 | 20, 22 | eqtr4i 2764 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘(2 − 1)) |
24 | 19, 23 | eleqtrdi 2843 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
(ℤ≥‘(2 − 1))) |
25 | | fzsuc2 13058 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ 𝐴
∈ (ℤ≥‘(2 − 1))) → (2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
26 | 10, 24, 25 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
27 | 9, 26 | eleqtrd 2835 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...𝐴) ∪ {(𝐴 + 1)})) |
28 | | elun 4039 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((2...𝐴) ∪ {(𝐴 + 1)}) ↔ (𝑥 ∈ (2...𝐴) ∨ 𝑥 ∈ {(𝐴 + 1)})) |
29 | 27, 28 | sylib 221 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(𝑥 ∈ (2...𝐴) ∨ 𝑥 ∈ {(𝐴 + 1)})) |
30 | 29 | ord 863 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(¬ 𝑥 ∈ (2...𝐴) → 𝑥 ∈ {(𝐴 + 1)})) |
31 | 8, 30 | mt3d 150 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ (2...𝐴)) |
32 | 31, 2 | elind 4084 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...𝐴) ∩
ℙ)) |
33 | 32 | expr 460 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (𝑥 ∈
((2...(𝐴 + 1)) ∩
ℙ) → 𝑥 ∈
((2...𝐴) ∩
ℙ))) |
34 | 33 | ssrdv 3883 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(𝐴 + 1)) ∩
ℙ) ⊆ ((2...𝐴)
∩ ℙ)) |
35 | | uzid 12341 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
36 | 35 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝐴 ∈
(ℤ≥‘𝐴)) |
37 | | peano2uz 12385 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘𝐴) → (𝐴 + 1) ∈
(ℤ≥‘𝐴)) |
38 | | fzss2 13040 |
. . . . . . 7
⊢ ((𝐴 + 1) ∈
(ℤ≥‘𝐴) → (2...𝐴) ⊆ (2...(𝐴 + 1))) |
39 | | ssrin 4124 |
. . . . . . 7
⊢
((2...𝐴) ⊆
(2...(𝐴 + 1)) →
((2...𝐴) ∩ ℙ)
⊆ ((2...(𝐴 + 1))
∩ ℙ)) |
40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...𝐴) ∩
ℙ) ⊆ ((2...(𝐴 +
1)) ∩ ℙ)) |
41 | 34, 40 | eqssd 3894 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(𝐴 + 1)) ∩
ℙ) = ((2...𝐴) ∩
ℙ)) |
42 | | peano2z 12106 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝐴 + 1) ∈
ℤ) |
43 | 42 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (𝐴 + 1) ∈
ℤ) |
44 | | flid 13271 |
. . . . . . . 8
⊢ ((𝐴 + 1) ∈ ℤ →
(⌊‘(𝐴 + 1)) =
(𝐴 + 1)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (⌊‘(𝐴 +
1)) = (𝐴 +
1)) |
46 | 45 | oveq2d 7188 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (2...(⌊‘(𝐴 + 1))) = (2...(𝐴 + 1))) |
47 | 46 | ineq1d 4102 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘(𝐴 + 1))) ∩ ℙ) = ((2...(𝐴 + 1)) ∩
ℙ)) |
48 | | flid 13271 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
49 | 48 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (⌊‘𝐴) =
𝐴) |
50 | 49 | oveq2d 7188 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (2...(⌊‘𝐴)) = (2...𝐴)) |
51 | 50 | ineq1d 4102 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘𝐴)) ∩ ℙ) = ((2...𝐴) ∩ ℙ)) |
52 | 41, 47, 51 | 3eqtr4d 2783 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘(𝐴 + 1))) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
53 | | zre 12068 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
54 | 53 | adantr 484 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝐴 ∈
ℝ) |
55 | | peano2re 10893 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
56 | | ppisval 25843 |
. . . . 5
⊢ ((𝐴 + 1) ∈ ℝ →
((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(⌊‘(𝐴 + 1))) ∩ ℙ)) |
57 | 54, 55, 56 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(⌊‘(𝐴 + 1))) ∩ ℙ)) |
58 | | ppisval 25843 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
59 | 54, 58 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,]𝐴) ∩
ℙ) = ((2...(⌊‘𝐴)) ∩ ℙ)) |
60 | 52, 57, 59 | 3eqtr4d 2783 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,](𝐴 + 1)) ∩
ℙ) = ((0[,]𝐴) ∩
ℙ)) |
61 | 60 | sumeq1d 15153 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
62 | | chtval 25849 |
. . 3
⊢ ((𝐴 + 1) ∈ ℝ →
(θ‘(𝐴 + 1)) =
Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
63 | 54, 55, 62 | 3syl 18 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘(𝐴 +
1)) = Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
64 | | chtval 25849 |
. . 3
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
65 | 54, 64 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
66 | 61, 63, 65 | 3eqtr4d 2783 |
1
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘(𝐴 +
1)) = (θ‘𝐴)) |