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 elfzelz 
 |-  ( k e. ( M ... N ) -> k e. ZZ )
7 6 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k e. ZZ )
8 4 zred 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> if ( I <_ M , I , M ) e. RR )
9 8 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ M , I , M ) e. RR )
10 zre 
 |-  ( M e. ZZ -> M e. RR )
11 10 3ad2ant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> M e. RR )
12 11 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> M e. RR )
13 6 zred 
 |-  ( k e. ( M ... N ) -> k e. RR )
14 13 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k e. RR )
15 zre 
 |-  ( I e. ZZ -> I e. RR )
16 10 15 anim12i 
 |-  ( ( M e. ZZ /\ I e. ZZ ) -> ( M e. RR /\ I e. RR ) )
17 16 ancomd 
 |-  ( ( M e. ZZ /\ I e. ZZ ) -> ( I e. RR /\ M e. RR ) )
18 17 3adant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( I e. RR /\ M e. RR ) )
19 18 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> ( I e. RR /\ M e. RR ) )
20 min2 
 |-  ( ( I e. RR /\ M e. RR ) -> if ( I <_ M , I , M ) <_ M )
21 19 20 syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ M , I , M ) <_ M )
22 elfzle1 
 |-  ( k e. ( M ... N ) -> M <_ k )
23 22 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> M <_ k )
24 9 12 14 21 23 letrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ M , I , M ) <_ k )
25 eluz2 
 |-  ( k e. ( ZZ>= ` if ( I <_ M , I , M ) ) <-> ( if ( I <_ M , I , M ) e. ZZ /\ k e. ZZ /\ if ( I <_ M , I , M ) <_ k ) )
26 5 7 24 25 syl3anbrc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k e. ( ZZ>= ` if ( I <_ M , I , M ) ) )
27 simp2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> N e. ZZ )
28 27 2 ifcld 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> if ( I <_ N , N , I ) e. ZZ )
29 28 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ N , N , I ) e. ZZ )
30 zre 
 |-  ( N e. ZZ -> N e. RR )
31 30 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> N e. RR )
32 31 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> N e. RR )
33 28 zred 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> if ( I <_ N , N , I ) e. RR )
34 33 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ N , N , I ) e. RR )
35 elfzle2 
 |-  ( k e. ( M ... N ) -> k <_ N )
36 35 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k <_ N )
37 30 15 anim12i 
 |-  ( ( N e. ZZ /\ I e. ZZ ) -> ( N e. RR /\ I e. RR ) )
38 37 3adant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( N e. RR /\ I e. RR ) )
39 38 ancomd 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( I e. RR /\ N e. RR ) )
40 max2 
 |-  ( ( I e. RR /\ N e. RR ) -> N <_ if ( I <_ N , N , I ) )
41 39 40 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> N <_ if ( I <_ N , N , I ) )
42 41 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> N <_ if ( I <_ N , N , I ) )
43 14 32 34 36 42 letrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> k <_ if ( I <_ N , N , I ) )
44 eluz2 
 |-  ( if ( I <_ N , N , I ) e. ( ZZ>= ` k ) <-> ( k e. ZZ /\ if ( I <_ N , N , I ) e. ZZ /\ k <_ if ( I <_ N , N , I ) ) )
45 7 29 43 44 syl3anbrc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) /\ k e. ( M ... N ) ) -> if ( I <_ N , N , I ) e. ( ZZ>= ` k ) )
46 elfzuzb 
 |-  ( k e. ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) <-> ( k e. ( ZZ>= ` if ( I <_ M , I , M ) ) /\ if ( I <_ N , N , I ) e. ( ZZ>= ` k ) ) )
47 26 45 46 sylanbrc 
 |-  ( ( ( 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 ) ) )
48 47 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 ) ) ) )
49 48 ssrdv 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( M ... N ) C_ ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) )
50 49 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 ) ) )
51 1 50 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 ) ) )
52 4 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> if ( I <_ M , I , M ) e. ZZ )
53 28 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> if ( I <_ N , N , I ) e. ZZ )
54 2 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> I e. ZZ )
55 52 53 54 3jca 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( if ( I <_ M , I , M ) e. ZZ /\ if ( I <_ N , N , I ) e. ZZ /\ I e. ZZ ) )
56 16 3adant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) -> ( M e. RR /\ I e. RR ) )
57 56 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( M e. RR /\ I e. RR ) )
58 57 ancomd 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( I e. RR /\ M e. RR ) )
59 min1 
 |-  ( ( I e. RR /\ M e. RR ) -> if ( I <_ M , I , M ) <_ I )
60 58 59 syl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> if ( I <_ M , I , M ) <_ I )
61 38 adantl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( N e. RR /\ I e. RR ) )
62 61 ancomd 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( I e. RR /\ N e. RR ) )
63 max1 
 |-  ( ( I e. RR /\ N e. RR ) -> I <_ if ( I <_ N , N , I ) )
64 62 63 syl 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> I <_ if ( I <_ N , N , I ) )
65 60 64 jca 
 |-  ( ( S C_ ( M ... N ) /\ ( M e. ZZ /\ N e. ZZ /\ I e. ZZ ) ) -> ( if ( I <_ M , I , M ) <_ I /\ I <_ if ( I <_ N , N , I ) ) )
66 elfz2 
 |-  ( I e. ( if ( I <_ M , I , M ) ... if ( I <_ N , N , I ) ) <-> ( ( if ( I <_ M , I , M ) e. ZZ /\ if ( I <_ N , N , I ) e. ZZ /\ I e. ZZ ) /\ ( if ( I <_ M , I , M ) <_ I /\ I <_ if ( I <_ N , N , I ) ) ) )
67 55 65 66 sylanbrc 
 |-  ( ( 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 ) ) )
68 67 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 ) ) )
69 51 68 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 ) ) )