Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fdc Structured version   Unicode version

Theorem fdc 26487
Description: Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010.)
Hypotheses
Ref Expression
fdc.1  |-  A  e. 
_V
fdc.2  |-  M  e.  ZZ
fdc.3  |-  Z  =  ( ZZ>= `  M )
fdc.4  |-  N  =  ( M  +  1 )
fdc.5  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( ph 
<->  ps ) )
fdc.6  |-  ( b  =  ( f `  k )  ->  ( ps 
<->  ch ) )
fdc.7  |-  ( a  =  ( f `  n )  ->  ( th 
<->  ta ) )
fdc.8  |-  ( et 
->  C  e.  A
)
fdc.9  |-  ( et 
->  R  Fr  A
)
fdc.10  |-  ( ( et  /\  a  e.  A )  ->  ( th  \/  E. b  e.  A  ph ) )
fdc.11  |-  ( ( ( et  /\  ph )  /\  ( a  e.  A  /\  b  e.  A ) )  -> 
b R a )
Assertion
Ref Expression
fdc  |-  ( et 
->  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  C  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) )
Distinct variable groups:    C, f, n    A, a, b, f, n    M, a, b, f, k, n    Z, a, b, n    N, a, b, f, k, n    R, a, b    ph, f,
k    ps, a    ch, a,
b, n    th, f, n    ta, a, b    et, a, b
Allowed substitution hints:    ph( n, a, b)    ps( f, k, n, b)    ch( f, k)    th( k,
a, b)    ta( f,
k, n)    et( f,
k, n)    A( k)    C( k, a, b)    R( f, k, n)    Z( f,
k)

Proof of Theorem fdc
Dummy variables  c 
d  g  m  x  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fdc.8 . 2  |-  ( et 
->  C  e.  A
)
2 fdc.2 . . . . . . . . . . . . . . . . . . 19  |-  M  e.  ZZ
3 uzid 10531 . . . . . . . . . . . . . . . . . . 19  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
42, 3ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  M  e.  ( ZZ>= `  M )
5 fdc.3 . . . . . . . . . . . . . . . . . 18  |-  Z  =  ( ZZ>= `  M )
64, 5eleqtrri 2515 . . . . . . . . . . . . . . . . 17  |-  M  e.  Z
7 eqid 2442 . . . . . . . . . . . . . . . . . . . . . 22  |-  { <. M ,  a >. }  =  { <. M ,  a
>. }
82elexi 2971 . . . . . . . . . . . . . . . . . . . . . . 23  |-  M  e. 
_V
9 vex 2965 . . . . . . . . . . . . . . . . . . . . . . 23  |-  a  e. 
_V
108, 9fsn 5935 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( {
<. M ,  a >. } : { M } --> { a }  <->  { <. M , 
a >. }  =  { <. M ,  a >. } )
117, 10mpbir 202 . . . . . . . . . . . . . . . . . . . . 21  |-  { <. M ,  a >. } : { M } --> { a }
12 snssi 3966 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  A  ->  { a }  C_  A )
13 fss 5628 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { <. M ,  a
>. } : { M }
--> { a }  /\  { a }  C_  A
)  ->  { <. M , 
a >. } : { M } --> A )
1411, 12, 13sylancr 646 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  A  ->  { <. M ,  a >. } : { M } --> A )
15 fzsn 11125 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
162, 15ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M ... M )  =  { M }
1716feq2i 5615 . . . . . . . . . . . . . . . . . . . 20  |-  ( {
<. M ,  a >. } : ( M ... M ) --> A  <->  { <. M , 
a >. } : { M } --> A )
1814, 17sylibr 205 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  A  ->  { <. M ,  a >. } :
( M ... M
) --> A )
1918adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  { <. M , 
a >. } : ( M ... M ) --> A )
208, 9fvsn 5955 . . . . . . . . . . . . . . . . . . 19  |-  ( {
<. M ,  a >. } `  M )  =  a
2120a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  ( { <. M ,  a >. } `  M )  =  a )
22 simpr 449 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  th )
23 snex 4434 . . . . . . . . . . . . . . . . . . 19  |-  { <. M ,  a >. }  e.  _V
24 feq1 5605 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  { <. M , 
a >. }  ->  (
f : ( M ... M ) --> A  <->  { <. M ,  a
>. } : ( M ... M ) --> A ) )
25 fveq1 5756 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  { <. M , 
a >. }  ->  (
f `  M )  =  ( { <. M ,  a >. } `  M ) )
2625eqeq1d 2450 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  { <. M , 
a >. }  ->  (
( f `  M
)  =  a  <->  ( { <. M ,  a >. } `  M )  =  a ) )
2725, 20syl6eq 2490 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  { <. M , 
a >. }  ->  (
f `  M )  =  a )
28 sbceq2a 3178 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  M )  =  a  ->  ( [. ( f `  M
)  /  a ]. th 
<->  th ) )
2927, 28syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  { <. M , 
a >. }  ->  ( [. ( f `  M
)  /  a ]. th 
<->  th ) )
3026, 29anbi12d 693 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  { <. M , 
a >. }  ->  (
( ( f `  M )  =  a  /\  [. ( f `
 M )  / 
a ]. th )  <->  ( ( { <. M ,  a
>. } `  M )  =  a  /\  th ) ) )
3124, 30anbi12d 693 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  { <. M , 
a >. }  ->  (
( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) )  <->  ( { <. M ,  a >. } : ( M ... M ) --> A  /\  ( ( { <. M ,  a >. } `  M )  =  a  /\  th ) ) ) )
3223, 31spcev 3049 . . . . . . . . . . . . . . . . . 18  |-  ( ( { <. M ,  a
>. } : ( M ... M ) --> A  /\  ( ( {
<. M ,  a >. } `  M )  =  a  /\  th )
)  ->  E. f
( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) )
3319, 21, 22, 32syl12anc 1183 . . . . . . . . . . . . . . . . 17  |-  ( ( a  e.  A  /\  th )  ->  E. f
( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) )
34 oveq2 6118 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( M ... n )  =  ( M ... M
) )
3534feq2d 5610 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  (
f : ( M ... n ) --> A  <-> 
f : ( M ... M ) --> A ) )
36 fvex 5771 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f `
 n )  e. 
_V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( f `  n )  ->  ( th 
<->  ta ) )
3836, 37sbcie 3201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [. ( f `  n
)  /  a ]. th 
<->  ta )
39 fveq2 5757 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  M  ->  (
f `  n )  =  ( f `  M ) )
40 dfsbcq 3169 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f `  n )  =  ( f `  M )  ->  ( [. ( f `  n
)  /  a ]. th 
<-> 
[. ( f `  M )  /  a ]. th ) )
4139, 40syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  M  ->  ( [. ( f `  n
)  /  a ]. th 
<-> 
[. ( f `  M )  /  a ]. th ) )
4238, 41syl5bbr 252 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( ta 
<-> 
[. ( f `  M )  /  a ]. th ) )
4342anbi2d 686 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  (
( ( f `  M )  =  a  /\  ta )  <->  ( (
f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) )
44 oveq2 6118 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  M  ->  ( N ... n )  =  ( N ... M
) )
45 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  N  =  ( M  +  1 )
4645oveq1i 6120 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N ... M )  =  ( ( M  + 
1 ) ... M
)
472zrei 10319 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  M  e.  RR
4847ltp1i 9945 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  M  < 
( M  +  1 )
49 peano2z 10349 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( M  e.  ZZ  ->  ( M  +  1 )  e.  ZZ )
502, 49ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( M  +  1 )  e.  ZZ
51 fzn 11102 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( M  +  1 )  e.  ZZ  /\  M  e.  ZZ )  ->  ( M  <  ( M  +  1 )  <-> 
( ( M  + 
1 ) ... M
)  =  (/) ) )
5250, 2, 51mp2an 655 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  <  ( M  + 
1 )  <->  ( ( M  +  1 ) ... M )  =  (/) )
5348, 52mpbi 201 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( M  +  1 ) ... M )  =  (/)
5446, 53eqtri 2462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N ... M )  =  (/)
5544, 54syl6eq 2490 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( N ... n )  =  (/) )
5655raleqdv 2916 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  ( A. k  e.  ( N ... n ) ch  <->  A. k  e.  (/)  ch )
)
5735, 43, 563anbi123d 1255 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  M  ->  (
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  a  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  ( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. ( f `
 M )  / 
a ]. th )  /\  A. k  e.  (/)  ch )
) )
58 ral0 3756 . . . . . . . . . . . . . . . . . . . . 21  |-  A. k  e.  (/)  ch
59 df-3an 939 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f : ( M ... M ) --> A  /\  ( ( f `
 M )  =  a  /\  [. (
f `  M )  /  a ]. th )  /\  A. k  e.  (/)  ch )  <->  ( (
f : ( M ... M ) --> A  /\  ( ( f `
 M )  =  a  /\  [. (
f `  M )  /  a ]. th ) )  /\  A. k  e.  (/)  ch )
)
6058, 59mpbiran2 887 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f : ( M ... M ) --> A  /\  ( ( f `
 M )  =  a  /\  [. (
f `  M )  /  a ]. th )  /\  A. k  e.  (/)  ch )  <->  ( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. ( f `
 M )  / 
a ]. th ) ) )
6157, 60syl6bb 254 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  M  ->  (
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  a  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  ( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. ( f `
 M )  / 
a ]. th ) ) ) )
6261exbidv 1637 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  M  ->  ( E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  a  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  E. f
( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) ) )
6362rspcev 3058 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  Z  /\  E. f ( f : ( M ... M
) --> A  /\  (
( f `  M
)  =  a  /\  [. ( f `  M
)  /  a ]. th ) ) )  ->  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  a  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) )
646, 33, 63sylancr 646 . . . . . . . . . . . . . . . 16  |-  ( ( a  e.  A  /\  th )  ->  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  a  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) )
6564adantll 696 . . . . . . . . . . . . . . 15  |-  ( ( ( et  /\  a  e.  A )  /\  th )  ->  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  a  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) )
6665a1d 24 . . . . . . . . . . . . . 14  |-  ( ( ( et  /\  a  e.  A )  /\  th )  ->  ( A. d  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  -.  d R a  ->  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  a  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
67 fdc.11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( et  /\  ph )  /\  ( a  e.  A  /\  b  e.  A ) )  -> 
b R a )
68 breq1 4240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  b  ->  (
d R a  <->  b R
a ) )
6968rspcev 3058 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  e.  ( A 
\  { c  e.  A  |  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  /\  b R a )  ->  E. d  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) d R a )
7069expcom 426 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b R a  ->  (
b  e.  ( A 
\  { c  e.  A  |  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  ->  E. d  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) d R a ) )
7167, 70syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( et  /\  ph )  /\  ( a  e.  A  /\  b  e.  A ) )  -> 
( b  e.  ( A  \  { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  ->  E. d  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) d R a ) )
72 dfrex2 2724 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. d  e.  ( A 
\  { c  e.  A  |  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) d R a  <->  -.  A. d  e.  ( A  \  { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  -.  d R a )
7371, 72syl6ib 219 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( et  /\  ph )  /\  ( a  e.  A  /\  b  e.  A ) )  -> 
( b  e.  ( A  \  { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  ->  -.  A. d  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  -.  d R a ) )
7473con2d 110 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( et  /\  ph )  /\  ( a  e.  A  /\  b  e.  A ) )  -> 
( A. d  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  -.  d R a  ->  -.  b  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) ) )
75 eldif 3316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  e.  ( A  \ 
( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) )  <->  ( b  e.  A  /\  -.  b  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) ) )
7675simplbi2 610 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  e.  A  ->  ( -.  b  e.  ( A  \  { c  e.  A  |  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  ->  b  e.  ( A  \  ( A  \  { c  e.  A  |  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) ) ) )
77 ssrab2 3414 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } 
C_  A
78 dfss4 3560 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } 
C_  A  <->  ( A  \  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) )  =  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )
7977, 78mpbi 201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A 
\  ( A  \  { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) )  =  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) }
8079eleq2i 2506 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  e.  ( A  \ 
( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) )  <->  b  e.  { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )
81 eqeq2 2451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  b  ->  (
( f `  M
)  =  c  <->  ( f `  M )  =  b ) )
8281anbi1d 687 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  b  ->  (
( ( f `  M )  =  c  /\  ta )  <->  ( (
f `  M )  =  b  /\  ta )
) )
83823anbi2d 1260 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  b  ->  (
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  ( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n ) ch ) ) )
8483exbidv 1637 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  =  b  ->  ( E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
8584rexbidv 2732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  =  b  ->  ( E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
8685elrab3 3099 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  e.  A  ->  (
b  e.  { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) }  <->  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
8780, 86syl5bb 250 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  e.  A  ->  (
b  e.  ( A 
\  ( A  \  { c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } ) )  <->  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
8876, 87sylibd 207 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  A  ->  ( -.  b  e.  ( A  \  { c  e.  A  |  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  ->  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
8988ad2antll 711 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( et  /\  ph )  /\  ( a  e.  A  /\  b  e.  A ) )  -> 
( -.  b  e.  ( A  \  {
c  e.  A  |  E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  c  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) } )  ->  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
90 oveq2 6118 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( M ... n )  =  ( M ... m
) )
9190feq2d 5610 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
f : ( M ... n ) --> A  <-> 
f : ( M ... m ) --> A ) )
92 fveq2 5757 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
f `  n )  =  ( f `  m ) )
93 dfsbcq 3169 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f `  n )  =  ( f `  m )  ->  ( [. ( f `  n
)  /  a ]. th 
<-> 
[. ( f `  m )  /  a ]. th ) )
9492, 93syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  m  ->  ( [. ( f `  n
)  /  a ]. th 
<-> 
[. ( f `  m )  /  a ]. th ) )
9538, 94syl5bbr 252 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( ta 
<-> 
[. ( f `  m )  /  a ]. th ) )
9695anbi2d 686 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
( ( f `  M )  =  b  /\  ta )  <->  ( (
f `  M )  =  b  /\  [. (
f `  m )  /  a ]. th ) ) )
97 oveq2 6118 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( N ... n )  =  ( N ... m
) )
9897raleqdv 2916 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  ( A. k  e.  ( N ... n ) ch  <->  A. k  e.  ( N ... m ) ch ) )
9991, 96, 983anbi123d 1255 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  m  ->  (
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  ( f : ( M ... m ) --> A  /\  ( ( f `  M )  =  b  /\  [. ( f `
 m )  / 
a ]. th )  /\  A. k  e.  ( N ... m ) ch ) ) )
10099exbidv 1637 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  ( E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  E. f
( f : ( M ... m ) --> A  /\  ( ( f `  M )  =  b  /\  [. (
f `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) ch ) ) )
101100cbvrexv 2939 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  E. m  e.  Z  E. f
( f : ( M ... m ) --> A  /\  ( ( f `  M )  =  b  /\  [. (
f `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) ch ) )
102 feq1 5605 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  g  ->  (
f : ( M ... m ) --> A  <-> 
g : ( M ... m ) --> A ) )
103 fveq1 5756 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  (
f `  M )  =  ( g `  M ) )
104103eqeq1d 2450 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  (
( f `  M
)  =  b  <->  ( g `  M )  =  b ) )
105 fveq1 5756 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  (
f `  m )  =  ( g `  m ) )
106 dfsbcq 3169 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f `  m )  =  ( g `  m )  ->  ( [. ( f `  m
)  /  a ]. th 
<-> 
[. ( g `  m )  /  a ]. th ) )
107105, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  ( [. ( f `  m
)  /  a ]. th 
<-> 
[. ( g `  m )  /  a ]. th ) )
108104, 107anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  g  ->  (
( ( f `  M )  =  b  /\  [. ( f `
 m )  / 
a ]. th )  <->  ( (
g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th ) ) )
109 fvex 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 ( k  - 
1 ) )  e. 
_V
110 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( ph 
<->  ps ) )
111110sbcbidv 3224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( [. ( f `  k
)  /  b ]. ph  <->  [. ( f `  k
)  /  b ]. ps ) )
112109, 111sbcie 3201 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( f `  k
)  /  b ]. ps )
113 fvex 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 k )  e. 
_V
114 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  =  ( f `  k )  ->  ( ps 
<->  ch ) )
115113, 114sbcie 3201 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( [. ( f `  k
)  /  b ]. ps 
<->  ch )
116112, 115bitri 242 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  ch )
117 fveq1 5756 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  =  g  ->  (
f `  ( k  -  1 ) )  =  ( g `  ( k  -  1 ) ) )
118 dfsbcq 3169 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f `  ( k  -  1 ) )  =  ( g `  ( k  -  1 ) )  ->  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph ) )
119117, 118syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  g  ->  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph ) )
120 fveq1 5756 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f  =  g  ->  (
f `  k )  =  ( g `  k ) )
121 dfsbcq 3169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f `  k )  =  ( g `  k )  ->  ( [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  k
)  /  b ]. ph ) )
122120, 121syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  =  g  ->  ( [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  k
)  /  b ]. ph ) )
123122sbcbidv 3224 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  g  ->  ( [. ( g `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )
124119, 123bitrd 246 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )
125116, 124syl5bbr 252 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  ( ch 
<-> 
[. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )
126125ralbidv 2731 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  g  ->  ( A. k  e.  ( N ... m ) ch  <->  A. k  e.  ( N ... m ) [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )
127102, 108, 1263anbi123d 1255 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  g  ->  (
( f : ( M ... m ) --> A  /\  ( ( f `  M )  =  b  /\  [. (
f `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) ch )  <->  ( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  b  /\  [. ( g `
 m )  / 
a ]. th )  /\  A. k  e.  ( N ... m ) [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) ) )
128127cbvexv 1988 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. f ( f : ( M ... m
) --> A  /\  (
( f `  M
)  =  b  /\  [. ( f `  m
)  /  a ]. th )  /\  A. k  e.  ( N ... m
) ch )  <->  E. g
( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )
129128rexbii 2736 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. m  e.  Z  E. f ( f : ( M ... m
) --> A  /\  (
( f `  M
)  =  b  /\  [. ( f `  m
)  /  a ]. th )  /\  A. k  e.  ( N ... m
) ch )  <->  E. m  e.  Z  E. g
( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )
130101, 129bitri 242 . . . . . . . . . . . . . . . . . . 19  |-  ( E. n  e.  Z  E. f ( f : ( M ... n
) --> A  /\  (
( f `  M
)  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch )  <->  E. m  e.  Z  E. g
( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )
1315peano2uzs 10562 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  Z )
132131ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( et 
/\  ph )  /\  (
a  e.  A  /\  b  e.  A )
)  /\  m  e.  Z )  /\  (
g : ( M ... m ) --> A  /\  ( ( g `
 M )  =  b  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )  -> 
( m  +  1 )  e.  Z )
133 sbceq2a 3178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d  =  b  ->  ( [. d  /  b ]. ph  <->  ph ) )
134133anbi1d 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  =  b  ->  (
( [. d  /  b ]. ph  /\  a  e.  A )  <->  ( ph  /\  a  e.  A ) ) )
135134anbi1d 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( d  =  b  ->  (
( ( [. d  /  b ]. ph  /\  a  e.  A )  /\  m  e.  Z
)  <->  ( ( ph  /\  a  e.  A )  /\  m  e.  Z
) ) )
136 eqeq2 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( d  =  b  ->  (
( g `  M
)  =  d  <->  ( g `  M )  =  b ) )
137136anbi1d 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d  =  b  ->  (
( ( g `  M )  =  d  /\  [. ( g `
 m )  / 
a ]. th )  <->  ( (
g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th ) ) )
1381373anbi2d 1260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  =  b  ->  (
( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  d  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  <->  ( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  b  /\  [. ( g `
 m )  / 
a ]. th )  /\  A. k  e.  ( N ... m ) [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) ) )
139138imbi1d 310 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( d  =  b  ->  (
( ( g : ( M ... m
) --> A  /\  (
( g `  M
)  =  d  /\  [. ( g `  m
)  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  ->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) )  <-> 
( ( g : ( M ... m
) --> A  /\  (
( g `  M
)  =  b  /\  [. ( g `  m
)  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  ->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) ) ) )
140135, 139imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( d  =  b  ->  (
( ( ( [. d  /  b ]. ph  /\  a  e.  A )  /\  m  e.  Z
)  ->  ( (
g : ( M ... m ) --> A  /\  ( ( g `
 M )  =  d  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  ->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) ) )  <->  ( ( (
ph  /\  a  e.  A )  /\  m  e.  Z )  ->  (
( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  ->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) ) ) ) )
141 sbceq2a 3178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  ( [. c  /  a ]. [. d  /  b ]. ph  <->  [. d  /  b ]. ph ) )
142 eleq1 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  (
c  e.  A  <->  a  e.  A ) )
143141, 142anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  <->  ( [. d  /  b ]. ph  /\  a  e.  A )
) )
144143anbi1d 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( ( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  /\  m  e.  Z
)  <->  ( ( [. d  /  b ]. ph  /\  a  e.  A )  /\  m  e.  Z
) ) )
145 eqeq2 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  =  a  ->  (
( f `  M
)  =  c  <->  ( f `  M )  =  a ) )
146145anbi1d 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( c  =  a  ->  (
( ( f `  M )  =  c  /\  [. ( f `
 ( m  + 
1 ) )  / 
a ]. th )  <->  ( (
f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th ) ) )
1471463anbi2d 1260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  (
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  c  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch )  <->  ( f : ( M ... ( m  +  1
) ) --> A  /\  ( ( f `  M )  =  a  /\  [. ( f `
 ( m  + 
1 ) )  / 
a ]. th )  /\  A. k  e.  ( N ... ( m  + 
1 ) ) ch ) ) )
148147exbidv 1637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  ( E. f ( f : ( M ... (
m  +  1 ) ) --> A  /\  (
( f `  M
)  =  c  /\  [. ( f `  (
m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch )  <->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) ) )
149148imbi2d 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( ( g : ( M ... m
) --> A  /\  (
( g `  M
)  =  d  /\  [. ( g `  m
)  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  ->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  c  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) )  <-> 
( ( g : ( M ... m
) --> A  /\  (
( g `  M
)  =  d  /\  [. ( g `  m
)  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  ->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) ) ) )
150144, 149imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  a  ->  (
( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  /\  m  e.  Z
)  ->  ( (
g : ( M ... m ) --> A  /\  ( ( g `
 M )  =  d  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  ->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  c  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) ) )  <->  ( ( (
[. d  /  b ]. ph  /\  a  e.  A )  /\  m  e.  Z )  ->  (
( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  d  /\  [. (
g `  m )  /  a ]. th )  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph )  ->  E. f
( f : ( M ... ( m  +  1 ) ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th )  /\  A. k  e.  ( N ... (
m  +  1 ) ) ch ) ) ) ) )
151 peano2uz 10561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( ZZ>= `  M )
)
152151, 5eleq2s 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  M
) )
153 elfzp12 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( m  +  1 )  e.  ( ZZ>= `  M
)  ->  ( x  e.  ( M ... (
m  +  1 ) )  <->  ( x  =  M  \/  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) ) )
154152, 153syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  (
x  e.  ( M ... ( m  + 
1 ) )  <->  ( x  =  M  \/  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) ) )
155154ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  e.  ( M ... ( m  +  1 ) )  <-> 
( x  =  M  \/  x  e.  ( ( M  +  1 ) ... ( m  +  1 ) ) ) ) )
156 iftrue 3769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  c )
157156eleq1d 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  M  ->  ( if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A  <->  c  e.  A ) )
158157biimprcd 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  A  ->  (
x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A ) )
159158ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) )  e.  A ) )
160 1re 9121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  1  e.  RR
16147, 160readdcli 9134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( M  +  1 )  e.  RR
16247, 161ltnlei 9225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( M  <  ( M  + 
1 )  <->  -.  ( M  +  1 )  <_  M )
16348, 162mpbi 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  -.  ( M  +  1 )  <_  M
164 eleq1 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  M  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  <->  M  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )
165 elfzle1 11091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( M  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  ( M  +  1 )  <_  M )
166164, 165syl6bi 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  =  M  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( M  +  1 )  <_  M )
)
167166com12 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  (
x  =  M  -> 
( M  +  1 )  <_  M )
)
168163, 167mtoi 172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  -.  x  =  M )
169168adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  -.  x  =  M )
170 iffalse 3770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( -.  x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  ( g `
 ( x  - 
1 ) ) )
171169, 170syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  ( g `
 ( x  - 
1 ) ) )
172 elfzelz 11090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  x  e.  ZZ )
173172adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  x  e.  ZZ )
174 eluzelz 10527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( m  e.  ( ZZ>= `  M
)  ->  m  e.  ZZ )
175174, 5eleq2s 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( m  e.  Z  ->  m  e.  ZZ )
176175peano2zd 10409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ZZ )
177 1z 10342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  1  e.  ZZ
178 fzsubel 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( M  + 
1 )  e.  ZZ  /\  ( m  +  1 )  e.  ZZ )  /\  ( x  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  <-> 
( x  -  1 )  e.  ( ( ( M  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) )
179178biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( ( M  + 
1 )  e.  ZZ  /\  ( m  +  1 )  e.  ZZ )  /\  ( x  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  ( x  - 
1 )  e.  ( ( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) ) ) )
180177, 179mpanr2 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( ( M  + 
1 )  e.  ZZ  /\  ( m  +  1 )  e.  ZZ )  /\  x  e.  ZZ )  ->  ( x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) )  ->  ( x  -  1 )  e.  ( ( ( M  +  1 )  - 
1 ) ... (
( m  +  1 )  -  1 ) ) ) )
18150, 180mpanl1 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( m  +  1 )  e.  ZZ  /\  x  e.  ZZ )  ->  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  ( x  - 
1 )  e.  ( ( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) ) ) )
182181ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  +  1 )  e.  ZZ  ->  (
x  e.  ZZ  ->  ( x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( x  -  1 )  e.  ( ( ( M  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
183176, 182syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
x  e.  ZZ  ->  ( x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( x  -  1 )  e.  ( ( ( M  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
184183com23 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( x  e.  ZZ  ->  ( x  -  1 )  e.  ( ( ( M  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
185184imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( x  e.  ZZ  ->  ( x  -  1 )  e.  ( ( ( M  +  1 )  - 
1 ) ... (
( m  +  1 )  -  1 ) ) ) )
186173, 185mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( x  - 
1 )  e.  ( ( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) ) )
18747recni 9133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  M  e.  CC
188 ax-1cn 9079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  1  e.  CC
189 pncan 9342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( M  e.  CC  /\  1  e.  CC )  ->  ( ( M  + 
1 )  -  1 )  =  M )
190187, 188, 189mp2an 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( M  +  1 )  -  1 )  =  M
191190a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
( M  +  1 )  -  1 )  =  M )
192175zcnd 10407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  m  e.  CC )
193 pncan 9342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  CC  /\  1  e.  CC )  ->  ( ( m  + 
1 )  -  1 )  =  m )
194192, 188, 193sylancl 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
( m  +  1 )  -  1 )  =  m )
195191, 194oveq12d 6128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( m  e.  Z  ->  (
( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) )  =  ( M ... m ) )
196195adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( ( ( M  +  1 )  -  1 ) ... ( ( m  + 
1 )  -  1 ) )  =  ( M ... m ) )
197186, 196eleqtrd 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( x  - 
1 )  e.  ( M ... m ) )
198 ffvelrn 5897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( g : ( M ... m ) --> A  /\  ( x  - 
1 )  e.  ( M ... m ) )  ->  ( g `  ( x  -  1 ) )  e.  A
)
199197, 198sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( g : ( M ... m ) --> A  /\  ( m  e.  Z  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )  -> 
( g `  (
x  -  1 ) )  e.  A )
200199anassrs 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( g : ( M ... m ) --> A  /\  m  e.  Z )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  (
g `  ( x  -  1 ) )  e.  A )
201200ancom1s 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  (
g `  ( x  -  1 ) )  e.  A )
202171, 201eqeltrd 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A )
203202ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  ->  ( x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) )  ->  if (
x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) )  e.  A ) )
204203adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) )  e.  A ) )
205159, 204jaod 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( ( x  =  M  \/  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A ) )
206155, 205sylbid 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  e.  ( M ... ( m  +  1 ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) )  e.  A ) )
207206ralrimiv 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  ->  A. x  e.  ( M ... ( m  + 
1 ) ) if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A )
208 eqid 2442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( M ... ( m  +  1
) )  |->  if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) ) )  =  ( x  e.  ( M ... ( m  +  1
) )  |->  if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) ) )
209208fmpt 5919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A. x  e.  ( M ... ( m  +  1 ) ) if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) )  e.  A  <->  ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) : ( M ... ( m  +  1
) ) --> A )
210207, 209sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) : ( M ... (
m  +  1 ) ) --> A )
211210adantlll 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) : ( M ... (
m  +  1 ) ) --> A )
2122113ad2antr1 1123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  /\  m  e.  Z
)  /\  ( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  d  /\  [. ( g `
 m )  / 
