Metamath Proof Explorer

Theorem ssfzunsnext

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, 13-Nov-2021)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> S C_ ( M ... N ) )
2 simp3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> I e. ZZ )
3 simp1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> M e. ZZ )
4 2 3 ifcld 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> if ( I <_ M , I , M ) e. ZZ )
5 4 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ M , I , M ) e. ZZ )
6 simp2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> N e. ZZ )
7 6 2 ifcld 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> if ( I <_ N , N , I ) e. ZZ )
8 7 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ N , N , I ) e. ZZ )
9 elfzelz 
 |-  ( k e. ( M ... N ) -> k e. ZZ )
10 9 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k e. ZZ )
11 4 zred 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> if ( I <_ M , I , M ) e. RR )
12 11 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ M , I , M ) e. RR )
13 zre 
 |-  ( M e. ZZ -> M e. RR )
14 13 3ad2ant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> M e. RR )
15 14 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> M e. RR )
16 9 zred 
 |-  ( k e. ( M ... N ) -> k e. RR )
17 16 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k e. RR )
18 zre 
 |-  ( I e. ZZ -> I e. RR )
19 13 18 anim12i 
 |-  ( ( M e. ZZ /\ I e. ZZ ) -> ( M e. RR /\ I e. RR ) )
20 19 ancomd 
 |-  ( ( M e. ZZ /\ I e. ZZ ) -> ( I e. RR /\ M e. RR ) )
21 20 3adant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( I e. RR /\ M e. RR ) )
22 21 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> ( I e. RR /\ M e. RR ) )
23 min2 
 |-  ( ( I e. RR /\ M e. RR ) -> if ( I <_ M , I , M ) <_ M )
24 22 23 syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ M , I , M ) <_ M )
25 elfzle1 
 |-  ( k e. ( M ... N ) -> M <_ k )
26 25 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> M <_ k )
27 12 15 17 24 26 letrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ M , I , M ) <_ k )
28 zre 
 |-  ( N e. ZZ -> N e. RR )
29 28 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> N e. RR )
30 29 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> N e. RR )
31 7 zred 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> if ( I <_ N , N , I ) e. RR )
32 31 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ N , N , I ) e. RR )
33 elfzle2 
 |-  ( k e. ( M ... N ) -> k <_ N )
34 33 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k <_ N )
35 28 18 anim12i 
 |-  ( ( N e. ZZ /\ I e. ZZ ) -> ( N e. RR /\ I e. RR ) )
36 35 3adant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( N e. RR /\ I e. RR ) )
37 36 ancomd 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( I e. RR /\ N e. RR ) )
38 max2 
 |-  ( ( I e. RR /\ N e. RR ) -> N <_ if ( I <_ N , N , I ) )
39 37 38 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> N <_ if ( I <_ N , N , I ) )
40 39 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> N <_ if ( I <_ N , N , I ) )
41 17 30 32 34 40 letrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k <_ if ( I <_ N , N , I ) )
42 5 8 10 27 41 elfzd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k e. ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
43 42 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( k e. ( M ... N ) -> k e. ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) ) )
44 43 ssrdv 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( M ... N ) C_ ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
45 44 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( M ... N ) C_ ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
46 1 45 sstrd 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> S C_ ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
47 4 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> if ( I <_ M , I , M ) e. ZZ )
48 7 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> if ( I <_ N , N , I ) e. ZZ )
49 2 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> I e. ZZ )
50 19 3adant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( M e. RR /\ I e. RR ) )
51 50 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( M e. RR /\ I e. RR ) )
52 51 ancomd 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( I e. RR /\ M e. RR ) )
53 min1 
 |-  ( ( I e. RR /\ M e. RR ) -> if ( I <_ M , I , M ) <_ I )
54 52 53 syl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> if ( I <_ M , I , M ) <_ I )
55 36 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( N e. RR /\ I e. RR ) )
56 55 ancomd 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( I e. RR /\ N e. RR ) )
57 max1 
 |-  ( ( I e. RR /\ N e. RR ) -> I <_ if ( I <_ N , N , I ) )
58 56 57 syl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> I <_ if ( I <_ N , N , I ) )
59 47 48 49 54 58 elfzd 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> I e. ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
60 59 snssd 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> { I } C_ ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
61 46 60 unssd 
 |-  ( ( 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 ) ) )