Proof of Theorem elnnzs
| Step | Hyp | Ref
| Expression |
| 1 | | nnsno 28329 |
. . . 4
⊢ (𝑁 ∈ ℕs
→ 𝑁 ∈ No ) |
| 2 | | orc 868 |
. . . 4
⊢ (𝑁 ∈ ℕs
→ (𝑁 ∈
ℕs ∨ (( -us ‘𝑁) ∈ ℕs ∨ 𝑁 = 0s
))) |
| 3 | | nnsgt0 28342 |
. . . 4
⊢ (𝑁 ∈ ℕs
→ 0s <s 𝑁) |
| 4 | 1, 2, 3 | jca31 514 |
. . 3
⊢ (𝑁 ∈ ℕs
→ ((𝑁 ∈ No ∧ (𝑁 ∈ ℕs ∨ ((
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s ))) ∧ 0s
<s 𝑁)) |
| 5 | | idd 24 |
. . . . . . 7
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → (𝑁 ∈ ℕs → 𝑁 ∈
ℕs)) |
| 6 | | negscl 28068 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
No → ( -us ‘𝑁) ∈ No
) |
| 7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → ( -us ‘𝑁) ∈
No ) |
| 8 | | 0sno 27871 |
. . . . . . . . . . . . . 14
⊢
0s ∈ No |
| 9 | | sltneg 28077 |
. . . . . . . . . . . . . 14
⊢ ((
0s ∈ No ∧ 𝑁 ∈ No )
→ ( 0s <s 𝑁 ↔ ( -us ‘𝑁) <s ( -us ‘
0s ))) |
| 10 | 8, 9 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
No → ( 0s <s 𝑁 ↔ ( -us ‘𝑁) <s ( -us ‘
0s ))) |
| 11 | | negs0s 28058 |
. . . . . . . . . . . . . 14
⊢ (
-us ‘ 0s ) = 0s |
| 12 | 11 | breq2i 5151 |
. . . . . . . . . . . . 13
⊢ ((
-us ‘𝑁)
<s ( -us ‘ 0s ) ↔ ( -us
‘𝑁) <s
0s ) |
| 13 | 10, 12 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
No → ( 0s <s 𝑁 ↔ ( -us ‘𝑁) <s 0s
)) |
| 14 | 13 | biimpa 476 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → ( -us ‘𝑁) <s 0s
) |
| 15 | | sltasym 27793 |
. . . . . . . . . . . 12
⊢ (((
-us ‘𝑁)
∈ No ∧ 0s ∈ No ) → (( -us ‘𝑁) <s 0s → ¬
0s <s ( -us ‘𝑁))) |
| 16 | 8, 15 | mpan2 691 |
. . . . . . . . . . 11
⊢ ((
-us ‘𝑁)
∈ No → (( -us ‘𝑁) <s 0s →
¬ 0s <s ( -us ‘𝑁))) |
| 17 | 7, 14, 16 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → ¬ 0s <s (
-us ‘𝑁)) |
| 18 | | nnsgt0 28342 |
. . . . . . . . . 10
⊢ ((
-us ‘𝑁)
∈ ℕs → 0s <s ( -us
‘𝑁)) |
| 19 | 17, 18 | nsyl 140 |
. . . . . . . . 9
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → ¬ ( -us ‘𝑁) ∈
ℕs) |
| 20 | | sgt0ne0 27879 |
. . . . . . . . . . 11
⊢ (
0s <s 𝑁
→ 𝑁 ≠ 0s
) |
| 21 | 20 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → 𝑁 ≠ 0s ) |
| 22 | 21 | neneqd 2945 |
. . . . . . . . 9
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → ¬ 𝑁 = 0s ) |
| 23 | | ioran 986 |
. . . . . . . . 9
⊢ (¬ ((
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s ) ↔ (¬ (
-us ‘𝑁)
∈ ℕs ∧ ¬ 𝑁 = 0s )) |
| 24 | 19, 22, 23 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → ¬ (( -us
‘𝑁) ∈
ℕs ∨ 𝑁
= 0s )) |
| 25 | 24 | pm2.21d 121 |
. . . . . . 7
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → ((( -us ‘𝑁) ∈ ℕs
∨ 𝑁 = 0s )
→ 𝑁 ∈
ℕs)) |
| 26 | 5, 25 | jaod 860 |
. . . . . 6
⊢ ((𝑁 ∈
No ∧ 0s <s 𝑁) → ((𝑁 ∈ ℕs ∨ ((
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s )) → 𝑁 ∈
ℕs)) |
| 27 | 26 | ex 412 |
. . . . 5
⊢ (𝑁 ∈
No → ( 0s <s 𝑁 → ((𝑁 ∈ ℕs ∨ ((
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s )) → 𝑁 ∈
ℕs))) |
| 28 | 27 | com23 86 |
. . . 4
⊢ (𝑁 ∈
No → ((𝑁
∈ ℕs ∨ (( -us ‘𝑁) ∈ ℕs ∨ 𝑁 = 0s )) → (
0s <s 𝑁
→ 𝑁 ∈
ℕs))) |
| 29 | 28 | imp31 417 |
. . 3
⊢ (((𝑁 ∈
No ∧ (𝑁 ∈
ℕs ∨ (( -us ‘𝑁) ∈ ℕs ∨ 𝑁 = 0s ))) ∧
0s <s 𝑁)
→ 𝑁 ∈
ℕs) |
| 30 | 4, 29 | impbii 209 |
. 2
⊢ (𝑁 ∈ ℕs
↔ ((𝑁 ∈ No ∧ (𝑁 ∈ ℕs ∨ ((
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s ))) ∧ 0s
<s 𝑁)) |
| 31 | | elzs2 28385 |
. . . 4
⊢ (𝑁 ∈ ℤs
↔ (𝑁 ∈ No ∧ (𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ (
-us ‘𝑁)
∈ ℕs))) |
| 32 | | 3orcomb 1094 |
. . . . . 6
⊢ ((𝑁 ∈ ℕs ∨
𝑁 = 0s ∨ (
-us ‘𝑁)
∈ ℕs) ↔ (𝑁 ∈ ℕs ∨ (
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s )) |
| 33 | | 3orass 1090 |
. . . . . 6
⊢ ((𝑁 ∈ ℕs ∨
( -us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s ) ↔ (𝑁 ∈ ℕs ∨ ((
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s ))) |
| 34 | 32, 33 | bitri 275 |
. . . . 5
⊢ ((𝑁 ∈ ℕs ∨
𝑁 = 0s ∨ (
-us ‘𝑁)
∈ ℕs) ↔ (𝑁 ∈ ℕs ∨ ((
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s ))) |
| 35 | 34 | anbi2i 623 |
. . . 4
⊢ ((𝑁 ∈
No ∧ (𝑁 ∈
ℕs ∨ 𝑁
= 0s ∨ ( -us ‘𝑁) ∈ ℕs)) ↔ (𝑁 ∈
No ∧ (𝑁 ∈
ℕs ∨ (( -us ‘𝑁) ∈ ℕs ∨ 𝑁 = 0s
)))) |
| 36 | 31, 35 | bitri 275 |
. . 3
⊢ (𝑁 ∈ ℤs
↔ (𝑁 ∈ No ∧ (𝑁 ∈ ℕs ∨ ((
-us ‘𝑁)
∈ ℕs ∨ 𝑁 = 0s )))) |
| 37 | 36 | anbi1i 624 |
. 2
⊢ ((𝑁 ∈ ℤs
∧ 0s <s 𝑁) ↔ ((𝑁 ∈ No
∧ (𝑁 ∈
ℕs ∨ (( -us ‘𝑁) ∈ ℕs ∨ 𝑁 = 0s ))) ∧
0s <s 𝑁)) |
| 38 | 30, 37 | bitr4i 278 |
1
⊢ (𝑁 ∈ ℕs
↔ (𝑁 ∈
ℤs ∧ 0s <s 𝑁)) |