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 ) ) )