Step | Hyp | Ref
| Expression |
1 | | elnn0 11294 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
2 | 1 | biimpi 206 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
3 | 2 | ord 392 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (¬ 𝑁 ∈
ℕ → 𝑁 =
0)) |
4 | 3 | con1d 139 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (¬ 𝑁 = 0 →
𝑁 ∈
ℕ)) |
5 | 4 | imp 445 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ¬ 𝑁 = 0) →
𝑁 ∈
ℕ) |
6 | 5 | adantrr 753 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
𝑁 ∈
ℕ) |
7 | | nn0z 11400 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
8 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ¬ 𝑁 = 0) →
𝑁 ∈
ℤ) |
9 | | odd2np1 15065 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ¬ 𝑁 = 0) →
(¬ 2 ∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
11 | | zcn 11382 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
12 | | 2cn 11091 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
13 | | mulcl 10020 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · 𝑛) ∈ ℂ) |
14 | 12, 13 | mpan 706 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (2
· 𝑛) ∈
ℂ) |
15 | | ax-1cn 9994 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
16 | | pncan 10287 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑛) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
17 | 14, 15, 16 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℂ → (((2
· 𝑛) + 1) − 1)
= (2 · 𝑛)) |
18 | 17 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℂ → ((((2
· 𝑛) + 1) − 1)
/ 2) = ((2 · 𝑛) /
2)) |
19 | | 2ne0 11113 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
20 | | divcan3 10711 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝑛) / 2) = 𝑛) |
21 | 12, 19, 20 | mp3an23 1416 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℂ → ((2
· 𝑛) / 2) = 𝑛) |
22 | 18, 21 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℂ → ((((2
· 𝑛) + 1) − 1)
/ 2) = 𝑛) |
23 | 11, 22 | syl 17 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → ((((2
· 𝑛) + 1) − 1)
/ 2) = 𝑛) |
24 | | id 22 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℤ) |
25 | 23, 24 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → ((((2
· 𝑛) + 1) − 1)
/ 2) ∈ ℤ) |
26 | | oveq1 6657 |
. . . . . . . . 9
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((2 · 𝑛) + 1) − 1) = (𝑁 − 1)) |
27 | 26 | oveq1d 6665 |
. . . . . . . 8
⊢ (((2
· 𝑛) + 1) = 𝑁 → ((((2 · 𝑛) + 1) − 1) / 2) = ((𝑁 − 1) /
2)) |
28 | 27 | eleq1d 2686 |
. . . . . . 7
⊢ (((2
· 𝑛) + 1) = 𝑁 → (((((2 · 𝑛) + 1) − 1) / 2) ∈
ℤ ↔ ((𝑁 −
1) / 2) ∈ ℤ)) |
29 | 25, 28 | syl5ibcom 235 |
. . . . . 6
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) = 𝑁 → ((𝑁 − 1) / 2) ∈
ℤ)) |
30 | 29 | rexlimiv 3027 |
. . . . 5
⊢
(∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 → ((𝑁 − 1) / 2) ∈
ℤ) |
31 | 10, 30 | syl6bi 243 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ¬ 𝑁 = 0) →
(¬ 2 ∥ 𝑁 →
((𝑁 − 1) / 2) ∈
ℤ)) |
32 | 31 | impr 649 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
((𝑁 − 1) / 2) ∈
ℤ) |
33 | | nnm1nn0 11334 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
34 | 6, 33 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
(𝑁 − 1) ∈
ℕ0) |
35 | 34 | nn0red 11352 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
(𝑁 − 1) ∈
ℝ) |
36 | 34 | nn0ge0d 11354 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
0 ≤ (𝑁 −
1)) |
37 | | 2re 11090 |
. . . . 5
⊢ 2 ∈
ℝ |
38 | 37 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
2 ∈ ℝ) |
39 | | 2pos 11112 |
. . . . 5
⊢ 0 <
2 |
40 | 39 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
0 < 2) |
41 | | divge0 10892 |
. . . 4
⊢ ((((𝑁 − 1) ∈ ℝ ∧
0 ≤ (𝑁 − 1)) ∧
(2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁 − 1) / 2)) |
42 | 35, 36, 38, 40, 41 | syl22anc 1327 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
0 ≤ ((𝑁 − 1) /
2)) |
43 | | elnn0z 11390 |
. . 3
⊢ (((𝑁 − 1) / 2) ∈
ℕ0 ↔ (((𝑁 − 1) / 2) ∈ ℤ ∧ 0 ≤
((𝑁 − 1) /
2))) |
44 | 32, 42, 43 | sylanbrc 698 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
((𝑁 − 1) / 2) ∈
ℕ0) |
45 | 6, 44 | jca 554 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (¬ 𝑁 = 0 ∧
¬ 2 ∥ 𝑁)) →
(𝑁 ∈ ℕ ∧
((𝑁 − 1) / 2) ∈
ℕ0)) |