Proof of Theorem elfz0ubfz0
Step | Hyp | Ref
| Expression |
1 | | elfz2nn0 10021 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁)) |
2 | | elfz2 9926 |
. . . . . 6
⊢ (𝐿 ∈ (𝐾...𝑁) ↔ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))) |
3 | | simpr1 988 |
. . . . . . . 8
⊢ ((((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) ∧ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁)) → 𝐾 ∈
ℕ0) |
4 | | elnn0z 9186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℤ
∧ 0 ≤ 𝐾)) |
5 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐿 ∈
ℤ) |
6 | | 0z 9184 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℤ |
7 | | zletr 9222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℤ ∧ 𝐾
∈ ℤ ∧ 𝐿
∈ ℤ) → ((0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿) → 0 ≤ 𝐿)) |
8 | 6, 7 | mp3an1 1306 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤
𝐾 ∧ 𝐾 ≤ 𝐿) → 0 ≤ 𝐿)) |
9 | | elnn0z 9186 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐿 ∈ ℕ0
↔ (𝐿 ∈ ℤ
∧ 0 ≤ 𝐿)) |
10 | 9 | simplbi2 383 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ∈ ℤ → (0 ≤
𝐿 → 𝐿 ∈
ℕ0)) |
11 | 5, 8, 10 | sylsyld 58 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤
𝐾 ∧ 𝐾 ≤ 𝐿) → 𝐿 ∈
ℕ0)) |
12 | 11 | expd 256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝐾 → (𝐾 ≤ 𝐿 → 𝐿 ∈
ℕ0))) |
13 | 12 | impancom 258 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) → (𝐿 ∈ ℤ → (𝐾 ≤ 𝐿 → 𝐿 ∈
ℕ0))) |
14 | 4, 13 | sylbi 120 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
→ (𝐿 ∈ ℤ
→ (𝐾 ≤ 𝐿 → 𝐿 ∈
ℕ0))) |
15 | 14 | com13 80 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ≤ 𝐿 → (𝐿 ∈ ℤ → (𝐾 ∈ ℕ0 → 𝐿 ∈
ℕ0))) |
16 | 15 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁) → (𝐿 ∈ ℤ → (𝐾 ∈ ℕ0 → 𝐿 ∈
ℕ0))) |
17 | 16 | com12 30 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ ℤ → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁) → (𝐾 ∈ ℕ0 → 𝐿 ∈
ℕ0))) |
18 | 17 | 3ad2ant3 1005 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁) → (𝐾 ∈ ℕ0 → 𝐿 ∈
ℕ0))) |
19 | 18 | imp 123 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) → (𝐾 ∈ ℕ0 → 𝐿 ∈
ℕ0)) |
20 | 19 | com12 30 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (((𝐾 ∈ ℤ
∧ 𝑁 ∈ ℤ
∧ 𝐿 ∈ ℤ)
∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) → 𝐿 ∈
ℕ0)) |
21 | 20 | 3ad2ant1 1003 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝐾
≤ 𝑁) → (((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) → 𝐿 ∈
ℕ0)) |
22 | 21 | impcom 124 |
. . . . . . . 8
⊢ ((((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) ∧ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁)) → 𝐿 ∈
ℕ0) |
23 | | simplrl 525 |
. . . . . . . 8
⊢ ((((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) ∧ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁)) → 𝐾 ≤ 𝐿) |
24 | 3, 22, 23 | 3jca 1162 |
. . . . . . 7
⊢ ((((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) ∧ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁)) → (𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐾 ≤ 𝐿)) |
25 | 24 | ex 114 |
. . . . . 6
⊢ (((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) → ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁) → (𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐾 ≤ 𝐿))) |
26 | 2, 25 | sylbi 120 |
. . . . 5
⊢ (𝐿 ∈ (𝐾...𝑁) → ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁) → (𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐾 ≤ 𝐿))) |
27 | 26 | com12 30 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝐾
≤ 𝑁) → (𝐿 ∈ (𝐾...𝑁) → (𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐾 ≤ 𝐿))) |
28 | 1, 27 | sylbi 120 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (𝐿 ∈ (𝐾...𝑁) → (𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐾 ≤ 𝐿))) |
29 | 28 | imp 123 |
. 2
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → (𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐾 ≤ 𝐿)) |
30 | | elfz2nn0 10021 |
. 2
⊢ (𝐾 ∈ (0...𝐿) ↔ (𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐾 ≤ 𝐿)) |
31 | 29, 30 | sylibr 133 |
1
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐾 ∈ (0...𝐿)) |