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

Theorem fdc 26381
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 10484 . . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . 17  |-  M  e.  Z
7 eqid 2430 . . . . . . . . . . . . . . . . . . . . . 22  |-  { <. M ,  a >. }  =  { <. M ,  a
>. }
82elexi 2952 . . . . . . . . . . . . . . . . . . . . . . 23  |-  M  e. 
_V
9 vex 2946 . . . . . . . . . . . . . . . . . . . . . . 23  |-  a  e. 
_V
108, 9fsn 5892 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( {
<. M ,  a >. } : { M } --> { a }  <->  { <. M , 
a >. }  =  { <. M ,  a >. } )
117, 10mpbir 201 . . . . . . . . . . . . . . . . . . . . 21  |-  { <. M ,  a >. } : { M } --> { a }
12 snssi 3929 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  A  ->  { a }  C_  A )
13 fss 5585 . . . . . . . . . . . . . . . . . . . . 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 11078 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
162, 15ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M ... M )  =  { M }
1716feq2i 5572 . . . . . . . . . . . . . . . . . . . 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 5912 . . . . . . . . . . . . . . . . . . 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 4392 . . . . . . . . . . . . . . . . . . 19  |-  { <. M ,  a >. }  e.  _V
24 feq1 5562 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  { <. M , 
a >. }  ->  (
f : ( M ... M ) --> A  <->  { <. M ,  a
>. } : ( M ... M ) --> A ) )
25 fveq1 5713 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  { <. M , 
a >. }  ->  (
f `  M )  =  ( { <. M ,  a >. } `  M ) )
2625eqeq1d 2438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  { <. M , 
a >. }  ->  (
( f `  M
)  =  a  <->  ( { <. M ,  a >. } `  M )  =  a ) )
2725, 20syl6eq 2478 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  { <. M , 
a >. }  ->  (
f `  M )  =  a )
28 sbceq2a 3159 . . . . . . . . . . . . . . . . . . . . . 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 3030 . . . . . . . . . . . . . . . . . 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 6075 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( M ... n )  =  ( M ... M
) )
3534feq2d 5567 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  (
f : ( M ... n ) --> A  <-> 
f : ( M ... M ) --> A ) )
36 fvex 5728 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f `
 n )  e. 
