Step | Hyp | Ref
| Expression |
1 | | odd2np1 11810 |
. . 3
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
2 | | 0xr 7945 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
3 | | 1re 7898 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
4 | 3 | rexri 7956 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ* |
5 | | halfre 9070 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ |
6 | 5 | rexri 7956 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ* |
7 | 2, 4, 6 | 3pm3.2i 1165 |
. . . . . . . . . . 11
⊢ (0 ∈
ℝ* ∧ 1 ∈ ℝ* ∧ (1 / 2) ∈
ℝ*) |
8 | | halfgt0 9072 |
. . . . . . . . . . . 12
⊢ 0 < (1
/ 2) |
9 | | halflt1 9074 |
. . . . . . . . . . . 12
⊢ (1 / 2)
< 1 |
10 | 8, 9 | pm3.2i 270 |
. . . . . . . . . . 11
⊢ (0 <
(1 / 2) ∧ (1 / 2) < 1) |
11 | | elioo3g 9846 |
. . . . . . . . . . 11
⊢ ((1 / 2)
∈ (0(,)1) ↔ ((0 ∈ ℝ* ∧ 1 ∈
ℝ* ∧ (1 / 2) ∈ ℝ*) ∧ (0 < (1
/ 2) ∧ (1 / 2) < 1))) |
12 | 7, 10, 11 | mpbir2an 932 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ (0(,)1) |
13 | | zltaddlt1le 9943 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (1 / 2)
∈ (0(,)1)) → ((𝑛
+ (1 / 2)) < 𝑀 ↔
(𝑛 + (1 / 2)) ≤ 𝑀)) |
14 | 12, 13 | mp3an3 1316 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑛 + (1 / 2)) < 𝑀 ↔ (𝑛 + (1 / 2)) ≤ 𝑀)) |
15 | | zcn 9196 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
16 | 15 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 ∈
ℂ) |
17 | | 1cnd 7915 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 1 ∈
ℂ) |
18 | | 2cn 8928 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
19 | | 2ap0 8950 |
. . . . . . . . . . . . 13
⊢ 2 #
0 |
20 | 18, 19 | pm3.2i 270 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 # 0) |
21 | 20 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (2
∈ ℂ ∧ 2 # 0)) |
22 | | muldivdirap 8603 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → (((2 · 𝑛) + 1) / 2) = (𝑛 + (1 / 2))) |
23 | 16, 17, 21, 22 | syl3anc 1228 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) / 2) =
(𝑛 + (1 /
2))) |
24 | 23 | breq1d 3992 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) <
𝑀 ↔ (𝑛 + (1 / 2)) < 𝑀)) |
25 | 23 | breq1d 3992 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) ≤
𝑀 ↔ (𝑛 + (1 / 2)) ≤ 𝑀)) |
26 | 14, 24, 25 | 3bitr4rd 220 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) / 2) ≤
𝑀 ↔ (((2 ·
𝑛) + 1) / 2) < 𝑀)) |
27 | | oveq1 5849 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) / 2) = (𝑁 / 2)) |
28 | 27 | breq1d 3992 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) / 2) ≤ 𝑀 ↔ (𝑁 / 2) ≤ 𝑀)) |
29 | 27 | breq1d 3992 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) / 2) < 𝑀 ↔ (𝑁 / 2) < 𝑀)) |
30 | 28, 29 | bibi12d 234 |
. . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((((2 · 𝑛) + 1) / 2) ≤ 𝑀 ↔ (((2 · 𝑛) + 1) / 2) < 𝑀) ↔ ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))) |
31 | 26, 30 | syl5ibcom 154 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))) |
32 | 31 | ex 114 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
33 | 32 | adantl 275 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
34 | 33 | com23 78 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
35 | 34 | rexlimdva 2583 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
36 | 1, 35 | sylbid 149 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 → (𝑀 ∈ ℤ → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)))) |
37 | 36 | 3imp 1183 |
1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)) |