a ]. th )  /\  A. k  e.  ( N ... m ) [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )  ->  (
x  e.  ( M ... ( m  + 
1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) ) ) : ( M ... ( m  +  1 ) ) --> A )
213 eluzfz1 11095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( m  +  1 )  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... ( m  +  1 ) ) )
214151, 213syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... ( m  +  1 ) ) )
215214, 5eleq2s 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  e.  Z  ->  M  e.  ( M ... (
m  +  1 ) ) )
216 vex 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  c  e. 
_V
217156, 208, 216fvmpt 5835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( M  e.  ( M ... ( m  +  1
) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M )  =  c )
218215, 217syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M )  =  c )
219218ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  /\  m  e.  Z
)  /\  ( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  d  /\  [. ( g `
 m )  / 
a ]. th )  /\  A. k  e.  ( N ... m ) [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M )  =  c )
220 eluzfz2 11096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  +  1 )  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( M ... (
m  +  1 ) ) )
221151, 220syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( M ... (
m  +  1 ) ) )
222221, 5eleq2s 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( M ... ( m  +  1
) ) )
223 eqeq1 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  ( m  + 
1 )  ->  (
x  =  M  <->  ( m  +  1 )  =  M ) )
224 oveq1 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  ( m  + 
1 )  ->  (
x  -  1 )  =  ( ( m  +  1 )  - 
1 ) )
225224fveq2d 5761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  ( m  + 
1 )  ->  (
g `  ( x  -  1 ) )  =  ( g `  ( ( m  + 
1 )  -  1 ) ) )
226223, 225ifbieq2d 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( m  + 
1 )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  if ( ( m  +  1 )  =  M , 
c ,  ( g `
 ( ( m  +  1 )  - 
1 ) ) ) )
227 fvex 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g `
 ( ( m  +  1 )  - 
1 ) )  e. 
_V
228216, 227ifex 3821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  if ( ( m  +  1 )  =  M , 
c ,  ( g `
 ( ( m  +  1 )  - 
1 ) ) )  e.  _V
229226, 208, 228fvmpt 5835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( m  +  1 )  e.  ( M ... ( m  +  1
) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  =  if ( ( m  + 
1 )  =  M ,  c ,  ( g `  ( ( m  +  1 )  -  1 ) ) ) )
230222, 229syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  =  if ( ( m  + 
1 )  =  M ,  c ,  ( g `  ( ( m  +  1 )  -  1 ) ) ) )
231 eluzle 10529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  <_  m )
232231, 5eleq2s 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( m  e.  Z  ->  M  <_  m )
233 zleltp1 10357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( M  e.  ZZ  /\  m  e.  ZZ )  ->  ( M  <_  m  <->  M  <  ( m  + 
1 ) ) )
2342, 175, 233sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( m  e.  Z  ->  ( M  <_  m  <->  M  <  ( m  +  1 ) ) )
235232, 234mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( m  e.  Z  ->  M  <  ( m  +  1 ) )
236 ltne 9201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( M  e.  RR  /\  M  <  ( m  + 
1 ) )  -> 
( m  +  1 )  =/=  M )
23747, 235, 236sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  (
m  +  1 )  =/=  M )
238237neneqd 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  -.  ( m  +  1
)  =  M )
239 iffalse 3770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( -.  ( m  +  1 )  =  M  ->  if ( ( m  + 
1 )  =  M ,  c ,  ( g `  ( ( m  +  1 )  -  1 ) ) )  =  ( g `
 ( ( m  +  1 )  - 
1 ) ) )
240238, 239syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  Z  ->  if ( ( m  + 
1 )  =  M ,  c ,  ( g `  ( ( m  +  1 )  -  1 ) ) )  =  ( g `
 ( ( m  +  1 )  - 
1 ) ) )
241194fveq2d 5761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  Z  ->  (
g `  ( (
m  +  1 )  -  1 ) )  =  ( g `  m ) )
242230, 240, 2413eqtrd 2478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  =  ( g `  m ) )
243 dfsbcq 3169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  =  ( g `  m )  ->  ( [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  /  a ]. th  <->  [. ( g `  m )  /  a ]. th ) )
244242, 243syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  e.  Z  ->  ( [. ( ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) `
 ( m  + 
1 ) )  / 
a ]. th  <->  [. ( g `
 m )  / 
a ]. th ) )
245244biimpar 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( m  e.  Z  /\  [. ( g `  m
)  /  a ]. th )  ->  [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  /  a ]. th )
246245ad2ant2l 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  /\  m  e.  Z
)  /\  ( (
g `  M )  =  d  /\  [. (
g `  m )  /  a ]. th ) )  ->  [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  /  a ]. th )
2472463ad2antr2 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  /\  m  e.  Z
)  /\  ( g : ( M ... m ) --> A  /\  ( ( g `  M )  =  d  /\  [. ( g `
 m )  / 
a ]. th )  /\  A. k  e.  ( N ... m ) [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )  ->  [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  /  a ]. th )
248 eluzp1p1 10542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
249248, 5eleq2s 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
25045fveq2i 5760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ZZ>= `  N )  =  (
ZZ>= `  ( M  + 
1 ) )
251249, 250syl6eleqr 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  N
) )
252 elfzp12 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  +  1 )  e.  ( ZZ>= `  N
)  ->  ( j  e.  ( N ... (
m  +  1 ) )  <->  ( j  =  N  \/  j  e.  ( ( N  + 
1 ) ... (
m  +  1 ) ) ) ) )
253251, 252syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( m  e.  Z  ->  (
j  e.  ( N ... ( m  + 
1 ) )  <->  ( j  =  N  \/  j  e.  ( ( N  + 
1 ) ... (
m  +  1 ) ) ) ) )
254253biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  Z  /\  j  e.  ( N ... ( m  +  1 ) ) )  -> 
( j  =  N  \/  j  e.  ( ( N  +  1 ) ... ( m  +  1 ) ) ) )
255254adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( [. c  / 
a ]. [. d  / 
b ]. ph  /\  m  e.  Z )  /\  j  e.  ( N ... (
m  +  1 ) ) )  ->  (
j  =  N  \/  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) ) )
256255adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  m  e.  Z )  /\  ( ( g `  M )  =  d  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )  /\  j  e.  ( N ... ( m  +  1 ) ) )  -> 
( j  =  N  \/  j  e.  ( ( N  +  1 ) ... ( m  +  1 ) ) ) )
257 oveq1 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  =  N  ->  (
j  -  1 )  =  ( N  - 
1 ) )
25845oveq1i 6120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( N  -  1 )  =  ( ( M  + 
1 )  -  1 )
259258, 190eqtri 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( N  -  1 )  =  M
260257, 259syl6eq 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( j  =  N  ->  (
j  -  1 )  =  M )
261260fveq2d 5761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( j  =  N  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( j  -  1 ) )  =  ( ( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M ) )
262261ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( j  -  1 ) )  =  ( ( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M ) )
263218adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M )  =  c )
264262, 263eqtrd 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( j  -  1 ) )  =  c )
265 dfsbcq 3169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( j  -  1 ) )  =  c  ->  ( [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( j  -  1 ) )  /  a ]. [. ( ( x  e.  ( M ... ( m  +  1
) )  |->  if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) ) ) `  j )  /  b ]. ph  <->  [. c  / 
a ]. [. ( ( x  e.  ( M ... ( m  + 
1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) ) ) `  j
)  /  b ]. ph ) )
266264, 265syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  ( [. ( ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) `
 ( j  - 
1 ) )  / 
a ]. [. ( ( x  e.  ( M ... ( m  + 
1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) ) ) `  j
)  /  b ]. ph  <->  [. c  /  a ]. [. ( ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) `
 j )  / 
b ]. ph ) )
26745eqeq2i 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  =  N  <->  j  =  ( M  +  1
) )
268 fveq2 5757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  =  ( M  + 
1 )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  j )  =  ( ( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) ) )
269267, 268sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( j  =  N  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  j )  =  ( ( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) ) )
270269ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  j )  =  ( ( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) ) )
27147, 161, 48ltleii 9227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  M  <_ 
( M  +  1 )
272 eluz2 10525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( M  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( M  +  1 )  e.  ZZ  /\  M  <_ 
( M  +  1 ) ) )
2732, 50, 271, 272mpbir3an 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( M  +  1 )  e.  ( ZZ>= `  M )
274 fzss1 11122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( M  +  1 )  e.  ( ZZ>= `  M
)  ->  ( ( M  +  1 ) ... ( m  + 
1 ) )  C_  ( M ... ( m  +  1 ) ) )
275273, 274ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( M  +  1 ) ... ( m  + 
1 ) )  C_  ( M ... ( m  +  1 ) )
276 eluzfz1 11095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... m ) )
277276, 5eleq2s 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( m  e.  Z  ->  M  e.  ( M ... m
) )
278 fzaddel 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( M  e.  ZZ  /\  m  e.  ZZ )  /\  ( M  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( M  e.  ( M ... m )  <-> 
( M  +  1 )  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) ) )
2792, 177, 278mpanr12 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( M  e.  ZZ  /\  m  e.  ZZ )  ->  ( M  e.  ( M ... m )  <-> 
( M  +  1 )  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) ) )
2802, 175, 279sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( m  e.  Z  ->  ( M  e.  ( M ... m )  <->  ( M  +  1 )  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )
281277, 280mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( m  e.  Z  ->  ( M  +  1 )  e.  ( ( M  +  1 ) ... ( m  +  1 ) ) )
282275, 281sseldi 3332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( m  e.  Z  ->  ( M  +  1 )  e.  ( M ... ( m  +  1
) ) )
283 eqeq1 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  ( M  + 
1 )  ->  (
x  =  M  <->  ( M  +  1 )  =  M ) )
284 oveq1 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  =  ( M  + 
1 )  ->  (
x  -  1 )  =  ( ( M  +  1 )  - 
1 ) )
285284, 190syl6eq 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  ( M  + 
1 )  ->  (
x  -  1 )  =  M )
286285fveq2d 5761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  ( M  + 
1 )  ->  (
g `  ( x  -  1 ) )  =  ( g `  M ) )
287283, 286ifbieq2d 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( x  =  ( M  + 
1 )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) ) )
288 fvex 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( g `
 M )  e. 
