Step |
Hyp |
Ref |
Expression |
1 |
|
fzfid |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... 𝐴 ) ∈ Fin ) |
2 |
|
inss1 |
⊢ ( ( 2 ... 𝐴 ) ∩ ℙ ) ⊆ ( 2 ... 𝐴 ) |
3 |
|
ssfi |
⊢ ( ( ( 2 ... 𝐴 ) ∈ Fin ∧ ( ( 2 ... 𝐴 ) ∩ ℙ ) ⊆ ( 2 ... 𝐴 ) ) → ( ( 2 ... 𝐴 ) ∩ ℙ ) ∈ Fin ) |
4 |
1 2 3
|
sylancl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... 𝐴 ) ∩ ℙ ) ∈ Fin ) |
5 |
|
zre |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ ) |
6 |
5
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℝ ) |
7 |
6
|
ltp1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 < ( 𝐴 + 1 ) ) |
8 |
|
peano2z |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ ) |
9 |
8
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℤ ) |
10 |
9
|
zred |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℝ ) |
11 |
6 10
|
ltnled |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 < ( 𝐴 + 1 ) ↔ ¬ ( 𝐴 + 1 ) ≤ 𝐴 ) ) |
12 |
7 11
|
mpbid |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ¬ ( 𝐴 + 1 ) ≤ 𝐴 ) |
13 |
|
elinel1 |
⊢ ( ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) → ( 𝐴 + 1 ) ∈ ( 2 ... 𝐴 ) ) |
14 |
|
elfzle2 |
⊢ ( ( 𝐴 + 1 ) ∈ ( 2 ... 𝐴 ) → ( 𝐴 + 1 ) ≤ 𝐴 ) |
15 |
13 14
|
syl |
⊢ ( ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) → ( 𝐴 + 1 ) ≤ 𝐴 ) |
16 |
12 15
|
nsyl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ¬ ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) |
17 |
|
ovex |
⊢ ( 𝐴 + 1 ) ∈ V |
18 |
|
hashunsng |
⊢ ( ( 𝐴 + 1 ) ∈ V → ( ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∈ Fin ∧ ¬ ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) = ( ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) + 1 ) ) ) |
19 |
17 18
|
ax-mp |
⊢ ( ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∈ Fin ∧ ¬ ( 𝐴 + 1 ) ∈ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) = ( ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) + 1 ) ) |
20 |
4 16 19
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) = ( ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) + 1 ) ) |
21 |
|
ppival2 |
⊢ ( ( 𝐴 + 1 ) ∈ ℤ → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) |
22 |
9 21
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) ) |
23 |
|
2z |
⊢ 2 ∈ ℤ |
24 |
|
zcn |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ ) |
25 |
24
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℂ ) |
26 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
27 |
|
pncan |
⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 ) |
28 |
25 26 27
|
sylancl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 ) |
29 |
|
prmuz2 |
⊢ ( ( 𝐴 + 1 ) ∈ ℙ → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) ) |
30 |
29
|
adantl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) ) |
31 |
|
uz2m1nn |
⊢ ( ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ ) |
32 |
30 31
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 𝐴 + 1 ) − 1 ) ∈ ℕ ) |
33 |
28 32
|
eqeltrrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℕ ) |
34 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
35 |
|
2m1e1 |
⊢ ( 2 − 1 ) = 1 |
36 |
35
|
fveq2i |
⊢ ( ℤ≥ ‘ ( 2 − 1 ) ) = ( ℤ≥ ‘ 1 ) |
37 |
34 36
|
eqtr4i |
⊢ ℕ = ( ℤ≥ ‘ ( 2 − 1 ) ) |
38 |
33 37
|
eleqtrdi |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) ) |
39 |
|
fzsuc2 |
⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ) |
40 |
23 38 39
|
sylancr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( 𝐴 + 1 ) ) = ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ) |
41 |
40
|
ineq1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ∩ ℙ ) ) |
42 |
|
indir |
⊢ ( ( ( 2 ... 𝐴 ) ∪ { ( 𝐴 + 1 ) } ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) ) |
43 |
41 42
|
eqtrdi |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) ) ) |
44 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℙ ) |
45 |
44
|
snssd |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → { ( 𝐴 + 1 ) } ⊆ ℙ ) |
46 |
|
df-ss |
⊢ ( { ( 𝐴 + 1 ) } ⊆ ℙ ↔ ( { ( 𝐴 + 1 ) } ∩ ℙ ) = { ( 𝐴 + 1 ) } ) |
47 |
45 46
|
sylib |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( { ( 𝐴 + 1 ) } ∩ ℙ ) = { ( 𝐴 + 1 ) } ) |
48 |
47
|
uneq2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ ( { ( 𝐴 + 1 ) } ∩ ℙ ) ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) |
49 |
43 48
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) |
50 |
49
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) = ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) ) |
51 |
22 50
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ♯ ‘ ( ( ( 2 ... 𝐴 ) ∩ ℙ ) ∪ { ( 𝐴 + 1 ) } ) ) ) |
52 |
|
ppival2 |
⊢ ( 𝐴 ∈ ℤ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) ) |
53 |
52
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) ) |
54 |
53
|
oveq1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( π ‘ 𝐴 ) + 1 ) = ( ( ♯ ‘ ( ( 2 ... 𝐴 ) ∩ ℙ ) ) + 1 ) ) |
55 |
20 51 54
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝐴 + 1 ) ) = ( ( π ‘ 𝐴 ) + 1 ) ) |