Step | Hyp | Ref
| Expression |
1 | | inss2 3834 |
. . . . . . . . . . 11
⊢
((2...(𝐴 + 1)) ∩
ℙ) ⊆ ℙ |
2 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...(𝐴 + 1)) ∩
ℙ)) |
3 | 1, 2 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈
ℙ) |
4 | | simprl 794 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
¬ (𝐴 + 1) ∈
ℙ) |
5 | | nelne2 2891 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℙ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝑥 ≠ (𝐴 + 1)) |
6 | 3, 4, 5 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ≠ (𝐴 + 1)) |
7 | | velsn 4193 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {(𝐴 + 1)} ↔ 𝑥 = (𝐴 + 1)) |
8 | 7 | necon3bbii 2841 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ {(𝐴 + 1)} ↔ 𝑥 ≠ (𝐴 + 1)) |
9 | 6, 8 | sylibr 224 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
¬ 𝑥 ∈ {(𝐴 + 1)}) |
10 | | inss1 3833 |
. . . . . . . . . . . 12
⊢
((2...(𝐴 + 1)) ∩
ℙ) ⊆ (2...(𝐴 +
1)) |
11 | 10, 2 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ (2...(𝐴 + 1))) |
12 | | 2z 11409 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
13 | | zcn 11382 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
ℂ) |
15 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
16 | | pncan 10287 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
17 | 14, 15, 16 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
((𝐴 + 1) − 1) = 𝐴) |
18 | | elfzuz2 12346 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (2...(𝐴 + 1)) → (𝐴 + 1) ∈
(ℤ≥‘2)) |
19 | | uz2m1nn 11763 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 + 1) ∈
(ℤ≥‘2) → ((𝐴 + 1) − 1) ∈
ℕ) |
20 | 11, 18, 19 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
((𝐴 + 1) − 1) ∈
ℕ) |
21 | 17, 20 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
ℕ) |
22 | | nnuz 11723 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
23 | | 2m1e1 11135 |
. . . . . . . . . . . . . . 15
⊢ (2
− 1) = 1 |
24 | 23 | fveq2i 6194 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘(2 − 1)) =
(ℤ≥‘1) |
25 | 22, 24 | eqtr4i 2647 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘(2 − 1)) |
26 | 21, 25 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝐴 ∈
(ℤ≥‘(2 − 1))) |
27 | | fzsuc2 12398 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ 𝐴
∈ (ℤ≥‘(2 − 1))) → (2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
28 | 12, 26, 27 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(2...(𝐴 + 1)) = ((2...𝐴) ∪ {(𝐴 + 1)})) |
29 | 11, 28 | eleqtrd 2703 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...𝐴) ∪ {(𝐴 + 1)})) |
30 | | elun 3753 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((2...𝐴) ∪ {(𝐴 + 1)}) ↔ (𝑥 ∈ (2...𝐴) ∨ 𝑥 ∈ {(𝐴 + 1)})) |
31 | 29, 30 | sylib 208 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(𝑥 ∈ (2...𝐴) ∨ 𝑥 ∈ {(𝐴 + 1)})) |
32 | 31 | ord 392 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
(¬ 𝑥 ∈ (2...𝐴) → 𝑥 ∈ {(𝐴 + 1)})) |
33 | 9, 32 | mt3d 140 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ (2...𝐴)) |
34 | 33, 3 | elind 3798 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (¬
(𝐴 + 1) ∈ ℙ
∧ 𝑥 ∈ ((2...(𝐴 + 1)) ∩ ℙ))) →
𝑥 ∈ ((2...𝐴) ∩
ℙ)) |
35 | 34 | expr 643 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (𝑥 ∈
((2...(𝐴 + 1)) ∩
ℙ) → 𝑥 ∈
((2...𝐴) ∩
ℙ))) |
36 | 35 | ssrdv 3609 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(𝐴 + 1)) ∩
ℙ) ⊆ ((2...𝐴)
∩ ℙ)) |
37 | | uzid 11702 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
38 | 37 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ 𝐴 ∈
(ℤ≥‘𝐴)) |
39 | | peano2uz 11741 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘𝐴) → (𝐴 + 1) ∈
(ℤ≥‘𝐴)) |
40 | | fzss2 12381 |
. . . . 5
⊢ ((𝐴 + 1) ∈
(ℤ≥‘𝐴) → (2...𝐴) ⊆ (2...(𝐴 + 1))) |
41 | | ssrin 3838 |
. . . . 5
⊢
((2...𝐴) ⊆
(2...(𝐴 + 1)) →
((2...𝐴) ∩ ℙ)
⊆ ((2...(𝐴 + 1))
∩ ℙ)) |
42 | 38, 39, 40, 41 | 4syl 19 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...𝐴) ∩
ℙ) ⊆ ((2...(𝐴 +
1)) ∩ ℙ)) |
43 | 36, 42 | eqssd 3620 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ ((2...(𝐴 + 1)) ∩
ℙ) = ((2...𝐴) ∩
ℙ)) |
44 | 43 | fveq2d 6195 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (#‘((2...(𝐴 +
1)) ∩ ℙ)) = (#‘((2...𝐴) ∩ ℙ))) |
45 | | peano2z 11418 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 + 1) ∈
ℤ) |
46 | 45 | adantr 481 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (𝐴 + 1) ∈
ℤ) |
47 | | ppival2 24854 |
. . 3
⊢ ((𝐴 + 1) ∈ ℤ →
(π‘(𝐴 + 1))
= (#‘((2...(𝐴 + 1))
∩ ℙ))) |
48 | 46, 47 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (π‘(𝐴 + 1)) = (#‘((2...(𝐴 + 1)) ∩ ℙ))) |
49 | | ppival2 24854 |
. . 3
⊢ (𝐴 ∈ ℤ →
(π‘𝐴) =
(#‘((2...𝐴) ∩
ℙ))) |
50 | 49 | adantr 481 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (π‘𝐴) = (#‘((2...𝐴) ∩ ℙ))) |
51 | 44, 48, 50 | 3eqtr4d 2666 |
1
⊢ ((𝐴 ∈ ℤ ∧ ¬
(𝐴 + 1) ∈ ℙ)
→ (π‘(𝐴 + 1)) = (π‘𝐴)) |