_V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( f `  n )  ->  ( th 
<->  ta ) )
3836, 37sbcie 3182 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [. ( f `  n
)  /  a ]. th 
<->  ta )
39 fveq2 5714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  M  ->  (
f `  n )  =  ( f `  M ) )
40 dfsbcq 3150 . . . . . . . . . . . . . . . . . . . . . . . 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 6075 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  M  ->  ( N ... n )  =  ( N ... M
) )
45 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  N  =  ( M  +  1 )
4645oveq1i 6077 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N ... M )  =  ( ( M  + 
1 ) ... M
)
472zrei 10272 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  M  e.  RR
4847ltp1i 9898 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  M  < 
( M  +  1 )
49 peano2z 10302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( M  e.  ZZ  ->  ( M  +  1 )  e.  ZZ )
502, 49ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( M  +  1 )  e.  ZZ
51 fzn 11055 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N ... M )  =  (/)
5544, 54syl6eq 2478 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( N ... n )  =  (/) )
5655raleqdv 2897 . . . . . . . . . . . . . . . . . . . . 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 3719 . . . . . . . . . . . . . . . . . . . . 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 3039 . . . . . . . . . . . . . . . . 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 4202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  b  ->  (
d R a  <->  b R
a ) )
6968rspcev 3039 . . . . . . . . . . . . . . . . . . . . . 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 2705 . . . . . . . . . . . . . . . . . . . 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 3317 . . . . . . . . . . . . . . . . . . . . 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 3415 . . . . . . . . . . . . . . . . . . . . . . 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 3562 . . . . . . . . . . . . . . . . . . . . . . 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 2494 . . . . . . . . . . . . . . . . . . . . 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 2439 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2713 . . . . . . . . . . . . . . . . . . . . . 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 3080 . . . . . . . . . . . . . . . . . . . . 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 6075 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( M ... n )  =  ( M ... m
) )
9190feq2d 5567 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
f : ( M ... n ) --> A  <-> 
f : ( M ... m ) --> A ) )
92 fveq2 5714 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
f `  n )  =  ( f `  m ) )
93 dfsbcq 3150 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6075 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( N ... n )  =  ( N ... m
) )
9897raleqdv 2897 . . . . . . . . . . . . . . . . . . . . . . 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 2920 . . . . . . . . . . . . . . . . . . . 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 5562 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  g  ->  (
f : ( M ... m ) --> A  <-> 
g : ( M ... m ) --> A ) )
103 fveq1 5713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  (
f `  M )  =  ( g `  M ) )
104103eqeq1d 2438 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  (
( f `  M
)  =  b  <->  ( g `  M )  =  b ) )
105 fveq1 5713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  (
f `  m )  =  ( g `  m ) )
106 dfsbcq 3150 . . . . . . . . . . . . . . . . . . . . . . . . 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 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 ( k  - 
1 ) )  e. 
_V
110 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( ph 
<->  ps ) )
111110sbcbidv 3202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( [. ( f `  k
)  /  b ]. ph  <->  [. ( f `  k
)  /  b ]. ps ) )
112109, 111sbcie 3182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( f `  k
)  /  b ]. ps )
113 fvex 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 k )  e. 
_V
114 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  =  ( f `  k )  ->  ( ps 
<->  ch ) )
115113, 114sbcie 3182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( [. ( f `  k
)  /  b ]. ps 
<->  ch )
116112, 115bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  ch )
117 fveq1 5713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  =  g  ->  (
f `  ( k  -  1 ) )  =  ( g `  ( k  -  1 ) ) )
118 dfsbcq 3150 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f  =  g  ->  (
f `  k )  =  ( g `  k ) )
121 dfsbcq 3150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3202 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2712 . . . . . . . . . . . . . . . . . . . . . . 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 2717 . . . . . . . . . . . . . . . . . . . 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 10515 . . . . . . . . . . . . . . . . . . . . . . . 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 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  ( [. c  /  a ]. [. d  /  b ]. ph  <->  [. d  /  b ]. ph ) )
142 eleq1 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( ZZ>= `  M )
)
152151, 5eleq2s 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  M
) )
153 elfzp12 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  c )
157156eleq1d 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  1  e.  RR
16147, 160readdcli 9087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( M  +  1 )  e.  RR
16247, 161ltnlei 9178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( M  <  ( M  + 
1 )  <->  -.  ( M  +  1 )  <_  M )
16348, 162mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  -.  ( M  +  1 )  <_  M
164 eleq1 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  M  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  <->  M  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )
165 elfzle1 11044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( m  e.  ( ZZ>= `  M
)  ->  m  e.  ZZ )
175174, 5eleq2s 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( m  e.  Z  ->  m  e.  ZZ )
176175peano2zd 10362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ZZ )
177 1z 10295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  1  e.  ZZ
178 fzsubel 11072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  M  e.  CC
188 ax-1cn 9032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  1  e.  CC
189 pncan 9295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  m  e.  CC )
193 pncan 9295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( x  - 
1 )  e.  ( M ... m ) )
198 ffvelrn 5854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  e.  Z  ->  M  e.  ( M ... (
m  +  1 ) ) )
216 vex 2946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  c  e. 
_V
217156, 208, 216fvmpt 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( M ... ( m  +  1
) ) )
223 eqeq1 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  ( m  + 
1 )  ->  (
x  =  M  <->  ( m  +  1 )  =  M ) )
224 oveq1 6074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  ( m  + 
1 )  ->  (
x  -  1 )  =  ( ( m  +  1 )  - 
1 ) )
225224fveq2d 5718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  ( m  + 
1 )  ->  (
g `  ( x  -  1 ) )  =  ( g `  ( ( m  + 
1 )  -  1 ) ) )
226223, 225ifbieq2d 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( m  + 
1 )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  if ( ( m  +  1 )  =  M , 
c ,  ( g `
 ( ( m  +  1 )  - 
1 ) ) ) )
227 fvex 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g `
 ( ( m  +  1 )  - 
1 ) )  e. 
_V
228216, 227ifex 3784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  if ( ( m  +  1 )  =  M , 
c ,  ( g `
 ( ( m  +  1 )  - 
1 ) ) )  e.  _V
229226, 208, 228fvmpt 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  <_  m )
232231, 5eleq2s 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( m  e.  Z  ->  M  <_  m )
233 zleltp1 10310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( M  e.  RR  /\  M  <  ( m  + 
1 ) )  -> 
( m  +  1 )  =/=  M )
23747, 235, 236sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  (
m  +  1 )  =/=  M )
238237neneqd 2609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  -.  ( m  +  1
)  =  M )
239 iffalse 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  Z  ->  (
g `  ( (
m  +  1 )  -  1 ) )  =  ( g `  m ) )
242230, 240, 2413eqtrd 2466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  =  ( g `  m ) )
243 dfsbcq 3150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
249248, 5eleq2s 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
25045fveq2i 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ZZ>= `  N )  =  (
ZZ>= `  ( M  + 
1 ) )
251249, 250syl6eleqr 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  N
) )
252 elfzp12 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  =  N  ->  (
j  -  1 )  =  ( N  - 
1 ) )
25845oveq1i 6077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( N  -  1 )  =  ( ( M  + 
1 )  -  1 )
259258, 190eqtri 2450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( N  -  1 )  =  M
260257, 259syl6eq 2478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( j  =  N  ->  (
j  -  1 )  =  M )
261260fveq2d 5718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  =  N  <->  j  =  ( M  +  1
) )
268 fveq2 5714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  M  <_ 
( M  +  1 )
272 eluz2 10478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... m ) )
277276, 5eleq2s 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( m  e.  Z  ->  M  e.  ( M ... m
) )
278 fzaddel 11071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( m  e.  Z  ->  ( M  +  1 )  e.  ( M ... ( m  +  1
) ) )
283 eqeq1 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  ( M  + 
1 )  ->  (
x  =  M  <->  ( M  +  1 )  =  M ) )
284 oveq1 6074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  =  ( M  + 
1 )  ->  (
x  -  1 )  =  ( ( M  +  1 )  - 
1 ) )
285284, 190syl6eq 2478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  ( M  + 
1 )  ->  (
x  -  1 )  =  M )
286285fveq2d 5718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  ( M  + 
1 )  ->  (
g `  ( x  -  1 ) )  =  ( g `  M ) )
287283, 286ifbieq2d 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( x  =  ( M  + 
1 )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) ) )
288 fvex 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( g `
 M )  e. 
_V
289216, 288ifex 3784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) )  e.  _V
290287, 208, 289fvmpt 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( M  +  1 )  =/= 
M
293 ifnefalse 3734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  N  e.  ZZ
310 peano2z 10302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
311309, 310ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( N  +  1 )  e.  ZZ
312 fzsubel 11072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  N  e.  RR
321320recni 9086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  N  e.  CC
322 pncan 9295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
323321, 188, 322