Proof of Theorem eluz2
| Step | Hyp | Ref
| Expression |
| 1 | | eluzel2 12883 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
| 2 | | simp1 1137 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ) |
| 3 | | eluz1 12882 |
. . . 4
⊢ (𝑀 ∈ ℤ → (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
| 4 | | ibar 528 |
. . . 4
⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))) |
| 5 | 3, 4 | bitrd 279 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))) |
| 6 | | 3anass 1095 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
| 7 | 5, 6 | bitr4di 289 |
. 2
⊢ (𝑀 ∈ ℤ → (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
| 8 | 1, 2, 7 | pm5.21nii 378 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |