| Step | Hyp | Ref
| Expression |
| 1 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...(𝐴 + 1)) ∩
ℙ)) |
| 2 | 1 | elin2d 4205 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈
ℙ) |
| 3 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
¬ (𝐴 + 1) ∈
ℙ) |
| 4 | | nelne2 3040 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℙ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝑥 ≠ (𝐴 + 1)) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ≠ (𝐴 + 1)) |
| 6 | | velsn 4642 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {(𝐴 + 1)} ↔ 𝑥 = (𝐴 + 1)) |
| 7 | 6 | necon3bbii 2988 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ {(𝐴 + 1)} ↔ 𝑥 ≠ (𝐴 + 1)) |
| 8 | 5, 7 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
¬ 𝑥 ∈ {(𝐴 + 1)}) |
| 9 | 1 | elin1d 4204 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ (2...(𝐴 + 1))) |
| 10 | | 2z 12649 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
| 11 | | zcn 12618 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
| 12 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
ℂ) |
| 13 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
| 14 | | pncan 11514 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
| 15 | 12, 13, 14 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
((𝐴 + 1) − 1) = 𝐴) |
| 16 | | elfzuz2 13569 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (2...(𝐴 + 1)) → (𝐴 + 1) ∈
(ℤ≥‘2)) |
| 17 | | uz2m1nn 12965 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 + 1) ∈
(ℤ≥‘2) → ((𝐴 + 1) − 1) ∈
ℕ) |
| 18 | 9, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
((𝐴 + 1) − 1) ∈
ℕ) |
| 19 | 15, 18 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
ℕ) |
| 20 | | nnuz 12921 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
| 21 | | 2m1e1 12392 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
| 22 | 21 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘(2 − 1)) =
(ℤ≥‘1) |
| 23 | 20, 22 | eqtr4i 2768 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘(2 − 1)) |
| 24 | 19, 23 | eleqtrdi 2851 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
(ℤ≥‘(2 − 1))) |
| 25 | | fzsuc2 13622 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ 𝐴
∈ (ℤ≥‘(2 − 1))) → (2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
| 26 | 10, 24, 25 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
| 27 | 9, 26 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...𝐴) ∪ {(𝐴 + 1)})) |
| 28 | | elun 4153 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((2...𝐴) ∪ {(𝐴 + 1)}) ↔ (𝑥 ∈ (2...𝐴) ∨ 𝑥 ∈ {(𝐴 + 1)})) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(𝑥 ∈ (2...𝐴) ∨ 𝑥 ∈ {(𝐴 + 1)})) |
| 30 | 29 | ord 865 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(¬ 𝑥 ∈ (2...𝐴) → 𝑥 ∈ {(𝐴 + 1)})) |
| 31 | 8, 30 | mt3d 148 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ (2...𝐴)) |
| 32 | 31, 2 | elind 4200 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...𝐴) ∩
ℙ)) |
| 33 | 32 | expr 456 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (𝑥 ∈
((2...(𝐴 + 1)) ∩
ℙ) → 𝑥 ∈
((2...𝐴) ∩
ℙ))) |
| 34 | 33 | ssrdv 3989 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(𝐴 + 1)) ∩
ℙ) ⊆ ((2...𝐴)
∩ ℙ)) |
| 35 | | uzid 12893 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
| 36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝐴 ∈
(ℤ≥‘𝐴)) |
| 37 | | peano2uz 12943 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘𝐴) → (𝐴 + 1) ∈
(ℤ≥‘𝐴)) |
| 38 | | fzss2 13604 |
. . . . . . 7
⊢ ((𝐴 + 1) ∈
(ℤ≥‘𝐴) → (2...𝐴) ⊆ (2...(𝐴 + 1))) |
| 39 | | ssrin 4242 |
. . . . . . 7
⊢
((2...𝐴) ⊆
(2...(𝐴 + 1)) →
((2...𝐴) ∩ ℙ)
⊆ ((2...(𝐴 + 1))
∩ ℙ)) |
| 40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...𝐴) ∩
ℙ) ⊆ ((2...(𝐴 +
1)) ∩ ℙ)) |
| 41 | 34, 40 | eqssd 4001 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(𝐴 + 1)) ∩
ℙ) = ((2...𝐴) ∩
ℙ)) |
| 42 | | peano2z 12658 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝐴 + 1) ∈
ℤ) |
| 43 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (𝐴 + 1) ∈
ℤ) |
| 44 | | flid 13848 |
. . . . . . . 8
⊢ ((𝐴 + 1) ∈ ℤ →
(⌊‘(𝐴 + 1)) =
(𝐴 + 1)) |
| 45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (⌊‘(𝐴 +
1)) = (𝐴 +
1)) |
| 46 | 45 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (2...(⌊‘(𝐴 + 1))) = (2...(𝐴 + 1))) |
| 47 | 46 | ineq1d 4219 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘(𝐴 + 1))) ∩ ℙ) = ((2...(𝐴 + 1)) ∩
ℙ)) |
| 48 | | flid 13848 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
| 49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (⌊‘𝐴) =
𝐴) |
| 50 | 49 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (2...(⌊‘𝐴)) = (2...𝐴)) |
| 51 | 50 | ineq1d 4219 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘𝐴)) ∩ ℙ) = ((2...𝐴) ∩ ℙ)) |
| 52 | 41, 47, 51 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(⌊‘(𝐴 + 1))) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
| 53 | | zre 12617 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
| 54 | 53 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝐴 ∈
ℝ) |
| 55 | | peano2re 11434 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
| 56 | | ppisval 27147 |
. . . . 5
⊢ ((𝐴 + 1) ∈ ℝ →
((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(⌊‘(𝐴 + 1))) ∩ ℙ)) |
| 57 | 54, 55, 56 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,](𝐴 + 1)) ∩
ℙ) = ((2...(⌊‘(𝐴 + 1))) ∩ ℙ)) |
| 58 | | ppisval 27147 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
| 59 | 54, 58 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,]𝐴) ∩
ℙ) = ((2...(⌊‘𝐴)) ∩ ℙ)) |
| 60 | 52, 57, 59 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((0[,](𝐴 + 1)) ∩
ℙ) = ((0[,]𝐴) ∩
ℙ)) |
| 61 | 60 | sumeq1d 15736 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
| 62 | | chtval 27153 |
. . 3
⊢ ((𝐴 + 1) ∈ ℝ →
(θ‘(𝐴 + 1)) =
Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
| 63 | 54, 55, 62 | 3syl 18 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘(𝐴 +
1)) = Σ𝑝 ∈
((0[,](𝐴 + 1)) ∩
ℙ)(log‘𝑝)) |
| 64 | | chtval 27153 |
. . 3
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
| 65 | 54, 64 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
| 66 | 61, 63, 65 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (θ‘(𝐴 +
1)) = (θ‘𝐴)) |