Proof of Theorem elincfzoext
| Step | Hyp | Ref
| Expression |
| 1 | | elfzole1 13707 |
. . . 4
⊢ (𝑍 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑍) |
| 2 | | elfzoelz 13699 |
. . . . . . . . 9
⊢ (𝑍 ∈ (𝑀..^𝑁) → 𝑍 ∈ ℤ) |
| 3 | 2 | zred 12722 |
. . . . . . . 8
⊢ (𝑍 ∈ (𝑀..^𝑁) → 𝑍 ∈ ℝ) |
| 4 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝑀 ≤ 𝑍) → 𝑍 ∈ ℝ) |
| 5 | | nn0addge1 12572 |
. . . . . . 7
⊢ ((𝑍 ∈ ℝ ∧ 𝐼 ∈ ℕ0)
→ 𝑍 ≤ (𝑍 + 𝐼)) |
| 6 | 4, 5 | sylan 580 |
. . . . . 6
⊢ (((𝑍 ∈ (𝑀..^𝑁) ∧ 𝑀 ≤ 𝑍) ∧ 𝐼 ∈ ℕ0) → 𝑍 ≤ (𝑍 + 𝐼)) |
| 7 | | elfzoel1 13697 |
. . . . . . . . . . . 12
⊢ (𝑍 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℤ) |
| 8 | 7 | zred 12722 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℝ) |
| 9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑀 ∈
ℝ) |
| 10 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑍 ∈
ℝ) |
| 11 | | nn0re 12535 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℝ) |
| 12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝐼 ∈
ℝ) |
| 13 | 10, 12 | readdcld 11290 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → (𝑍 + 𝐼) ∈ ℝ) |
| 14 | | letr 11355 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑍 ∈ ℝ ∧ (𝑍 + 𝐼) ∈ ℝ) → ((𝑀 ≤ 𝑍 ∧ 𝑍 ≤ (𝑍 + 𝐼)) → 𝑀 ≤ (𝑍 + 𝐼))) |
| 15 | 9, 10, 13, 14 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → ((𝑀 ≤ 𝑍 ∧ 𝑍 ≤ (𝑍 + 𝐼)) → 𝑀 ≤ (𝑍 + 𝐼))) |
| 16 | 15 | exp4b 430 |
. . . . . . . 8
⊢ (𝑍 ∈ (𝑀..^𝑁) → (𝐼 ∈ ℕ0 → (𝑀 ≤ 𝑍 → (𝑍 ≤ (𝑍 + 𝐼) → 𝑀 ≤ (𝑍 + 𝐼))))) |
| 17 | 16 | com23 86 |
. . . . . . 7
⊢ (𝑍 ∈ (𝑀..^𝑁) → (𝑀 ≤ 𝑍 → (𝐼 ∈ ℕ0 → (𝑍 ≤ (𝑍 + 𝐼) → 𝑀 ≤ (𝑍 + 𝐼))))) |
| 18 | 17 | imp31 417 |
. . . . . 6
⊢ (((𝑍 ∈ (𝑀..^𝑁) ∧ 𝑀 ≤ 𝑍) ∧ 𝐼 ∈ ℕ0) → (𝑍 ≤ (𝑍 + 𝐼) → 𝑀 ≤ (𝑍 + 𝐼))) |
| 19 | 6, 18 | mpd 15 |
. . . . 5
⊢ (((𝑍 ∈ (𝑀..^𝑁) ∧ 𝑀 ≤ 𝑍) ∧ 𝐼 ∈ ℕ0) → 𝑀 ≤ (𝑍 + 𝐼)) |
| 20 | 19 | exp31 419 |
. . . 4
⊢ (𝑍 ∈ (𝑀..^𝑁) → (𝑀 ≤ 𝑍 → (𝐼 ∈ ℕ0 → 𝑀 ≤ (𝑍 + 𝐼)))) |
| 21 | 1, 20 | mpd 15 |
. . 3
⊢ (𝑍 ∈ (𝑀..^𝑁) → (𝐼 ∈ ℕ0 → 𝑀 ≤ (𝑍 + 𝐼))) |
| 22 | 21 | imp 406 |
. 2
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑀 ≤ (𝑍 + 𝐼)) |
| 23 | | elfzoel2 13698 |
. . . . 5
⊢ (𝑍 ∈ (𝑀..^𝑁) → 𝑁 ∈ ℤ) |
| 24 | 23 | zred 12722 |
. . . 4
⊢ (𝑍 ∈ (𝑀..^𝑁) → 𝑁 ∈ ℝ) |
| 25 | 24 | adantr 480 |
. . 3
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑁 ∈
ℝ) |
| 26 | | elfzolt2 13708 |
. . . 4
⊢ (𝑍 ∈ (𝑀..^𝑁) → 𝑍 < 𝑁) |
| 27 | 26 | adantr 480 |
. . 3
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑍 < 𝑁) |
| 28 | 10, 25, 12, 27 | ltadd1dd 11874 |
. 2
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → (𝑍 + 𝐼) < (𝑁 + 𝐼)) |
| 29 | 2 | adantr 480 |
. . . 4
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑍 ∈
ℤ) |
| 30 | | nn0z 12638 |
. . . . 5
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℤ) |
| 31 | 30 | adantl 481 |
. . . 4
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝐼 ∈
ℤ) |
| 32 | 29, 31 | zaddcld 12726 |
. . 3
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → (𝑍 + 𝐼) ∈ ℤ) |
| 33 | 7 | adantr 480 |
. . 3
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑀 ∈
ℤ) |
| 34 | 23 | adantr 480 |
. . . 4
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑁 ∈
ℤ) |
| 35 | 34, 31 | zaddcld 12726 |
. . 3
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → (𝑁 + 𝐼) ∈ ℤ) |
| 36 | | elfzo 13701 |
. . 3
⊢ (((𝑍 + 𝐼) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑁 + 𝐼) ∈ ℤ) → ((𝑍 + 𝐼) ∈ (𝑀..^(𝑁 + 𝐼)) ↔ (𝑀 ≤ (𝑍 + 𝐼) ∧ (𝑍 + 𝐼) < (𝑁 + 𝐼)))) |
| 37 | 32, 33, 35, 36 | syl3anc 1373 |
. 2
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → ((𝑍 + 𝐼) ∈ (𝑀..^(𝑁 + 𝐼)) ↔ (𝑀 ≤ (𝑍 + 𝐼) ∧ (𝑍 + 𝐼) < (𝑁 + 𝐼)))) |
| 38 | 22, 28, 37 | mpbir2and 713 |
1
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → (𝑍 + 𝐼) ∈ (𝑀..^(𝑁 + 𝐼))) |