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

Theorem fdc 26558
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 10258 . . . . . . . . . . . . . . . . . . 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 2369 . . . . . . . . . . . . . . . . 17  |-  M  e.  Z
7 eqid 2296 . . . . . . . . . . . . . . . . . . . . . 22  |-  { <. M ,  a >. }  =  { <. M ,  a
>. }
82elexi 2810 . . . . . . . . . . . . . . . . . . . . . . 23  |-  M  e. 
_V
9 vex 2804 . . . . . . . . . . . . . . . . . . . . . . 23  |-  a  e. 
_V
108, 9fsn 5712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( {
<. M ,  a >. } : { M } --> { a }  <->  { <. M , 
a >. }  =  { <. M ,  a >. } )
117, 10mpbir 200 . . . . . . . . . . . . . . . . . . . . 21  |-  { <. M ,  a >. } : { M } --> { a }
12 snssi 3775 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  A  ->  { a }  C_  A )
13 fss 5413 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { <. M ,  a
>. } : { M }
--> { a }  /\  { a }  C_  A
)  ->  { <. M , 
a >. } : { M } --> A )
1411, 12, 13sylancr 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  A  ->  { <. M ,  a >. } : { M } --> A )
15 fzsn 10849 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
162, 15ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M ... M )  =  { M }
1716feq2i 5400 . . . . . . . . . . . . . . . . . . . 20  |-  ( {
<. M ,  a >. } : ( M ... M ) --> A  <->  { <. M , 
a >. } : { M } --> A )
1814, 17sylibr 203 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  A  ->  { <. M ,  a >. } :
( M ... M
) --> A )
1918adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  { <. M , 
a >. } : ( M ... M ) --> A )
208, 9fvsn 5729 . . . . . . . . . . . . . . . . . . 19  |-  ( {
<. M ,  a >. } `  M )  =  a
2120a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  ( { <. M ,  a >. } `  M )  =  a )
22 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  A  /\  th )  ->  th )
23 snex 4232 . . . . . . . . . . . . . . . . . . 19  |-  { <. M ,  a >. }  e.  _V
24 feq1 5391 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  { <. M , 
a >. }  ->  (
f : ( M ... M ) --> A  <->  { <. M ,  a
>. } : ( M ... M ) --> A ) )
25 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  { <. M , 
a >. }  ->  (
f `  M )  =  ( { <. M ,  a >. } `  M ) )
2625eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  { <. M , 
a >. }  ->  (
( f `  M
)  =  a  <->  ( { <. M ,  a >. } `  M )  =  a ) )
2725, 20syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  { <. M , 
a >. }  ->  (
f `  M )  =  a )
28 sbceq1a 3014 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( f `  M )  ->  ( th 
<-> 
[. ( f `  M )  /  a ]. th ) )
2928eqcoms 2299 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f `  M )  =  a  ->  ( th 
<-> 
[. ( f `  M )  /  a ]. th ) )
3029bicomd 192 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  M )  =  a  ->  ( [. ( f `  M
)  /  a ]. th 
<->  th ) )
3127, 30syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  { <. M , 
a >. }  ->  ( [. ( f `  M
)  /  a ]. th 
<->  th ) )
3226, 31anbi12d 691 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  { <. M , 
a >. }  ->  (
( ( f `  M )  =  a  /\  [. ( f `
 M )  / 
a ]. th )  <->  ( ( { <. M ,  a
>. } `  M )  =  a  /\  th ) ) )
3324, 32anbi12d 691 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
3423, 33spcev 2888 . . . . . . . . . . . . . . . . . 18  |-  ( ( { <. M ,  a
>. } : ( M ... M ) --> A  /\  ( ( {
<. M ,  a >. } `  M )  =  a  /\  th )
)  ->  E. f
( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) )
3519, 21, 22, 34syl12anc 1180 . . . . . . . . . . . . . . . . 17  |-  ( ( a  e.  A  /\  th )  ->  E. f
( f : ( M ... M ) --> A  /\  ( ( f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) )
36 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( M ... n )  =  ( M ... M
) )
3736feq2d 5396 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  (
f : ( M ... n ) --> A  <-> 
f : ( M ... M ) --> A ) )
38 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f `
 n )  e. 
_V
39 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( f `  n )  ->  ( th 
<->  ta ) )
4038, 39sbcie 3038 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [. ( f `  n
)  /  a ]. th 
<->  ta )
41 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  M  ->  (
f `  n )  =  ( f `  M ) )
42 dfsbcq 3006 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f `  n )  =  ( f `  M )  ->  ( [. ( f `  n
)  /  a ]. th 
<-> 
[. ( f `  M )  /  a ]. th ) )
4341, 42syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  M  ->  ( [. ( f `  n
)  /  a ]. th 
<-> 
[. ( f `  M )  /  a ]. th ) )
4440, 43syl5bbr 250 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( ta 
<-> 
[. ( f `  M )  /  a ]. th ) )
4544anbi2d 684 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  (
( ( f `  M )  =  a  /\  ta )  <->  ( (
f `  M )  =  a  /\  [. (
f `  M )  /  a ]. th ) ) )
46 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  M  ->  ( N ... n )  =  ( N ... M
) )
47 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  N  =  ( M  +  1 )
4847oveq1i 5884 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N ... M )  =  ( ( M  + 
1 ) ... M
)
492zrei 10046 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  M  e.  RR
5049ltp1i 9676 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  M  < 
( M  +  1 )
51 peano2z 10076 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( M  e.  ZZ  ->  ( M  +  1 )  e.  ZZ )
522, 51ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( M  +  1 )  e.  ZZ
53 fzn 10826 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( M  +  1 )  e.  ZZ  /\  M  e.  ZZ )  ->  ( M  <  ( M  +  1 )  <-> 
( ( M  + 
1 ) ... M
)  =  (/) ) )
5452, 2, 53mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  <  ( M  + 
1 )  <->  ( ( M  +  1 ) ... M )  =  (/) )
5550, 54mpbi 199 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( M  +  1 ) ... M )  =  (/)
5648, 55eqtri 2316 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N ... M )  =  (/)
5746, 56syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  M  ->  ( N ... n )  =  (/) )
5857raleqdv 2755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  M  ->  ( A. k  e.  ( N ... n ) ch  <->  A. k  e.  (/)  ch )
)
5937, 45, 583anbi123d 1252 . . . . . . . . . . . . . . . . . . . 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 )
) )
60 ral0 3571 . . . . . . . . . . . . . . . . . . . . 21  |-  A. k  e.  (/)  ch
61 df-3an 936 . . . . . . . . . . . . . . . . . . . . 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 )
)
6260, 61mpbiran2 885 . . . . . . . . . . . . . . . . . . . 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 ) ) )
6359, 62syl6bb 252 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
6463exbidv 1616 . . . . . . . . . . . . . . . . . 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 ) ) ) )
6564rspcev 2897 . . . . . . . . . . . . . . . . 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 ) )
666, 35, 65sylancr 644 . . . . . . . . . . . . . . . 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 ) )
6766adantll 694 . . . . . . . . . . . . . . 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 ) )
6867a1d 22 . . . . . . . . . . . . . 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 ) ) )
69 fdc.11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( et  /\  ph )  /\  ( a  e.  A  /\  b  e.  A ) )  -> 
b R a )
70 breq1 4042 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  =  b  ->  (
d R a  <->  b R
a ) )
7170rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 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 )
7271expcom 424 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) )
7369, 72syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) )
74 dfrex2 2569 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 )
7573, 74syl6ib 217 . . . . . . . . . . . . . . . . . . . 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 ) } )  ->  -.  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 ) )
7675con2d 107 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) } ) ) )
77 eldif 3175 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) } ) ) )
7877simplbi2 608 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) } ) ) ) )
79 ssrab2 3271 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { 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
80 dfss4 3416 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { 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 ) } )
8179, 80mpbi 199 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) }
8281eleq2i 2360 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) } )
83 eqeq2 2305 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  b  ->  (
( f `  M
)  =  c  <->  ( f `  M )  =  b ) )
8483anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  b  ->  (
( ( f `  M )  =  c  /\  ta )  <->  ( (
f `  M )  =  b  /\  ta )
) )
85843anbi2d 1257 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 ) ) )
8685exbidv 1616 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) )
8786rexbidv 2577 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) )
8887elrab3 2937 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) )
8982, 88syl5bb 248 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) )
9078, 89sylibd 205 . . . . . . . . . . . . . . . . . . . 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 ) } )  ->  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
9190ad2antll 709 . . . . . . . . . . . . . . . . . . 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 ) } )  ->  E. n  e.  Z  E. f
( f : ( M ... n ) --> A  /\  ( ( f `  M )  =  b  /\  ta )  /\  A. k  e.  ( N ... n
) ch ) ) )
92 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  m  ->  ( M ... n )  =  ( M ... m
) )
9392feq2d 5396 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  (
f : ( M ... n ) --> A  <-> 
f : ( M ... m ) --> A ) )
94 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  m  ->  (
f `  n )  =  ( f `  m ) )
95 dfsbcq 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f `  n )  =  ( f `  m )  ->  ( [. ( f `  n
)  /  a ]. th 
<-> 
[. ( f `  m )  /  a ]. th ) )
9694, 95syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  ( [. ( f `  n
)  /  a ]. th 
<-> 
[. ( f `  m )  /  a ]. th ) )
9740, 96syl5bbr 250 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  m  ->  ( ta 
<-> 
[. ( f `  m )  /  a ]. th ) )
9897anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  (
( ( f `  M )  =  b  /\  ta )  <->  ( (
f `  M )  =  b  /\  [. (
f `  m )  /  a ]. th ) ) )
99 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  m  ->  ( N ... n )  =  ( N ... m
) )
10099raleqdv 2755 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  ( A. k  e.  ( N ... n ) ch  <->  A. k  e.  ( N ... m ) ch ) )
10193, 98, 1003anbi123d 1252 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) )
102101exbidv 1616 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) )
103102cbvrexv 2778 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) )
104 feq1 5391 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  (
f : ( M ... m ) --> A  <-> 
g : ( M ... m ) --> A ) )
105 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  g  ->  (
f `  M )  =  ( g `  M ) )
106105eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  (
( f `  M
)  =  b  <->  ( g `  M )  =  b ) )
107 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  g  ->  (
f `  m )  =  ( g `  m ) )
108 dfsbcq 3006 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f `  m )  =  ( g `  m )  ->  ( [. ( f `  m
)  /  a ]. th 
<-> 
[. ( g `  m )  /  a ]. th ) )
109107, 108syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  ( [. ( f `  m
)  /  a ]. th 
<-> 
[. ( g `  m )  /  a ]. th ) )
110106, 109anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  (
( ( f `  M )  =  b  /\  [. ( f `
 m )  / 
a ]. th )  <->  ( (
g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th ) ) )
111 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f `
 ( k  - 
1 ) )  e. 
_V
112 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( ph 
<->  ps ) )
113112sbcbidv 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f `  ( k  -  1 ) )  ->  ( [. ( f `  k
)  /  b ]. ph  <->  [. ( f `  k
)  /  b ]. ps ) )
114111, 113sbcie 3038 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( f `  k
)  /  b ]. ps )
115 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f `
 k )  e. 
_V
116 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( b  =  ( f `  k )  ->  ( ps 
<->  ch ) )
117115, 116sbcie 3038 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( [. ( f `  k
)  /  b ]. ps 
<->  ch )
118114, 117bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  ch )
119 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f  =  g  ->  (
f `  ( k  -  1 ) )  =  ( g `  ( k  -  1 ) ) )
120 dfsbcq 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f `  ( k  -  1 ) )  =  ( g `  ( k  -  1 ) )  ->  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph ) )
121119, 120syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  =  g  ->  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph ) )
122 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f  =  g  ->  (
f `  k )  =  ( g `  k ) )
123 dfsbcq 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( f `  k )  =  ( g `  k )  ->  ( [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  k
)  /  b ]. ph ) )
124122, 123syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f  =  g  ->  ( [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  k
)  /  b ]. ph ) )
125124sbcbidv 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  =  g  ->  ( [. ( g `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )
126121, 125bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  g  ->  ( [. ( f `  (
k  -  1 ) )  /  a ]. [. ( f `  k
)  /  b ]. ph  <->  [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )
127118, 126syl5bbr 250 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  g  ->  ( ch 
<-> 
[. ( g `  ( k  -  1 ) )  /  a ]. [. ( g `  k )  /  b ]. ph ) )
128127ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  g  ->  ( A. k  e.  ( N ... m ) ch  <->  A. k  e.  ( N ... m ) [. ( g `  (
k  -  1 ) )  /  a ]. [. ( g `  k
)  /  b ]. ph ) )
129104, 110, 1283anbi123d 1252 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) )
130129cbvexv 1956 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) )
131130rexbii 2581 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) )
132103, 131bitri 240 . . . . . . . . . . . . . . . . . . . 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. 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 ) )
1335peano2uzs 10289 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  Z )
134133ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 )
135 sbceq2a 3015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( d  =  b  ->  ( [. d  /  b ]. ph  <->  ph ) )
136135anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d  =  b  ->  (
( [. d  /  b ]. ph  /\  a  e.  A )  <->  ( ph  /\  a  e.  A ) ) )
137136anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  =  b  ->  (
( ( [. d  /  b ]. ph  /\  a  e.  A )  /\  m  e.  Z
)  <->  ( ( ph  /\  a  e.  A )  /\  m  e.  Z
) ) )
138 eqeq2 2305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( d  =  b  ->  (
( g `  M
)  =  d  <->  ( g `  M )  =  b ) )
139138anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( d  =  b  ->  (
( ( g `  M )  =  d  /\  [. ( g `
 m )  / 
a ]. th )  <->  ( (
g `  M )  =  b  /\  [. (
g `  m )  /  a ]. th ) ) )
1401393anbi2d 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) ) )
141140imbi1d 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  ->  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 ) ) ) )
142137, 141imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) ) )
143 sbceq2a 3015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( c  =  a  ->  ( [. c  /  a ]. [. d  /  b ]. ph  <->  [. d  /  b ]. ph ) )
144 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( c  =  a  ->  (
c  e.  A  <->  a  e.  A ) )
145143, 144anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  (
( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  <->  ( [. d  /  b ]. ph  /\  a  e.  A )
) )
146145anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
( ( [. c  /  a ]. [. d  /  b ]. ph  /\  c  e.  A )  /\  m  e.  Z
)  <->  ( ( [. d  /  b ]. ph  /\  a  e.  A )  /\  m  e.  Z
) ) )
147 eqeq2 2305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  a  ->  (
( f `  M
)  =  c  <->  ( f `  M )  =  a ) )
148147anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  =  a  ->  (
( ( f `  M )  =  c  /\  [. ( f `
 ( m  + 
1 ) )  / 
a ]. th )  <->  ( (
f `  M )  =  a  /\  [. (
f `  ( m  +  1 ) )  /  a ]. th ) ) )
1491483anbi2d 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 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 ) ) )
150149exbidv 1616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) ) )
151150imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) ) ) )
152146, 151imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) ) ) )
153 peano2uz 10288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( ZZ>= `  M )
)
154153, 5eleq2s 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  M
) )
155 elfzp12 10877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  +  1 )  e.  ( ZZ>= `  M
)  ->  ( x  e.  ( M ... (
m  +  1 ) )  <->  ( x  =  M  \/  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) ) )
156154, 155syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  (
x  e.  ( M ... ( m  + 
1 ) )  <->  ( x  =  M  \/  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) ) )
157156ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  e.  ( M ... ( m  +  1 ) )  <-> 
( x  =  M  \/  x  e.  ( ( M  +  1 ) ... ( m  +  1 ) ) ) ) )
158 iftrue 3584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  c )
159158eleq1d 2362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  M  ->  ( if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A  <->  c  e.  A ) )
160159biimprcd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( c  e.  A  ->  (
x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A ) )
161160ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) )  e.  A ) )
162 1re 8853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  1  e.  RR
16349, 162readdcli 8866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( M  +  1 )  e.  RR
16449, 163ltnlei 8955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( M  <  ( M  + 
1 )  <->  -.  ( M  +  1 )  <_  M )
16550, 164mpbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  -.  ( M  +  1 )  <_  M
166 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  =  M  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  <->  M  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )
167 elfzle1 10815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( M  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  ( M  +  1 )  <_  M )
168166, 167syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  M  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( M  +  1 )  <_  M )
)
169168com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  (
x  =  M  -> 
( M  +  1 )  <_  M )
)
170165, 169mtoi 169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  -.  x  =  M )
171170adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  -.  x  =  M )
172 iffalse 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -.  x  =  M  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  ( g `
 ( x  - 
1 ) ) )
173171, 172syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  ( g `
 ( x  - 
1 ) ) )
174 elfzelz 10814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  x  e.  ZZ )
175174adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  x  e.  ZZ )
176 eluzelz 10254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( m  e.  ( ZZ>= `  M
)  ->  m  e.  ZZ )
177176, 5eleq2s 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( m  e.  Z  ->  m  e.  ZZ )
178177peano2zd 10136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ZZ )
179 1z 10069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  1  e.  ZZ
180 fzsubel 10843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( ( 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 ) ) ) )
181180biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
182179, 181mpanr2 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( ( 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 ) ) ) )
18352, 182mpanl1 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( m  +  1 )  e.  ZZ  /\  x  e.  ZZ )  ->  ( x  e.  ( ( M  +  1 ) ... ( m  +  1 ) )  ->  ( x  - 
1 )  e.  ( ( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) ) ) )
184183ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( m  +  1 )  e.  ZZ  ->  (
x  e.  ZZ  ->  ( x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( x  -  1 )  e.  ( ( ( M  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
185178, 184syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( m  e.  Z  ->  (
x  e.  ZZ  ->  ( x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( x  -  1 )  e.  ( ( ( M  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
186185com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) )  -> 
( x  e.  ZZ  ->  ( x  -  1 )  e.  ( ( ( M  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
187186imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( x  e.  ZZ  ->  ( x  -  1 )  e.  ( ( ( M  +  1 )  - 
1 ) ... (
( m  +  1 )  -  1 ) ) ) )
188175, 187mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( x  - 
1 )  e.  ( ( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) ) )
18949recni 8865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  M  e.  CC
190 ax-1cn 8811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  1  e.  CC
191 pncan 9073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( M  e.  CC  /\  1  e.  CC )  ->  ( ( M  + 
1 )  -  1 )  =  M )
192189, 190, 191mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( M  +  1 )  -  1 )  =  M
193192a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
( M  +  1 )  -  1 )  =  M )
194177zcnd 10134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( m  e.  Z  ->  m  e.  CC )
195 pncan 9073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  CC  /\  1  e.  CC )  ->  ( ( m  + 
1 )  -  1 )  =  m )
196194, 190, 195sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
( m  +  1 )  -  1 )  =  m )
197193, 196oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( m  e.  Z  ->  (
( ( M  + 
1 )  -  1 ) ... ( ( m  +  1 )  -  1 ) )  =  ( M ... m ) )
198197adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( ( ( M  +  1 )  -  1 ) ... ( ( m  + 
1 )  -  1 ) )  =  ( M ... m ) )
199188, 198eleqtrd 2372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  Z  /\  x  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) )  ->  ( x  - 
1 )  e.  ( M ... m ) )
200 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( g : ( M ... m ) --> A  /\  ( x  - 
1 )  e.  ( M ... m ) )  ->  ( g `  ( x  -  1 ) )  e.  A
)
201199, 200sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( g : ( M ... m ) --> A  /\  ( m  e.  Z  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )  -> 
( g `  (
x  -  1 ) )  e.  A )
202201anassrs 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( g : ( M ... m ) --> A  /\  m  e.  Z )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  (
g `  ( x  -  1 ) )  e.  A )
203202ancom1s 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  (
g `  ( x  -  1 ) )  e.  A )
204173, 203eqeltrd 2370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  /\  x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  e.  A )
205204ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  Z  /\  g : ( M ... m ) --> A )  ->  ( x  e.  ( ( M  + 
1 ) ... (
m  +  1 ) )  ->  if (
x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) )  e.  A ) )
206205adantll 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( 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 ) )
207161, 206jaod 369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( 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 ) )
208157, 207sylbid 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( c  e.  A  /\  m  e.  Z
)  /\  g :
( M ... m
) --> A )  -> 
( x  e.  ( M ... ( m  +  1 ) )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) )  e.  A ) )
209208ralrimiv 2638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( 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 )
210 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( M ... ( m  +  1
) )  |->  if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) ) )  =  ( x  e.  ( M ... ( m  +  1
) )  |->  if ( x  =  M , 
c ,  ( g `
 ( x  - 
1 ) ) ) )
211210fmpt 5697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 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 )
212209, 211sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( 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 )
213212adantlll 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( [. 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 )
2142133ad2antr1 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( [. 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 )
215 eluzfz1 10819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( m  +  1 )  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... ( m  +  1 ) ) )
216153, 215syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... ( m  +  1 ) ) )
217216, 5eleq2s 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  e.  Z  ->  M  e.  ( M ... (
m  +  1 ) ) )
218 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  c  e. 
_V
219158, 210, 218fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( M  e.  ( M ... ( m  +  1
) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M )  =  c )
220217, 219syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M )  =  c )
221220ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( [. 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 )
222 eluzfz2 10820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( m  +  1 )  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( M ... (
m  +  1 ) ) )
223153, 222syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( M ... (
m  +  1 ) ) )
224223, 5eleq2s 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( M ... ( m  +  1
) ) )
225 eqeq1 2302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  ( m  + 
1 )  ->  (
x  =  M  <->  ( m  +  1 )  =  M ) )
226 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  =  ( m  + 
1 )  ->  (
x  -  1 )  =  ( ( m  +  1 )  - 
1 ) )
227226fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  ( m  + 
1 )  ->  (
g `  ( x  -  1 ) )  =  ( g `  ( ( m  + 
1 )  -  1 ) ) )
228225, 227ifbieq2d 3598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  ( m  + 
1 )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  if ( ( m  +  1 )  =  M , 
c ,  ( g `
 ( ( m  +  1 )  - 
1 ) ) ) )
229 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( g `
 ( ( m  +  1 )  - 
1 ) )  e. 
_V
230218, 229ifex 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  if ( ( m  +  1 )  =  M , 
c ,  ( g `
 ( ( m  +  1 )  - 
1 ) ) )  e.  _V
231228, 210, 230fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 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 ) ) ) )
232224, 231syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 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 ) ) ) )
233 eluzle 10256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  <_  m )
234233, 5eleq2s 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  Z  ->  M  <_  m )
235 zleltp1 10084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( M  e.  ZZ  /\  m  e.  ZZ )  ->  ( M  <_  m  <->  M  <  ( m  + 
1 ) ) )
2362, 177, 235sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  Z  ->  ( M  <_  m  <->  M  <  ( m  +  1 ) ) )
237234, 236mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( m  e.  Z  ->  M  <  ( m  +  1 ) )
238 ltne 8933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( M  e.  RR  /\  M  <  ( m  + 
1 ) )  -> 
( m  +  1 )  =/=  M )
23949, 237, 238sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( m  e.  Z  ->  (
m  +  1 )  =/=  M )
240239neneqd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( m  e.  Z  ->  -.  ( m  +  1
)  =  M )
241 iffalse 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( -.  ( m  +  1 )  =  M  ->  if ( ( m  + 
1 )  =  M ,  c ,  ( g `  ( ( m  +  1 )  -  1 ) ) )  =  ( g `
 ( ( m  +  1 )  - 
1 ) ) )
242240, 241syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  if ( ( m  + 
1 )  =  M ,  c ,  ( g `  ( ( m  +  1 )  -  1 ) ) )  =  ( g `
 ( ( m  +  1 )  - 
1 ) ) )
243196fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( m  e.  Z  ->  (
g `  ( (
m  +  1 )  -  1 ) )  =  ( g `  m ) )
244232, 242, 2433eqtrd 2332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  =  ( g `  m ) )
245 dfsbcq 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( 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 ) )
246244, 245syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  e.  Z  ->  ( [. ( ( x  e.  ( M ... (
m  +  1 ) )  |->  if ( x  =  M ,  c ,  ( g `  ( x  -  1
) ) ) ) `
 ( m  + 
1 ) )  / 
a ]. th  <->  [. ( g `
 m )  / 
a ]. th ) )
247246biimpar 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( m  e.  Z  /\  [. ( g `  m
)  /  a ]. th )  ->  [. (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( m  +  1
) )  /  a ]. th )
248247ad2ant2l 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( [. 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 )
2492483ad2antr2 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( [. 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 )
250 eluzp1p1 10269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( m  e.  ( ZZ>= `  M
)  ->  ( m  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
251250, 5eleq2s 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
25247fveq2i 5544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ZZ>= `  N )  =  (
ZZ>= `  ( M  + 
1 ) )
253251, 252syl6eleqr 2387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( m  e.  Z  ->  (
m  +  1 )  e.  ( ZZ>= `  N
) )
254 elfzp12 10877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  +  1 )  e.  ( ZZ>= `  N
)  ->  ( j  e.  ( N ... (
m  +  1 ) )  <->  ( j  =  N  \/  j  e.  ( ( N  + 
1 ) ... (
m  +  1 ) ) ) ) )
255253, 254syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( m  e.  Z  ->  (
j  e.  ( N ... ( m  + 
1 ) )  <->  ( j  =  N  \/  j  e.  ( ( N  + 
1 ) ... (
m  +  1 ) ) ) ) )
256255biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( m  e.  Z  /\  j  e.  ( N ... ( m  +  1 ) ) )  -> 
( j  =  N  \/  j  e.  ( ( N  +  1 ) ... ( m  +  1 ) ) ) )
257256adantll 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( [. c  / 
a ]. [. d  / 
b ]. ph  /\  m  e.  Z )  /\  j  e.  ( N ... (
m  +  1 ) ) )  ->  (
j  =  N  \/  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) ) )
258257adantlr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  e.  ( N ... ( m  +  1 ) ) )  -> 
( j  =  N  \/  j  e.  ( ( N  +  1 ) ... ( m  +  1 ) ) ) )
259 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( j  =  N  ->  (
j  -  1 )  =  ( N  - 
1 ) )
26047oveq1i 5884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( N  -  1 )  =  ( ( M  + 
1 )  -  1 )
261260, 192eqtri 2316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( N  -  1 )  =  M
262259, 261syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  =  N  ->  (
j  -  1 )  =  M )
263262fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( 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 ) )
264263ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( 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 ) )
265220adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  M )  =  c )
266264, 265eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( j  -  1 ) )  =  c )
267 dfsbcq 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( 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 ) )
268266, 267syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( 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 ) )
26947eqeq2i 2306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( j  =  N  <->  j  =  ( M  +  1
) )
270 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( 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
) ) )
271269, 270sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( 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
) ) )
272271ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( 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
) ) )
27349, 163, 50ltleii 8957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  M  <_ 
( M  +  1 )
274 eluz2 10252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( M  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( M  +  1 )  e.  ZZ  /\  M  <_ 
( M  +  1 ) ) )
2752, 52, 273, 274mpbir3an 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( M  +  1 )  e.  ( ZZ>= `  M )
276 fzss1 10846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( M  +  1 )  e.  ( ZZ>= `  M
)  ->  ( ( M  +  1 ) ... ( m  + 
1 ) )  C_  ( M ... ( m  +  1 ) ) )
277275, 276ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( M  +  1 ) ... ( m  + 
1 ) )  C_  ( M ... ( m  +  1 ) )
278 eluzfz1 10819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( m  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... m ) )
279278, 5eleq2s 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( m  e.  Z  ->  M  e.  ( M ... m
) )
280 fzaddel 10842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( ( M  e.  ZZ  /\  m  e.  ZZ )  /\  ( M  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( M  e.  ( M ... m )  <-> 
( M  +  1 )  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) ) )
2812, 179, 280mpanr12 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( M  e.  ZZ  /\  m  e.  ZZ )  ->  ( M  e.  ( M ... m )  <-> 
( M  +  1 )  e.  ( ( M  +  1 ) ... ( m  + 
1 ) ) ) )
2822, 177, 281sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( m  e.  Z  ->  ( M  e.  ( M ... m )  <->  ( M  +  1 )  e.  ( ( M  + 
1 ) ... (
m  +  1 ) ) ) )
283279, 282mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( m  e.  Z  ->  ( M  +  1 )  e.  ( ( M  +  1 ) ... ( m  +  1 ) ) )
284277, 283sseldi 3191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( m  e.  Z  ->  ( M  +  1 )  e.  ( M ... ( m  +  1
) ) )
285 eqeq1 2302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  ( M  + 
1 )  ->  (
x  =  M  <->  ( M  +  1 )  =  M ) )
286 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( x  =  ( M  + 
1 )  ->  (
x  -  1 )  =  ( ( M  +  1 )  - 
1 ) )
287286, 192syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  =  ( M  + 
1 )  ->  (
x  -  1 )  =  M )
288287fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  ( M  + 
1 )  ->  (
g `  ( x  -  1 ) )  =  ( g `  M ) )
289285, 288ifbieq2d 3598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  ( M  + 
1 )  ->  if ( x  =  M ,  c ,  ( g `  ( x  -  1 ) ) )  =  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) ) )
290 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( g `
 M )  e. 
_V
291218, 290ifex 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) )  e.  _V
292289, 210, 291fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( 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 ) ) )
293284, 292syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) )  =  if ( ( M  + 
1 )  =  M ,  c ,  ( g `  M ) ) )
29449, 50gtneii 8946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( M  +  1 )  =/= 
M
295 ifnefalse 3586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( M  +  1 )  =/=  M  ->  if ( ( M  + 
1 )  =  M ,  c ,  ( g `  M ) )  =  ( g `
 M ) )
