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