Step | Hyp | Ref
| Expression |
1 | | odd2np1 11843 |
. . 3
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
2 | | 0xr 7978 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
3 | | 1re 7931 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
4 | 3 | rexri 7989 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ* |
5 | | halfre 9103 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ |
6 | 5 | rexri 7989 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ* |
7 | 2, 4, 6 | 3pm3.2i 1175 |
. . . . . . . . . . 11
⊢ (0 ∈
ℝ* ∧ 1 ∈ ℝ* ∧ (1 / 2) ∈
ℝ*) |
8 | | halfgt0 9105 |
. . . . . . . . . . . 12
⊢ 0 < (1
/ 2) |
9 | | halflt1 9107 |
. . . . . . . . . . . 12
⊢ (1 / 2)
< 1 |
10 | 8, 9 | pm3.2i 272 |
. . . . . . . . . . 11
⊢ (0 <
(1 / 2) ∧ (1 / 2) < 1) |
11 | | elioo3g 9879 |
. . . . . . . . . . 11
⊢ ((1 / 2)
∈ (0(,)1) ↔ ((0 ∈ ℝ* ∧ 1 ∈
ℝ* ∧ (1 / 2) ∈ ℝ*) ∧ (0 < (1
/ 2) ∧ (1 / 2) < 1))) |
12 | 7, 10, 11 | mpbir2an 942 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ (0(,)1) |
13 | | zltaddlt1le 9976 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (1 / 2)
∈ (0(,)1)) → ((𝑛
+ (1 / 2)) < 𝑀 ↔
(𝑛 + (1 / 2)) ≤ 𝑀)) |
14 | 12, 13 | mp3an3 1326 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑛 + (1 / 2)) < 𝑀 ↔ (𝑛 + (1 / 2)) ≤ 𝑀)) |
15 | | zcn 9229 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
16 | 15 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 ∈
ℂ) |
17 | | 1cnd 7948 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 1 ∈
ℂ) |
18 | | 2cn 8961 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
19 | | 2ap0 8983 |
. . . . . . . . . . . . 13
⊢ 2 #
0 |
20 | 18, 19 | pm3.2i 272 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 # 0) |
21 | 20 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (2
∈ ℂ ∧ 2 # 0)) |
22 | | muldivdirap 8636 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → (((2 · 𝑛) + 1) / 2) = (𝑛 + (1 / 2))) |
23 | 16, 17, 21, 22 | syl3anc 1238 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) / 2) =
(𝑛 + (1 /
2))) |
24 | 23 | breq1d 4008 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) <
𝑀 ↔ (𝑛 + (1 / 2)) < 𝑀)) |
25 | 23 | breq1d 4008 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) ≤
𝑀 ↔ (𝑛 + (1 / 2)) ≤ 𝑀)) |
26 | 14, 24, 25 | 3bitr4rd 221 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) ≤
𝑀 ↔ (((2 ·
𝑛) + 1) / 2) < 𝑀)) |
27 | | oveq1 5872 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) / 2) = (𝑁 / 2)) |
28 | 27 | breq1d 4008 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) / 2) ≤ 𝑀 ↔ (𝑁 / 2) ≤ 𝑀)) |
29 | 27 | breq1d 4008 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) / 2) < 𝑀 ↔ (𝑁 / 2) < 𝑀)) |
30 | 28, 29 | bibi12d 235 |
. . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((((2 · 𝑛) + 1) / 2) ≤ 𝑀 ↔ (((2 · 𝑛) + 1) / 2) < 𝑀) ↔ ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))) |
31 | 26, 30 | syl5ibcom 155 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))) |
32 | 31 | ex 115 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
33 | 32 | adantl 277 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
34 | 33 | com23 78 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
35 | 34 | rexlimdva 2592 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
36 | 1, 35 | sylbid 150 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
37 | 36 | 3imp 1193 |
1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)) |