Step | Hyp | Ref
| Expression |
1 | | elnn0 11171 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
2 | 1 | biimpi 205 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
3 | 2 | ord 391 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (¬ 𝑁 ∈
ℕ → 𝑁 =
0)) |
4 | 3 | con1d 138 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (¬ 𝑁 = 0 →
𝑁 ∈
ℕ)) |
5 | 4 | imp 444 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ¬ 𝑁 = 0) →
𝑁 ∈
ℕ) |
6 | 5 | adantrr 749 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
𝑁 ∈
ℕ) |
7 | | nn0z 11277 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ¬ 𝑁 = 0) →
𝑁 ∈
ℤ) |
9 | | odd2np1 14903 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ¬ 𝑁 = 0) →
(¬ 2 ∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
11 | | zcn 11259 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
12 | | 2cn 10968 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
13 | | mulcl 9899 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · 𝑛) ∈ ℂ) |
14 | 12, 13 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (2
· 𝑛) ∈
ℂ) |
15 | | ax-1cn 9873 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
16 | | pncan 10166 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑛) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
17 | 14, 15, 16 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℂ → (((2
· 𝑛) + 1) − 1)
= (2 · 𝑛)) |
18 | 17 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℂ → ((((2
· 𝑛) + 1) − 1)
/ 2) = ((2 · 𝑛) /
2)) |
19 | | 2ne0 10990 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
20 | | divcan3 10590 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝑛) / 2) = 𝑛) |
21 | 12, 19, 20 | mp3an23 1408 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℂ → ((2
· 𝑛) / 2) = 𝑛) |
22 | 18, 21 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℂ → ((((2
· 𝑛) + 1) − 1)
/ 2) = 𝑛) |
23 | 11, 22 | syl 17 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → ((((2
· 𝑛) + 1) − 1)
/ 2) = 𝑛) |
24 | | id 22 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℤ) |
25 | 23, 24 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → ((((2
· 𝑛) + 1) − 1)
/ 2) ∈ ℤ) |
26 | | oveq1 6556 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) − 1) = (𝑁 − 1)) |
27 | 26 | oveq1d 6564 |
. . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) − 1) / 2) = ((𝑁 − 1) /
2)) |
28 | 27 | eleq1d 2672 |
. . . . . . 7
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((((2 · 𝑛) + 1) − 1) / 2) ∈
ℤ ↔ ((𝑁 −
1) / 2) ∈ ℤ)) |
29 | 25, 28 | syl5ibcom 234 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 − 1) / 2) ∈
ℤ)) |
30 | 29 | rexlimiv 3009 |
. . . . 5
⊢
(∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 → ((𝑁 − 1) / 2) ∈
ℤ) |
31 | 10, 30 | syl6bi 242 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ¬ 𝑁 = 0) →
(¬ 2 ∥ 𝑁 →
((𝑁 − 1) / 2) ∈
ℤ)) |
32 | 31 | impr 647 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
((𝑁 − 1) / 2) ∈
ℤ) |
33 | | nnm1nn0 11211 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
34 | 6, 33 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
(𝑁 − 1) ∈
ℕ0) |
35 | 34 | nn0red 11229 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
(𝑁 − 1) ∈
ℝ) |
36 | 34 | nn0ge0d 11231 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
0 ≤ (𝑁 −
1)) |
37 | | 2re 10967 |
. . . . 5
⊢ 2 ∈
ℝ |
38 | 37 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
2 ∈ ℝ) |
39 | | 2pos 10989 |
. . . . 5
⊢ 0 <
2 |
40 | 39 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
0 < 2) |
41 | | divge0 10771 |
. . . 4
⊢ ((((𝑁 − 1) ∈ ℝ ∧
0 ≤ (𝑁 − 1)) ∧
(2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁 − 1) / 2)) |
42 | 35, 36, 38, 40, 41 | syl22anc 1319 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
0 ≤ ((𝑁 − 1) /
2)) |
43 | | elnn0z 11267 |
. . 3
⊢ (((𝑁 − 1) / 2) ∈
ℕ0 ↔ (((𝑁 − 1) / 2) ∈ ℤ ∧ 0 ≤
((𝑁 − 1) /
2))) |
44 | 32, 42, 43 | sylanbrc 695 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
((𝑁 − 1) / 2) ∈
ℕ0) |
45 | 6, 44 | jca 553 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
(𝑁 ∈ ℕ ∧
((𝑁 − 1) / 2) ∈
ℕ0)) |