Proof of Theorem elnnz
Step | Hyp | Ref
| Expression |
1 | | nnre 10904 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
2 | | orc 399 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) |
3 | | nngt0 10926 |
. . . 4
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
4 | 1, 2, 3 | jca31 555 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁)) |
5 | | idd 24 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → (𝑁 ∈ ℕ → 𝑁 ∈
ℕ)) |
6 | | lt0neg2 10414 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → (0 <
𝑁 ↔ -𝑁 < 0)) |
7 | | renegcl 10223 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ → -𝑁 ∈
ℝ) |
8 | | 0re 9919 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
9 | | ltnsym 10014 |
. . . . . . . . . . . . 13
⊢ ((-𝑁 ∈ ℝ ∧ 0 ∈
ℝ) → (-𝑁 < 0
→ ¬ 0 < -𝑁)) |
10 | 7, 8, 9 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → (-𝑁 < 0 → ¬ 0 <
-𝑁)) |
11 | 6, 10 | sylbid 229 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → (0 <
𝑁 → ¬ 0 <
-𝑁)) |
12 | 11 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → ¬ 0 <
-𝑁) |
13 | | nngt0 10926 |
. . . . . . . . . 10
⊢ (-𝑁 ∈ ℕ → 0 <
-𝑁) |
14 | 12, 13 | nsyl 134 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → ¬ -𝑁 ∈
ℕ) |
15 | | gt0ne0 10372 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → 𝑁 ≠ 0) |
16 | 15 | neneqd 2787 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → ¬ 𝑁 = 0) |
17 | | ioran 510 |
. . . . . . . . 9
⊢ (¬
(-𝑁 ∈ ℕ ∨
𝑁 = 0) ↔ (¬ -𝑁 ∈ ℕ ∧ ¬
𝑁 = 0)) |
18 | 14, 16, 17 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → ¬ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
19 | 18 | pm2.21d 117 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → ((-𝑁 ∈ ℕ ∨ 𝑁 = 0) → 𝑁 ∈ ℕ)) |
20 | 5, 19 | jaod 394 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 0 <
𝑁) → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ)) |
21 | 20 | ex 449 |
. . . . 5
⊢ (𝑁 ∈ ℝ → (0 <
𝑁 → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ))) |
22 | 21 | com23 84 |
. . . 4
⊢ (𝑁 ∈ ℝ → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (0 < 𝑁 → 𝑁 ∈ ℕ))) |
23 | 22 | imp31 447 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁) → 𝑁 ∈ ℕ) |
24 | 4, 23 | impbii 198 |
. 2
⊢ (𝑁 ∈ ℕ ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁)) |
25 | | elz 11256 |
. . . 4
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))) |
26 | | 3orrot 1037 |
. . . . . 6
⊢ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
27 | | 3orass 1034 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) |
28 | 26, 27 | bitri 263 |
. . . . 5
⊢ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) |
29 | 28 | anbi2i 726 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)) ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))) |
30 | 25, 29 | bitri 263 |
. . 3
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))) |
31 | 30 | anbi1i 727 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 0 <
𝑁) ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁)) |
32 | 24, 31 | bitr4i 266 |
1
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) |