Proof of Theorem fz0fzelfz0
Step | Hyp | Ref
| Expression |
1 | | elfz2nn0 10068 |
. . . 4
⊢ (𝑁 ∈ (0...𝑅) ↔ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) |
2 | | elfz2 9972 |
. . . . . 6
⊢ (𝑀 ∈ (𝑁...𝑅) ↔ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅))) |
3 | | simplr 525 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → 𝑀 ∈ ℤ) |
4 | | 0red 7921 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ 0 ∈ ℝ) |
5 | | nn0re 9144 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
6 | 5 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ 𝑁 ∈
ℝ) |
7 | | zre 9216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
8 | 7 | adantl 275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ 𝑀 ∈
ℝ) |
9 | 4, 6, 8 | 3jca 1172 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ (0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ)) |
10 | 9 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → (0 ∈ ℝ ∧
𝑁 ∈ ℝ ∧
𝑀 ∈
ℝ)) |
11 | | nn0ge0 9160 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
12 | 11 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ 0 ≤ 𝑁) |
13 | 12 | anim1i 338 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → (0 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)) |
14 | | letr 8002 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ ∧ 𝑀
∈ ℝ) → ((0 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 0 ≤ 𝑀)) |
15 | 10, 13, 14 | sylc 62 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → 0 ≤ 𝑀) |
16 | | elnn0z 9225 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℤ
∧ 0 ≤ 𝑀)) |
17 | 3, 15, 16 | sylanbrc 415 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → 𝑀 ∈
ℕ0) |
18 | 17 | exp31 362 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑀 ∈ ℤ
→ (𝑁 ≤ 𝑀 → 𝑀 ∈
ℕ0))) |
19 | 18 | com23 78 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ≤ 𝑀 → (𝑀 ∈ ℤ → 𝑀 ∈
ℕ0))) |
20 | 19 | 3ad2ant1 1013 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈
ℕ0 ∧ 𝑁
≤ 𝑅) → (𝑁 ≤ 𝑀 → (𝑀 ∈ ℤ → 𝑀 ∈
ℕ0))) |
21 | 20 | com13 80 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑁 ≤ 𝑀 → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → 𝑀 ∈
ℕ0))) |
22 | 21 | adantrd 277 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → ((𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → 𝑀 ∈
ℕ0))) |
23 | 22 | 3ad2ant3 1015 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → 𝑀 ∈
ℕ0))) |
24 | 23 | imp 123 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → 𝑀 ∈
ℕ0)) |
25 | 24 | imp 123 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) → 𝑀 ∈
ℕ0) |
26 | | simpr2 999 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) → 𝑅 ∈
ℕ0) |
27 | | simplrr 531 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) → 𝑀 ≤ 𝑅) |
28 | 25, 26, 27 | 3jca 1172 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅)) |
29 | 28 | ex 114 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅))) |
30 | 2, 29 | sylbi 120 |
. . . . 5
⊢ (𝑀 ∈ (𝑁...𝑅) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅))) |
31 | 30 | com12 30 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈
ℕ0 ∧ 𝑁
≤ 𝑅) → (𝑀 ∈ (𝑁...𝑅) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅))) |
32 | 1, 31 | sylbi 120 |
. . 3
⊢ (𝑁 ∈ (0...𝑅) → (𝑀 ∈ (𝑁...𝑅) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅))) |
33 | 32 | imp 123 |
. 2
⊢ ((𝑁 ∈ (0...𝑅) ∧ 𝑀 ∈ (𝑁...𝑅)) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅)) |
34 | | elfz2nn0 10068 |
. 2
⊢ (𝑀 ∈ (0...𝑅) ↔ (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅)) |
35 | 33, 34 | sylibr 133 |
1
⊢ ((𝑁 ∈ (0...𝑅) ∧ 𝑀 ∈ (𝑁...𝑅)) → 𝑀 ∈ (0...𝑅)) |