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 |
|
peano2z |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ ) |
43 |
42
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 𝐴 + 1 ) ∈ ℤ ) |
44 |
|
flid |
⊢ ( ( 𝐴 + 1 ) ∈ ℤ → ( ⌊ ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) ) |
45 |
43 44
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ⌊ ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) ) |
46 |
45
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) = ( 2 ... ( 𝐴 + 1 ) ) ) |
47 |
46
|
ineq1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) = ( ( 2 ... ( 𝐴 + 1 ) ) ∩ ℙ ) ) |
48 |
|
flid |
⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 ) |
49 |
48
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ⌊ ‘ 𝐴 ) = 𝐴 ) |
50 |
49
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) = ( 2 ... 𝐴 ) ) |
51 |
50
|
ineq1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... 𝐴 ) ∩ ℙ ) ) |
52 |
41 47 51
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) |
53 |
|
zre |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ ) |
54 |
53
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → 𝐴 ∈ ℝ ) |
55 |
|
peano2re |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ ) |
56 |
|
ppisval |
⊢ ( ( 𝐴 + 1 ) ∈ ℝ → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) ) |
57 |
54 55 56
|
3syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ∩ ℙ ) ) |
58 |
|
ppisval |
⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) |
59 |
54 58
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) |
60 |
52 57 59
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) = ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) |
61 |
60
|
sumeq1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
62 |
|
chtval |
⊢ ( ( 𝐴 + 1 ) ∈ ℝ → ( θ ‘ ( 𝐴 + 1 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
63 |
54 55 62
|
3syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ ( 𝐴 + 1 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 + 1 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
64 |
|
chtval |
⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
65 |
54 64
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
66 |
61 63 65
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ ( 𝐴 + 1 ) ∈ ℙ ) → ( θ ‘ ( 𝐴 + 1 ) ) = ( θ ‘ 𝐴 ) ) |