Proof of Theorem nn0sub
| Step | Hyp | Ref
| Expression |
| 1 | | nn0re 12535 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
| 2 | | nn0re 12535 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 3 | | leloe 11347 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 ≤ 𝑁 ↔ (𝑀 < 𝑁 ∨ 𝑀 = 𝑁))) |
| 4 | 1, 2, 3 | syl2an 596 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝑀 < 𝑁 ∨ 𝑀 = 𝑁))) |
| 5 | | elnn0 12528 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
| 6 | | elnn0 12528 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
| 7 | | nnsub 12310 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
| 8 | 7 | ex 412 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))) |
| 9 | | nngt0 12297 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 10 | | nncn 12274 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 11 | 10 | subid1d 11609 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 0) = 𝑁) |
| 12 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
| 13 | 11, 12 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 0) ∈
ℕ) |
| 14 | 9, 13 | 2thd 265 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (0 <
𝑁 ↔ (𝑁 − 0) ∈
ℕ)) |
| 15 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑀 = 0 → (𝑀 < 𝑁 ↔ 0 < 𝑁)) |
| 16 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (𝑁 − 𝑀) = (𝑁 − 0)) |
| 17 | 16 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑀 = 0 → ((𝑁 − 𝑀) ∈ ℕ ↔ (𝑁 − 0) ∈
ℕ)) |
| 18 | 15, 17 | bibi12d 345 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → ((𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ) ↔ (0 < 𝑁 ↔ (𝑁 − 0) ∈
ℕ))) |
| 19 | 14, 18 | imbitrrid 246 |
. . . . . . . . 9
⊢ (𝑀 = 0 → (𝑁 ∈ ℕ → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))) |
| 20 | 8, 19 | jaoi 858 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → (𝑁 ∈ ℕ → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))) |
| 21 | 6, 20 | sylbi 217 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑁 ∈ ℕ
→ (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))) |
| 22 | | nn0nlt0 12552 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ ¬ 𝑀 <
0) |
| 23 | 22 | pm2.21d 121 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (𝑀 < 0 → (0
− 𝑀) ∈
ℕ)) |
| 24 | | nngt0 12297 |
. . . . . . . . . 10
⊢ ((0
− 𝑀) ∈ ℕ
→ 0 < (0 − 𝑀)) |
| 25 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 26 | | posdif 11756 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑀 < 0
↔ 0 < (0 − 𝑀))) |
| 27 | 1, 25, 26 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (𝑀 < 0 ↔ 0
< (0 − 𝑀))) |
| 28 | 24, 27 | imbitrrid 246 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ ((0 − 𝑀)
∈ ℕ → 𝑀
< 0)) |
| 29 | 23, 28 | impbid 212 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (𝑀 < 0 ↔ (0
− 𝑀) ∈
ℕ)) |
| 30 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (𝑀 < 𝑁 ↔ 𝑀 < 0)) |
| 31 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → (𝑁 − 𝑀) = (0 − 𝑀)) |
| 32 | 31 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑁 = 0 → ((𝑁 − 𝑀) ∈ ℕ ↔ (0 − 𝑀) ∈
ℕ)) |
| 33 | 30, 32 | bibi12d 345 |
. . . . . . . 8
⊢ (𝑁 = 0 → ((𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ) ↔ (𝑀 < 0 ↔ (0 − 𝑀) ∈ ℕ))) |
| 34 | 29, 33 | syl5ibrcom 247 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑁 = 0 → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))) |
| 35 | 21, 34 | jaod 860 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ ((𝑁 ∈ ℕ
∨ 𝑁 = 0) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))) |
| 36 | 5, 35 | biimtrid 242 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (𝑁 ∈
ℕ0 → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))) |
| 37 | 36 | imp 406 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
| 38 | | nn0cn 12536 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 39 | | nn0cn 12536 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
| 40 | | subeq0 11535 |
. . . . . 6
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑁 − 𝑀) = 0 ↔ 𝑁 = 𝑀)) |
| 41 | 38, 39, 40 | syl2anr 597 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 − 𝑀) = 0 ↔ 𝑁 = 𝑀)) |
| 42 | | eqcom 2744 |
. . . . 5
⊢ (𝑁 = 𝑀 ↔ 𝑀 = 𝑁) |
| 43 | 41, 42 | bitr2di 288 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 = 𝑁 ↔ (𝑁 − 𝑀) = 0)) |
| 44 | 37, 43 | orbi12d 919 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 < 𝑁 ∨ 𝑀 = 𝑁) ↔ ((𝑁 − 𝑀) ∈ ℕ ∨ (𝑁 − 𝑀) = 0))) |
| 45 | 4, 44 | bitrd 279 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ≤ 𝑁 ↔ ((𝑁 − 𝑀) ∈ ℕ ∨ (𝑁 − 𝑀) = 0))) |
| 46 | | elnn0 12528 |
. 2
⊢ ((𝑁 − 𝑀) ∈ ℕ0 ↔ ((𝑁 − 𝑀) ∈ ℕ ∨ (𝑁 − 𝑀) = 0)) |
| 47 | 45, 46 | bitr4di 289 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈
ℕ0)) |