Proof of Theorem elfz2
Step | Hyp | Ref
| Expression |
1 | | anass 462 |
. 2
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))) |
2 | | df-3an 1113 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈
ℤ)) |
3 | 2 | anbi1i 617 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
4 | | elfz1 12624 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
5 | | 3anass 1120 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) ↔ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
6 | | ibar 524 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
7 | 5, 6 | syl5bb 275 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
8 | 4, 7 | bitrd 271 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
9 | | fzf 12623 |
. . . . . . 7
⊢
...:(ℤ × ℤ)⟶𝒫 ℤ |
10 | 9 | fdmi 6288 |
. . . . . 6
⊢ dom ... =
(ℤ × ℤ) |
11 | 10 | ndmov 7078 |
. . . . 5
⊢ (¬
(𝑀 ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝑀...𝑁) = ∅) |
12 | 11 | eleq2d 2892 |
. . . 4
⊢ (¬
(𝑀 ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ∈ ∅)) |
13 | | noel 4148 |
. . . . . 6
⊢ ¬
𝐾 ∈
∅ |
14 | 13 | pm2.21i 117 |
. . . . 5
⊢ (𝐾 ∈ ∅ → (𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
15 | | simpl 476 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
16 | 14, 15 | pm5.21ni 369 |
. . . 4
⊢ (¬
(𝑀 ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝐾 ∈ ∅ ↔
((𝑀 ∈ ℤ ∧
𝑁 ∈ ℤ) ∧
(𝐾 ∈ ℤ ∧
(𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
17 | 12, 16 | bitrd 271 |
. . 3
⊢ (¬
(𝑀 ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
18 | 8, 17 | pm2.61i 177 |
. 2
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))) |
19 | 1, 3, 18 | 3bitr4ri 296 |
1
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |