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 | |- B = ( A + 1 ) |
|
| jm2.27dlem5.3 | |- ( 1 ... B ) C_ ( 1 ... C ) |
||
| Assertion | jm2.27dlem5 | |- ( 1 ... A ) C_ ( 1 ... C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jm2.27dlem5.2 | |- B = ( A + 1 ) |
|
| 2 | jm2.27dlem5.3 | |- ( 1 ... B ) C_ ( 1 ... C ) |
|
| 3 | fzssp1 | |- ( 1 ... A ) C_ ( 1 ... ( A + 1 ) ) |
|
| 4 | 1 | oveq2i | |- ( 1 ... B ) = ( 1 ... ( A + 1 ) ) |
| 5 | 3 4 | sseqtrri | |- ( 1 ... A ) C_ ( 1 ... B ) |
| 6 | 5 2 | sstri | |- ( 1 ... A ) C_ ( 1 ... C ) |