Proof of Theorem nno
Step | Hyp | Ref
| Expression |
1 | | eluz2b3 9563 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) |
2 | | nnnn0 9142 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
3 | | nn0o1gt2 11864 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁)) |
4 | 2, 3 | sylan 281 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁)) |
5 | | eqneqall 2350 |
. . . . . . 7
⊢ (𝑁 = 1 → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈
ℕ)) |
6 | 5 | a1d 22 |
. . . . . 6
⊢ (𝑁 = 1 → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ0)
→ (𝑁 ≠ 1 →
((𝑁 − 1) / 2) ∈
ℕ))) |
7 | | nn0z 9232 |
. . . . . . . . . . . 12
⊢ (((𝑁 + 1) / 2) ∈
ℕ0 → ((𝑁 + 1) / 2) ∈ ℤ) |
8 | | peano2zm 9250 |
. . . . . . . . . . . 12
⊢ (((𝑁 + 1) / 2) ∈ ℤ →
(((𝑁 + 1) / 2) − 1)
∈ ℤ) |
9 | 7, 8 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) / 2) ∈
ℕ0 → (((𝑁 + 1) / 2) − 1) ∈
ℤ) |
10 | 9 | ad2antlr 486 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → (((𝑁 + 1) / 2) − 1) ∈
ℤ) |
11 | | 2cn 8949 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
12 | 11 | mulid2i 7923 |
. . . . . . . . . . . . . 14
⊢ (1
· 2) = 2 |
13 | | nnre 8885 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
14 | 13 | ltp1d 8846 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1)) |
15 | 14 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 𝑁 < (𝑁 + 1)) |
16 | | 2re 8948 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
17 | 16 | a1i 9 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
18 | | peano2nn 8890 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
19 | 18 | nnred 8891 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) |
20 | | lttr 7993 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (𝑁 +
1) ∈ ℝ) → ((2 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 2 < (𝑁 + 1))) |
21 | 17, 13, 19, 20 | syl3anc 1233 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → ((2 <
𝑁 ∧ 𝑁 < (𝑁 + 1)) → 2 < (𝑁 + 1))) |
22 | 21 | expdimp 257 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝑁 < (𝑁 + 1) → 2 < (𝑁 + 1))) |
23 | 15, 22 | mpd 13 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 2 < (𝑁 + 1)) |
24 | 12, 23 | eqbrtrid 4024 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (1 · 2)
< (𝑁 +
1)) |
25 | | 1red 7935 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 1 ∈
ℝ) |
26 | 19 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (𝑁 + 1) ∈
ℝ) |
27 | | 2pos 8969 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
2 |
28 | 16, 27 | pm3.2i 270 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℝ ∧ 0 < 2) |
29 | 28 | a1i 9 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (2 ∈ ℝ
∧ 0 < 2)) |
30 | | ltmuldiv 8790 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ (𝑁 +
1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((1 ·
2) < (𝑁 + 1) ↔ 1
< ((𝑁 + 1) /
2))) |
31 | 25, 26, 29, 30 | syl3anc 1233 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((1 · 2)
< (𝑁 + 1) ↔ 1 <
((𝑁 + 1) /
2))) |
32 | 24, 31 | mpbid 146 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 1 < ((𝑁 + 1) / 2)) |
33 | 19 | rehalfcld 9124 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 2) ∈
ℝ) |
34 | 33 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → ((𝑁 + 1) / 2) ∈
ℝ) |
35 | 25, 34 | posdifd 8451 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → (1 < ((𝑁 + 1) / 2) ↔ 0 <
(((𝑁 + 1) / 2) −
1))) |
36 | 32, 35 | mpbid 146 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 2 <
𝑁) → 0 < (((𝑁 + 1) / 2) −
1)) |
37 | 36 | adantlr 474 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → 0 < (((𝑁 + 1) / 2) − 1)) |
38 | | elnnz 9222 |
. . . . . . . . . 10
⊢ ((((𝑁 + 1) / 2) − 1) ∈
ℕ ↔ ((((𝑁 + 1) /
2) − 1) ∈ ℤ ∧ 0 < (((𝑁 + 1) / 2) − 1))) |
39 | 10, 37, 38 | sylanbrc 415 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → (((𝑁 + 1) / 2) − 1) ∈
ℕ) |
40 | | nncn 8886 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
41 | | xp1d2m1eqxm1d2 9130 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) /
2)) |
42 | 40, 41 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) /
2)) |
43 | 42 | eleq1d 2239 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) / 2) − 1) ∈
ℕ ↔ ((𝑁 −
1) / 2) ∈ ℕ)) |
44 | 43 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔
((𝑁 − 1) / 2) ∈
ℕ)) |
45 | 44 | adantr 274 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔
((𝑁 − 1) / 2) ∈
ℕ)) |
46 | 39, 45 | mpbid 146 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → ((𝑁 − 1) / 2) ∈
ℕ) |
47 | 46 | a1d 22 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) ∧ 2 < 𝑁) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈
ℕ)) |
48 | 47 | expcom 115 |
. . . . . 6
⊢ (2 <
𝑁 → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈
ℕ))) |
49 | 6, 48 | jaoi 711 |
. . . . 5
⊢ ((𝑁 = 1 ∨ 2 < 𝑁) → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ0)
→ (𝑁 ≠ 1 →
((𝑁 − 1) / 2) ∈
ℕ))) |
50 | 4, 49 | mpcom 36 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈
ℕ)) |
51 | 50 | impancom 258 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → (((𝑁 + 1) / 2) ∈
ℕ0 → ((𝑁 − 1) / 2) ∈
ℕ)) |
52 | 1, 51 | sylbi 120 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (((𝑁 + 1) / 2) ∈ ℕ0 →
((𝑁 − 1) / 2) ∈
ℕ)) |
53 | 52 | imp 123 |
1
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ0)
→ ((𝑁 − 1) / 2)
∈ ℕ) |