Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem42 Structured version   Unicode version

Theorem fourierdlem42 31772
Description: The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem42.b  |-  ( ph  ->  B  e.  RR )
fourierdlem42.c  |-  ( ph  ->  C  e.  RR )
fourierdlem42.bc  |-  ( ph  ->  B  <  C )
fourierdlem42.t  |-  T  =  ( C  -  B
)
fourierdlem42.a  |-  ( ph  ->  A  C_  ( B [,] C ) )
fourierdlem42.af  |-  ( ph  ->  A  e.  Fin )
fourierdlem42.ba  |-  ( ph  ->  B  e.  A )
fourierdlem42.ca  |-  ( ph  ->  C  e.  A )
fourierdlem42.d  |-  D  =  ( abs  o.  -  )
fourierdlem42.i  |-  I  =  ( ( A  X.  A )  \  _I  )
fourierdlem42.r  |-  R  =  ran  ( D  |`  I )
fourierdlem42.e  |-  E  =  sup ( R ,  RR ,  `'  <  )
fourierdlem42.x  |-  ( ph  ->  X  e.  RR )
fourierdlem42.y  |-  ( ph  ->  Y  e.  RR )
fourierdlem42.j  |-  J  =  ( topGen `  ran  (,) )
fourierdlem42.k  |-  K  =  ( Jt  ( X [,] Y ) )
fourierdlem42.h  |-  H  =  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A }
fourierdlem42.15  |-  ( ps  <->  ( ( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) ) )
Assertion
Ref Expression
fourierdlem42  |-  ( ph  ->  H  e.  Fin )
Distinct variable groups:    A, a,
b, j, k, x   
x, B    x, C    x, D    E, a, b, j, k    H, a, b, x   
x, I    J, a,
b    K, a, b, x   
x, R    T, a,
b, j, k, x   
x, X    x, Y    ph, a, b, x    ps, j, k
Allowed substitution hints:    ph( j, k)    ps( x, a, b)    B( j, k, a, b)    C( j, k, a, b)    D( j, k, a, b)    R( j, k, a, b)    E( x)    H( j, k)    I(
j, k, a, b)    J( x, j, k)    K( j, k)    X( j, k, a, b)    Y( j, k, a, b)

Proof of Theorem fourierdlem42
Dummy variables  c 
d  i  l  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem42.x . . . . 5  |-  ( ph  ->  X  e.  RR )
2 fourierdlem42.y . . . . 5  |-  ( ph  ->  Y  e.  RR )
3 fourierdlem42.j . . . . . 6  |-  J  =  ( topGen `  ran  (,) )
4 fourierdlem42.k . . . . . 6  |-  K  =  ( Jt  ( X [,] Y ) )
53, 4icccmp 21198 . . . . 5  |-  ( ( X  e.  RR  /\  Y  e.  RR )  ->  K  e.  Comp )
61, 2, 5syl2anc 661 . . . 4  |-  ( ph  ->  K  e.  Comp )
76adantr 465 . . 3  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  K  e.  Comp )
8 fourierdlem42.h . . . . . 6  |-  H  =  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A }
9 ssrab2 3590 . . . . . . 7  |-  { x  e.  ( X [,] Y
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A }  C_  ( X [,] Y )
109a1i 11 . . . . . 6  |-  ( ph  ->  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A }  C_  ( X [,] Y ) )
118, 10syl5eqss 3553 . . . . 5  |-  ( ph  ->  H  C_  ( X [,] Y ) )
12 retop 21136 . . . . . . . . . 10  |-  ( topGen ` 
ran  (,) )  e.  Top
133, 12eqeltri 2551 . . . . . . . . 9  |-  J  e. 
Top
1413a1i 11 . . . . . . . 8  |-  ( ph  ->  J  e.  Top )
151, 2iccssred 31426 . . . . . . . 8  |-  ( ph  ->  ( X [,] Y
)  C_  RR )
16 uniretop 21137 . . . . . . . . . 10  |-  RR  =  U. ( topGen `  ran  (,) )
173unieqi 4260 . . . . . . . . . . 11  |-  U. J  =  U. ( topGen `  ran  (,) )
1817eqcomi 2480 . . . . . . . . . 10  |-  U. ( topGen `
 ran  (,) )  =  U. J
