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

Theorem fdc 26440
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 10492 . . . . . . . . . . . . . . . . . . 19  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
42, 3ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  M  e.  ( ZZ>= `  M )
5 fdc.3 . . . . . . . . . . . . . . . . . 18  |-  Z  =  ( ZZ>= `  M )
64, 5eleqtrri 2508 . . . . . . . . . . . . . . . . 17  |-  M  e.  Z
7 eqid 2435 . . . . . . . . . . . . . . . . . . . . . 22  |-  { <. M ,  a >. }  =  { <. M ,  a
>. }
82elexi 2957 . . . . . . . . . . . . . . . . . . . . . . 23  |-  M  e. 
_V
9 vex 2951 . . . . . . . . . . . . . . . . . . . . . . 23  |-  a  e. 
_V
108, 9fsn 5898 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( {
<. M ,  a >. } : { M } --> { a }  <->  { <. M , 
a >. }  =  { <. M ,  a >. } )
117, 10mpbir 201 . . . . . . . . . . . . . . . . . . . . 21  |-  { <. M ,  a >. } : { M } --> { a }
12 snssi 3934 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  A  ->  { a }  C_  A )
13 fss 5591 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { <. M ,  a
>. } : { M }
--> { a }  /\  { a }  C_  A
)  ->  { <. M , 
a >. } : { M } --> A )
1411, 12, 13sylancr 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  A  ->  { <. M ,  a >. } : { M } --> A )
15 fzsn 11086 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
162, 15ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M ... M )  =  { M }
1716feq2i 5578 . . . . . . . . . . . . . . . . . . . 20  |-  ( {
<. M ,  a >. } : ( M ... M ) --> A  <->  { <. M , 
a >. } : { M } --> A )
1814, 17sylibr 204 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  A  ->  { <. M ,  a >. } :
( M ... M
) --> A )
1918adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  { <. M , 
a >. } : ( M ... M ) --> A )
208, 9fvsn 5918 . . . . . . . . . . . . . . . . . . 19  |-  ( {
<. M ,  a >. } `  M )  =  a
2120a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  ( { <. M ,  a >. } `  M )  =  a )
22 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  th )
23 snex 4397 . . . . . . . . . . . . . . . . . . 19  |-  { <. M ,  a >. }  e.  _V
24 feq1 5568 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  { <. M , 
a >. }  ->  (
f : ( M ... M ) --> A  <->  { <. M ,  a
>. } : ( M ... M ) --> A ) )
25 fveq1 5719 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  { <. M , 
a >. }  ->  (
f `  M )  =  ( { <. M ,  a >. } `  M ) )
2625eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  { <. M , 
a >. }  ->  (
( f `  M
)  =  a  <->  ( { <. M ,  a >. } `  M )  =  a ) )
2725, 20syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  { <. M , 
a >. }  ->  (
f `  M )  =  a )
28 sbceq2a 3164 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  M )  =  a  ->  ( [. ( f `  M
)  /  a ]. th 
<->  th ) )
2927, 28syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  { <. M , 
a >. }  ->  ( [. ( f `  M
)  /  a ]. th 
<->  th ) )
3026, 29anbi12d 692 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  { <. M , 
a >. }  ->  (
( ( f `  M )  =  a  /\  [. ( f `
 M )  / 
a ]. th )  <->  ( ( { <. M ,  a
>. } `  M )  =  a  /\  th ) ) )
3124, 30anbi12d 692 . . . . . . . . . . . . . . . . . . 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 3035 . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . 17  |-  ( ( a  e.  A  /\  th )  ->  E. f
( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) )
34 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( M ... n )  =  ( M ... M
) )
3534feq2d 5573 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  (
f : ( M ... n ) --> A  <-> 
f : ( M ... M ) --> A ) )
36 fvex 5734 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f `
 n )  e. 
_V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( f `  n )  ->  ( th 
<->  ta ) )
3836, 37sbcie 3187 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [. ( f `  n
)  /  a ]. th 
<->  ta )
39 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  M  ->  (
f `  n )  =  ( f `  M ) )
40 dfsbcq 3155 . . . . . . . . . . . . . . . . . . . . . . . 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 251 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( ta 
<-> 
[. ( f `  M )  /  a ]. th ) )
4342anbi2d 685 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  (
( ( f `  M )  =  a  /\  ta )  <->  ( (
f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) )
44 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  M  ->  ( N ... n )  =  ( N ... M
) )
45 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  N  =  ( M  +  1 )
4645oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N ... M )  =  ( ( M  + 
1 ) ... M
)
472zrei 10280 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  M  e.  RR
4847ltp1i 9906 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  M  < 
( M  +  1 )
49 peano2z 10310 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( M  e.  ZZ  ->  ( M  +  1 )  e.  ZZ )
502, 49ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( M  +  1 )  e.  ZZ
51 fzn 11063 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( M  +  1 )  e.  ZZ  /\  M  e.  ZZ )  ->  ( M  <  ( M  +  1 )  <-> 
( ( M  + 
1 ) ... M
)  =  (/) ) )
5250, 2, 51mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  <  ( M  + 
1 )  <->  ( ( M  +  1 ) ... M )  =  (/) )
5348, 52mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( M  +  1 ) ... M )  =  (/)
5446, 53eqtri 2455 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N ... M )  =  (/)
5544, 54syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( N ... n )  =  (/) )
5655raleqdv 2902 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  ( A. k  e.  ( N ... n ) ch  <->  A. k  e.  (/)  ch )
)
5735, 43, 563anbi123d 1254 . . . . . . . . . . . . . . . . . . . 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 3724 . . . . . . . . . . . . . . . . . . . . 21  |-  A. k  e.  (/)  ch
59 df-3an 938 . . . . . . . . . . . . . . . . . . . . 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 886 . . . . . . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . . . . . . 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 1636 . . . . . . . . . . . . . . . . . 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 3044 . . . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . . . 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 695 . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . 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 4207 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  b  ->  (
d R a  <->  b R
a ) )
6968rspcev 3044 . . . . . . . . . . . . . . . . . . . . . 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 425 . . . . . . . . . . . . . . . . . . . . 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 2710 . . . . . . . . . . . . . . . . . . . 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 218 . . . . . . . . . . . . . . . . . . 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 109 . . . . . . . . . . . . . . . . . 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 3322 . . . . . . . . . . . . . . . . . . . . 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 609 . . . . . . . . . . . . . . . . . . . 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 3420 . . . . . . . . . . . . . . . . . . . . . . 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 3567 . . . . . . . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . . . . . . . . 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 2499 . . . . . . . . . . . . . . . . . . . . 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 2444 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  b  ->  (
( f `  M
)  =  c  <->  ( f `  M )  =  b ) )
8281anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  b  ->  (
( ( f `  M )  =  c  /\  ta )  <->  ( (
f `  M )  =  b  /\  ta )
) )
83823anbi2d 1259 . . . . . . . . . . . . . . . . . . . . . . . 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 1636 . . . . . . . . . . . . . . . . . . . . . . 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 2718 . . . . . . . . . . . . . . . . . . . . . 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 3085 . . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . . 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 206 . . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . . 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 6081 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( M ... n )  =  ( M ... m
) )
9190feq2d 5573 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
f : ( M ... n ) --> A  <-> 
f : ( M ... m ) --> A ) )
92 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
f `  n )  =  ( f `  m ) )
93 dfsbcq 3155 . . . . . . . . . . . . . . . . . . . . . . . . . 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 251 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( ta 
<-> 
[. ( f `  m )  /  a ]. th ) )
9695anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
( ( f `  M )  =  b  /\  ta )  <->  ( (
f `  M )  =  b  /\  [. (
f `  m )  /  a ]. th ) ) )
97 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( N ... n )  =  ( N ... m
) )
9897raleqdv 2902 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  ( A. k  e.  ( N ... n ) ch  <->  A. k  e.  ( N ... m ) ch ) )
9991, 96, 983anbi123d 1254 . . . . . . . . . . . . . . . . . . . . . 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 1636 . . . . . . . . . . . . . . . . . . . . 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 2925 . . . . . . . . . . . . . . . . . . . 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 5568 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  g  ->  (
f : ( M ... m ) --> A  <-> 
g : ( M ... m ) --> A ) )
103 fveq1 5719 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  (
f `  M )  =  ( g `  M ) )
104103eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  (
( f `  M
)  =  b  <->  ( g `  M )  =  b ) )
105 fveq1 5719 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  (
f `  m )  =  ( g `  m ) )
106 dfsbcq 3155 . . . . . . . . . . . . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  g  ->  (
( ( f `  M )  =  b  /\  [. ( f `
 m )  / 
a ]. th )  <->  ( (
g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th ) ) )
109 fvex 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 ( k  - 
1 ) )  e. 
_V
110 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( ph 
<->  ps ) )
111110sbcbidv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( [. ( f `  k
)  /  b ]. ph  <->  [. ( f `  k
)  /  b ]. ps ) )
112109, 111sbcie 3187 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( f `  k
)  /  b ]. ps )
113 fvex 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 k )  e. 
_V
114 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  =  ( f `  k )  ->  ( ps 
<->  ch ) )
115113, 114sbcie 3187 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( [. ( f `  k
)  /  b ]. ps 
<->  ch )
116112, 115bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  ch )
117 fveq1 5719 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  =  g  ->  (
f `  ( k  -  1 ) )  =  ( g `  ( k  -  1 ) ) )
118 dfsbcq 3155 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5719 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f  =  g  ->  (
f `  k )  =  ( g `  k ) )
121 dfsbcq 3155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3207 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  g  ->  ( [. ( g `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )
124119, 123bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )
125116, 124syl5bbr 251 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  ( ch 
<-> 
[. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )
126125ralbidv 2717 . . . . . . . . . . . . . . . . . . . . . . 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 1254 . . . . . . . . . . . . . . . . . . . . . 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 1985 . . . . . . . . . . . . . . . . . . . . 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 2722 . . . . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . . . . . 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 10523 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  Z )
132131ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . 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 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d  =  b  ->  ( [. d  /  b ]. ph  <->  ph ) )
134133anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  =  b  ->  (
( [. d  /  b ]. ph  /\  a  e.  A )  <->  ( ph  /\  a  e.  A ) ) )
135134anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( d  =  b  ->  (
( ( [. d  /  b ]. ph  /\  a  e.  A )  /\  m  e.  Z
)  <->  ( ( ph  /\  a  e.  A )  /\  m  e.  Z
) ) )
136 eqeq2 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( d  =  b  ->  (
( g `  M
)  =  d  <->  ( g `  M )  =  b ) )
137136anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d  =  b  ->  (
( ( g `  M )  =  d  /\  [. ( g `
 m )  / 
a ]. th )  <->  ( (
g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th ) ) )
1381373anbi2d 1259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 312 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  ( [. c  /  a ]. [. d  /  b ]. ph  <->  [. d  /  b ]. ph ) )
142 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  (
c  e.  A  <->  a  e.  A ) )
143141, 142anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  <->  ( [. d  /  b ]. ph  /\  a  e.  A )
) )
144143anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  =  a  ->  (
( f `  M
)  =  c  <->  ( f `  M )  =  a ) )
146145anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( c  =  a  ->  (
( ( f `  M )  =  c  /\  [. ( f `
 ( m  + 
1 ) )  / 
a ]. th )  <->  ( (
f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th ) ) )
1471463anbi2d 1259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( ZZ>= `  M )
)
152151, 5eleq2s 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  M
) )
153 elfzp12 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  c )
157156eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  M  ->  ( if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A  <->  c  e.  A ) )
158157biimprcd 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  A  ->  (
x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A ) )
159158ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) )  e.  A ) )
160 1re 9082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  1  e.  RR
16147, 160readdcli 9095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( M  +  1 )  e.  RR
16247, 161ltnlei 9186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( M  <  ( M  + 
1 )  <->  -.  ( M  +  1 )  <_  M )
16348, 162mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  -.  ( M  +  1 )  <_  M
164 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  M  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  <->  M  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )
165 elfzle1 11052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( M  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  ( M  +  1 )  <_  M )
166164, 165syl6bi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  =  M  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( M  +  1 )  <_  M )
)
167166com12 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  (
x  =  M  -> 
( M  +  1 )  <_  M )
)
168163, 167mtoi 171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  -.  x  =  M )
169168adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  -.  x  =  M )
170 iffalse 3738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  x  e.  ZZ )
173172adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  x  e.  ZZ )
174 eluzelz 10488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( m  e.  ( ZZ>= `  M
)  ->  m  e.  ZZ )
175174, 5eleq2s 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( m  e.  Z  ->  m  e.  ZZ )
176175peano2zd 10370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ZZ )
177 1z 10303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  1  e.  ZZ
178 fzsubel 11080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( m  +  1 )  e.  ZZ  /\  x  e.  ZZ )  ->  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  ( x  - 
1 )  e.  ( ( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) ) ) )
182181ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( x  e.  ZZ  ->  ( x  -  1 )  e.  ( ( ( M  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
185184imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  M  e.  CC
188 ax-1cn 9040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  1  e.  CC
189 pncan 9303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( M  e.  CC  /\  1  e.  CC )  ->  ( ( M  + 
1 )  -  1 )  =  M )
190187, 188, 189mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( M  +  1 )  -  1 )  =  M
191190a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
( M  +  1 )  -  1 )  =  M )
192175zcnd 10368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  m  e.  CC )
193 pncan 9303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  CC  /\  1  e.  CC )  ->  ( ( m  + 
1 )  -  1 )  =  m )
194192, 188, 193sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
( m  +  1 )  -  1 )  =  m )
195191, 194oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( m  e.  Z  ->  (
( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) )  =  ( M ... m ) )
196195adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( ( ( M  +  1 )  -  1 ) ... ( ( m  + 
1 )  -  1 ) )  =  ( M ... m ) )
197186, 196eleqtrd 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( x  - 
1 )  e.  ( M ... m ) )
198 ffvelrn 5860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( g : ( M ... m ) --> A  /\  ( x  - 
1 )  e.  ( M ... m ) )  ->  ( g `  ( x  -  1 ) )  e.  A
)
199197, 198sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( g : ( M ... m ) --> A  /\  ( m  e.  Z  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )  -> 
( g `  (
x  -  1 ) )  e.  A )
200199anassrs 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( g : ( M ... m ) --> A  /\  m  e.  Z )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  (
g `  ( x  -  1 ) )  e.  A )
201200ancom1s 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  (
g `  ( x  -  1 ) )  e.  A )
202171, 201eqeltrd 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A )
203202ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  ->  ( x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) )  ->  if (
x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) )  e.  A ) )
204203adantll 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  e.  Z  ->  M  e.  ( M ... (
m  +  1 ) ) )
216 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  c  e. 
_V
217156, 208, 216fvmpt 5798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( M ... ( m  +  1
) ) )
223 eqeq1 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  ( m  + 
1 )  ->  (
x  =  M  <->  ( m  +  1 )  =  M ) )
224 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  ( m  + 
1 )  ->  (
x  -  1 )  =  ( ( m  +  1 )  - 
1 ) )
225224fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  ( m  + 
1 )  ->  (
g `  ( x  -  1 ) )  =  ( g `  ( ( m  + 
1 )  -  1 ) ) )
226223, 225ifbieq2d 3751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( m  + 
1 )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  if ( ( m  +  1 )  =  M , 
c ,  ( g `
 ( ( m  +  1 )  - 
1 ) ) ) )
227 fvex 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g `
 ( ( m  +  1 )  - 
1 ) )  e. 
_V
228216, 227ifex 3789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  if ( ( m  +  1 )  =  M , 
c ,  ( g `
 ( ( m  +  1 )  - 
1 ) ) )  e.  _V
229226, 208, 228fvmpt 5798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  <_  m )
232231, 5eleq2s 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( m  e.  Z  ->  M  <_  m )
233 zleltp1 10318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( M  e.  ZZ  /\  m  e.  ZZ )  ->  ( M  <_  m  <->  M  <  ( m  + 
1 ) ) )
2342, 175, 233sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( m  e.  Z  ->  ( M  <_  m  <->  M  <  ( m  +  1 ) ) )
235232, 234mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( m  e.  Z  ->  M  <  ( m  +  1 ) )
236 ltne 9162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( M  e.  RR  /\  M  <  ( m  + 
1 ) )  -> 
( m  +  1 )  =/=  M )
23747, 235, 236sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  (
m  +  1 )  =/=  M )
238237neneqd 2614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  -.  ( m  +  1
)  =  M )
239 iffalse 3738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  Z  ->  (
g `  ( (
m  +  1 )  -  1 ) )  =  ( g `  m ) )
242230, 240, 2413eqtrd 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  =  ( g `  m ) )
243 dfsbcq 3155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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  +  1
) )  /  a ]. th )
248 eluzp1p1 10503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
249248, 5eleq2s 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
25045fveq2i 5723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ZZ>= `  N )  =  (
ZZ>= `  ( M  + 
1 ) )
251249, 250syl6eleqr 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  N
) )
252 elfzp12 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  Z  /\  j  e.  ( N ... ( m  +  1 ) ) )  -> 
( j  =  N  \/  j  e.  ( ( N  +  1 ) ... ( m  +  1 ) ) ) )
255254adantll 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( [. c  / 
a ]. [. d  / 
b ]. ph  /\  m  e.  Z )  /\  j  e.  ( N ... (
m  +  1 ) ) )  ->  (
j  =  N  \/  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) ) )
256255adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  =  N  ->  (
j  -  1 )  =  ( N  - 
1 ) )
25845oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( N  -  1 )  =  ( ( M  + 
1 )  -  1 )
259258, 190eqtri 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( N  -  1 )  =  M
260257, 259syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( j  =  N  ->  (
j  -  1 )  =  M )
261260fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  =  N  <->  j  =  ( M  +  1
) )
268 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  M  <_ 
( M  +  1 )
272 eluz2 10486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( M  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( M  +  1 )  e.  ZZ  /\  M  <_ 
( M  +  1 ) ) )
2732, 50, 271, 272mpbir3an 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( M  +  1 )  e.  ( ZZ>= `  M )
274 fzss1 11083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( M  +  1 )  e.  ( ZZ>= `  M
)  ->  ( ( M  +  1 ) ... ( m  + 
1 ) )  C_  ( M ... ( m  +  1 ) ) )
275273, 274ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( M  +  1 ) ... ( m  + 
1 ) )  C_  ( M ... ( m  +  1 ) )
276 eluzfz1 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... m ) )
277276, 5eleq2s 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( m  e.  Z  ->  M  e.  ( M ... m
) )
278 fzaddel 11079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( M  e.  ZZ  /\  m  e.  ZZ )  ->  ( M  e.  ( M ... m )  <-> 
( M  +  1 )  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) ) )
2802, 175, 279sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( m  e.  Z  ->  ( M  e.  ( M ... m )  <->  ( M  +  1 )  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )
281277, 280mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( m  e.  Z  ->  ( M  +  1 )  e.  ( ( M  +  1 ) ... ( m  +  1 ) ) )
282275, 281sseldi 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( m  e.  Z  ->  ( M  +  1 )  e.  ( M ... ( m  +  1
) ) )
283 eqeq1 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  ( M  + 
1 )  ->  (
x  =  M  <->  ( M  +  1 )  =  M ) )
284 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  =  ( M  + 
1 )  ->  (
x  -  1 )  =  ( ( M  +  1 )  - 
1 ) )
285284, 190syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  ( M  + 
1 )  ->  (
x  -  1 )  =  M )
286285fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  ( M  + 
1 )  ->  (
g `  ( x  -  1 ) )  =  ( g `  M ) )
287283, 286ifbieq2d 3751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( x  =  ( M  + 
1 )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) ) )
288 fvex 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( g `
 M )  e. 
_V
289216, 288ifex 3789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) )  e.  _V
290287, 208, 289fvmpt 5798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( M  +  1 )  =/= 
M
293 ifnefalse 3739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( M  +  1 )  =/=  M  ->  if ( ( M  + 
1 )  =  M ,  c ,  ( g `  M ) )  =  ( g `
 M ) )
294292, 293ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) )  =  ( g `  M )
295291, 294syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) )  =  ( g `  M ) )
296295adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
g `  M )  =  d )
298270, 296, 2973eqtrd 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( j  e.  ( ( N  +  1 ) ... ( m  +  1 ) )  ->  j  e.  ZZ )
308307adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) )  ->  j  e.  ZZ )
30945, 50eqeltri 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  N  e.  ZZ
310 peano2z 10310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
311309, 310ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( N  +  1 )  e.  ZZ
312 fzsubel 11080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
j  e.  ZZ  ->  ( j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) )  -> 
( j  -  1 )  e.  ( ( ( N  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
317316com23 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) )  -> 
( j  e.  ZZ  ->  ( j  -  1 )  e.  ( ( ( N  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
318317imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  N  e.  RR
321320recni 9094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  N  e.  CC
322 pncan 9303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
323321,