Step | Hyp | Ref
| Expression |
1 | | odd2np1 16060 |
. . 3
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
2 | | halfre 12197 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 2)
∈ ℝ |
3 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (1 / 2)
∈ ℝ) |
4 | | 1red 10986 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 1 ∈
ℝ) |
5 | | zre 12333 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℝ) |
6 | 3, 4, 5 | 3jca 1127 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ)) |
7 | 6 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ)) |
8 | | halflt1 12201 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
< 1 |
9 | | axltadd 11058 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((1 / 2) < 1
→ (𝑛 + (1 / 2)) <
(𝑛 + 1))) |
10 | 7, 8, 9 | mpisyl 21 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + (1 / 2)) < (𝑛 + 1)) |
11 | | zre 12333 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
12 | 11 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑀 ∈
ℝ) |
13 | 5, 3 | readdcld 11014 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (𝑛 + (1 / 2)) ∈
ℝ) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + (1 / 2)) ∈
ℝ) |
15 | | peano2z 12371 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (𝑛 + 1) ∈
ℤ) |
16 | 15 | zred 12436 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (𝑛 + 1) ∈
ℝ) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + 1) ∈
ℝ) |
18 | | lttr 11061 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ (𝑛 + (1 / 2)) ∈ ℝ ∧
(𝑛 + 1) ∈ ℝ)
→ ((𝑀 < (𝑛 + (1 / 2)) ∧ (𝑛 + (1 / 2)) < (𝑛 + 1)) → 𝑀 < (𝑛 + 1))) |
19 | 12, 14, 17, 18 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 < (𝑛 + (1 / 2)) ∧ (𝑛 + (1 / 2)) < (𝑛 + 1)) → 𝑀 < (𝑛 + 1))) |
20 | 10, 19 | mpan2d 691 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) → 𝑀 < (𝑛 + 1))) |
21 | | zleltp1 12381 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ≤ 𝑛 ↔ 𝑀 < (𝑛 + 1))) |
22 | 21 | ancoms 459 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑛 ↔ 𝑀 < (𝑛 + 1))) |
23 | 20, 22 | sylibrd 258 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) → 𝑀 ≤ 𝑛)) |
24 | | halfgt0 12199 |
. . . . . . . . . . . 12
⊢ 0 < (1
/ 2) |
25 | 3, 5 | jca 512 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ)) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ)) |
27 | | ltaddpos 11475 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ) → (0 < (1 / 2) ↔ 𝑛 < (𝑛 + (1 / 2)))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 <
(1 / 2) ↔ 𝑛 <
(𝑛 + (1 /
2)))) |
29 | 24, 28 | mpbii 232 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 < (𝑛 + (1 / 2))) |
30 | 5 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 ∈
ℝ) |
31 | | lelttr 11075 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑛 + (1 / 2)) ∈ ℝ)
→ ((𝑀 ≤ 𝑛 ∧ 𝑛 < (𝑛 + (1 / 2))) → 𝑀 < (𝑛 + (1 / 2)))) |
32 | 12, 30, 14, 31 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 ≤ 𝑛 ∧ 𝑛 < (𝑛 + (1 / 2))) → 𝑀 < (𝑛 + (1 / 2)))) |
33 | 29, 32 | mpan2d 691 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑛 → 𝑀 < (𝑛 + (1 / 2)))) |
34 | 23, 33 | impbid 211 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) ↔ 𝑀 ≤ 𝑛)) |
35 | | zcn 12334 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
36 | | 1cnd 10980 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 1 ∈
ℂ) |
37 | | 2cnne0 12193 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
38 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (2 ∈
ℂ ∧ 2 ≠ 0)) |
39 | | muldivdir 11678 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · 𝑛) + 1) / 2) = (𝑛 + (1 / 2))) |
40 | 35, 36, 38, 39 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) / 2) =
(𝑛 + (1 /
2))) |
41 | 40 | breq2d 5085 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑛 + (1 / 2)))) |
42 | 41 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑛 + (1 / 2)))) |
43 | | 2z 12362 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℤ → 2 ∈
ℤ) |
45 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℤ) |
46 | 44, 45 | zmulcld 12442 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℤ) |
47 | 46 | zcnd 12437 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℂ) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (2
· 𝑛) ∈
ℂ) |
49 | | pncan1 11409 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑛) ∈ ℂ
→ (((2 · 𝑛) +
1) − 1) = (2 · 𝑛)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) − 1)
= (2 · 𝑛)) |
51 | 50 | oveq1d 7282 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) − 1)
/ 2) = ((2 · 𝑛) /
2)) |
52 | | 2cnd 12061 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 ∈
ℂ) |
53 | | 2ne0 12087 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 ≠
0) |
55 | 35, 52, 54 | divcan3d 11766 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) / 2) = 𝑛) |
56 | 55 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2
· 𝑛) / 2) = 𝑛) |
57 | 51, 56 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) − 1)
/ 2) = 𝑛) |
58 | 57 | breq2d 5085 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2) ↔
𝑀 ≤ 𝑛)) |
59 | 34, 42, 58 | 3bitr4d 311 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 ≤ ((((2 · 𝑛) + 1) − 1) /
2))) |
60 | | oveq1 7274 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) / 2) = (𝑁 / 2)) |
61 | 60 | breq2d 5085 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑁 / 2))) |
62 | | oveq1 7274 |
. . . . . . . . . . 11
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) − 1) = (𝑁 − 1)) |
63 | 62 | oveq1d 7282 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) − 1) / 2) = ((𝑁 − 1) /
2)) |
64 | 63 | breq2d 5085 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) |
65 | 61, 64 | bibi12d 346 |
. . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2)) ↔ (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2)))) |
66 | 59, 65 | syl5ibcom 244 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2)))) |
67 | 66 | ex 413 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
68 | 67 | adantl 482 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
69 | 68 | com23 86 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
70 | 69 | rexlimdva 3211 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
71 | 1, 70 | sylbid 239 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
72 | 71 | 3imp 1110 |
1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) |