296294, 295ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  if ( ( M  +  1 )  =  M , 
c ,  ( g `
 M ) )  =  ( g `  M )
297293, 296syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( m  e.  Z  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) )  =  ( g `  M ) )
298297adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  ( M  +  1
) )  =  ( g `  M ) )
299 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
g `  M )  =  d )
300272, 298, 2993eqtrd 2332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  ( ( g `  M )  =  d  /\  j  =  N ) )  ->  (
( x  e.  ( M ... ( m  +  1 ) ) 
|->  if ( x  =  M ,  c ,  ( g `  (
x  -  1 ) ) ) ) `  j )  =  d )
301 dfsbcq 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( ( 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 ) )
302300, 301syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( 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 ) )
303302sbcbidv 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( 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 ) )
304268, 303bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ]. [. d  /  b ]. ph ) )
305304biimparc 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
[. 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 )
306305anassrs 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
307306anassrs 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
308307adantlrr 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( [. 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 )
309 elfzelz 10814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( j  e.  ( ( N  +  1 ) ... ( m  +  1 ) )  ->  j  e.  ZZ )
310309adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) )  ->  j  e.  ZZ )
31147, 52eqeltri 2366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  N  e.  ZZ
312 peano2z 10076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
313311, 312ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( N  +  1 )  e.  ZZ
314 fzsubel 10843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( 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 ) ) ) )
315314biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
316179, 315mpanr2 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( ( 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 ) ) ) )
317316ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
318313, 178, 317sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( m  e.  Z  ->  (
j  e.  ZZ  ->  ( j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) )  -> 
( j  -  1 )  e.  ( ( ( N  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
319318com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( m  e.  Z  ->  (
j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) )  -> 
( j  e.  ZZ  ->  ( j  -  1 )  e.  ( ( ( N  +  1 )  -  1 ) ... ( ( m  +  1 )  - 
1 ) ) ) ) )
320319imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  Z  /\  j  e.  ( ( N  +  1 ) ... ( m  + 
1 ) ) )  ->  ( j  e.  ZZ  ->  ( j  -  1 )  e.  ( (