| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | odd2np1 16379 | . . 3
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) | 
| 2 |  | 0xr 11309 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ* | 
| 3 |  | 1xr 11321 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ* | 
| 4 |  | halfre 12481 | . . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ | 
| 5 | 4 | rexri 11320 | . . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ* | 
| 6 | 2, 3, 5 | 3pm3.2i 1339 | . . . . . . . . . . 11
⊢ (0 ∈
ℝ* ∧ 1 ∈ ℝ* ∧ (1 / 2) ∈
ℝ*) | 
| 7 |  | halfgt0 12483 | . . . . . . . . . . . 12
⊢ 0 < (1
/ 2) | 
| 8 |  | halflt1 12485 | . . . . . . . . . . . 12
⊢ (1 / 2)
< 1 | 
| 9 | 7, 8 | pm3.2i 470 | . . . . . . . . . . 11
⊢ (0 <
(1 / 2) ∧ (1 / 2) < 1) | 
| 10 |  | elioo3g 13417 | . . . . . . . . . . 11
⊢ ((1 / 2)
∈ (0(,)1) ↔ ((0 ∈ ℝ* ∧ 1 ∈
ℝ* ∧ (1 / 2) ∈ ℝ*) ∧ (0 < (1
/ 2) ∧ (1 / 2) < 1))) | 
| 11 | 6, 9, 10 | mpbir2an 711 | . . . . . . . . . 10
⊢ (1 / 2)
∈ (0(,)1) | 
| 12 |  | zltaddlt1le 13546 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (1 / 2)
∈ (0(,)1)) → ((𝑛
+ (1 / 2)) < 𝑀 ↔
(𝑛 + (1 / 2)) ≤ 𝑀)) | 
| 13 | 11, 12 | mp3an3 1451 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑛 + (1 / 2)) < 𝑀 ↔ (𝑛 + (1 / 2)) ≤ 𝑀)) | 
| 14 |  | zcn 12620 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) | 
| 15 | 14 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 ∈
ℂ) | 
| 16 |  | 1cnd 11257 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 1 ∈
ℂ) | 
| 17 |  | 2cnne0 12477 | . . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 18 | 17 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (2
∈ ℂ ∧ 2 ≠ 0)) | 
| 19 |  | muldivdir 11961 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · 𝑛) + 1) / 2) = (𝑛 + (1 / 2))) | 
| 20 | 15, 16, 18, 19 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) / 2) =
(𝑛 + (1 /
2))) | 
| 21 | 20 | breq1d 5152 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) <
𝑀 ↔ (𝑛 + (1 / 2)) < 𝑀)) | 
| 22 | 20 | breq1d 5152 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) ≤
𝑀 ↔ (𝑛 + (1 / 2)) ≤ 𝑀)) | 
| 23 | 13, 21, 22 | 3bitr4rd 312 | . . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) ≤
𝑀 ↔ (((2 ·
𝑛) + 1) / 2) < 𝑀)) | 
| 24 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) / 2) = (𝑁 / 2)) | 
| 25 | 24 | breq1d 5152 | . . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) / 2) ≤ 𝑀 ↔ (𝑁 / 2) ≤ 𝑀)) | 
| 26 | 24 | breq1d 5152 | . . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) / 2) < 𝑀 ↔ (𝑁 / 2) < 𝑀)) | 
| 27 | 25, 26 | bibi12d 345 | . . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((((2 · 𝑛) + 1) / 2) ≤ 𝑀 ↔ (((2 · 𝑛) + 1) / 2) < 𝑀) ↔ ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))) | 
| 28 | 23, 27 | syl5ibcom 245 | . . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))) | 
| 29 | 28 | ex 412 | . . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) | 
| 30 | 29 | adantl 481 | . . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) | 
| 31 | 30 | com23 86 | . . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) | 
| 32 | 31 | rexlimdva 3154 | . . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) | 
| 33 | 1, 32 | sylbid 240 | . 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) | 
| 34 | 33 | 3imp 1110 | 1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)) |