Theorem jm2.27dlem5

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	$$⊢\left(1\dots B\right)\subseteq \left(1\dots C\right)$$
Assertion	jm2.27dlem5	$$⊢\left(1\dots A\right)\subseteq \left(1\dots C\right)$$

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem5.2	$$⊢B=A+1$$
2		jm2.27dlem5.3	$$⊢\left(1\dots B\right)\subseteq \left(1\dots C\right)$$
3		fzssp1	$$⊢\left(1\dots A\right)\subseteq \left(1\dots A+1\right)$$
4	1	oveq2i	$$⊢\left(1\dots B\right)=\left(1\dots A+1\right)$$
5	3 4	sseqtrri	$$⊢\left(1\dots A\right)\subseteq \left(1\dots B\right)$$
6	5 2	sstri	$$⊢\left(1\dots A\right)\subseteq \left(1\dots C\right)$$