Step | Hyp | Ref
| Expression |
1 | | prmnn 16263 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | | nnnn0 12126 |
. . . 4
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℕ0) |
3 | | oddnn02np1 15941 |
. . . 4
⊢ (𝑃 ∈ ℕ0
→ (¬ 2 ∥ 𝑃
↔ ∃𝑛 ∈
ℕ0 ((2 · 𝑛) + 1) = 𝑃)) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ (𝑃 ∈ ℙ → (¬ 2
∥ 𝑃 ↔
∃𝑛 ∈
ℕ0 ((2 · 𝑛) + 1) = 𝑃)) |
5 | | iftrue 4461 |
. . . . . . . . 9
⊢ (2
∥ 𝑛 → if(2
∥ 𝑛, (𝑛 / 2), ((𝑛 − 1) / 2)) = (𝑛 / 2)) |
6 | 5 | adantr 484 |
. . . . . . . 8
⊢ ((2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) = (𝑛 / 2)) |
7 | | 2nn 11932 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
8 | | nn0ledivnn 12728 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ 2 ∈ ℕ) → (𝑛 / 2) ≤ 𝑛) |
9 | 7, 8 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (𝑛 / 2) ≤ 𝑛) |
10 | 9 | adantl 485 |
. . . . . . . 8
⊢ ((2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ (𝑛 / 2) ≤ 𝑛) |
11 | 6, 10 | eqbrtrd 5091 |
. . . . . . 7
⊢ ((2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) ≤ 𝑛) |
12 | | iffalse 4464 |
. . . . . . . . 9
⊢ (¬ 2
∥ 𝑛 → if(2
∥ 𝑛, (𝑛 / 2), ((𝑛 − 1) / 2)) = ((𝑛 − 1) / 2)) |
13 | 12 | adantr 484 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) = ((𝑛 − 1) /
2)) |
14 | | nn0re 12128 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) |
15 | | peano2rem 11174 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
16 | 15 | rehalfcld 12106 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → ((𝑛 − 1) / 2) ∈
ℝ) |
17 | 14, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ((𝑛 − 1) / 2)
∈ ℝ) |
18 | 14 | rehalfcld 12106 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (𝑛 / 2) ∈
ℝ) |
19 | 14 | lem1d 11794 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (𝑛 − 1) ≤
𝑛) |
20 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (𝑛 − 1) ∈
ℝ) |
21 | | 2re 11933 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
22 | | 2pos 11962 |
. . . . . . . . . . . . . 14
⊢ 0 <
2 |
23 | 21, 22 | pm3.2i 474 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℝ ∧ 0 < 2) |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (2 ∈ ℝ ∧ 0 < 2)) |
25 | | lediv1 11726 |
. . . . . . . . . . . 12
⊢ (((𝑛 − 1) ∈ ℝ ∧
𝑛 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑛 − 1) ≤ 𝑛 ↔ ((𝑛 − 1) / 2) ≤ (𝑛 / 2))) |
26 | 20, 14, 24, 25 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ ((𝑛 − 1) ≤
𝑛 ↔ ((𝑛 − 1) / 2) ≤ (𝑛 / 2))) |
27 | 19, 26 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ((𝑛 − 1) / 2)
≤ (𝑛 /
2)) |
28 | 17, 18, 14, 27, 9 | letrd 11018 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ((𝑛 − 1) / 2)
≤ 𝑛) |
29 | 28 | adantl 485 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ ((𝑛 − 1) / 2)
≤ 𝑛) |
30 | 13, 29 | eqbrtrd 5091 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) ≤ 𝑛) |
31 | 11, 30 | pm2.61ian 812 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) ≤ 𝑛) |
32 | 31 | ad2antlr 727 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → if(2 ∥
𝑛, (𝑛 / 2), ((𝑛 − 1) / 2)) ≤ 𝑛) |
33 | | nn0z 12229 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
34 | 33 | adantl 485 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
→ 𝑛 ∈
ℤ) |
35 | | eqcom 2746 |
. . . . . . 7
⊢ (((2
· 𝑛) + 1) = 𝑃 ↔ 𝑃 = ((2 · 𝑛) + 1)) |
36 | 35 | biimpi 219 |
. . . . . 6
⊢ (((2
· 𝑛) + 1) = 𝑃 → 𝑃 = ((2 · 𝑛) + 1)) |
37 | | flodddiv4 16006 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ∧ 𝑃 = ((2 · 𝑛) + 1)) →
(⌊‘(𝑃 / 4)) =
if(2 ∥ 𝑛, (𝑛 / 2), ((𝑛 − 1) / 2))) |
38 | 34, 36, 37 | syl2an 599 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) →
(⌊‘(𝑃 / 4)) =
if(2 ∥ 𝑛, (𝑛 / 2), ((𝑛 − 1) / 2))) |
39 | | oveq1 7241 |
. . . . . . . . . 10
⊢ (𝑃 = ((2 · 𝑛) + 1) → (𝑃 − 1) = (((2 · 𝑛) + 1) −
1)) |
40 | 39 | eqcoms 2747 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑃 → (𝑃 − 1) = (((2 · 𝑛) + 1) −
1)) |
41 | 40 | adantl 485 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → (𝑃 − 1) = (((2 ·
𝑛) + 1) −
1)) |
42 | | 2nn0 12136 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 2 ∈ ℕ0) |
44 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℕ0) |
45 | 43, 44 | nn0mulcld 12184 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (2 · 𝑛)
∈ ℕ0) |
46 | 45 | nn0cnd 12181 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (2 · 𝑛)
∈ ℂ) |
47 | | pncan1 11285 |
. . . . . . . . . 10
⊢ ((2
· 𝑛) ∈ ℂ
→ (((2 · 𝑛) +
1) − 1) = (2 · 𝑛)) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (((2 · 𝑛) +
1) − 1) = (2 · 𝑛)) |
49 | 48 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → (((2 ·
𝑛) + 1) − 1) = (2
· 𝑛)) |
50 | 41, 49 | eqtrd 2779 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → (𝑃 − 1) = (2 · 𝑛)) |
51 | 50 | oveq1d 7249 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → ((𝑃 − 1) / 2) = ((2 ·
𝑛) / 2)) |
52 | | nn0cn 12129 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) |
53 | | 2cnd 11937 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 2 ∈ ℂ) |
54 | | 2ne0 11963 |
. . . . . . . . 9
⊢ 2 ≠
0 |
55 | 54 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 2 ≠ 0) |
56 | 52, 53, 55 | divcan3d 11642 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((2 · 𝑛) / 2)
= 𝑛) |
57 | 56 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → ((2 ·
𝑛) / 2) = 𝑛) |
58 | 51, 57 | eqtrd 2779 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → ((𝑃 − 1) / 2) = 𝑛) |
59 | 32, 38, 58 | 3brtr4d 5101 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) →
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2)) |
60 | 59 | rexlimdva2 3216 |
. . 3
⊢ (𝑃 ∈ ℙ →
(∃𝑛 ∈
ℕ0 ((2 · 𝑛) + 1) = 𝑃 → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2))) |
61 | 4, 60 | sylbid 243 |
. 2
⊢ (𝑃 ∈ ℙ → (¬ 2
∥ 𝑃 →
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2))) |
62 | 61 | imp 410 |
1
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2)) |