This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzoss1

Description: Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzoss1 ⊢ K ∈ ℤ ≥ M → K ..^ N ⊆ M ..^ N

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ K ..^ N = ∅ → K ..^ N ⊆ M ..^ N ↔ ∅ ⊆ M ..^ N
2 fzon0 ⊢ K ..^ N ≠ ∅ ↔ K ∈ K ..^ N
3 elfzoel2 ⊢ K ∈ K ..^ N → N ∈ ℤ
4 2 3 sylbi ⊢ K ..^ N ≠ ∅ → N ∈ ℤ
5 fzss1 ⊢ K ∈ ℤ ≥ M → K … N − 1 ⊆ M … N − 1
6 5 adantr ⊢ K ∈ ℤ ≥ M ∧ N ∈ ℤ → K … N − 1 ⊆ M … N − 1
7 fzoval ⊢ N ∈ ℤ → K ..^ N = K … N − 1
8 7 adantl ⊢ K ∈ ℤ ≥ M ∧ N ∈ ℤ → K ..^ N = K … N − 1
9 fzoval ⊢ N ∈ ℤ → M ..^ N = M … N − 1
10 9 adantl ⊢ K ∈ ℤ ≥ M ∧ N ∈ ℤ → M ..^ N = M … N − 1
11 6 8 10 3sstr4d ⊢ K ∈ ℤ ≥ M ∧ N ∈ ℤ → K ..^ N ⊆ M ..^ N
12 4 11 sylan2 ⊢ K ∈ ℤ ≥ M ∧ K ..^ N ≠ ∅ → K ..^ N ⊆ M ..^ N
13 0ss ⊢ ∅ ⊆ M ..^ N
14 13 a1i ⊢ K ∈ ℤ ≥ M → ∅ ⊆ M ..^ N
15 1 12 14 pm2.61ne ⊢ K ∈ ℤ ≥ M → K ..^ N ⊆ M ..^ N