| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prmnn 16712 | . . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 2 |  | nnnn0 12535 | . . . 4
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℕ0) | 
| 3 |  | oddnn02np1 16386 | . . . 4
⊢ (𝑃 ∈ ℕ0
→ (¬ 2 ∥ 𝑃
↔ ∃𝑛 ∈
ℕ0 ((2 · 𝑛) + 1) = 𝑃)) | 
| 4 | 1, 2, 3 | 3syl 18 | . . 3
⊢ (𝑃 ∈ ℙ → (¬ 2
∥ 𝑃 ↔
∃𝑛 ∈
ℕ0 ((2 · 𝑛) + 1) = 𝑃)) | 
| 5 |  | iftrue 4530 | . . . . . . . . 9
⊢ (2
∥ 𝑛 → if(2
∥ 𝑛, (𝑛 / 2), ((𝑛 − 1) / 2)) = (𝑛 / 2)) | 
| 6 | 5 | adantr 480 | . . . . . . . 8
⊢ ((2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) = (𝑛 / 2)) | 
| 7 |  | 2nn 12340 | . . . . . . . . . 10
⊢ 2 ∈
ℕ | 
| 8 |  | nn0ledivnn 13149 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ 2 ∈ ℕ) → (𝑛 / 2) ≤ 𝑛) | 
| 9 | 7, 8 | mpan2 691 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (𝑛 / 2) ≤ 𝑛) | 
| 10 | 9 | adantl 481 | . . . . . . . 8
⊢ ((2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ (𝑛 / 2) ≤ 𝑛) | 
| 11 | 6, 10 | eqbrtrd 5164 | . . . . . . 7
⊢ ((2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) ≤ 𝑛) | 
| 12 |  | iffalse 4533 | . . . . . . . . 9
⊢ (¬ 2
∥ 𝑛 → if(2
∥ 𝑛, (𝑛 / 2), ((𝑛 − 1) / 2)) = ((𝑛 − 1) / 2)) | 
| 13 | 12 | adantr 480 | . . . . . . . 8
⊢ ((¬ 2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) = ((𝑛 − 1) /
2)) | 
| 14 |  | nn0re 12537 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) | 
| 15 |  | peano2rem 11577 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) | 
| 16 | 15 | rehalfcld 12515 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → ((𝑛 − 1) / 2) ∈
ℝ) | 
| 17 | 14, 16 | syl 17 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ((𝑛 − 1) / 2)
∈ ℝ) | 
| 18 | 14 | rehalfcld 12515 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (𝑛 / 2) ∈
ℝ) | 
| 19 | 14 | lem1d 12202 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (𝑛 − 1) ≤
𝑛) | 
| 20 | 14, 15 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (𝑛 − 1) ∈
ℝ) | 
| 21 |  | 2re 12341 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ | 
| 22 |  | 2pos 12370 | . . . . . . . . . . . . . 14
⊢ 0 <
2 | 
| 23 | 21, 22 | pm3.2i 470 | . . . . . . . . . . . . 13
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 24 | 23 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (2 ∈ ℝ ∧ 0 < 2)) | 
| 25 |  | lediv1 12134 | . . . . . . . . . . . 12
⊢ (((𝑛 − 1) ∈ ℝ ∧
𝑛 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑛 − 1) ≤ 𝑛 ↔ ((𝑛 − 1) / 2) ≤ (𝑛 / 2))) | 
| 26 | 20, 14, 24, 25 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ ((𝑛 − 1) ≤
𝑛 ↔ ((𝑛 − 1) / 2) ≤ (𝑛 / 2))) | 
| 27 | 19, 26 | mpbid 232 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ((𝑛 − 1) / 2)
≤ (𝑛 /
2)) | 
| 28 | 17, 18, 14, 27, 9 | letrd 11419 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ((𝑛 − 1) / 2)
≤ 𝑛) | 
| 29 | 28 | adantl 481 | . . . . . . . 8
⊢ ((¬ 2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ ((𝑛 − 1) / 2)
≤ 𝑛) | 
| 30 | 13, 29 | eqbrtrd 5164 | . . . . . . 7
⊢ ((¬ 2
∥ 𝑛 ∧ 𝑛 ∈ ℕ0)
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) ≤ 𝑛) | 
| 31 | 11, 30 | pm2.61ian 811 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
→ if(2 ∥ 𝑛,
(𝑛 / 2), ((𝑛 − 1) / 2)) ≤ 𝑛) | 
| 32 | 31 | ad2antlr 727 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → if(2 ∥
𝑛, (𝑛 / 2), ((𝑛 − 1) / 2)) ≤ 𝑛) | 
| 33 |  | nn0z 12640 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) | 
| 34 | 33 | adantl 481 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
→ 𝑛 ∈
ℤ) | 
| 35 |  | eqcom 2743 | . . . . . . 7
⊢ (((2
· 𝑛) + 1) = 𝑃 ↔ 𝑃 = ((2 · 𝑛) + 1)) | 
| 36 | 35 | biimpi 216 | . . . . . 6
⊢ (((2
· 𝑛) + 1) = 𝑃 → 𝑃 = ((2 · 𝑛) + 1)) | 
| 37 |  | flodddiv4 16453 | . . . . . 6
⊢ ((𝑛 ∈ ℤ ∧ 𝑃 = ((2 · 𝑛) + 1)) →
(⌊‘(𝑃 / 4)) =
if(2 ∥ 𝑛, (𝑛 / 2), ((𝑛 − 1) / 2))) | 
| 38 | 34, 36, 37 | syl2an 596 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) →
(⌊‘(𝑃 / 4)) =
if(2 ∥ 𝑛, (𝑛 / 2), ((𝑛 − 1) / 2))) | 
| 39 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑃 = ((2 · 𝑛) + 1) → (𝑃 − 1) = (((2 · 𝑛) + 1) −
1)) | 
| 40 | 39 | eqcoms 2744 | . . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑃 → (𝑃 − 1) = (((2 · 𝑛) + 1) −
1)) | 
| 41 | 40 | adantl 481 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → (𝑃 − 1) = (((2 ·
𝑛) + 1) −
1)) | 
| 42 |  | 2nn0 12545 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 | 
| 43 | 42 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 2 ∈ ℕ0) | 
| 44 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℕ0) | 
| 45 | 43, 44 | nn0mulcld 12594 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (2 · 𝑛)
∈ ℕ0) | 
| 46 | 45 | nn0cnd 12591 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (2 · 𝑛)
∈ ℂ) | 
| 47 |  | pncan1 11688 | . . . . . . . . . 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 2776 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → (𝑃 − 1) = (2 · 𝑛)) | 
| 51 | 50 | oveq1d 7447 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → ((𝑃 − 1) / 2) = ((2 ·
𝑛) / 2)) | 
| 52 |  | nn0cn 12538 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) | 
| 53 |  | 2cnd 12345 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 2 ∈ ℂ) | 
| 54 |  | 2ne0 12371 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 55 | 54 | a1i 11 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 2 ≠ 0) | 
| 56 | 52, 53, 55 | divcan3d 12049 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((2 · 𝑛) / 2)
= 𝑛) | 
| 57 | 56 | ad2antlr 727 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → ((2 ·
𝑛) / 2) = 𝑛) | 
| 58 | 51, 57 | eqtrd 2776 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) → ((𝑃 − 1) / 2) = 𝑛) | 
| 59 | 32, 38, 58 | 3brtr4d 5174 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
∧ ((2 · 𝑛) + 1)
= 𝑃) →
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2)) | 
| 60 | 59 | rexlimdva2 3156 | . . 3
⊢ (𝑃 ∈ ℙ →
(∃𝑛 ∈
ℕ0 ((2 · 𝑛) + 1) = 𝑃 → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2))) | 
| 61 | 4, 60 | sylbid 240 | . 2
⊢ (𝑃 ∈ ℙ → (¬ 2
∥ 𝑃 →
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2))) | 
| 62 | 61 | imp 406 | 1
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2)) |