Step | Hyp | Ref
| Expression |
1 | | odd2np1 15065 |
. . 3
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
2 | | 0xr 10086 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
3 | | 1re 10039 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
4 | 3 | rexri 10097 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ* |
5 | | halfre 11246 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ |
6 | 5 | rexri 10097 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ* |
7 | 2, 4, 6 | 3pm3.2i 1239 |
. . . . . . . . . . 11
⊢ (0 ∈
ℝ* ∧ 1 ∈ ℝ* ∧ (1 / 2) ∈
ℝ*) |
8 | | halfgt0 11248 |
. . . . . . . . . . . 12
⊢ 0 < (1
/ 2) |
9 | | halflt1 11250 |
. . . . . . . . . . . 12
⊢ (1 / 2)
< 1 |
10 | 8, 9 | pm3.2i 471 |
. . . . . . . . . . 11
⊢ (0 <
(1 / 2) ∧ (1 / 2) < 1) |
11 | | elioo3g 12204 |
. . . . . . . . . . 11
⊢ ((1 / 2)
∈ (0(,)1) ↔ ((0 ∈ ℝ* ∧ 1 ∈
ℝ* ∧ (1 / 2) ∈ ℝ*) ∧ (0 < (1
/ 2) ∧ (1 / 2) < 1))) |
12 | 7, 10, 11 | mpbir2an 955 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ (0(,)1) |
13 | | zltaddlt1le 12324 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (1 / 2)
∈ (0(,)1)) → ((𝑛
+ (1 / 2)) < 𝑀 ↔
(𝑛 + (1 / 2)) ≤ 𝑀)) |
14 | 12, 13 | mp3an3 1413 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑛 + (1 / 2)) < 𝑀 ↔ (𝑛 + (1 / 2)) ≤ 𝑀)) |
15 | | zcn 11382 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
16 | 15 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 ∈
ℂ) |
17 | | 1cnd 10056 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 1 ∈
ℂ) |
18 | | 2cnne0 11242 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
19 | 18 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (2
∈ ℂ ∧ 2 ≠ 0)) |
20 | | muldivdir 10720 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · 𝑛) + 1) / 2) = (𝑛 + (1 / 2))) |
21 | 16, 17, 19, 20 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) / 2) =
(𝑛 + (1 /
2))) |
22 | 21 | breq1d 4663 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) <
𝑀 ↔ (𝑛 + (1 / 2)) < 𝑀)) |
23 | 21 | breq1d 4663 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) ≤
𝑀 ↔ (𝑛 + (1 / 2)) ≤ 𝑀)) |
24 | 14, 22, 23 | 3bitr4rd 301 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) ≤
𝑀 ↔ (((2 ·
𝑛) + 1) / 2) < 𝑀)) |
25 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) / 2) = (𝑁 / 2)) |
26 | 25 | breq1d 4663 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) / 2) ≤ 𝑀 ↔ (𝑁 / 2) ≤ 𝑀)) |
27 | 25 | breq1d 4663 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) / 2) < 𝑀 ↔ (𝑁 / 2) < 𝑀)) |
28 | 26, 27 | bibi12d 335 |
. . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((((2 · 𝑛) + 1) / 2) ≤ 𝑀 ↔ (((2 · 𝑛) + 1) / 2) < 𝑀) ↔ ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))) |
29 | 24, 28 | syl5ibcom 235 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))) |
30 | 29 | ex 450 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
31 | 30 | adantl 482 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
32 | 31 | com23 86 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
33 | 32 | rexlimdva 3031 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
34 | 1, 33 | sylbid 230 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
35 | 34 | 3imp 1256 |
1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)) |