1916, 18eqtri 2496 . . . . . . . . 9  |-  RR  =  U. J
2019restuni 19531 . . . . . . . 8  |-  ( ( J  e.  Top  /\  ( X [,] Y ) 
C_  RR )  -> 
( X [,] Y
)  =  U. ( Jt  ( X [,] Y ) ) )
2114, 15, 20syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( X [,] Y
)  =  U. ( Jt  ( X [,] Y ) ) )
224unieqi 4260 . . . . . . . . 9  |-  U. K  =  U. ( Jt  ( X [,] Y ) )
2322eqcomi 2480 . . . . . . . 8  |-  U. ( Jt  ( X [,] Y ) )  =  U. K
2423a1i 11 . . . . . . 7  |-  ( ph  ->  U. ( Jt  ( X [,] Y ) )  =  U. K )
2521, 24eqtrd 2508 . . . . . 6  |-  ( ph  ->  ( X [,] Y
)  =  U. K
)
26 eqid 2467 . . . . . . 7  |-  U. K  =  U. K
2726a1i 11 . . . . . 6  |-  ( ph  ->  U. K  =  U. K )
2825, 27eqtrd 2508 . . . . 5  |-  ( ph  ->  ( X [,] Y
)  =  U. K
)
2911, 28sseqtrd 3545 . . . 4  |-  ( ph  ->  H  C_  U. K )
3029adantr 465 . . 3  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  H  C_ 
U. K )
31 simpr 461 . . 3  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  -.  H  e.  Fin )
3226bwth 19778 . . 3  |-  ( ( K  e.  Comp  /\  H  C_ 
U. K  /\  -.  H  e.  Fin )  ->  E. x  e.  U. K x  e.  (
( limPt `  K ) `  H ) )
337, 30, 31, 32syl3anc 1228 . 2  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  E. x  e.  U. K x  e.  ( ( limPt `  K
) `  H )
)
3411, 15sstrd 3519 . . . . . . . . . . . 12  |-  ( ph  ->  H  C_  RR )
3534adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  U. K )  ->  H  C_  RR )
3635adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  H  C_  RR )
37 ne0i 3796 . . . . . . . . . . 11  |-  ( x  e.  ( ( limPt `  J ) `  H
)  ->  ( ( limPt `  J ) `  H )  =/=  (/) )
3837adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  -> 
( ( limPt `  J
) `  H )  =/=  (/) )
39 fourierdlem42.e . . . . . . . . . . . . 13  |-  E  =  sup ( R ,  RR ,  `'  <  )
40 fourierdlem42.r . . . . . . . . . . . . . . 15  |-  R  =  ran  ( D  |`  I )
41 absf 13150 . . . . . . . . . . . . . . . . . . . . 21  |-  abs : CC
--> RR
42 ffn 5737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
4341, 42ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  abs  Fn  CC
44 subf 9834 . . . . . . . . . . . . . . . . . . . . 21  |-  -  :
( CC  X.  CC )
--> CC
45 ffn 5737 . . . . . . . . . . . . . . . . . . . . 21  |-  (  -  : ( CC  X.  CC ) --> CC  ->  -  Fn  ( CC  X.  CC ) )
4644, 45ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  -  Fn  ( CC  X.  CC )
47 frn 5743 . . . . . . . . . . . . . . . . . . . . 21  |-  (  -  : ( CC  X.  CC ) --> CC  ->  ran  - 
C_  CC )
4844, 47ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ran  -  C_  CC
49 fnco 5695 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( abs  Fn  CC  /\  -  Fn  ( CC  X.  CC )  /\  ran  -  C_  CC )  ->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) )
5043, 46, 48, 49mp3an 1324 . . . . . . . . . . . . . . . . . . 19  |-  ( abs 
o.  -  )  Fn  ( CC  X.  CC )
51 fourierdlem42.d . . . . . . . . . . . . . . . . . . . 20  |-  D  =  ( abs  o.  -  )
5251fneq1i 5681 . . . . . . . . . . . . . . . . . . 19  |-  ( D  Fn  ( CC  X.  CC )  <->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) )
5350, 52mpbir 209 . . . . . . . . . . . . . . . . . 18  |-  D  Fn  ( CC  X.  CC )
5453a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  D  Fn  ( CC 
X.  CC ) )
55 fourierdlem42.i . . . . . . . . . . . . . . . . . 18  |-  I  =  ( ( A  X.  A )  \  _I  )
56 fourierdlem42.a . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  C_  ( B [,] C ) )
57 fourierdlem42.b . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  RR )
58 fourierdlem42.c . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  C  e.  RR )
5957, 58iccssred 31426 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( B [,] C
)  C_  RR )
60 ax-resscn 9561 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  C_  CC
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  RR  C_  CC )
6259, 61sstrd 3519 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( B [,] C
)  C_  CC )
6356, 62sstrd 3519 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  C_  CC )
64 xpss12 5114 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  C_  CC  /\  A  C_  CC )  ->  ( A  X.  A )  C_  ( CC  X.  CC ) )
6563, 63, 64syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  X.  A
)  C_  ( CC  X.  CC ) )
66 ssdifss 3640 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  X.  A ) 
C_  ( CC  X.  CC )  ->  ( ( A  X.  A ) 
\  _I  )  C_  ( CC  X.  CC ) )
6765, 66syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  X.  A )  \  _I  )  C_  ( CC  X.  CC ) )
6855, 67syl5eqss 3553 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  I  C_  ( CC  X.  CC ) )
69 fnssres 5700 . . . . . . . . . . . . . . . . 17  |-  ( ( D  Fn  ( CC 
X.  CC )  /\  I  C_  ( CC  X.  CC ) )  ->  ( D  |`  I )  Fn  I )
7054, 68, 69syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  |`  I )  Fn  I )
71 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  I )
72 fvres 5886 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  I  ->  (
( D  |`  I ) `
 x )  =  ( D `  x
) )
7371, 72syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  =  ( D `  x
) )
7451fveq1i 5873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D `
 x )  =  ( ( abs  o.  -  ) `  x
)
7574a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  I )  ->  ( D `  x )  =  ( ( abs 
o.  -  ) `  x ) )
76 ffun 5739 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (  -  : ( CC  X.  CC ) --> CC  ->  Fun  -  )
7744, 76ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  Fun  -
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  I )  ->  Fun  -  )
7968adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  I )  ->  I  C_  ( CC  X.  CC ) )
8079, 71sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  ( CC  X.  CC ) )
8144fdmi 5742 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  dom  -  =  ( CC  X.  CC )
8281eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( CC 
X.  CC )  =  dom  -
8382a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  I )  ->  ( CC  X.  CC )  =  dom  -  )
8480, 83eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  dom  -  )
85 fvco 5950 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Fun  -  /\  x  e.  dom  -  )  -> 
( ( abs  o.  -  ) `  x
)  =  ( abs `  (  -  `  x
) ) )
8678, 84, 85syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  I )  ->  (
( abs  o.  -  ) `  x )  =  ( abs `  (  -  `  x ) ) )
8773, 75, 863eqtrd 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  =  ( abs `  (  -  `  x ) ) )
8841a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  I )  ->  abs : CC --> RR )
8944a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  I )  ->  -  :
( CC  X.  CC )
--> CC )
9089, 80ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  I )  ->  (  -  `  x )  e.  CC )
9188, 90ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  ( abs `  (  -  `  x ) )  e.  RR )
9287, 91eqeltrd 2555 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  e.  RR )
93 elxp2 5023 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( CC  X.  CC )  <->  E. y  e.  CC  E. z  e.  CC  x  =  <. y ,  z
>. )
9480, 93sylib 196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  I )  ->  E. y  e.  CC  E. z  e.  CC  x  =  <. y ,  z >. )
95 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  <. y ,  z
>.  ->  (  -  `  x )  =  (  -  `  <. y ,  z >. )
)
96953ad2ant3 1019 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  x
)  =  (  -  ` 
<. y ,  z >.
) )
97 df-ov 6298 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  -  z )  =  (  -  `  <. y ,  z >. )
98 simp1l 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  ph )
99 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  x  =  <. y ,  z
>. )
10099eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  <. y ,  z >.  =  x )
101 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  x  e.  I )
102100, 101eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  <. y ,  z >.  e.  I
)
103102adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  I )  /\  x  =  <. y ,  z
>. )  ->  <. y ,  z >.  e.  I
)
1041033adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  -> 
<. y ,  z >.  e.  I )
10563adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  A  C_  CC )
10655eleq2i 2545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( <.
y ,  z >.  e.  I  <->  <. y ,  z
>.  e.  ( ( A  X.  A )  \  _I  ) )
107106biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( <.
y ,  z >.  e.  I  ->  <. y ,  z >.  e.  ( ( A  X.  A
)  \  _I  )
)
108 eldif 3491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( <.
y ,  z >.  e.  ( ( A  X.  A )  \  _I  ) 
<->  ( <. y ,  z
>.  e.  ( A  X.  A )  /\  -.  <.
y ,  z >.  e.  _I  ) )
109107, 108sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( <.
y ,  z >.  e.  I  ->  ( <.
y ,  z >.  e.  ( A  X.  A
)  /\  -.  <. y ,  z >.  e.  _I  ) )
110109simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
y ,  z >.  e.  I  ->  <. y ,  z >.  e.  ( A  X.  A ) )
111 opelxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
y ,  z >.  e.  ( A  X.  A
)  <->  ( y  e.  A  /\  z  e.  A ) )
112110, 111sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
y ,  z >.  e.  I  ->  ( y  e.  A  /\  z  e.  A ) )
113112adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  ( y  e.  A  /\  z  e.  A ) )
114113simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  e.  A )
115105, 114sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  e.  CC )
116113simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  z  e.  A )
117105, 116sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  z  e.  CC )
118109simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( <.
y ,  z >.  e.  I  ->  -.  <. y ,  z >.  e.  _I  )
119 df-br 4454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  _I  z  <->  <. y ,  z >.  e.  _I  )
120118, 119sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
y ,  z >.  e.  I  ->  -.  y  _I  z )
121 vex 3121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  z  e. 
_V
122 ideqg 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  e.  _V  ->  (
y  _I  z  <->  y  =  z ) )
123121, 122ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  _I  z  <->  y  =  z )
124120, 123sylnib 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
y ,  z >.  e.  I  ->  -.  y  =  z )
125124neqned 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
y ,  z >.  e.  I  ->  y  =/=  z )
126125adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  =/=  z )
127115, 117, 126subne0d 9951 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  ( y  -  z )  =/=  0 )
12898, 104, 127syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  ( y  -  z
)  =/=  0 )
12997, 128syl5eqner 2768 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  <. y ,  z >. )  =/=  0 )
13096, 129eqnetrd 2760 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  x
)  =/=  0 )
1311303exp 1195 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  I )  ->  (
( y  e.  CC  /\  z  e.  CC )  ->  ( x  = 
<. y ,  z >.  ->  (  -  `  x
)  =/=  0 ) ) )
132131rexlimdvv 2965 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  I )  ->  ( E. y  e.  CC  E. z  e.  CC  x  =  <. y ,  z
>.  ->  (  -  `  x )  =/=  0
) )
13394, 132mpd 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  I )  ->  (  -  `  x )  =/=  0 )
134 absgt0 13137 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (  -  `  x )  e.  CC  ->  (
(  -  `  x
)  =/=  0  <->  0  <  ( abs `  (  -  `  x ) ) ) )
13590, 134syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  I )  ->  (
(  -  `  x
)  =/=  0  <->  0  <  ( abs `  (  -  `  x ) ) ) )
136133, 135mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  0  <  ( abs `  (  -  `  x ) ) )
13787eqcomd 2475 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  ( abs `  (  -  `  x ) )  =  ( ( D  |`  I ) `  x
) )
138136, 137breqtrd 4477 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  0  <  ( ( D  |`  I ) `  x
) )
13992, 138jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (
( ( D  |`  I ) `  x
)  e.  RR  /\  0  <  ( ( D  |`  I ) `  x
) ) )
140 elrp 11234 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( D  |`  I ) `
 x )  e.  RR+ 
<->  ( ( ( D  |`  I ) `  x
)  e.  RR  /\  0  <  ( ( D  |`  I ) `  x
) ) )
141139, 140sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  e.  RR+ )
142141ralrimiva 2881 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. x  e.  I 
( ( D  |`  I ) `  x
)  e.  RR+ )
143 fnfvrnss 6060 . . . . . . . . . . . . . . . 16  |-  ( ( ( D  |`  I )  Fn  I  /\  A. x  e.  I  (
( D  |`  I ) `
 x )  e.  RR+ )  ->  ran  ( D  |`  I )  C_  RR+ )
14470, 142, 143syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ran  ( D  |`  I )  C_  RR+ )
14540, 144syl5eqss 3553 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  C_  RR+ )
146 ltso 9677 . . . . . . . . . . . . . . . . 17  |-  <  Or  RR
147146a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  <  Or  RR )
148 cnvso 5552 . . . . . . . . . . . . . . . 16  |-  (  < 
Or  RR  <->  `'  <  Or  RR )
149147, 148sylib 196 . . . . . . . . . . . . . . 15  |-  ( ph  ->  `'  <  Or  RR )
150 fneq1 5675 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  =  ( abs  o.  -  )  ->  ( D  Fn  ( CC  X.  CC )  <->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) ) )
15151, 150ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( D  Fn  ( CC  X.  CC )  <->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) )
15250, 151mpbir 209 . . . . . . . . . . . . . . . . . . . 20  |-  D  Fn  ( CC  X.  CC )
153152a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  D  Fn  ( CC 
X.  CC ) )
154153, 68, 69syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  |`  I )  Fn  I )
155 fourierdlem42.af . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  Fin )
156 xpfi 7803 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  Fin  /\  A  e.  Fin )  ->  ( A  X.  A
)  e.  Fin )
157155, 155, 156syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  X.  A
)  e.  Fin )
158 diffi 7763 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  X.  A )  e.  Fin  ->  (
( A  X.  A
)  \  _I  )  e.  Fin )
159157, 158syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( A  X.  A )  \  _I  )  e.  Fin )
16055, 159syl5eqel 2559 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  I  e.  Fin )
161 fnfi 7810 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( D  |`  I )  Fn  I  /\  I  e.  Fin )  ->  ( D  |`  I )  e. 
Fin )
162154, 160, 161syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  |`  I )  e.  Fin )
163 rnfi 7817 . . . . . . . . . . . . . . . . 17  |-  ( ( D  |`  I )  e.  Fin  ->  ran  ( D  |`  I )  e.  Fin )
164162, 163syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  ( D  |`  I )  e.  Fin )
16540, 164syl5eqel 2559 . . . . . . . . . . . . . . 15  |-  ( ph  ->  R  e.  Fin )
16640a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  R  =  ran  ( D  |`  I ) )
16751a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  D  =  ( abs 
o.  -  ) )
168167reseq1d 5278 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( D  |`  I )  =  ( ( abs 
o.  -  )  |`  I ) )
169168fveq1d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  |`  I ) `  <. B ,  C >. )  =  ( ( ( abs  o.  -  )  |`  I ) `  <. B ,  C >. )
)
170 fourierdlem42.ba . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  e.  A )
171 fourierdlem42.ca . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  C  e.  A )
172170, 171jca 532 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( B  e.  A  /\  C  e.  A
) )
173 opelxp 5035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <. B ,  C >.  e.  ( A  X.  A
)  <->  ( B  e.  A  /\  C  e.  A ) )
174172, 173sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> 
<. B ,  C >.  e.  ( A  X.  A
) )
175 fourierdlem42.bc . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  B  <  C )
17657, 175ltned 9732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  =/=  C )
177176neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  -.  B  =  C )
178 ideqg 5160 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( C  e.  A  ->  ( B  _I  C  <->  B  =  C ) )
179171, 178syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( B  _I  C  <->  B  =  C ) )
180177, 179mtbird 301 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  -.  B  _I  C
)
181 df-br 4454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B  _I  C  <->  <. B ,  C >.  e.  _I  )
182180, 181sylnib 304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  <. B ,  C >.  e.  _I  )
183174, 182eldifd 3492 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  -> 
<. B ,  C >.  e.  ( ( A  X.  A )  \  _I  ) )
184183, 55syl6eleqr 2566 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
<. B ,  C >.  e.  I )
185 fvres 5886 . . . . . . . . . . . . . . . . . . . 20  |-  ( <. B ,  C >.  e.  I  ->  ( (
( abs  o.  -  )  |`  I ) `  <. B ,  C >. )  =  ( ( abs 
o.  -  ) `  <. B ,  C >. ) )
186184, 185syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( abs 
o.  -  )  |`  I ) `
 <. B ,  C >. )  =  ( ( abs  o.  -  ) `  <. B ,  C >. ) )
