Step | Hyp | Ref
| Expression |
1 | | odd2np1 11832 |
. . 3
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
2 | | halfre 9091 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 2)
∈ ℝ |
3 | 2 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (1 / 2)
∈ ℝ) |
4 | | 1red 7935 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 1 ∈
ℝ) |
5 | | zre 9216 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℝ) |
6 | 3, 4, 5 | 3jca 1172 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ)) |
7 | 6 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ)) |
8 | | halflt1 9095 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
< 1 |
9 | | axltadd 7989 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((1 / 2) < 1
→ (𝑛 + (1 / 2)) <
(𝑛 + 1))) |
10 | 7, 8, 9 | mpisyl 1439 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + (1 / 2)) < (𝑛 + 1)) |
11 | | zre 9216 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
12 | 11 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑀 ∈
ℝ) |
13 | 5, 3 | readdcld 7949 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (𝑛 + (1 / 2)) ∈
ℝ) |
14 | 13 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + (1 / 2)) ∈
ℝ) |
15 | | peano2z 9248 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (𝑛 + 1) ∈
ℤ) |
16 | 15 | zred 9334 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (𝑛 + 1) ∈
ℝ) |
17 | 16 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑛 + 1) ∈
ℝ) |
18 | | lttr 7993 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ (𝑛 + (1 / 2)) ∈ ℝ ∧
(𝑛 + 1) ∈ ℝ)
→ ((𝑀 < (𝑛 + (1 / 2)) ∧ (𝑛 + (1 / 2)) < (𝑛 + 1)) → 𝑀 < (𝑛 + 1))) |
19 | 12, 14, 17, 18 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 < (𝑛 + (1 / 2)) ∧ (𝑛 + (1 / 2)) < (𝑛 + 1)) → 𝑀 < (𝑛 + 1))) |
20 | 10, 19 | mpan2d 426 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) → 𝑀 < (𝑛 + 1))) |
21 | | zleltp1 9267 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ≤ 𝑛 ↔ 𝑀 < (𝑛 + 1))) |
22 | 21 | ancoms 266 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑛 ↔ 𝑀 < (𝑛 + 1))) |
23 | 20, 22 | sylibrd 168 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) → 𝑀 ≤ 𝑛)) |
24 | | halfgt0 9093 |
. . . . . . . . . . . 12
⊢ 0 < (1
/ 2) |
25 | 3, 5 | jca 304 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ)) |
26 | 25 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ)) |
27 | | ltaddpos 8371 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 𝑛
∈ ℝ) → (0 < (1 / 2) ↔ 𝑛 < (𝑛 + (1 / 2)))) |
28 | 26, 27 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 <
(1 / 2) ↔ 𝑛 <
(𝑛 + (1 /
2)))) |
29 | 24, 28 | mpbii 147 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 < (𝑛 + (1 / 2))) |
30 | 5 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑛 ∈
ℝ) |
31 | | lelttr 8008 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑛 + (1 / 2)) ∈ ℝ)
→ ((𝑀 ≤ 𝑛 ∧ 𝑛 < (𝑛 + (1 / 2))) → 𝑀 < (𝑛 + (1 / 2)))) |
32 | 12, 30, 14, 31 | syl3anc 1233 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 ≤ 𝑛 ∧ 𝑛 < (𝑛 + (1 / 2))) → 𝑀 < (𝑛 + (1 / 2)))) |
33 | 29, 32 | mpan2d 426 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑛 → 𝑀 < (𝑛 + (1 / 2)))) |
34 | 23, 33 | impbid 128 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑛 + (1 / 2)) ↔ 𝑀 ≤ 𝑛)) |
35 | | zcn 9217 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
36 | | 1cnd 7936 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 1 ∈
ℂ) |
37 | | 2cn 8949 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
38 | | 2ap0 8971 |
. . . . . . . . . . . . . 14
⊢ 2 #
0 |
39 | 37, 38 | pm3.2i 270 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 # 0) |
40 | 39 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (2 ∈
ℂ ∧ 2 # 0)) |
41 | | muldivdirap 8624 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → (((2 · 𝑛) + 1) / 2) = (𝑛 + (1 / 2))) |
42 | 35, 36, 40, 41 | syl3anc 1233 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) / 2) =
(𝑛 + (1 /
2))) |
43 | 42 | breq2d 4001 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑛 + (1 / 2)))) |
44 | 43 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑛 + (1 / 2)))) |
45 | | 2z 9240 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
46 | 45 | a1i 9 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℤ → 2 ∈
ℤ) |
47 | | id 19 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℤ) |
48 | 46, 47 | zmulcld 9340 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℤ) |
49 | 48 | zcnd 9335 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℂ) |
50 | 49 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (2
· 𝑛) ∈
ℂ) |
51 | | pncan1 8296 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑛) ∈ ℂ
→ (((2 · 𝑛) +
1) − 1) = (2 · 𝑛)) |
52 | 50, 51 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) − 1)
= (2 · 𝑛)) |
53 | 52 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) − 1)
/ 2) = ((2 · 𝑛) /
2)) |
54 | | 2cnd 8951 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 ∈
ℂ) |
55 | 38 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 #
0) |
56 | 35, 54, 55 | divcanap3d 8712 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) / 2) = 𝑛) |
57 | 56 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2
· 𝑛) / 2) = 𝑛) |
58 | 53, 57 | eqtrd 2203 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((2
· 𝑛) + 1) − 1)
/ 2) = 𝑛) |
59 | 58 | breq2d 4001 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2) ↔
𝑀 ≤ 𝑛)) |
60 | 34, 44, 59 | 3bitr4d 219 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 ≤ ((((2 · 𝑛) + 1) − 1) /
2))) |
61 | | oveq1 5860 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) / 2) = (𝑁 / 2)) |
62 | 61 | breq2d 4001 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 < (𝑁 / 2))) |
63 | | oveq1 5860 |
. . . . . . . . . . 11
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) − 1) = (𝑁 − 1)) |
64 | 63 | oveq1d 5868 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) − 1) / 2) = ((𝑁 − 1) /
2)) |
65 | 64 | breq2d 4001 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) |
66 | 62, 65 | bibi12d 234 |
. . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((𝑀 < (((2 · 𝑛) + 1) / 2) ↔ 𝑀 ≤ ((((2 · 𝑛) + 1) − 1) / 2)) ↔ (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2)))) |
67 | 60, 66 | syl5ibcom 154 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2)))) |
68 | 67 | ex 114 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
69 | 68 | adantl 275 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑀 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
70 | 69 | com23 78 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((2
· 𝑛) + 1) = 𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
71 | 70 | rexlimdva 2587 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
72 | 1, 71 | sylbid 149 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 → (𝑀 ∈ ℤ → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))))) |
73 | 72 | 3imp 1188 |
1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) |