_V
289216, 288ifex 3821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) )  e.  _V
290287, 208, 289fvmpt 5835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( M  +  1 )  e.  ( M ... ( m  +  1
) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) )  =  if ( ( M  + 
1 )  =  M ,  c ,  ( g `  M ) ) )
291282, 290syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) )  =  if ( ( M  + 
1 )  =  M ,  c ,  ( g `  M ) ) )
29247, 48gtneii 9216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( M  +  1 )  =/= 
M
293 ifnefalse 3771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( M  +  1 )  =/=  M  ->  if ( ( M  + 
1 )  =  M ,  c ,  ( g `  M ) )  =  ( g `
 M ) )
294292, 293ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) )  =  ( g `  M )
295291, 294syl6eq 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) )  =  ( g `  M ) )
296295adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) )  =  ( g `  M ) )
297 simprl 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
g `  M )  =  d )
298270, 296, 2973eqtrd 2478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  j )  =  d )
299 dfsbcq 3169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  j )  =  d  ->  ( [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  j )  /  b ]. ph  <->  [. d  /  b ]. ph ) )
300298, 299syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  ( [. ( ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) `
 j )  / 
b ]. ph  <->  [. d  / 
b ]. ph ) )
301300sbcbidv 3224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  ( [. c  /  a ]. [. ( ( x  e.  ( M ... ( m  +  1
) )  |->  if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) ) ) `  j )  /  b ]. ph  <->  [. c  / 
a ]. [. d  / 
b ]. ph ) )
302266, 301bitrd 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  ( [. ( ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) `
 ( j  - 
1 ) )  / 
a ]. [. ( ( x  e.  ( M ... ( m  + 
1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) ) ) `  j
)  /  b ]. ph  <->  [. c  /  a ]. [. d  /  b ]. ph ) )
303302biimparc 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
[. c  /  a ]. [. d  /  b ]. ph  /\  ( m  e.  Z  /\  (
( g `  M
)  =  d  /\  j  =  N )
) )  ->  [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( j  -  1 ) )  /  a ]. [. ( ( x  e.  ( M ... ( m  +  1
) )  |->  if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) ) ) `  j )  /  b ]. ph )
304303anassrs 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( [. c  / 
a ]. [. d  / 
b ]. ph  /\  m  e.  Z )  /\  (
( g `  M
)  =  d  /\  j  =  N )
)  ->  [. ( ( x  e.  ( M ... ( m  + 
1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) ) ) `  (
j  -  1 ) )  /  a ]. [. ( ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) `
 j )  / 
b ]. ph )
305304anassrs 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  m  e.  Z )  /\  ( g `  M
)  =  d )  /\  j  =  N )  ->  [. ( ( x  e.  ( M ... ( m  + 
1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) ) ) `  (
j  -  1 ) )  /  a ]. [. ( ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) `
 j )  / 
b ]. ph )
306305adantlrr 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( [. c  /  a ]. [. d  /  b ]. ph  /\  m  e.  Z )  /\  ( ( g `  M )  =  d  /\  A. k  e.  ( N ... m
) [. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )  /\  j  =  N )  ->  [. ( ( x  e.  ( M ... ( m  +  1
) )  |->  if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) ) ) `  ( j  -  1 ) )  /  a ]. [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  j )  /  b ]. ph )
307 elfzelz 11090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( j  e.  ( ( N  +  1 ) ... ( m  +  1 ) )  ->  j  e.  ZZ )
308307adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) )  ->  j  e.  ZZ )
30945, 50eqeltri 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  N  e.  ZZ
310 peano2z 10349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
311309, 310ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( N  +  1 )  e.  ZZ
312 fzsubel 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( ( N  + 
1 )  e.  ZZ  /\  ( m  +  1 )  e.  ZZ )  /\  ( j  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( j  e.  ( ( N  +  1 ) ... ( m  +  1 ) )  <-> 
( j  -  1 )  e.  ( ( ( N  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) )
313312biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( ( N  + 
1 )  e.  ZZ  /\  ( m  +  1 )  e.  ZZ )  /\  ( j  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( j  e.  ( ( N  +  1 ) ... ( m  +  1 ) )  ->  ( j  - 
1 )  e.  ( ( ( N  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) ) ) )
314177, 313mpanr2 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( ( N  + 
1 )  e.  ZZ  /\  ( m  +  1 )  e.  ZZ )  /\  j  e.  ZZ )  ->  ( j  e.  ( ( N  + 
1 ) ... (
m  +  1 ) )  ->  ( j  -  1 )  e.  ( ( ( N  +  1 )  - 
1 ) ... (
( m  +  1 )  -  1 ) ) ) )
315314ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( ( N  +  1 )  e.  ZZ  /\  ( m  +  1
)  e.  ZZ )  ->  ( j  e.  ZZ  ->  ( j  e.  ( ( N  + 
1 ) ... (
m  +  1 ) )  ->  ( j  -  1 )  e.  ( ( ( N  +  1 )  - 
1 ) ... (
( m  +  1 )  -  1 ) ) ) ) )
316311, 176, 315sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
j  e.  ZZ  ->  ( j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) )  -> 
( j  -  1 )  e.  ( ( ( N  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
317316com23 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) )  -> 
( j  e.  ZZ  ->  ( j  -  1 )  e.  ( ( ( N  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
318317imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) )  ->  ( j  e.  ZZ  ->  ( j  -  1 )  e.  ( ( ( N  +  1 )  - 
1 ) ... (
( m  +  1 )  -  1 ) ) ) )
319308, 318mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  Z  /\  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) )  ->  ( j  - 
1 )  e.  ( ( ( N  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) ) )
320309zrei 10319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  N  e.  RR
321320recni 9133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  N  e.  CC
322 pncan 9342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
323321,