Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clscnc Unicode version

Theorem clscnc 26010
Description: Closure of concatenation. (Contributed by FL, 2-Feb-2014.)
Assertion
Ref Expression
clscnc  |-  ( ( A  e.  ( Kleene `  C )  /\  B  e.  ( Kleene `  C )
)  ->  ( A  conc  B )  e.  (
Kleene `  C ) )

Proof of Theorem clscnc
Dummy variables  a 
b  c  d are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isconc1 26006 . . . . 5  |-  ( B  e.  ( Kleene `  C
)  ->  ( (/)  conc  B
)  =  B )
2 eleq1 2343 . . . . . . 7  |-  ( B  =  ( (/)  conc  B
)  ->  ( B  e.  ( Kleene `  C )  <->  (
(/)  conc  B )  e.  ( Kleene `  C )
) )
32biimpd 198 . . . . . 6  |-  ( B  =  ( (/)  conc  B
)  ->  ( B  e.  ( Kleene `  C )  ->  ( (/)  conc  B )  e.  ( Kleene `  C
) ) )
43eqcoms 2286 . . . . 5  |-  ( (
(/)  conc  B )  =  B  ->  ( B  e.  ( Kleene `  C )  ->  ( (/)  conc  B )  e.  ( Kleene `  C
) ) )
51, 4mpcom 32 . . . 4  |-  ( B  e.  ( Kleene `  C
)  ->  ( (/)  conc  B
)  e.  ( Kleene `  C ) )
6 oveq1 5865 . . . . 5  |-  ( A  =  (/)  ->  ( A 
conc  B )  =  (
(/)  conc  B ) )
76eleq1d 2349 . . . 4  |-  ( A  =  (/)  ->  ( ( A  conc  B )  e.  ( Kleene `  C )  <->  (
(/)  conc  B )  e.  ( Kleene `  C )
) )
85, 7syl5ibr 212 . . 3  |-  ( A  =  (/)  ->  ( B  e.  ( Kleene `  C
)  ->  ( A  conc  B )  e.  (
Kleene `  C ) ) )
98adantld 453 . 2  |-  ( A  =  (/)  ->  ( ( A  e.  ( Kleene `  C )  /\  B  e.  ( Kleene `  C )
)  ->  ( A  conc  B )  e.  (
Kleene `  C ) ) )
10 isconc2 26007 . . . . . . 7  |-  ( A  e.  ( Kleene `  C
)  ->  ( A  conc 
(/) )  =  A )
11 eleq1 2343 . . . . . . . . 9  |-  ( A  =  ( A  conc  (/) )  ->  ( A  e.  ( Kleene `  C )  <->  ( A  conc  (/) )  e.  ( Kleene `  C )
) )
1211biimpd 198 . . . . . . . 8  |-  ( A  =  ( A  conc  (/) )  ->  ( A  e.  ( Kleene `  C )  ->  ( A  conc  (/) )  e.  ( Kleene `  C )
) )
1312eqcoms 2286 . . . . . . 7  |-  ( ( A  conc  (/) )  =  A  ->  ( A  e.  ( Kleene `  C )  ->  ( A  conc  (/) )  e.  ( Kleene `  C )
) )
1410, 13mpcom 32 . . . . . 6  |-  ( A  e.  ( Kleene `  C
)  ->  ( A  conc 
(/) )  e.  (
Kleene `  C ) )
15 oveq2 5866 . . . . . . 7  |-  ( B  =  (/)  ->  ( A 
conc  B )  =  ( A  conc  (/) ) )
1615eleq1d 2349 . . . . . 6  |-  ( B  =  (/)  ->  ( ( A  conc  B )  e.  ( Kleene `  C )  <->  ( A  conc  (/) )  e.  ( Kleene `  C )
) )
1714, 16syl5ibr 212 . . . . 5  |-  ( B  =  (/)  ->  ( A  e.  ( Kleene `  C
)  ->  ( A  conc  B )  e.  (
Kleene `  C ) ) )
1817adantrd 454 . . . 4  |-  ( B  =  (/)  ->  ( ( A  e.  ( Kleene `  C )  /\  B  e.  ( Kleene `  C )
)  ->  ( A  conc  B )  e.  (
Kleene `  C ) ) )
1918a1i 10 . . 3  |-  ( A  =/=  (/)  ->  ( B  =  (/)  ->  ( ( A  e.  ( Kleene `  C )  /\  B  e.  ( Kleene `  C )
)  ->  ( A  conc  B )  e.  (
Kleene `  C ) ) ) )
20 isconc3 26008 . . . . . 6  |-  ( ( A  e.  ( Kleene `  C )  /\  B  e.  ( Kleene `  C )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  -> 
( A  conc  B
)  =  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) ) )
21 elfvex 5555 . . . . . . . 8  |-  ( A  e.  ( Kleene `  C
)  ->  C  e.  _V )
22 isKleene 25988 . . . . . . . . 9  |-  ( C  e.  _V  ->  ( Kleene `
 C )  = 
U_ a  e.  NN0  ( C  ^m  (
1 ... a ) ) )
23 oveq2 5866 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  c  ->  (
1 ... a )  =  ( 1 ... c
) )
2423oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  c  ->  ( C  ^m  ( 1 ... a ) )  =  ( C  ^m  (
1 ... c ) ) )
2524cbviunv 3941 . . . . . . . . . . . . . . . . 17  |-  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) )  =  U_ c  e.  NN0  ( C  ^m  ( 1 ... c ) )
2625eleq2i 2347 . . . . . . . . . . . . . . . 16  |-  ( A  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  <->  A  e.  U_ c  e.  NN0  ( C  ^m  ( 1 ... c ) ) )
27 eliun 3909 . . . . . . . . . . . . . . . 16  |-  ( A  e.  U_ c  e. 
NN0  ( C  ^m  ( 1 ... c
) )  <->  E. c  e.  NN0  A  e.  ( C  ^m  ( 1 ... c ) ) )
2826, 27bitri 240 . . . . . . . . . . . . . . 15  |-  ( A  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  <->  E. c  e.  NN0  A  e.  ( C  ^m  ( 1 ... c ) ) )
29 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  d  ->  (
1 ... a )  =  ( 1 ... d
) )
3029oveq2d 5874 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  d  ->  ( C  ^m  ( 1 ... a ) )  =  ( C  ^m  (
1 ... d ) ) )
3130cbviunv 3941 . . . . . . . . . . . . . . . . . . . 20  |-  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) )  =  U_ d  e.  NN0  ( C  ^m  ( 1 ... d ) )
3231eleq2i 2347 . . . . . . . . . . . . . . . . . . 19  |-  ( B  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  <->  B  e.  U_ d  e.  NN0  ( C  ^m  ( 1 ... d ) ) )
33 eliun 3909 . . . . . . . . . . . . . . . . . . 19  |-  ( B  e.  U_ d  e. 
NN0  ( C  ^m  ( 1 ... d
) )  <->  E. d  e.  NN0  B  e.  ( C  ^m  ( 1 ... d ) ) )
3432, 33bitri 240 . . . . . . . . . . . . . . . . . 18  |-  ( B  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  <->  E. d  e.  NN0  B  e.  ( C  ^m  ( 1 ... d ) ) )
35 nn0addcl 9999 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( c  e.  NN0  /\  d  e.  NN0 )  -> 
( c  +  d )  e.  NN0 )
3635ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( d  e.  NN0  /\  c  e.  NN0 )  -> 
( c  +  d )  e.  NN0 )
3736ad2ant2r 727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( d  e.  NN0  /\  B  e.  ( C  ^m  ( 1 ... d ) ) )  /\  ( c  e. 
NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) ) )  ->  (
c  +  d )  e.  NN0 )
38373adant3 975 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( d  e.  NN0  /\  B  e.  ( C  ^m  ( 1 ... d ) ) )  /\  ( c  e. 
NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  /\  C  e. 
_V )  ->  (
c  +  d )  e.  NN0 )
3938adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( d  e. 
NN0  /\  B  e.  ( C  ^m  (
1 ... d ) ) )  /\  ( c  e.  NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
c  +  d )  e.  NN0 )
40 ovex 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 1 ... d )  e. 
_V
41 elmapg 6785 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( C  e.  _V  /\  ( 1 ... d
)  e.  _V )  ->  ( B  e.  ( C  ^m  ( 1 ... d ) )  <-> 
B : ( 1 ... d ) --> C ) )
4240, 41mpan2 652 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( C  e.  _V  ->  ( B  e.  ( C  ^m  ( 1 ... d
) )  <->  B :
( 1 ... d
) --> C ) )
43 ffn 5389 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( B : ( 1 ... d ) --> C  ->  B  Fn  ( 1 ... d ) )
44 ovex 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 1 ... c )  e. 
_V
45 elmapg 6785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( C  e.  _V  /\  ( 1 ... c
)  e.  _V )  ->  ( A  e.  ( C  ^m  ( 1 ... c ) )  <-> 
A : ( 1 ... c ) --> C ) )
4644, 45mpan2 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( C  e.  _V  ->  ( A  e.  ( C  ^m  ( 1 ... c
) )  <->  A :
( 1 ... c
) --> C ) )
47 ffn 5389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( A : ( 1 ... c ) --> C  ->  A  Fn  ( 1 ... c ) )
48 fseq1hash 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( c  e.  NN0  /\  A  Fn  ( 1 ... c ) )  ->  ( # `  A
)  =  c )
49 fseq1hash 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( d  e.  NN0  /\  B  Fn  ( 1 ... d ) )  ->  ( # `  B
)  =  d )
50 simpl2r 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  A : ( 1 ... c ) --> C )
51 elfzel1 10797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  ->  (
c  +  1 )  e.  ZZ )
5251adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
c  +  1 )  e.  ZZ )
53 nn0z 10046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64  |-  ( c  e.  NN0  ->  c  e.  ZZ )
54 nn0z 10046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64  |-  ( d  e.  NN0  ->  d  e.  ZZ )
55 zaddcl 10059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64  |-  ( ( c  e.  ZZ  /\  d  e.  ZZ )  ->  ( c  +  d )  e.  ZZ )
5653, 54, 55syl2anr 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63  |-  ( ( d  e.  NN0  /\  c  e.  NN0 )  -> 
( c  +  d )  e.  ZZ )
5756ad2ant2r 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C ) )  ->  ( c  +  d )  e.  ZZ )
58573adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( c  +  d )  e.  ZZ )
5958ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
c  +  d )  e.  ZZ )
6053adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63  |-  ( ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  c  e.  ZZ )
61603ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  c  e.  ZZ )
6261adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  c  e.  ZZ )
63 elfzelz 10798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  ->  a  e.  ZZ )
6462, 63anim12ci 550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
a  e.  ZZ  /\  c  e.  ZZ )
)
65 fzsubel 10827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( ( ( c  +  1 )  e.  ZZ  /\  ( c  +  d )  e.  ZZ )  /\  ( a  e.  ZZ  /\  c  e.  ZZ ) )  -> 
( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  <-> 
( a  -  c
)  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c ) ) ) )
6652, 59, 64, 65syl21anc 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  <->  ( a  -  c )  e.  ( ( ( c  +  1 )  -  c ) ... (
( c  +  d )  -  c ) ) ) )
6766biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  -> 
( a  -  c
)  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c ) ) ) )
6867ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  -> 
( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  ->  ( a  -  c )  e.  ( ( ( c  +  1 )  -  c
) ... ( ( c  +  d )  -  c ) ) ) ) )
6968com13 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  ->  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  -> 
( ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  -> 
( a  -  c
)  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c ) ) ) ) )
7069pm2.43i 43 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  ->  (
( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
a  -  c )  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c
) ) ) )
7170impcom 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
a  -  c )  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c
) ) )
72 simpl1r 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  B : ( 1 ... d ) --> C )
7372ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( ( a  -  c
)  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c ) )  /\  ( ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( (
c  +  1 ) ... ( c  +  d ) ) ) )  ->  B :
( 1 ... d
) --> C )
74 ax-1cn 8795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66  |-  1  e.  CC
7574a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65  |-  ( d  e.  NN0  ->  1  e.  CC )
76 nn0cn 9975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65  |-  ( c  e.  NN0  ->  c  e.  CC )
7775, 76anim12ci 550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64  |-  ( ( d  e.  NN0  /\  c  e.  NN0 )  -> 
( c  e.  CC  /\  1  e.  CC ) )
7877ad2ant2r 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C ) )  ->  ( c  e.  CC  /\  1  e.  CC ) )
79783adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( c  e.  CC  /\  1  e.  CC ) )
8079ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
c  e.  CC  /\  1  e.  CC )
)
81 pncan2 9058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( ( c  e.  CC  /\  1  e.  CC )  ->  ( ( c  +  1 )  -  c
)  =  1 )
8280, 81syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
( c  +  1 )  -  c )  =  1 )
83 nn0cn 9975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65  |-  ( d  e.  NN0  ->  d  e.  CC )
8483, 76anim12ci 550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64  |-  ( ( d  e.  NN0  /\  c  e.  NN0 )  -> 
( c  e.  CC  /\  d  e.  CC ) )
8584ad2ant2r 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C ) )  ->  ( c  e.  CC  /\  d  e.  CC ) )
86853adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( c  e.  CC  /\  d  e.  CC ) )
8786ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
c  e.  CC  /\  d  e.  CC )
)
88 pncan2 9058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( ( c  e.  CC  /\  d  e.  CC )  ->  ( ( c  +  d )  -  c
)  =  d )
8987, 88syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
( c  +  d )  -  c )  =  d )
9082, 89oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
( ( c  +  1 )  -  c
) ... ( ( c  +  d )  -  c ) )  =  ( 1 ... d
) )
9190eleq2d 2350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  (
( a  -  c
)  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c ) )  <->  ( a  -  c )  e.  ( 1 ... d
) ) )
9291biimpac 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( ( a  -  c
)  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c ) )  /\  ( ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( (
c  +  1 ) ... ( c  +  d ) ) ) )  ->  ( a  -  c )  e.  ( 1 ... d
) )
9373, 92jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( ( a  -  c
)  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c ) )  /\  ( ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( (
c  +  1 ) ... ( c  +  d ) ) ) )  ->  ( B : ( 1 ... d ) --> C  /\  ( a  -  c
)  e.  ( 1 ... d ) ) )
9493ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( a  -  c )  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c
) )  ->  (
( ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( (
c  +  1 ) ... ( c  +  d ) ) )  ->  ( B :
( 1 ... d
) --> C  /\  (
a  -  c )  e.  ( 1 ... d ) ) ) )
95 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( B : ( 1 ... d ) --> C  /\  ( a  -  c )  e.  ( 1 ... d ) )  ->  ( B `  ( a  -  c
) )  e.  C
)
9694, 95syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( a  -  c )  e.  ( ( ( c  +  1 )  -  c ) ... ( ( c  +  d )  -  c
) )  ->  (
( ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( (
c  +  1 ) ... ( c  +  d ) ) )  ->  ( B `  ( a  -  c
) )  e.  C
) )
9771, 96mpcom 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( ( ( ( d  e.  NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  /\  a  e.  ( ( c  +  1 ) ... (
c  +  d ) ) )  ->  ( B `  ( a  -  c ) )  e.  C )
98 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `
 ( a  -  c ) ) )  =  ( a  e.  ( ( c  +  1 ) ... (
c  +  d ) )  |->  ( B `  ( a  -  c
) ) )
9997, 98fmptd 5684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `  ( a  -  c ) ) ) : ( ( c  +  1 ) ... ( c  +  d ) ) --> C )
100 nn0re 9974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( c  e.  NN0  ->  c  e.  RR )
101100adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  c  e.  RR )
1021013ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  c  e.  RR )
103102adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  c  e.  RR )
104103ltp1d 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  c  <  ( c  +  1 ) )
105 fzdisj 10817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( c  <  ( c  +  1 )  ->  (
( 1 ... c
)  i^i  ( (
c  +  1 ) ... ( c  +  d ) ) )  =  (/) )
106104, 105syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
( 1 ... c
)  i^i  ( (
c  +  1 ) ... ( c  +  d ) ) )  =  (/) )
107 fun2 5406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( A : ( 1 ... c ) --> C  /\  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `
 ( a  -  c ) ) ) : ( ( c  +  1 ) ... ( c  +  d ) ) --> C )  /\  ( ( 1 ... c )  i^i  ( ( c  +  1 ) ... (
c  +  d ) ) )  =  (/) )  ->  ( A  u.  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) ) 
|->  ( B `  (
a  -  c ) ) ) ) : ( ( 1 ... c )  u.  (
( c  +  1 ) ... ( c  +  d ) ) ) --> C )
10850, 99, 106, 107syl21anc 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  ( A  u.  ( a  e.  ( ( c  +  1 ) ... (
c  +  d ) )  |->  ( B `  ( a  -  c
) ) ) ) : ( ( 1 ... c )  u.  ( ( c  +  1 ) ... (
c  +  d ) ) ) --> C )
109 simp2l 981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  c  e.  NN0 )
11047adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  A  Fn  (
1 ... c ) )
1111103ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  A  Fn  ( 1 ... c ) )
112 0fz1 10813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( c  e.  NN0  /\  A  Fn  ( 1 ... c ) )  ->  ( A  =  (/) 
<->  c  =  0 ) )
113112necon3bid 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59  |-  ( ( c  e.  NN0  /\  A  Fn  ( 1 ... c ) )  ->  ( A  =/=  (/) 
<->  c  =/=  0 ) )
114109, 111, 113syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( A  =/=  (/)  <->  c  =/=  0 ) )
115 simpr2l 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( ( c  =/=  0  /\  ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V ) )  -> 
c  e.  NN0 )
116 nn0ge0 9991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65  |-  ( c  e.  NN0  ->  0  <_ 
c )
117 0re 8838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67  |-  0  e.  RR
118 ltlen 8922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68  |-  ( ( 0  e.  RR  /\  c  e.  RR )  ->  ( 0  <  c  <->  ( 0  <_  c  /\  c  =/=  0 ) ) )
119118bicomd 192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67  |-  ( ( 0  e.  RR  /\  c  e.  RR )  ->  ( ( 0  <_ 
c  /\  c  =/=  0 )  <->  0  <  c ) )
120117, 100, 119sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66  |-  ( c  e.  NN0  ->  ( ( 0  <_  c  /\  c  =/=  0 )  <->  0  <  c ) )
121120biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65  |-  ( c  e.  NN0  ->  ( ( 0  <_  c  /\  c  =/=  0 )  -> 
0  <  c )
)
122116, 121mpand 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64  |-  ( c  e.  NN0  ->  ( c  =/=  0  ->  0  <  c ) )
123122adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63  |-  ( ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  ( c  =/=  0  ->  0  <  c ) )
1241233ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( c  =/=  0  ->  0  <  c ) )
125124impcom 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( ( c  =/=  0  /\  ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V ) )  -> 
0  <  c )
126 elnnnn0b 10008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61  |-  ( c  e.  NN  <->  ( c  e.  NN0  /\  0  < 
c ) )
127115, 125, 126sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( ( c  =/=  0  /\  ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V ) )  -> 
c  e.  NN )
128127ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59  |-  ( c  =/=  0  ->  (
( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  ->  c  e.  NN ) )
129 nnge1 9772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59  |-  ( c  e.  NN  ->  1  <_  c )
130128, 129syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( c  =/=  0  ->  (
( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  ->  1  <_  c ) )
131114, 130syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( A  =/=  (/)  ->  (
( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  ->  1  <_  c ) ) )
132131pm2.43a 45 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( A  =/=  (/)  ->  1  <_  c ) )
133132adantrd 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
1  <_  c )
)
134133imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  1  <_  c )
135 nn0ge0 9991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( d  e.  NN0  ->  0  <_ 
d )
136135adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  ->  0  <_  d
)
1371363ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  0  <_  d )
138137adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  0  <_  d )
139 nn0re 9974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60  |-  ( d  e.  NN0  ->  d  e.  RR )
140139, 100anim12ci 550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59  |-  ( ( d  e.  NN0  /\  c  e.  NN0 )  -> 
( c  e.  RR  /\  d  e.  RR ) )
141140ad2ant2r 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C ) )  ->  ( c  e.  RR  /\  d  e.  RR ) )
1421413adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  /\  ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  /\  C  e.  _V )  ->  ( c  e.  RR  /\  d  e.  RR ) )
143142adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
c  e.  RR  /\  d  e.  RR )
)
144 addge01 9284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( c  e.  RR  /\  d  e.  RR )  ->  ( 0  <_  d  <->  c  <_  ( c  +  d ) ) )
145144bicomd 192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( c  e.  RR  /\  d  e.  RR )  ->  ( c  <_  (
c  +  d )  <->  0  <_  d )
)
146143, 145syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
c  <_  ( c  +  d )  <->  0  <_  d ) )
147138, 146mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  c  <_  ( c  +  d ) )
148 1z 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  1  e.  ZZ
14958adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
c  +  d )  e.  ZZ )
150 elfz1 10787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( 1  e.  ZZ  /\  ( c  +  d )  e.  ZZ )  ->  ( c  e.  ( 1 ... (
c  +  d ) )  <->  ( c  e.  ZZ  /\  1  <_ 
c  /\  c  <_  ( c  +  d ) ) ) )
151148, 149, 150sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
c  e.  ( 1 ... ( c  +  d ) )  <->  ( c  e.  ZZ  /\  1  <_ 
c  /\  c  <_  ( c  +  d ) ) ) )
15262, 134, 147, 151mpbir3and 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  c  e.  ( 1 ... (
c  +  d ) ) )
153 fzsplit 10816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( c  e.  ( 1 ... ( c  +  d ) )  ->  (
1 ... ( c  +  d ) )  =  ( ( 1 ... c )  u.  (
( c  +  1 ) ... ( c  +  d ) ) ) )
154152, 153syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
1 ... ( c  +  d ) )  =  ( ( 1 ... c )  u.  (
( c  +  1 ) ... ( c  +  d ) ) ) )
155154feq2d 5380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
( A  u.  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `  ( a  -  c ) ) ) ) : ( 1 ... ( c  +  d ) ) --> C  <->  ( A  u.  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) ) 
|->  ( B `  (
a  -  c ) ) ) ) : ( ( 1 ... c )  u.  (
( c  +  1 ) ... ( c  +  d ) ) ) --> C ) )
156108, 155mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  ( A  u.  ( a  e.  ( ( c  +  1 ) ... (
c  +  d ) )  |->  ( B `  ( a  -  c
) ) ) ) : ( 1 ... ( c  +  d ) ) --> C )
157 simpl3 960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  C  e.  _V )
158 ovex 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( 1 ... ( c  +  d ) )  e. 
_V
159 elmapg 6785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( C  e.  _V  /\  ( 1 ... (
c  +  d ) )  e.  _V )  ->  ( ( A  u.  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) ) 
|->  ( B `  (
a  -  c ) ) ) )  e.  ( C  ^m  (
1 ... ( c  +  d ) ) )  <-> 
( A  u.  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `  ( a  -  c ) ) ) ) : ( 1 ... ( c  +  d ) ) --> C ) )
160157, 158, 159sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  (
( A  u.  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `  ( a  -  c ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) )  <-> 
( A  u.  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `  ( a  -  c ) ) ) ) : ( 1 ... ( c  +  d ) ) --> C ) )
161156, 160mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( ( d  e. 
NN0  /\  B :
( 1 ... d
) --> C )  /\  ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  ( A  u.  ( a  e.  ( ( c  +  1 ) ... (
c  +  d ) )  |->  ( B `  ( a  -  c
) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) )
1621613exp1 1167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  ->  ( ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  -> 
( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `  ( a  -  c ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) )
163 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( (
# `  A )  =  c  ->  ( (
# `  A )  +  1 )  =  ( c  +  1 ) )
164 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( (
# `  A )  =  c  ->  ( (
# `  A )  +  d )  =  ( c  +  d ) )
165163, 164oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( (
# `  A )  =  c  ->  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  d ) )  =  ( ( c  +  1 ) ... ( c  +  d ) ) )
166 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( (
# `  A )  =  c  ->  ( a  -  ( # `  A
) )  =  ( a  -  c ) )
167166fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( (
# `  A )  =  c  ->  ( B `
 ( a  -  ( # `  A ) ) )  =  ( B `  ( a  -  c ) ) )
168165, 167mpteq12dv 4098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( (
# `  A )  =  c  ->  ( a  e.  ( ( (
# `  A )  +  1 ) ... ( ( # `  A
)  +  d ) )  |->  ( B `  ( a  -  ( # `
 A ) ) ) )  =  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `  ( a  -  c ) ) ) )
169168uneq2d 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( (
# `  A )  =  c  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  d ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  =  ( A  u.  ( a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `
 ( a  -  c ) ) ) ) )
170169eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
# `  A )  =  c  ->  ( ( A  u.  ( a  e.  ( ( (
# `  A )  +  1 ) ... ( ( # `  A
)  +  d ) )  |->  ( B `  ( a  -  ( # `
 A ) ) ) ) )  e.  ( C  ^m  (
1 ... ( c  +  d ) ) )  <-> 
( A  u.  (
a  e.  ( ( c  +  1 ) ... ( c  +  d ) )  |->  ( B `  ( a  -  c ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) )
171170imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
# `  A )  =  c  ->  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  d ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) )  <->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( c  +  1 ) ... (
c  +  d ) )  |->  ( B `  ( a  -  c
) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) )
172171imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
# `  A )  =  c  ->  ( ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  d ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) )  <->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( c  +  1 ) ... (
c  +  d ) )  |->  ( B `  ( a  -  c
) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) )
173172imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
# `  A )  =  c  ->  ( ( ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  d ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) )  <->  ( (
c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( c  +  1 ) ... (
c  +  d ) )  |->  ( B `  ( a  -  c
) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) )
174162, 173syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  ->  ( ( # `  A )  =  c  ->  ( ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  -> 
( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  d ) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) )
175 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( (
# `  B )  =  d  ->  ( (
# `  A )  +  ( # `  B
) )  =  ( ( # `  A
)  +  d ) )
176175oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( (
# `  B )  =  d  ->  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  =  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  d ) ) )
177 eqidd 2284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( (
# `  B )  =  d  ->  ( B `
 ( a  -  ( # `  A ) ) )  =  ( B `  ( a  -  ( # `  A
) ) ) )
178176, 177mpteq12dv 4098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( (
# `  B )  =  d  ->  ( a  e.  ( ( (
# `  A )  +  1 ) ... ( ( # `  A
)  +  ( # `  B ) ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) )  =  ( a  e.  ( ( (
# `  A )  +  1 ) ... ( ( # `  A
)  +  d ) )  |->  ( B `  ( a  -  ( # `
 A ) ) ) ) )
