Metamath Proof Explorer


Theorem ssfzunsn

Description: A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 8-Jun-2021) (Proof shortened by AV, 13-Nov-2021)

Ref Expression
Assertion ssfzunsn
|- ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> ( S u. { I } ) C_ ( M ... if ( I <_ N , N , I ) ) )

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> S C_ ( M ... N ) )
2 eluzel2
 |-  ( I e. ( ZZ>= ` M ) -> M e. ZZ )
3 2 3ad2ant3
 |-  ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> M e. ZZ )
4 simp2
 |-  ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> N e. ZZ )
5 eluzelz
 |-  ( I e. ( ZZ>= ` M ) -> I e. ZZ )
6 5 3ad2ant3
 |-  ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> I e. ZZ )
7 ssfzunsnext
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( S u. { I } ) C_ ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
8 1 3 4 6 7 syl13anc
 |-  ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> ( S u. { I } ) C_ ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
9 eluz2
 |-  ( I e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ I e. ZZ /\ M <_ I ) )
10 zre
 |-  ( I e. ZZ -> I e. RR )
11 10 rexrd
 |-  ( I e. ZZ -> I e. RR* )
12 11 3ad2ant2
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> I e. RR* )
13 zre
 |-  ( M e. ZZ -> M e. RR )
14 13 rexrd
 |-  ( M e. ZZ -> M e. RR* )
15 14 3ad2ant1
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> M e. RR* )
16 simp3
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> M <_ I )
17 xrmineq
 |-  ( ( I e. RR* /\ M e. RR* /\ M <_ I ) -> if ( I <_ M , I , M ) = M )
18 12 15 16 17 syl3anc
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> if ( I <_ M , I , M ) = M )
19 18 eqcomd
 |-  ( ( M e. ZZ /\ I e. ZZ /\ M <_ I ) -> M = if ( I <_ M , I , M ) )
20 9 19 sylbi
 |-  ( I e. ( ZZ>= ` M ) -> M = if ( I <_ M , I , M ) )
21 20 3ad2ant3
 |-  ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> M = if ( I <_ M , I , M ) )
22 21 oveq1d
 |-  ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> ( M ... if ( I <_ N , N , I ) ) = ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
23 8 22 sseqtrrd
 |-  ( ( S C_ ( M ... N ) /\ N e. ZZ /\ I e. ( ZZ>= ` M ) ) -> ( S u. { I } ) C_ ( M ... if ( I <_ N , N , I ) ) )