Description: Lemma for rmydioph . Used with sselii to infer membership of midpoints of range; jm2.27dlem2 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | jm2.27dlem5.2 | ⊢ 𝐵 = ( 𝐴 + 1 ) | |
| jm2.27dlem5.3 | ⊢ ( 1 ... 𝐵 ) ⊆ ( 1 ... 𝐶 ) | ||
| Assertion | jm2.27dlem5 | ⊢ ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jm2.27dlem5.2 | ⊢ 𝐵 = ( 𝐴 + 1 ) | |
| 2 | jm2.27dlem5.3 | ⊢ ( 1 ... 𝐵 ) ⊆ ( 1 ... 𝐶 ) | |
| 3 | fzssp1 | ⊢ ( 1 ... 𝐴 ) ⊆ ( 1 ... ( 𝐴 + 1 ) ) | |
| 4 | 1 | oveq2i | ⊢ ( 1 ... 𝐵 ) = ( 1 ... ( 𝐴 + 1 ) ) |
| 5 | 3 4 | sseqtrri | ⊢ ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝐵 ) |
| 6 | 5 2 | sstri | ⊢ ( 1 ... 𝐴 ) ⊆ ( 1 ... 𝐶 ) |