Metamath Proof Explorer

Theorem metakunt18

Description: Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt18.1 
|- ( ph -> M e. NN )
metakunt18.2 
|- ( ph -> I e. NN )
metakunt18.3 
|- ( ph -> I <_ M )
Assertion metakunt18 
|- ( ph -> ( ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) /\ ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) /\ ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) /\ ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 metakunt18.1 
 |-  ( ph -> M e. NN )
2 metakunt18.2 
 |-  ( ph -> I e. NN )
3 metakunt18.3 
 |-  ( ph -> I <_ M )
4 2 nnred 
 |-  ( ph -> I e. RR )
5 4 ltm1d 
 |-  ( ph -> ( I - 1 ) < I )
6 fzdisj 
 |-  ( ( I - 1 ) < I -> ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) )
7 5 6 syl 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) )
8 1 nnzd 
 |-  ( ph -> M e. ZZ )
9 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
10 8 9 syl 
 |-  ( ph -> ( M ... M ) = { M } )
11 10 eqcomd 
 |-  ( ph -> { M } = ( M ... M ) )
12 11 ineq2d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i { M } ) = ( ( 1 ... ( I - 1 ) ) i^i ( M ... M ) ) )
13 2 nnzd 
 |-  ( ph -> I e. ZZ )
14 zlem1lt 
 |-  ( ( I e. ZZ /\ M e. ZZ ) -> ( I <_ M <-> ( I - 1 ) < M ) )
15 13 8 14 syl2anc 
 |-  ( ph -> ( I <_ M <-> ( I - 1 ) < M ) )
16 3 15 mpbid 
 |-  ( ph -> ( I - 1 ) < M )
17 fzdisj 
 |-  ( ( I - 1 ) < M -> ( ( 1 ... ( I - 1 ) ) i^i ( M ... M ) ) = (/) )
18 16 17 syl 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i ( M ... M ) ) = (/) )
19 12 18 eqtrd 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) )
20 11 ineq2d 
 |-  ( ph -> ( ( I ... ( M - 1 ) ) i^i { M } ) = ( ( I ... ( M - 1 ) ) i^i ( M ... M ) ) )
21 1 nnred 
 |-  ( ph -> M e. RR )
22 21 ltm1d 
 |-  ( ph -> ( M - 1 ) < M )
23 fzdisj 
 |-  ( ( M - 1 ) < M -> ( ( I ... ( M - 1 ) ) i^i ( M ... M ) ) = (/) )
24 22 23 syl 
 |-  ( ph -> ( ( I ... ( M - 1 ) ) i^i ( M ... M ) ) = (/) )
25 20 24 eqtrd 
 |-  ( ph -> ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) )
26 7 19 25 3jca 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) )
27 incom 
 |-  ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = ( ( 1 ... ( M - I ) ) i^i ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) )
28 27 a1i 
 |-  ( ph -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = ( ( 1 ... ( M - I ) ) i^i ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) )
29 21 4 resubcld 
 |-  ( ph -> ( M - I ) e. RR )
30 29 ltp1d 
 |-  ( ph -> ( M - I ) < ( ( M - I ) + 1 ) )
31 fzdisj 
 |-  ( ( M - I ) < ( ( M - I ) + 1 ) -> ( ( 1 ... ( M - I ) ) i^i ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) = (/) )
32 30 31 syl 
 |-  ( ph -> ( ( 1 ... ( M - I ) ) i^i ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) = (/) )
33 28 32 eqtrd 
 |-  ( ph -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) )
34 11 ineq2d 
 |-  ( ph -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( M ... M ) ) )
35 fzdisj 
 |-  ( ( M - 1 ) < M -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( M ... M ) ) = (/) )
36 22 35 syl 
 |-  ( ph -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( M ... M ) ) = (/) )
37 34 36 eqtrd 
 |-  ( ph -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) )
38 11 ineq2d 
 |-  ( ph -> ( ( 1 ... ( M - I ) ) i^i { M } ) = ( ( 1 ... ( M - I ) ) i^i ( M ... M ) ) )
39 2 nnrpd 
 |-  ( ph -> I e. RR+ )
40 21 39 ltsubrpd 
 |-  ( ph -> ( M - I ) < M )
41 fzdisj 
 |-  ( ( M - I ) < M -> ( ( 1 ... ( M - I ) ) i^i ( M ... M ) ) = (/) )
42 40 41 syl 
 |-  ( ph -> ( ( 1 ... ( M - I ) ) i^i ( M ... M ) ) = (/) )
43 38 42 eqtrd 
 |-  ( ph -> ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) )
44 33 37 43 3jca 
 |-  ( ph -> ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) /\ ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) /\ ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) ) )
45 26 44 jca 
 |-  ( ph -> ( ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) /\ ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) /\ ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) /\ ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) ) ) )