18777a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  Fun  -  )
18863, 170sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  e.  CC )
18963, 171sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  C  e.  CC )
190188, 189jca 532 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( B  e.  CC  /\  C  e.  CC ) )
191 opelxp 5035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <. B ,  C >.  e.  ( CC  X.  CC ) 
<->  ( B  e.  CC  /\  C  e.  CC ) )
192190, 191sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> 
<. B ,  C >.  e.  ( CC  X.  CC ) )
193192, 81syl6eleqr 2566 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  -> 
<. B ,  C >.  e. 
dom  -  )
194 fvco 5950 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Fun  -  /\  <. B ,  C >.  e.  dom  -  )  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  (  -  `  <. B ,  C >. ) ) )
195187, 193, 194syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  (  -  `  <. B ,  C >. ) ) )
196 df-ov 6298 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B  -  C )  =  (  -  `  <. B ,  C >. )
197196eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . 22  |-  (  -  ` 
<. B ,  C >. )  =  ( B  -  C )
198197a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  (  -  `  <. B ,  C >. )  =  ( B  -  C ) )
199198fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( abs `  (  -  `  <. B ,  C >. ) )  =  ( abs `  ( B  -  C ) ) )
200195, 199eqtrd 2508 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  ( B  -  C )
) )
201169, 186, 2003eqtrrd 2513 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  ( B  -  C )
)  =  ( ( D  |`  I ) `  <. B ,  C >. ) )
202 fnfvelrn 6029 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( D  |`  I )  Fn  I  /\  <. B ,  C >.  e.  I
)  ->  ( ( D  |`  I ) `  <. B ,  C >. )  e.  ran  ( D  |`  I ) )
203154, 184, 202syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  |`  I ) `  <. B ,  C >. )  e.  ran  ( D  |`  I ) )
204201, 203eqeltrd 2555 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( abs `  ( B  -  C )
)  e.  ran  ( D  |`  I ) )
205 ne0i 3796 . . . . . . . . . . . . . . . . 17  |-  ( ( abs `  ( B  -  C ) )  e.  ran  ( D  |`  I )  ->  ran  ( D  |`  I )  =/=  (/) )
206204, 205syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  ( D  |`  I )  =/=  (/) )
207166, 206eqnetrd 2760 . . . . . . . . . . . . . . 15  |-  ( ph  ->  R  =/=  (/) )
208 resss 5303 . . . . . . . . . . . . . . . . . . 19  |-  ( D  |`  I )  C_  D
209 rnss 5237 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  |`  I )  C_  D  ->  ran  ( D  |`  I )  C_  ran  D )
210208, 209ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ran  ( D  |`  I )  C_  ran  D
21151rneqi 5235 . . . . . . . . . . . . . . . . . . 19  |-  ran  D  =  ran  ( abs  o.  -  )
212 rncoss 5269 . . . . . . . . . . . . . . . . . . . 20  |-  ran  ( abs  o.  -  )  C_  ran  abs
213 frn 5743 . . . . . . . . . . . . . . . . . . . . 21  |-  ( abs
: CC --> RR  ->  ran 
abs  C_  RR )
21441, 213mp1i 12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( abs : CC --> RR  ->  ran 
abs  C_  RR )  ->  ran  abs  C_  RR )
215213, 214ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ran  abs  C_  RR
216212, 215sstri 3518 . . . . . . . . . . . . . . . . . . 19  |-  ran  ( abs  o.  -  )  C_  RR
217211, 216eqsstri 3539 . . . . . . . . . . . . . . . . . 18  |-  ran  D  C_  RR
218210, 217sstri 3518 . . . . . . . . . . . . . . . . 17  |-  ran  ( D  |`  I )  C_  RR
21940, 218eqsstri 3539 . . . . . . . . . . . . . . . 16  |-  R  C_  RR
220219a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  R  C_  RR )
221 fisupcl 7939 . . . . . . . . . . . . . . 15  |-  ( ( `'  <  Or  RR  /\  ( R  e.  Fin  /\  R  =/=  (/)  /\  R  C_  RR ) )  ->  sup ( R ,  RR ,  `'  <  )  e.  R )
222149, 165, 207, 220, 221syl13anc 1230 . . . . . . . . . . . . . 14  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  R )
223145, 222sseldd 3510 . . . . . . . . . . . . 13  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  RR+ )
22439, 223syl5eqel 2559 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  RR+ )
225224adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  U. K )  ->  E  e.  RR+ )
226225adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  E  e.  RR+ )
2273, 36, 38, 226lptre2pt 31505 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  E. y  e.  H  E. z  e.  H  ( y  =/=  z  /\  ( abs `  (
y  -  z ) )  <  E ) )
228 id 22 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ph )
229228ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  ph )
23034sselda 3509 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  H )  ->  y  e.  RR )
231230adantrr 716 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  H  /\  z  e.  H ) )  -> 
y  e.  RR )
232231adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  y  e.  RR )
23334sselda 3509 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  H )  ->  z  e.  RR )
234233adantrl 715 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  H  /\  z  e.  H ) )  -> 
z  e.  RR )
235234adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  z  e.  RR )
236 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  y  =/=  z )
237232, 235, 2363jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  (
y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )
238229, 237jca 532 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) ) )
2398eleq2i 2545 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  H  <->  y  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A }
)
240239biimpi 194 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  H  ->  y  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A } )
241 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  y  ->  (
x  +  ( k  x.  T ) )  =  ( y  +  ( k  x.  T
) ) )
242241eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
( x  +  ( k  x.  T ) )  e.  A  <->  ( y  +  ( k  x.  T ) )  e.  A ) )
243242rexbidv 2978 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  A
) )
244 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
245244oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  j  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
246245eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  j  ->  (
( y  +  ( k  x.  T ) )  e.  A  <->  ( y  +  ( j  x.  T ) )  e.  A ) )
247246cbvrexv 3094 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  A  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
)
248243, 247syl6bb 261 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
) )
249248elrab 3266 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  { x  e.  ( X [,] Y
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A } 
<->  ( y  e.  ( X [,] Y )  /\  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
) )
250240, 249sylib 196 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  H  ->  (
y  e.  ( X [,] Y )  /\  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  A ) )
251250simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  H  ->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
)
252251adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. j  e.  ZZ  ( y  +  ( j  x.  T ) )  e.  A )
2538eleq2i 2545 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  H  <->  z  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A }
)
254253biimpi 194 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  H  ->  z  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A } )
255 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
x  +  ( k  x.  T ) )  =  ( z  +  ( k  x.  T
) ) )
256255eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  (
( x  +  ( k  x.  T ) )  e.  A  <->  ( z  +  ( k  x.  T ) )  e.  A ) )
257256rexbidv 2978 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
) )
258257elrab 3266 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  { x  e.  ( X [,] Y
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A } 
<->  ( z  e.  ( X [,] Y )  /\  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
) )
259254, 258sylib 196 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  H  ->  (
z  e.  ( X [,] Y )  /\  E. k  e.  ZZ  (
z  +  ( k  x.  T ) )  e.  A ) )
260259simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  H  ->  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
)
261260adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. k  e.  ZZ  ( z  +  ( k  x.  T ) )  e.  A )
262252, 261jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  H  /\  z  e.  H )  ->  ( E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A  /\  E. k  e.  ZZ  ( z  +  ( k  x.  T ) )  e.  A ) )
263 reeanv 3034 . . . . . . . . . . . . . . . . 17  |-  ( E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A )  <-> 
( E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A  /\  E. k  e.  ZZ  ( z  +  ( k  x.  T ) )  e.  A ) )
264262, 263sylibr 212 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) )
265264ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  E. j  e.  ZZ  E. k  e.  ZZ  ( ( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) )
266228ad3antrrr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) )  /\  y  <  z )  ->  ph )
267 simpl1 999 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
y  e.  RR )
268 simpl2 1000 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
z  e.  RR )
269 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
y  <  z )
270267, 268, 2693jca 1176 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
271270adantll 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
272271adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
273 simplr 754 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) )  /\  y  <  z )  ->  E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) )
274 nfv 1683 . . . . . . . . . . . . . . . . . 18  |-  F/ b ( ( ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  ( abs `  (
y  -  z ) ) )
275 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  z  ->  (
b  e.  RR  <->  z  e.  RR ) )
276 breq2 4457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  z  ->  (
y  <  b  <->  y  <  z ) )
277275, 2763anbi23d 1302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
( y  e.  RR  /\  b  e.  RR  /\  y  <  b )  <->  ( y  e.  RR  /\  z  e.  RR  /\  y  < 
z ) ) )
278277anbi2d 703 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  (
( ph  /\  (
y  e.  RR  /\  b  e.  RR  /\  y  <  b ) )  <->  ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) ) ) )
279 nfv 1683 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ j  b  =  z
280 nfv 1683 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ k  b  =  z
281 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  z  ->  (
b  +  ( k  x.  T ) )  =  ( z  +  ( k  x.  T
) ) )
282281eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  z  ->  (
( b  +  ( k  x.  T ) )  e.  A  <->  ( z  +  ( k  x.  T ) )  e.  A ) )
283282anbi2d 703 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  z  ->  (
( ( y  +  ( j  x.  T
) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A )  <-> 
( ( y  +  ( j  x.  T
) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) ) )
284280, 283rexbid 2977 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  ( E. k  e.  ZZ  ( ( y  +  ( j  x.  T
) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A )  <->  E. k  e.  ZZ  ( ( y  +  ( j  x.  T
) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) ) )
285279, 284rexbid 2977 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  ( E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A )  <->  E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) ) )
286278, 285anbi12d 710 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  z  ->  (
( ( ph  /\  ( y  e.  RR  /\  b  e.  RR  /\  y  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( y  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  <->  ( ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  < 
z ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) ) ) )
287 oveq2 6303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
y  -  b )  =  ( y  -  z ) )
288287fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  ( abs `  ( y  -  b ) )  =  ( abs `  (
y  -  z ) ) )
289288breq2d 4465 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  z  ->  ( E  <_  ( abs `  (
y  -  b ) )  <->  E  <_  ( abs `  ( y  -  z
) ) ) )
290286, 289imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  z  ->  (
( ( ( ph  /\  ( y  e.  RR  /\  b  e.  RR  /\  y  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( y  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  ( abs `  (
y  -  b ) ) )  <->  ( (
( ph  /\  (
y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( z  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  ( abs `  ( y  -  z ) ) ) ) )
291 nfv 1683 . . . . . . . . . . . . . . . . . . 19  |-  F/ a ( ( ( ph  /\  ( y  e.  RR  /\  b  e.  RR  /\  y  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( y  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  ( abs `  (
y  -  b ) ) )
292 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  y  ->  (
a  e.  RR  <->  y  e.  RR ) )
293 breq1 4456 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  y  ->  (
a  <  b  <->  y  <  b ) )
294292, 2933anbi13d 1301 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
( a  e.  RR  /\  b  e.  RR  /\  a  <  b )  <->  ( y  e.  RR  /\  b  e.  RR  /\  y  < 
b ) ) )
295294anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  (
( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  <->  ( ph  /\  ( y  e.  RR  /\  b  e.  RR  /\  y  <  b ) ) ) )
296 nfv 1683 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ j  a  =  y
297 nfv 1683 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ k  a  =  y
298 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  y  ->  (
a  +  ( j  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
299298eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  y  ->  (
( a  +  ( j  x.  T ) )  e.  A  <->  ( y  +  ( j  x.  T ) )  e.  A ) )
300299anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  y  ->  (
( ( a  +  ( j  x.  T
) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A )  <-> 
( ( y  +  ( j  x.  T
) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) ) )
301297, 300rexbid 2977 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  ( E. k  e.  ZZ  ( ( a  +  ( j  x.  T
) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A )  <->  E. k  e.  ZZ  ( ( y  +  ( j  x.  T
) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) ) )
302296, 301rexbid 2977 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  ( E. j  e.  ZZ  E. k  e.  ZZ  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A )  <->  E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) ) )
303295, 302anbi12d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  y  ->  (
( ( ph  /\  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  <->  ( ( ph  /\  ( y  e.  RR  /\  b  e.  RR  /\  y  < 
b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) ) ) )
304 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
a  -  b )  =  ( y  -  b ) )
305304fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  ( abs `  ( a  -  b ) )  =  ( abs `  (
y  -  b ) ) )
306305breq2d 4465 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  y  ->  ( E  <_  ( abs `  (
a  -  b ) )  <->  E  <_  ( abs `  ( y  -  b
) ) ) )
307303, 306imbi12d 320 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  y  ->  (
( ( ( ph  /\  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  ( abs `  (
a  -  b ) ) )  <->  ( (
( ph  /\  (
y  e.  RR  /\  b  e.  RR  /\  y  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  (
( y  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  ( abs `  ( y  -  b ) ) ) ) )
308 fourierdlem42.15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ps  <->  ( ( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) ) )
309308biimpri 206 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  ps )
310308simprbi 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ps 
->  E. j  e.  ZZ  E. k  e.  ZZ  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )
311308biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  ( ( ph  /\  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  /\  E. j  e.  ZZ  E. k  e.  ZZ  ( ( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) ) )
312311simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  ( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) ) )
313312simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  ph )
314313, 57syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  B  e.  RR )
315314adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  B  e.  RR )
316313, 58syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  C  e.  RR )
317316adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  C  e.  RR )
318313, 56syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  A  C_  ( B [,] C ) )
319318sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( b  +  ( k  x.  T ) )  e.  A )  ->  (
b  +  ( k  x.  T ) )  e.  ( B [,] C ) )
320319adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( b  +  ( k  x.  T
) )  e.  ( B [,] C ) )
321318adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( a  +  ( j  x.  T ) )  e.  A )  ->  A  C_  ( B [,] C
) )
322 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( a  +  ( j  x.  T ) )  e.  A )  ->  (
a  +  ( j  x.  T ) )  e.  A )
323321, 322sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( a  +  ( j  x.  T ) )  e.  A )  ->  (
a  +  ( j  x.  T ) )  e.  ( B [,] C ) )
324323adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( a  +  ( j  x.  T
) )  e.  ( B [,] C ) )
325315, 317, 320, 324iccsuble 31446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  ( C  -  B )
)
326 fourierdlem42.t . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  T  =  ( C  -  B
)
327326eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( C  -  B )  =  T
328327a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( C  -  B )  =  T )
329325, 328breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T
)
3303293adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) )  <_  T )
331330adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )  /\  ( ( a  +  ( j  x.  T
) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  /\  -.  k  <_  j )  ->  (
( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T )
332 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  -.  k  <_  j )
333 zre 10880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  e.  ZZ  ->  j  e.  RR )
334333adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  j  e.  RR )
335334ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  j  e.  RR )
336 zre 10880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  ZZ  ->  k  e.  RR )
337336adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  k  e.  RR )
338337ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  k  e.  RR )
339335, 338ltnled 9743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  (
j  <  k  <->  -.  k  <_  j ) )
340332, 339mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  j  <  k )
34158, 57resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( C  -  B
)  e.  RR )
342326, 341syl5eqel 2559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  T  e.  RR )
343313, 342syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  T  e.  RR )
344343adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  ->  T  e.  RR )
345344adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  e.  RR )
346337adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  e.  RR )
347334adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
j  e.  RR )
348346, 347resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  -  j
)  e.  RR )
349348, 344remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  e.  RR )
350349adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
k  -  j )  x.  T )  e.  RR )
351312simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ps 
->  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )
352351simp2d 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ps 
->  b  e.  RR )
353352adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
b  e.  RR )
354336adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  e.  RR )
355343adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  e.  RR )
356354, 355remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  RR )
357356adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  x.  T
)  e.  RR )
358353, 357readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( b  +  ( k  x.  T ) )  e.  RR )
359351simp1d 1008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ps 
->  a  e.  RR )
360359adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
a  e.  RR )
361333adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  j  e.  ZZ )  ->  j  e.  RR )
362343adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  j  e.  ZZ )  ->  T  e.  RR )
363361, 362remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  j  e.  ZZ )  ->  (
j  x.  T )  e.  RR )
364363adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  x.  T
)  e.  RR )
365360, 364readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( a  +  ( j  x.  T ) )  e.  RR )
366358, 365resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  e.  RR )
367366adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) )  e.  RR )
368343recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ps 
->  T  e.  CC )
369368mulid2d 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ps 
->  ( 1  x.  T
)  =  T )
370369eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  T  =  (
1  x.  T ) )
371370ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  =  ( 1  x.  T
) )
372 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  <  k )
373 simplrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  e.  ZZ )
374 simplrr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  k  e.  ZZ )
375 zltlem1 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  <  k  <->  j  <_  ( k  - 
1 ) ) )
376373, 374, 375syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( j  <  k  <->  j  <_  (
k  -  1 ) ) )
377372, 376mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  <_  ( k  -  1 ) )
378 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  j  <_  ( k  -  1 ) )
379347adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  j  e.  RR )
380 peano2rem 9898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( k  e.  RR  ->  (
k  -  1 )  e.  RR )
381346, 380syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  -  1 )  e.  RR )
382381adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( k  -  1 )  e.  RR )
383 1re 9607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  1  e.  RR
384383a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  1  e.  RR )
385384, 379jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( 1  e.  RR  /\  j  e.  RR ) )
386 resubcl 9895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( 1  e.  RR  /\  j  e.  RR )  ->  ( 1  -  j
)  e.  RR )
387385, 386syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( 1  -  j )  e.  RR )
388379, 382, 387leadd1d 10158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  <_  ( k  -  1 )  <->  ( j  +  ( 1  -  j
) )  <_  (
( k  -  1 )  +  ( 1  -  j ) ) ) )
389378, 388mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  +  ( 1  -  j ) )  <_ 
( ( k  - 
1 )  +  ( 1  -  j ) ) )
390333recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( j  e.  ZZ  ->  j  e.  CC )
391390adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  j  e.  CC )
392 ax-1cn 9562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  1  e.  CC
393392a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  1  e.  CC )
394391, 393pncan3d 9945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  +  ( 1  -  j ) )  =  1 )
395394ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  +  ( 1  -  j ) )  =  1 )
396336recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( k  e.  ZZ  ->  k  e.  CC )
397396adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  k  e.  CC )
398397, 393, 391npncand 9966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( ( k  - 
1 )  +  ( 1  -  j ) )  =  ( k  -  j ) )
399398ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( (
k  -  1 )  +  ( 1  -  j ) )  =  ( k  -  j
) )
400395, 399breq12d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( (
j  +  ( 1  -  j ) )  <_  ( ( k  -  1 )  +  ( 1  -  j
) )  <->  1  <_  ( k  -  j ) ) )
401389, 400mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  1  <_  ( k  -  j ) )
402401ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  <_  (
k  -  1 )  ->  1  <_  (
k  -  j ) ) )
403402adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( j  <_  ( k  -  1 )  ->  1  <_  ( k  -  j ) ) )
404377, 403mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  1  <_  ( k  -  j ) )
405383a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  1  e.  RR )
406348adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( k  -  j )  e.  RR )
40757, 58posdifd 10151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ph  ->  ( B  <  C  <->  0  <  ( C  -  B ) ) )
408175, 407mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ph  ->  0  <  ( C  -  B ) )
409327a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ph  ->  ( C  -  B
)  =  T )
410408, 409breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  0  <  T )
411342, 410elrpd 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  T  e.  RR+ )
412313, 411syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ps 
->  T  e.  RR+ )
413412ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  e.  RR+ )
414405, 406, 413lemul1d 11307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( 1  <_  ( k  -  j )  <->  ( 1  x.  T )  <_ 
( ( k  -  j )  x.  T
) ) )
415404, 414mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( 1  x.  T )  <_ 
( ( k  -  j )  x.  T
) )
416371, 415eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  <_  ( ( k  -  j
)  x.  T ) )
417352, 359resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ps 
->  ( b  -  a
)  e.  RR )
418351simp3d 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ps 
->  a  <  b )
419359, 352posdifd 10151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ps 
->  ( a  <  b  <->  0  <  ( b  -  a ) ) )
420418, 419mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ps 
->  0  <  ( b  -  a ) )
421417, 420elrpd 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ps 
->  ( b  -  a
)  e.  RR+ )
422421adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( b  -  a
)  e.  RR+ )
423349, 422ltaddrp2d 11298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  <  ( (
b  -  a )  +  ( ( k  -  j )  x.  T ) ) )
424352recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ps 
->  b  e.  CC )
425424adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
b  e.  CC )
426356recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  CC )
427426adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  x.  T
)  e.  CC )
428359recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ps 
->  a  e.  CC )
429428adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
a  e.  CC )
430363recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  j  e.  ZZ )  ->  (
j  x.  T )  e.  CC )
431430adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  x.  T
)  e.  CC )
432425, 427, 429, 431addsub4d 9989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  =  ( ( b  -  a )  +  ( ( k  x.  T )  -  ( j  x.  T
) ) ) )
433396ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  e.  CC )
434390ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
j  e.  CC )
435368adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  ->  T  e.  CC )
436433, 434, 435subdird 10025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  =  ( ( k  x.  T )  -  ( j  x.  T ) ) )
437436eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  x.  T )  -  (
j  x.  T ) )  =  ( ( k  -  j )  x.  T ) )
438437oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  -  a )  +  ( ( k  x.  T
)  -  ( j  x.  T ) ) )  =  ( ( b  -  a )  +  ( ( k  -  j )  x.  T ) ) )
439432, 438eqtr2d 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  -  a )  +  ( ( k  -  j
)  x.  T ) )  =  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) ) )
440423, 439breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  <  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) ) )
441440adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
k  -  j )  x.  T )  < 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) ) )
442345, 350, 367, 416, 441lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  <  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) ) )
443345, 367ltnled 9743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( T  <  ( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  <->  -.  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) )  <_  T ) )
444442, 443mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  -.  (
( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T )
445444ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  <  k  ->  -.  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T
) )
446445adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  (
j  <  k  ->  -.  ( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  <_  T )
)
447340, 446mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  -.  ( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  <_  T )
4484473adantl3 1154 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )  /\  ( ( a  +  ( j  x.  T
) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  /\  -.  k  <_  j )  ->  -.  ( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  <_  T )
449331, 448condan 792 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  k  <_  j )
450220, 222sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  RR )
45139, 450syl5eqel 2559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  E  e.  RR )
452313, 451syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  E  e.  RR )
4534523ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  e.  RR )
454453ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  /\  k  <_  j )  /\  ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T ) ) )  ->  E  e.  RR )
4553443adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  T  e.  RR )
456455ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  /\  k  <_  j )  /\  ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T ) ) )  ->  T  e.  RR )
457334, 337resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  -  k
)  e.  RR )
458457adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  -  k
)  e.  RR )
459458, 344remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( j  -  k )  x.  T
)  e.  RR )
4604593adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  ( (
j  -  k )  x.  T )  e.  RR )
461460ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  /\  k  <_  j )  /\  ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T ) ) )  ->  ( ( j  -  k )  x.  T )  e.  RR )
462228, 172, 1753jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C ) )
463 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( d  =  C  ->  (
d  e.  A  <->  C  e.  A ) )
464463anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( d  =  C  ->  (
( B  e.  A  /\  d  e.  A
)  <->  ( B  e.  A  /\  C  e.  A ) ) )
465 breq2 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( d  =  C  ->  ( B  <  d  <->  B  <  C ) )
466464, 4653anbi23d 1302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( d  =  C  ->  (
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  <-> 
( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C ) ) )
467 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( d  =  C  ->  (
d  -  B )  =  ( C  -  B ) )
468467breq2d 4465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( d  =  C  ->  ( E  <_  ( d  -  B )  <->  E  <_  ( C  -  B ) ) )
469466, 468imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  (
( ( ph  /\  ( B  e.  A  /\  d  e.  A
)  /\  B  <  d )  ->  E  <_  ( d  -  B ) )  <->  ( ( ph  /\  ( B  e.  A  /\  C  e.  A
)  /\  B  <  C )  ->  E  <_  ( C  -  B ) ) ) )
4701703ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  B  e.  A )
471 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( c  =  B  ->  (
c  e.  A  <->  B  e.  A ) )
472471anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( c  =  B  ->  (
( c  e.  A  /\  d  e.  A
)  <->  ( B  e.  A  /\  d  e.  A ) ) )
473 breq1 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( c  =  B  ->  (
c  <  d  <->  B  <  d ) )
474472, 4733anbi23d 1302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( c  =  B  ->  (
( ph  /\  (
c  e.  A  /\  d  e.  A )  /\  c  <  d )  <-> 
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d ) ) )
475 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( c  =  B  ->  (
d  -  c )  =  ( d  -  B ) )
476475breq2d 4465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( c  =  B  ->  ( E  <_  ( d  -  c )  <->  E  <_  ( d  -  B ) ) )
477474, 476imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
( ( ph  /\  ( c  e.  A  /\  d  e.  A
)  /\  c  <  d )  ->  E  <_  ( d  -  c ) )  <->  ( ( ph  /\  ( B  e.  A  /\  d  e.  A
)  /\  B  <  d )  ->  E  <_  ( d  -  B ) ) ) )
47839a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E  =  sup ( R ,  RR ,  `'  <  ) )
479219a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  R  C_  RR )
480 0re 9608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  0  e.  RR
481480a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  0  e.  RR )
48240eleq2i 2545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( y  e.  R  <->  y  e.  ran  ( D  |`  I ) )
483482biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( y  e.  R  ->  y  e.  ran  ( D  |`  I ) )
484483adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  y  e.  R )  ->  y  e.  ran  ( D  |`  I ) )
48570adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  y  e.  R )  ->  ( D  |`  I )  Fn  I )
486 fvelrnb 5921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( D  |`  I )  Fn  I  ->  ( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )
487485, 486syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  y  e.  R )  ->  (
y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )
488484, 487mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  y  e.  R )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y )
489141rpge0d 11272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
ph  /\  x  e.  I )  ->  0  <_  ( ( D  |`  I ) `  x
) )
4904893adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  0  <_  (
( D  |`  I ) `
 x ) )
491 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  ( ( D  |`  I ) `  x
)  =  y )
492490, 491breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  0  <_  y
)
4934923exp 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ph  ->  ( x  e.  I  ->  ( ( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
) )
494493adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  y  e.  R )  ->  (
x  e.  I  -> 
( ( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
) )
495494rexlimdv 2957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  y  e.  R )  ->  ( E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
)
496488, 495mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  0  <_  y )
497496ralrimiva 2881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  A. y  e.  R 
0  <_  y )
498 breq1 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
499498ralbidv 2906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  =  0  ->  ( A. y  e.  R  x  <_  y  <->  A. y  e.  R  0  <_  y ) )
500499rspcev 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( 0  e.  RR  /\  A. y  e.  R  0  <_  y )  ->  E. x  e.  RR  A. y  e.  R  x  <_  y )
501481, 497, 500syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ph  ->  E. x  e.  RR  A. y  e.  R  x  <_  y )
5025013ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E. x  e.  RR  A. y  e.  R  x  <_  y
)
503 pm3.22 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( c  e.  A  /\  d  e.  A )  ->  ( d  e.  A  /\  c  e.  A
) )
504 opelxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( <.
d ,  c >.  e.  ( A  X.  A
)  <->  ( d  e.  A  /\  c  e.  A ) )
505503, 504sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( c  e.  A  /\  d  e.  A )  -> 
<. d ,  c >.  e.  ( A  X.  A
) )
5065053ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  ( A  X.  A ) )
50756, 59sstrd 3519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ph  ->  A  C_  RR )
508507sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( (
ph  /\  c  e.  A )  ->  c  e.  RR )
509508adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
c  e.  RR )
5105093adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  e.  RR )
511 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  <  d )
512510, 511ltned 9732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  =/=  d )
513512necomd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  d  =/=  c )
514513neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  -.  d  =  c )
515 df-br 4454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( d  _I  c  <->  <. d ,  c >.  e.  _I  )
516 vex 3121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  c  e. 
_V
517 ideqg 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( c  e.  _V  ->  (
d  _I  c  <->  d  =  c ) )
518516, 517ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( d  _I  c  <->  d  =  c )
519515, 518bitr3i 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( <.
d ,  c >.  e.  _I  <->  d  =  c )
520514, 519sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  -.  <.
d ,  c >.  e.  _I  )
521506, 520eldifd 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  ( ( A  X.  A
)  \  _I  )
)
522521, 55syl6eleqr 2566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  I
)
523 simp1 996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  ph )
524 simp2 997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
c  e.  A  /\  d  e.  A )
)
5251683ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ( D  |`  I )  =  ( ( abs  o.  -  )  |`  I ) )
526525fveq1d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
( ( abs  o.  -  )  |`  I ) `
 <. d ,  c
>. ) )
5275053ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  ( A  X.  A ) )
528 necom 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( c  =/=  d  <->  d  =/=  c )
529528biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( c  =/=  d  ->  d  =/=  c )
530529neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( c  =/=  d  ->  -.  d  =  c )
5315303ad2ant3 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  -.  d  =  c )
532531, 519sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  -.  <.
d ,  c >.  e.  _I  )
533527, 532eldifd 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  ( ( A  X.  A
)  \  _I  )
)
534533, 55syl6eleqr 2566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  I
)
535 fvres 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( <.
d ,  c >.  e.  I  ->  ( ( ( abs  o.  -  )  |`  I ) `  <. d ,  c >.
)  =  ( ( abs  o.  -  ) `  <. d ,  c
>. ) )
536534, 535syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( ( abs  o.  -  )  |`  I ) `
 <. d ,  c
>. )  =  (
( abs  o.  -  ) `  <. d ,  c
>. ) )
53777a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  Fun  -  )
538 simp1 996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ph )
539538, 534jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ( ph  /\  <. d ,  c
>.  e.  I ) )
540 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( x  =  <. d ,  c
>.  ->  ( x  e.  I  <->  <. d ,  c
>.  e.  I ) )
541540anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( x  =  <. d ,  c
>.  ->  ( ( ph  /\  x  e.  I )  <-> 
( ph  /\  <. d ,  c >.  e.  I
) ) )
542 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( x  =  <. d ,  c
>.  ->  ( x  e. 
dom  -  <->  <. d ,  c
>.  e.  dom  -  )
)
543541, 542imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  =  <. d ,  c
>.  ->  ( ( (
ph  /\  x  e.  I )  ->  x  e.  dom  -  )  <->  ( ( ph  /\  <. d ,  c
>.  e.  I )  ->  <. d ,  c >.  e.  dom  -  ) ) )
54484a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  e.  I  ->  (
( ph  /\  x  e.  I )  ->  x  e.  dom  -  ) )
545543, 544vtoclga 3182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( <.
d ,  c >.  e.  I  ->  ( (
ph  /\  <. d ,  c >.  e.  I
)  ->  <. d ,  c >.  e.  dom  -  ) )
546534, 539, 545sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  dom  -  )
547 fvco 5950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( Fun  -  /\  <. d ,  c >.  e.  dom  -  )  ->  ( ( abs  o.  -  ) `  <. d ,  c >.
)  =  ( abs `  (  -  `  <. d ,  c >. )
) )
548537, 546, 547syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( abs  o.  -  ) `  <. d ,  c
>. )  =  ( abs `  (  -  `  <. d ,  c >.
) ) )
549 df-ov 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( d  -  c )  =  (  -  `  <. d ,  c >. )
550549eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  (  -  ` 
<. d ,  c >.
)  =  ( d  -  c )
551550fveq2i 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( abs `  (  -  `  <. d ,  c >. )
)  =  ( abs `  ( d  -  c
) )
552551a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.