179178uneq2d 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( (
# `  B )  =  d  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  =  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  d ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) ) )
180179eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
# `  B )  =  d  ->  ( ( A  u.  ( a  e.  ( ( (
# `  A )  +  1 ) ... ( ( # `  A
)  +  ( # `  B ) ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) )  <-> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  d ) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) )
181180imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
# `  B )  =  d  ->  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) )  <-> 
( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  d ) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) )
182181imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
# `  B )  =  d  ->  ( ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) )  <->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  d ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) )
183182imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
# `  B )  =  d  ->  ( ( ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) )  <->  ( (
c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  d ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) )
184183imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
# `  B )  =  d  ->  ( ( ( # `  A
)  =  c  -> 
( ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  -> 
( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) )  <->  ( ( # `
 A )  =  c  ->  ( (
c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  d ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) )
185174, 184syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
# `  B )  =  d  ->  ( ( d  e.  NN0  /\  B : ( 1 ... d ) --> C )  ->  ( ( # `  A )  =  c  ->  ( ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  -> 
( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) )
186185exp3a 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
# `  B )  =  d  ->  ( d  e.  NN0  ->  ( B : ( 1 ... d ) --> C  -> 
( ( # `  A
)  =  c  -> 
( ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  -> 
( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) ) )
18749, 186syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( d  e.  NN0  /\  B  Fn  ( 1 ... d ) )  ->  ( d  e. 
NN0  ->  ( B :
( 1 ... d
) --> C  ->  (
( # `  A )  =  c  ->  (
( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) ) )
188187ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( d  e.  NN0  ->  ( B  Fn  ( 1 ... d )  ->  (
d  e.  NN0  ->  ( B : ( 1 ... d ) --> C  ->  ( ( # `  A )  =  c  ->  ( ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  -> 
( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) ) ) )
189188pm2.43a 45 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( d  e.  NN0  ->  ( B  Fn  ( 1 ... d )  ->  ( B : ( 1 ... d ) --> C  -> 
( ( # `  A
)  =  c  -> 
( ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  -> 
( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) ) )
190189com5l 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( B  Fn  ( 1 ... d )  ->  ( B : ( 1 ... d ) --> C  -> 
( ( # `  A
)  =  c  -> 
( ( c  e. 
NN0  /\  A :
( 1 ... c
) --> C )  -> 
( d  e.  NN0  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) ) )
191190imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( B  Fn  ( 1 ... d )  /\  B : ( 1 ... d ) --> C )  ->  ( ( # `  A )  =  c  ->  ( ( c  e.  NN0  /\  A :
( 1 ... c
) --> C )  -> 
( d  e.  NN0  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) )
192191com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
# `  A )  =  c  ->  ( ( c  e.  NN0  /\  A : ( 1 ... c ) --> C )  ->  ( ( B  Fn  ( 1 ... d )  /\  B : ( 1 ... d ) --> C )  ->  ( d  e. 
NN0  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) )
193192exp3a 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
# `  A )  =  c  ->  ( c  e.  NN0  ->  ( A : ( 1 ... c ) --> C  -> 
( ( B  Fn  ( 1 ... d
)  /\  B :
( 1 ... d
) --> C )  -> 
( d  e.  NN0  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) ) )
19448, 193syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( c  e.  NN0  /\  A  Fn  ( 1 ... c ) )  ->  ( c  e. 
NN0  ->  ( A :
( 1 ... c
) --> C  ->  (
( B  Fn  (
1 ... d )  /\  B : ( 1 ... d ) --> C )  ->  ( d  e. 
NN0  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) ) )
195194ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  e.  NN0  ->  ( A  Fn  ( 1 ... c )  ->  (
c  e.  NN0  ->  ( A : ( 1 ... c ) --> C  ->  ( ( B  Fn  ( 1 ... d )  /\  B : ( 1 ... d ) --> C )  ->  ( d  e. 
NN0  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) ) ) )
196195pm2.43a 45 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  NN0  ->  ( A  Fn  ( 1 ... c )  ->  ( A : ( 1 ... c ) --> C  -> 
( ( B  Fn  ( 1 ... d
)  /\  B :
( 1 ... d
) --> C )  -> 
( d  e.  NN0  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) ) )
197196com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( A  Fn  ( 1 ... c )  ->  ( A : ( 1 ... c ) --> C  -> 
( c  e.  NN0  ->  ( ( B  Fn  ( 1 ... d
)  /\  B :
( 1 ... d
) --> C )  -> 
( d  e.  NN0  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) ) )
19847, 197mpcom 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A : ( 1 ... c ) --> C  -> 
( c  e.  NN0  ->  ( ( B  Fn  ( 1 ... d
)  /\  B :
( 1 ... d
) --> C )  -> 
( d  e.  NN0  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) )
19946, 198syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( C  e.  _V  ->  ( A  e.  ( C  ^m  ( 1 ... c
) )  ->  (
c  e.  NN0  ->  ( ( B  Fn  (
1 ... d )  /\  B : ( 1 ... d ) --> C )  ->  ( d  e. 
NN0  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) ) )
200199com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( C  e.  _V  ->  (
c  e.  NN0  ->  ( A  e.  ( C  ^m  ( 1 ... c ) )  -> 
( ( B  Fn  ( 1 ... d
)  /\  B :
( 1 ... d
) --> C )  -> 
( d  e.  NN0  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) ) ) ) ) ) )
201200imp3a 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( C  e.  _V  ->  (
( c  e.  NN0  /\  A  e.  ( C  ^m  ( 1 ... c ) ) )  ->  ( ( B  Fn  ( 1 ... d )  /\  B : ( 1 ... d ) --> C )  ->  ( d  e. 
NN0  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) )
202201com25 85 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( C  e.  _V  ->  ( C  e.  _V  ->  ( ( B  Fn  (
1 ... d )  /\  B : ( 1 ... d ) --> C )  ->  ( d  e. 
NN0  ->  ( ( c  e.  NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) )
203202pm2.43i 43 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( C  e.  _V  ->  (
( B  Fn  (
1 ... d )  /\  B : ( 1 ... d ) --> C )  ->  ( d  e. 
NN0  ->  ( ( c  e.  NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) )
204203exp3acom3r 1360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( B  Fn  ( 1 ... d )  ->  ( B : ( 1 ... d ) --> C  -> 
( C  e.  _V  ->  ( d  e.  NN0  ->  ( ( c  e. 
NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) )
20543, 204mpcom 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( B : ( 1 ... d ) --> C  -> 
( C  e.  _V  ->  ( d  e.  NN0  ->  ( ( c  e. 
NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) )
20642, 205syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( C  e.  _V  ->  ( B  e.  ( C  ^m  ( 1 ... d
) )  ->  ( C  e.  _V  ->  ( d  e.  NN0  ->  ( ( c  e.  NN0  /\  A  e.  ( C  ^m  ( 1 ... c ) ) )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) ) )
207206pm2.43a 45 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( C  e.  _V  ->  ( B  e.  ( C  ^m  ( 1 ... d
) )  ->  (
d  e.  NN0  ->  ( ( c  e.  NN0  /\  A  e.  ( C  ^m  ( 1 ... c ) ) )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) )
208207com4l 78 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B  e.  ( C  ^m  ( 1 ... d
) )  ->  (
d  e.  NN0  ->  ( ( c  e.  NN0  /\  A  e.  ( C  ^m  ( 1 ... c ) ) )  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) ) )
209208impcom 419 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( d  e.  NN0  /\  B  e.  ( C  ^m  ( 1 ... d
) ) )  -> 
( ( c  e. 
NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) ) ) ) )
2102093imp1 1164 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( d  e. 
NN0  /\  B  e.  ( C  ^m  (
1 ... d ) ) )  /\  ( c  e.  NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( C  ^m  ( 1 ... ( c  +  d ) ) ) )
211 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  ( c  +  d )  ->  (
1 ... b )  =  ( 1 ... (
c  +  d ) ) )
212211oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  ( c  +  d )  ->  ( C  ^m  ( 1 ... b ) )  =  ( C  ^m  (
1 ... ( c  +  d ) ) ) )
213212eleq2d 2350 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  ( c  +  d )  ->  (
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) )  <->  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) ) )
214213rspcev 2884 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( c  +  d )  e.  NN0  /\  ( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... (
c  +  d ) ) ) )  ->  E. b  e.  NN0  ( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) )
21539, 210, 214syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( d  e. 
NN0  /\  B  e.  ( C  ^m  (
1 ... d ) ) )  /\  ( c  e.  NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  /\  C  e. 
_V )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) )
2162153exp1 1167 . . . . . . . . . . . . . . . . . . 19  |-  ( ( d  e.  NN0  /\  B  e.  ( C  ^m  ( 1 ... d
) ) )  -> 
( ( c  e. 
NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) ) ) ) )
217216rexlimiva 2662 . . . . . . . . . . . . . . . . . 18  |-  ( E. d  e.  NN0  B  e.  ( C  ^m  (
1 ... d ) )  ->  ( ( c  e.  NN0  /\  A  e.  ( C  ^m  (
1 ... c ) ) )  ->  ( C  e.  _V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) ) ) ) )
21834, 217sylbi 187 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  ->  (
( c  e.  NN0  /\  A  e.  ( C  ^m  ( 1 ... c ) ) )  ->  ( C  e. 
_V  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) ) ) ) )
219218com3l 75 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  NN0  /\  A  e.  ( C  ^m  ( 1 ... c
) ) )  -> 
( C  e.  _V  ->  ( B  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a ) )  -> 
( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  E. b  e.  NN0  ( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) ) ) ) )
220219rexlimiva 2662 . . . . . . . . . . . . . . 15  |-  ( E. c  e.  NN0  A  e.  ( C  ^m  (
1 ... c ) )  ->  ( C  e. 
_V  ->  ( B  e. 
U_ a  e.  NN0  ( C  ^m  (
1 ... a ) )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) ) ) ) )
22128, 220sylbi 187 . . . . . . . . . . . . . 14  |-  ( A  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  ->  ( C  e.  _V  ->  ( B  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) )  ->  (
( A  =/=  (/)  /\  B  =/=  (/) )  ->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) ) ) ) )
222221com12 27 . . . . . . . . . . . . 13  |-  ( C  e.  _V  ->  ( A  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  ->  ( B  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  ->  (
( A  =/=  (/)  /\  B  =/=  (/) )  ->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) ) ) ) )
2232223imp1 1164 . . . . . . . . . . . 12  |-  ( ( ( C  e.  _V  /\  A  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) )  /\  B  e.  U_ a  e.  NN0  ( C  ^m  (
1 ... a ) ) )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) )
224 oveq2 5866 . . . . . . . . . . . . . . . 16  |-  ( a  =  b  ->  (
1 ... a )  =  ( 1 ... b
) )
225224oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( a  =  b  ->  ( C  ^m  ( 1 ... a ) )  =  ( C  ^m  (
1 ... b ) ) )
226225cbviunv 3941 . . . . . . . . . . . . . 14  |-  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) )  =  U_ b  e.  NN0  ( C  ^m  ( 1 ... b ) )
227226eleq2i 2347 . . . . . . . . . . . . 13  |-  ( ( A  u.  ( a  e.  ( ( (
# `  A )  +  1 ) ... ( ( # `  A
)  +  ( # `  B ) ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a ) )  <->  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  U_ b  e. 
NN0  ( C  ^m  ( 1 ... b
) ) )
228 eliun 3909 . . . . . . . . . . . . 13  |-  ( ( A  u.  ( a  e.  ( ( (
# `  A )  +  1 ) ... ( ( # `  A
)  +  ( # `  B ) ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  U_ b  e.  NN0  ( C  ^m  ( 1 ... b ) )  <->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) )
229227, 228bitri 240 . . . . . . . . . . . 12  |-  ( ( A  u.  ( a  e.  ( ( (
# `  A )  +  1 ) ... ( ( # `  A
)  +  ( # `  B ) ) ) 
|->  ( B `  (
a  -  ( # `  A ) ) ) ) )  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a ) )  <->  E. b  e.  NN0  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( C  ^m  ( 1 ... b
) ) )
230223, 229sylibr 203 . . . . . . . . . . 11  |-  ( ( ( C  e.  _V  /\  A  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) )  /\  B  e.  U_ a  e.  NN0  ( C  ^m  (
1 ... a ) ) )  /\  ( A  =/=  (/)  /\  B  =/=  (/) ) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) ) )
2312303exp1 1167 . . . . . . . . . 10  |-  ( C  e.  _V  ->  ( A  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  ->  ( B  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) )  ->  (
( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) ) ) ) ) )
232 eleq2 2344 . . . . . . . . . . 11  |-  ( (
Kleene `  C )  = 
U_ a  e.  NN0  ( C  ^m  (
1 ... a ) )  ->  ( A  e.  ( Kleene `  C )  <->  A  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) ) ) )
233 eleq2 2344 . . . . . . . . . . . 12  |-  ( (
Kleene `  C )  = 
U_ a  e.  NN0  ( C  ^m  (
1 ... a ) )  ->  ( B  e.  ( Kleene `  C )  <->  B  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) ) ) )
234 eleq2 2344 . . . . . . . . . . . . 13  |-  ( (
Kleene `  C )  = 
U_ a  e.  NN0  ( C  ^m  (
1 ... a ) )  ->  ( ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( Kleene `  C )  <->  ( A  u.  ( a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) ) ) )
235234imbi2d 307 . . . . . . . . . . . 12  |-  ( (
Kleene `  C )  = 
U_ a  e.  NN0  ( C  ^m  (
1 ... a ) )  ->  ( ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( Kleene `  C ) )  <->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a
) ) ) ) )
236233, 235imbi12d 311 . . . . . . . . . . 11  |-  ( (
Kleene `  C )  = 
U_ a  e.  NN0  ( C  ^m  (
1 ... a ) )  ->  ( ( B  e.  ( Kleene `  C
)  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  ->  ( A  u.  ( a  e.  ( ( ( # `  A )  +  1 ) ... ( (
# `  A )  +  ( # `  B
) ) )  |->  ( B `  ( a  -  ( # `  A
) ) ) ) )  e.  ( Kleene `  C ) ) )  <-> 
( B  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a ) )  -> 
( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  U_ a  e. 
NN0  ( C  ^m  ( 1 ... a
) ) ) ) ) )
237232, 236imbi12d 311 . . . . . . . . . 10  |-  ( (
Kleene `  C )  = 
U_ a  e.  NN0  ( C  ^m  (
1 ... a ) )  ->  ( ( A  e.  ( Kleene `  C
)  ->  ( B  e.  ( Kleene `  C )  ->  ( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
( A  u.  (
a  e.  ( ( ( # `  A
)  +  1 ) ... ( ( # `  A )  +  (
# `  B )
) )  |->  ( B `
 ( a  -  ( # `  A ) ) ) ) )  e.  ( Kleene `  C
) ) ) )  <-> 
( A  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a ) )  -> 
( B  e.  U_ a  e.  NN0  ( C  ^m  ( 1 ... a ) )  -> 
( ( A  =/=  (/)  /\  B  =/=  (/) )  -> 
(