Proof of Theorem nno
Step | Hyp | Ref
| Expression |
1 | | eluz2b3 8691 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) |
2 | | nnnn0 8295 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
3 | | nn0o1gt2 10305 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁)) |
4 | 2, 3 | sylan 277 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁)) |
5 | | eqneqall 2255 |
. . . . . . 7
⊢ (𝑁 = 1 → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈
ℕ)) |
6 | 5 | a1d 22 |
. . . . . 6
⊢ (𝑁 = 1 → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ0)
→ (𝑁 ≠ 1 →
((𝑁 − 1) / 2) ∈
ℕ))) |
7 | | nn0z 8371 |
. . . . . . . . . . . 12
⊢ (((𝑁 + 1) / 2) ∈
ℕ0 → ((𝑁 + 1) / 2) ∈ ℤ) |
8 | | peano2zm 8389 |
. . . . . . . . . . . 12
⊢ (((𝑁 + 1) / 2) ∈ ℤ →
(((𝑁 + 1) / 2) − 1)
∈ ℤ) |
9 | 7, 8 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) / 2) ∈
ℕ0 → (((𝑁 + 1) / 2) − 1) ∈
ℤ) |
10 | 9 | ad2antlr 472 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → (((𝑁 + 1) / 2) − 1) ∈
ℤ) |
11 | | 2cn 8110 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
12 | 11 | mulid2i 7122 |
. . . . . . . . . . . . . 14
⊢ (1
· 2) = 2 |
13 | | nnre 8046 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
14 | 13 | ltp1d 8008 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1)) |
15 | 14 | adantr 270 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 𝑁 < (𝑁 + 1)) |
16 | | 2re 8109 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
17 | 16 | a1i 9 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
18 | | peano2nn 8051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
19 | 18 | nnred 8052 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) |
20 | | lttr 7185 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (𝑁 +
1) ∈ ℝ) → ((2 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 2 < (𝑁 + 1))) |
21 | 17, 13, 19, 20 | syl3anc 1169 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → ((2 <
𝑁 ∧ 𝑁 < (𝑁 + 1)) → 2 < (𝑁 + 1))) |
22 | 21 | expdimp 255 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝑁 < (𝑁 + 1) → 2 < (𝑁 + 1))) |
23 | 15, 22 | mpd 13 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 2 < (𝑁 + 1)) |
24 | 12, 23 | syl5eqbr 3818 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (1 · 2)
< (𝑁 +
1)) |
25 | | 1red 7134 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 1 ∈
ℝ) |
26 | 19 | adantr 270 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝑁 + 1) ∈
ℝ) |
27 | | 2pos 8130 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
2 |
28 | 16, 27 | pm3.2i 266 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℝ ∧ 0 < 2) |
29 | 28 | a1i 9 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (2 ∈ ℝ
∧ 0 < 2)) |
30 | | ltmuldiv 7952 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ (𝑁 +
1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((1 ·
2) < (𝑁 + 1) ↔ 1
< ((𝑁 + 1) /
2))) |
31 | 25, 26, 29, 30 | syl3anc 1169 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((1 · 2)
< (𝑁 + 1) ↔ 1 <
((𝑁 + 1) /
2))) |
32 | 24, 31 | mpbid 145 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 1 < ((𝑁 + 1) / 2)) |
33 | 19 | rehalfcld 8277 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 2) ∈
ℝ) |
34 | 33 | adantr 270 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝑁 + 1) / 2) ∈
ℝ) |
35 | 25, 34 | posdifd 7632 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (1 < ((𝑁 + 1) / 2) ↔ 0 <
(((𝑁 + 1) / 2) −
1))) |
36 | 32, 35 | mpbid 145 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 0 < (((𝑁 + 1) / 2) −
1)) |
37 | 36 | adantlr 460 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → 0 < (((𝑁 + 1) / 2) − 1)) |
38 | | elnnz 8361 |
. . . . . . . . . 10
⊢ ((((𝑁 + 1) / 2) − 1) ∈
ℕ ↔ ((((𝑁 + 1) /
2) − 1) ∈ ℤ ∧ 0 < (((𝑁 + 1) / 2) − 1))) |
39 | 10, 37, 38 | sylanbrc 408 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → (((𝑁 + 1) / 2) − 1) ∈
ℕ) |
40 | | nncn 8047 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
41 | | xp1d2m1eqxm1d2 8283 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) /
2)) |
42 | 40, 41 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) /
2)) |
43 | 42 | eleq1d 2147 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) / 2) − 1) ∈
ℕ ↔ ((𝑁 −
1) / 2) ∈ ℕ)) |
44 | 43 | adantr 270 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔
((𝑁 − 1) / 2) ∈
ℕ)) |
45 | 44 | adantr 270 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔
((𝑁 − 1) / 2) ∈
ℕ)) |
46 | 39, 45 | mpbid 145 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → ((𝑁 − 1) / 2) ∈
ℕ) |
47 | 46 | a1d 22 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈
ℕ)) |
48 | 47 | expcom 114 |
. . . . . 6
⊢ (2 <
𝑁 → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈
ℕ))) |
49 | 6, 48 | jaoi 668 |
. . . . 5
⊢ ((𝑁 = 1 ∨ 2 < 𝑁) → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ0)
→ (𝑁 ≠ 1 →
((𝑁 − 1) / 2) ∈
ℕ))) |
50 | 4, 49 | mpcom 36 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈
ℕ)) |
51 | 50 | impancom 256 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → (((𝑁 + 1) / 2) ∈
ℕ0 → ((𝑁 − 1) / 2) ∈
ℕ)) |
52 | 1, 51 | sylbi 119 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (((𝑁 + 1) / 2) ∈ ℕ0 →
((𝑁 − 1) / 2) ∈
ℕ)) |
53 | 52 | imp 122 |
1
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ0)
→ ((𝑁 − 1) / 2)
∈ ℕ) |