Step | Hyp | Ref
| Expression |
1 | | inss2 3834 |
. . . . . . . . . . . . 13
⊢
((2...(𝐴 + 1)) ∩
ℙ) ⊆ ℙ |
2 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...(𝐴 + 1)) ∩
ℙ)) |
3 | 1, 2 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈
ℙ) |
4 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
¬ (𝐴 + 1) ∈
ℙ) |
5 | | nelne2 2891 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℙ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝑥 ≠ (𝐴 + 1)) |
6 | 3, 4, 5 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ≠ (𝐴 + 1)) |
7 | | velsn 4193 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {(𝐴 + 1)} ↔ 𝑥 = (𝐴 + 1)) |
8 | 7 | necon3bbii 2841 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ {(𝐴 + 1)} ↔ 𝑥 ≠ (𝐴 + 1)) |
9 | 6, 8 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
¬ 𝑥 ∈ {(𝐴 + 1)}) |
10 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢
((2...(𝐴 + 1)) ∩
ℙ) ⊆ (2...(𝐴 +
1)) |
11 | 10, 2 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ (2...(𝐴 + 1))) |
12 | | 2z 11409 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
13 | | zcn 11382 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
ℂ) |
15 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
16 | | pncan 10287 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
17 | 14, 15, 16 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
((𝐴 + 1) − 1) = 𝐴) |
18 | | elfzuz2 12346 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (2...(𝐴 + 1)) → (𝐴 + 1) ∈
(ℤ≥‘2)) |
19 | | uz2m1nn 11763 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 + 1) ∈
(ℤ≥‘2) → ((𝐴 + 1) − 1) ∈
ℕ) |
20 | 11, 18, 19 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
((𝐴 + 1) − 1) ∈
ℕ) |
21 | 17, 20 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
ℕ) |
22 | | nnuz 11723 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
23 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
24 | 23 | fveq2i 6194 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘(2 − 1)) =
(ℤ≥‘1) |
25 | 22, 24 | eqtr4i 2647 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘(2 − 1)) |
26 | 21, 25 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
(ℤ≥‘(2 − 1))) |
27 | | fzsuc2 12398 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ 𝐴
∈ (ℤ≥‘(2 − 1))) → (2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
28 | 12, 26, 27 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
29 | 11, 28 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...𝐴) ∪ {(𝐴 + 1)})) |
30 | | elun 3753 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((2...𝐴) ∪ {(𝐴 + 1)}) ↔ (𝑥 ∈ (2...𝐴) ∨ 𝑥 ∈ {(𝐴 + 1)})) |
31 | 29, 30 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(𝑥 ∈ (2...𝐴) ∨ 𝑥 ∈ {(𝐴 + 1)})) |
32 | 31 | ord 392 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(¬ 𝑥 ∈ (2...𝐴) → 𝑥 ∈ {(𝐴 + 1)})) |
33 | 9, 32 | mt3d 140 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ (2...𝐴)) |
34 | 33, 3 | elind 3798 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...𝐴) ∩
ℙ)) |
35 | 34 | expr 643 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (𝑥 ∈
((2...(𝐴 + 1)) ∩
ℙ) → 𝑥 ∈
((2...𝐴) ∩
ℙ))) |
36 | 35 | ssrdv 3609 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(𝐴 + 1)) ∩
ℙ) ⊆ ((2...𝐴)
∩ ℙ)) |
37 | | uzid 11702 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
38 | 37 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝐴 ∈
(ℤ≥‘𝐴)) |
39 | | peano2uz 11741 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘𝐴) → (𝐴 + 1) ∈
(ℤ≥‘𝐴)) |
40 | | fzss2 12381 |
. . . . . . 7
⊢ ((𝐴 + 1) ∈
(ℤ≥‘𝐴) → (2...𝐴) ⊆ (2...(𝐴 + 1))) |
41 | | ssrin 3838 |
. . . . . . 7
⊢
((2...𝐴) ⊆
(2...(𝐴 + 1)) →
((2...𝐴) ∩ ℙ)
⊆ ((2...(𝐴 + 1))
∩ ℙ)) |
42 | 38, 39, 40, 41 | 4syl 19 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...𝐴) ∩
ℙ) ⊆ ((2...(𝐴 +
1)) ∩ ℙ)) |
43 | 36, 42 | eqssd 3620 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(𝐴 + 1)) ∩
ℙ) = ((2...𝐴) ∩
ℙ)) |
44 | | peano2z 11418 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝐴 + 1) ∈
ℤ) |
45 | 44 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (𝐴 + 1) ∈
ℤ) |
46 | | flid 12609 |
. . . . . . . 8
⊢ ((𝐴 + 1) ∈ ℤ →
(⌊‘(𝐴 + 1)) =
(𝐴 + 1)) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (⌊‘(𝐴 +
1)) = (𝐴 +
1)) |
48 | 47 | oveq2d 6666 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (2...(⌊‘(𝐴 + 1))) = (2...(𝐴 + 1))) |
49 | 48 | ineq1d 3813 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘(𝐴 + 1))) ∩ ℙ) = ((2...(𝐴 + 1)) ∩
ℙ)) |
50 | | flid 12609 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
51 | 50 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (⌊‘𝐴) =
𝐴) |
52 | 51 | oveq2d 6666 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (2...(⌊‘𝐴)) = (2...𝐴)) |
53 | 52 | ineq1d 3813 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘𝐴)) ∩ ℙ) = ((2...𝐴) ∩ ℙ)) |
54 | 43, 49, 53 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘(𝐴 + 1))) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
55 | | zre 11381 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
56 | 55 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝐴 ∈
ℝ) |
57 | | peano2re 10209 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
58 | | ppisval 24830 |
. . . . 5
⊢ ((𝐴 + 1) ∈ ℝ →
((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(⌊‘(𝐴 + 1))) ∩ ℙ)) |
59 | 56, 57, 58 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(⌊‘(𝐴 + 1))) ∩ ℙ)) |
60 | | ppisval 24830 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
61 | 56, 60 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,]𝐴) ∩
ℙ) = ((2...(⌊‘𝐴)) ∩ ℙ)) |
62 | 54, 59, 61 | 3eqtr4d 2666 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,](𝐴 + 1)) ∩
ℙ) = ((0[,]𝐴) ∩
ℙ)) |
63 | 62 | sumeq1d 14431 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
64 | | chtval 24836 |
. . 3
⊢ ((𝐴 + 1) ∈ ℝ →
(θ‘(𝐴 + 1)) =
Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
65 | 56, 57, 64 | 3syl 18 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘(𝐴 +
1)) = Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
66 | | chtval 24836 |
. . 3
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
67 | 56, 66 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
68 | 63, 65, 67 | 3eqtr4d 2666 |
1
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘(𝐴 +
1)) = (θ‘𝐴)) |