Step |
Hyp |
Ref |
Expression |
1 |
|
simprr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) |
2 |
1
|
elin2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ℙ ) |
3 |
|
simprl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ¬ ( 𝐴 + 1 ) ∈ ℙ ) |
4 |
|
nelne2 |
⊢ ( ( 𝑥 ∈ ℙ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → 𝑥 ≠ ( 𝐴 + 1 ) ) |
5 |
2 3 4
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ≠ ( 𝐴 + 1 ) ) |
6 |
|
velsn |
⊢ ( 𝑥 ∈ { ( 𝐴 + 1 ) } ↔ 𝑥 = ( 𝐴 + 1 ) ) |
7 |
6
|
necon3bbii |
⊢ ( ¬ 𝑥 ∈ { ( 𝐴 + 1 ) } ↔ 𝑥 ≠ ( 𝐴 + 1 ) ) |
8 |
5 7
|
sylibr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ¬ 𝑥 ∈ { ( 𝐴 + 1 ) } ) |
9 |
1
|
elin1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( 2 ... ( 𝐴 + 1 ) ) ) |
10 |
|
2z |
⊢ 2 ∈ ℤ |
11 |
|
zcn |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ ) |
12 |
11
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℂ ) |
13 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
14 |
|
pncan |
⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 ) |
15 |
12 13 14
|
sylancl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 ) |
16 |
|
elfzuz2 |
⊢ ( 𝑥 ∈ ( 2 ... ( 𝐴 + 1 ) ) → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) ) |
17 |
|
uz2m1nn |
⊢ ( ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ ) |
18 |
9 16 17
|
3syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ ) |
19 |
15 18
|
eqeltrrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℕ ) |
20 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
21 |
|
2m1e1 |
⊢ ( 2 − 1 ) = 1 |
22 |
21
|
fveq2i |
⊢ ( ℤ≥ ‘ ( 2 − 1 ) ) = ( ℤ≥ ‘ 1 ) |
23 |
20 22
|
eqtr4i |
⊢ ℕ = ( ℤ≥ ‘ ( 2 − 1 ) ) |
24 |
19 23
|
eleqtrdi |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) ) |
25 |
|
fzsuc2 |
⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ) |
26 |
10 24 25
|
sylancr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ) |
27 |
9 26
|
eleqtrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ) |
28 |
|
elun |
⊢ ( 𝑥 ∈ ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ↔ ( 𝑥 ∈ ( 2 ... 𝐴 ) ∨ 𝑥 ∈ { ( 𝐴 + 1 ) } ) ) |
29 |
27 28
|
sylib |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( 𝑥 ∈ ( 2 ... 𝐴 ) ∨ 𝑥 ∈ { ( 𝐴 + 1 ) } ) ) |
30 |
29
|
ord |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → ( ¬ 𝑥 ∈ ( 2 ... 𝐴 ) → 𝑥 ∈ { ( 𝐴 + 1 ) } ) ) |
31 |
8 30
|
mt3d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( 2 ... 𝐴 ) ) |
32 |
31 2
|
elind |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ¬ ( 𝐴 + 1 ) ∈ ℙ ∧ 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) → 𝑥 ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) |
33 |
32
|
expr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝑥 ∈ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) → 𝑥 ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) ) |
34 |
33
|
ssrdv |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ⊆ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) |
35 |
|
uzid |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) ) |
36 |
35
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) ) |
37 |
|
peano2uz |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) |
38 |
|
fzss2 |
⊢ ( ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 2 ... 𝐴 ) ⊆ ( 2 ... ( 𝐴 + 1 ) ) ) |
39 |
|
ssrin |
⊢ ( ( 2 ... 𝐴 ) ⊆ ( 2 ... ( 𝐴 + 1 ) ) → ( ( 2 ... 𝐴 ) ∩ ℙ ) ⊆ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) |
40 |
36 37 38 39
|
4syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... 𝐴 ) ∩ ℙ ) ⊆ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) |
41 |
34 40
|
eqssd |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... 𝐴 ) ∩ ℙ ) ) |
42 |
41
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) ) |
43 |
|
peano2z |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ ) |
44 |
43
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℤ ) |
45 |
|
ppival2 |
⊢ ( ( 𝐴 + 1 ) ∈ ℤ → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) |
46 |
44 45
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) |
47 |
|
ppival2 |
⊢ ( 𝐴 ∈ ℤ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) ) |
48 |
47
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) ) |
49 |
42 46 48
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( π ‘ 𝐴 ) ) |