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

Theorem fourierdlem42 31820
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 21307 . . . . 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 3570 . . . . . . 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 3533 . . . . 5  |-  ( ph  ->  H  C_  ( X [,] Y ) )
12 retop 21245 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  e.  Top
133, 12eqeltri 2527 . . . . . . 7  |-  J  e. 
Top
141, 2iccssred 31475 . . . . . . 7  |-  ( ph  ->  ( X [,] Y
)  C_  RR )
15 uniretop 21246 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
163unieqi 4243 . . . . . . . . 9  |-  U. J  =  U. ( topGen `  ran  (,) )
1715, 16eqtr4i 2475 . . . . . . . 8  |-  RR  =  U. J
1817restuni 19640 . . . . . . 7  |-  ( ( J  e.  Top  /\  ( X [,] Y ) 
C_  RR )  -> 
( X [,] Y
)  =  U. ( Jt  ( X [,] Y ) ) )
1913, 14, 18sylancr 663 . . . . . 6  |-  ( ph  ->  ( X [,] Y
)  =  U. ( Jt  ( X [,] Y ) ) )
204unieqi 4243 . . . . . . 7  |-  U. K  =  U. ( Jt  ( X [,] Y ) )
2120eqcomi 2456 . . . . . 6  |-  U. ( Jt  ( X [,] Y ) )  =  U. K
2219, 21syl6eq 2500 . . . . 5  |-  ( ph  ->  ( X [,] Y
)  =  U. K
)
2311, 22sseqtrd 3525 . . . 4  |-  ( ph  ->  H  C_  U. K )
2423adantr 465 . . 3  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  H  C_ 
U. K )
25 simpr 461 . . 3  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  -.  H  e.  Fin )
26 eqid 2443 . . . 4  |-  U. K  =  U. K
2726bwth 19887 . . 3  |-  ( ( K  e.  Comp  /\  H  C_ 
U. K  /\  -.  H  e.  Fin )  ->  E. x  e.  U. K x  e.  (
( limPt `  K ) `  H ) )
287, 24, 25, 27syl3anc 1229 . 2  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  E. x  e.  U. K x  e.  ( ( limPt `  K
) `  H )
)
2911, 14sstrd 3499 . . . . . . . . . 10  |-  ( ph  ->  H  C_  RR )
3029ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  H  C_  RR )
31 ne0i 3776 . . . . . . . . . 10  |-  ( x  e.  ( ( limPt `  J ) `  H
)  ->  ( ( limPt `  J ) `  H )  =/=  (/) )
3231adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  -> 
( ( limPt `  J
) `  H )  =/=  (/) )
33 fourierdlem42.e . . . . . . . . . . 11  |-  E  =  sup ( R ,  RR ,  `'  <  )
34 fourierdlem42.r . . . . . . . . . . . . 13  |-  R  =  ran  ( D  |`  I )
35 absf 13151 . . . . . . . . . . . . . . . . . 18  |-  abs : CC
--> RR
36 ffn 5721 . . . . . . . . . . . . . . . . . 18  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
3735, 36ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  abs  Fn  CC
38 subf 9827 . . . . . . . . . . . . . . . . . 18  |-  -  :
( CC  X.  CC )
--> CC
39 ffn 5721 . . . . . . . . . . . . . . . . . 18  |-  (  -  : ( CC  X.  CC ) --> CC  ->  -  Fn  ( CC  X.  CC ) )
4038, 39ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  -  Fn  ( CC  X.  CC )
41 frn 5727 . . . . . . . . . . . . . . . . . 18  |-  (  -  : ( CC  X.  CC ) --> CC  ->  ran  - 
C_  CC )
4238, 41ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ran  -  C_  CC
43 fnco 5679 . . . . . . . . . . . . . . . . 17  |-  ( ( abs  Fn  CC  /\  -  Fn  ( CC  X.  CC )  /\  ran  -  C_  CC )  ->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) )
4437, 40, 42, 43mp3an 1325 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  Fn  ( CC  X.  CC )
45 fourierdlem42.d . . . . . . . . . . . . . . . . 17  |-  D  =  ( abs  o.  -  )
4645fneq1i 5665 . . . . . . . . . . . . . . . 16  |-  ( D  Fn  ( CC  X.  CC )  <->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) )
4744, 46mpbir 209 . . . . . . . . . . . . . . 15  |-  D  Fn  ( CC  X.  CC )
48 fourierdlem42.i . . . . . . . . . . . . . . . 16  |-  I  =  ( ( A  X.  A )  \  _I  )
49 fourierdlem42.a . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  C_  ( B [,] C ) )
50 fourierdlem42.b . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  RR )
51 fourierdlem42.c . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  RR )
5250, 51iccssred 31475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( B [,] C
)  C_  RR )
53 ax-resscn 9552 . . . . . . . . . . . . . . . . . . . 20  |-  RR  C_  CC
5452, 53syl6ss 3501 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( B [,] C
)  C_  CC )
5549, 54sstrd 3499 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  C_  CC )
56 xpss12 5098 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  C_  CC  /\  A  C_  CC )  ->  ( A  X.  A )  C_  ( CC  X.  CC ) )
5755, 55, 56syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  X.  A
)  C_  ( CC  X.  CC ) )
5857ssdifssd 3627 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  X.  A )  \  _I  )  C_  ( CC  X.  CC ) )
5948, 58syl5eqss 3533 . . . . . . . . . . . . . . 15  |-  ( ph  ->  I  C_  ( CC  X.  CC ) )
60 fnssres 5684 . . . . . . . . . . . . . . 15  |-  ( ( D  Fn  ( CC 
X.  CC )  /\  I  C_  ( CC  X.  CC ) )  ->  ( D  |`  I )  Fn  I )
6147, 59, 60sylancr 663 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  |`  I )  Fn  I )
62 fvres 5870 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  I  ->  (
( D  |`  I ) `
 x )  =  ( D `  x
) )
6362adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  =  ( D `  x
) )
6445fveq1i 5857 . . . . . . . . . . . . . . . . . . 19  |-  ( D `
 x )  =  ( ( abs  o.  -  ) `  x
)
6564a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  ( D `  x )  =  ( ( abs 
o.  -  ) `  x ) )
66 ffun 5723 . . . . . . . . . . . . . . . . . . . 20  |-  (  -  : ( CC  X.  CC ) --> CC  ->  Fun  -  )
6738, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  Fun  -
6859sselda 3489 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  ( CC  X.  CC ) )
6938fdmi 5726 . . . . . . . . . . . . . . . . . . . 20  |-  dom  -  =  ( CC  X.  CC )
7068, 69syl6eleqr 2542 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  dom  -  )
71 fvco 5934 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  -  /\  x  e.  dom  -  )  -> 
( ( abs  o.  -  ) `  x
)  =  ( abs `  (  -  `  x
) ) )
7267, 70, 71sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (
( abs  o.  -  ) `  x )  =  ( abs `  (  -  `  x ) ) )
7363, 65, 723eqtrd 2488 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  =  ( abs `  (  -  `  x ) ) )
7438a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  -  :
( CC  X.  CC )
--> CC )
7574, 68ffvelrnd 6017 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (  -  `  x )  e.  CC )
7675abscld 13248 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  ( abs `  (  -  `  x ) )  e.  RR )
7773, 76eqeltrd 2531 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  e.  RR )
78 elxp2 5007 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( CC  X.  CC )  <->  E. y  e.  CC  E. z  e.  CC  x  =  <. y ,  z
>. )
7968, 78sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  E. y  e.  CC  E. z  e.  CC  x  =  <. y ,  z >. )
80 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  <. y ,  z
>.  ->  (  -  `  x )  =  (  -  `  <. y ,  z >. )
)
81803ad2ant3 1020 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  x
)  =  (  -  ` 
<. y ,  z >.
) )
82 df-ov 6284 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  -  z )  =  (  -  `  <. y ,  z >. )
83 simp1l 1021 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  ph )
84 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  x  =  <. y ,  z
>. )
85 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  x  e.  I )
8684, 85eqeltrrd 2532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  <. y ,  z >.  e.  I
)
8786adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  I )  /\  x  =  <. y ,  z
>. )  ->  <. y ,  z >.  e.  I
)
88873adant2 1016 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  -> 
<. y ,  z >.  e.  I )
8955adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  A  C_  CC )
9048eleq2i 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
y ,  z >.  e.  I  <->  <. y ,  z
>.  e.  ( ( A  X.  A )  \  _I  ) )
91 eldif 3471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
y ,  z >.  e.  ( ( A  X.  A )  \  _I  ) 
<->  ( <. y ,  z
>.  e.  ( A  X.  A )  /\  -.  <.
y ,  z >.  e.  _I  ) )
9290, 91sylbb 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
y ,  z >.  e.  I  ->  ( <.
y ,  z >.  e.  ( A  X.  A
)  /\  -.  <. y ,  z >.  e.  _I  ) )
9392simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
y ,  z >.  e.  I  ->  <. y ,  z >.  e.  ( A  X.  A ) )
94 opelxp 5019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
y ,  z >.  e.  ( A  X.  A
)  <->  ( y  e.  A  /\  z  e.  A ) )
9593, 94sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
y ,  z >.  e.  I  ->  ( y  e.  A  /\  z  e.  A ) )
9695adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  ( y  e.  A  /\  z  e.  A ) )
9796simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  e.  A )
9889, 97sseldd 3490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  e.  CC )
9996simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  z  e.  A )
10089, 99sseldd 3490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  z  e.  CC )
10192simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
y ,  z >.  e.  I  ->  -.  <. y ,  z >.  e.  _I  )
102 df-br 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  _I  z  <->  <. y ,  z >.  e.  _I  )
103101, 102sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
y ,  z >.  e.  I  ->  -.  y  _I  z )
104 vex 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  z  e. 
_V
105104ideq 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  _I  z  <->  y  =  z )
106103, 105sylnib 304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
y ,  z >.  e.  I  ->  -.  y  =  z )
107106neqned 2646 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
y ,  z >.  e.  I  ->  y  =/=  z )
108107adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  =/=  z )
10998, 100, 108subne0d 9945 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  ( y  -  z )  =/=  0 )
11083, 88, 109syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  ( y  -  z
)  =/=  0 )
11182, 110syl5eqner 2744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  <. y ,  z >. )  =/=  0 )
11281, 111eqnetrd 2736 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  x
)  =/=  0 )
1131123exp 1196 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  (
( y  e.  CC  /\  z  e.  CC )  ->  ( x  = 
<. y ,  z >.  ->  (  -  `  x
)  =/=  0 ) ) )
114113rexlimdvv 2941 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  ( E. y  e.  CC  E. z  e.  CC  x  =  <. y ,  z
>.  ->  (  -  `  x )  =/=  0
) )
11579, 114mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (  -  `  x )  =/=  0 )
116 absgt0 13138 . . . . . . . . . . . . . . . . . . 19  |-  ( (  -  `  x )  e.  CC  ->  (
(  -  `  x
)  =/=  0  <->  0  <  ( abs `  (  -  `  x ) ) ) )
11775, 116syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (
(  -  `  x
)  =/=  0  <->  0  <  ( abs `  (  -  `  x ) ) ) )
118115, 117mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  0  <  ( abs `  (  -  `  x ) ) )
11973eqcomd 2451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  ( abs `  (  -  `  x ) )  =  ( ( D  |`  I ) `  x
) )
120118, 119breqtrd 4461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  0  <  ( ( D  |`  I ) `  x
) )
12177, 120elrpd 11264 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  e.  RR+ )
122121ralrimiva 2857 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  I 
( ( D  |`  I ) `  x
)  e.  RR+ )
123 fnfvrnss 6044 . . . . . . . . . . . . . 14  |-  ( ( ( D  |`  I )  Fn  I  /\  A. x  e.  I  (
( D  |`  I ) `
 x )  e.  RR+ )  ->  ran  ( D  |`  I )  C_  RR+ )
12461, 122, 123syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  ( D  |`  I )  C_  RR+ )
12534, 124syl5eqss 3533 . . . . . . . . . . . 12  |-  ( ph  ->  R  C_  RR+ )
126 ltso 9668 . . . . . . . . . . . . . . 15  |-  <  Or  RR
127126a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  <  Or  RR )
128 cnvso 5536 . . . . . . . . . . . . . 14  |-  (  < 
Or  RR  <->  `'  <  Or  RR )
129127, 128sylib 196 . . . . . . . . . . . . 13  |-  ( ph  ->  `'  <  Or  RR )
130 fourierdlem42.af . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  Fin )
131 xpfi 7793 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  Fin  /\  A  e.  Fin )  ->  ( A  X.  A
)  e.  Fin )
132130, 130, 131syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A  X.  A
)  e.  Fin )
133 diffi 7753 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  X.  A )  e.  Fin  ->  (
( A  X.  A
)  \  _I  )  e.  Fin )
134132, 133syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( A  X.  A )  \  _I  )  e.  Fin )
13548, 134syl5eqel 2535 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  I  e.  Fin )
136 fnfi 7800 . . . . . . . . . . . . . . . 16  |-  ( ( ( D  |`  I )  Fn  I  /\  I  e.  Fin )  ->  ( D  |`  I )  e. 
Fin )
13761, 135, 136syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  |`  I )  e.  Fin )
138 rnfi 7807 . . . . . . . . . . . . . . 15  |-  ( ( D  |`  I )  e.  Fin  ->  ran  ( D  |`  I )  e.  Fin )
139137, 138syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  ( D  |`  I )  e.  Fin )
14034, 139syl5eqel 2535 . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  Fin )
14134a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  =  ran  ( D  |`  I ) )
14245a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  D  =  ( abs 
o.  -  ) )
143142reseq1d 5262 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  |`  I )  =  ( ( abs 
o.  -  )  |`  I ) )
144143fveq1d 5858 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  |`  I ) `  <. B ,  C >. )  =  ( ( ( abs  o.  -  )  |`  I ) `  <. B ,  C >. )
)
145 fourierdlem42.ba . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  A )
146 fourierdlem42.ca . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  A )
147 opelxp 5019 . . . . . . . . . . . . . . . . . . . . 21  |-  ( <. B ,  C >.  e.  ( A  X.  A
)  <->  ( B  e.  A  /\  C  e.  A ) )
148145, 146, 147sylanbrc 664 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
<. B ,  C >.  e.  ( A  X.  A
) )
149 fourierdlem42.bc . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  <  C )
15050, 149ltned 9724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  =/=  C )
151150neneqd 2645 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  B  =  C )
152 ideqg 5144 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( C  e.  A  ->  ( B  _I  C  <->  B  =  C ) )
153146, 152syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( B  _I  C  <->  B  =  C ) )
154151, 153mtbird 301 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  B  _I  C
)
155 df-br 4438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( B  _I  C  <->  <. B ,  C >.  e.  _I  )
156154, 155sylnib 304 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  <. B ,  C >.  e.  _I  )
157148, 156eldifd 3472 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
<. B ,  C >.  e.  ( ( A  X.  A )  \  _I  ) )
158157, 48syl6eleqr 2542 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
<. B ,  C >.  e.  I )
159 fvres 5870 . . . . . . . . . . . . . . . . . 18  |-  ( <. B ,  C >.  e.  I  ->  ( (
( abs  o.  -  )  |`  I ) `  <. B ,  C >. )  =  ( ( abs 
o.  -  ) `  <. B ,  C >. ) )
160158, 159syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( abs 
o.  -  )  |`  I ) `
 <. B ,  C >. )  =  ( ( abs  o.  -  ) `  <. B ,  C >. ) )
16150recnd 9625 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  CC )
16251recnd 9625 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  CC )
163 opelxp 5019 . . . . . . . . . . . . . . . . . . . . 21  |-  ( <. B ,  C >.  e.  ( CC  X.  CC ) 
<->  ( B  e.  CC  /\  C  e.  CC ) )
164161, 162, 163sylanbrc 664 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
<. B ,  C >.  e.  ( CC  X.  CC ) )
165164, 69syl6eleqr 2542 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
<. B ,  C >.  e. 
dom  -  )
166 fvco 5934 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  -  /\  <. B ,  C >.  e.  dom  -  )  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  (  -  `  <. B ,  C >. ) ) )
16767, 165, 166sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  (  -  `  <. B ,  C >. ) ) )
168 df-ov 6284 . . . . . . . . . . . . . . . . . . . . 21  |-  ( B  -  C )  =  (  -  `  <. B ,  C >. )
169168eqcomi 2456 . . . . . . . . . . . . . . . . . . . 20  |-  (  -  ` 
<. B ,  C >. )  =  ( B  -  C )
170169a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  (  -  `  <. B ,  C >. )  =  ( B  -  C ) )
171170fveq2d 5860 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  (  -  `  <. B ,  C >. ) )  =  ( abs `  ( B  -  C ) ) )
172167, 171eqtrd 2484 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  ( B  -  C )
) )
173144, 160, 1723eqtrrd 2489 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( abs `  ( B  -  C )
)  =  ( ( D  |`  I ) `  <. B ,  C >. ) )
174 fnfvelrn 6013 . . . . . . . . . . . . . . . . 17  |-  ( ( ( D  |`  I )  Fn  I  /\  <. B ,  C >.  e.  I
)  ->  ( ( D  |`  I ) `  <. B ,  C >. )  e.  ran  ( D  |`  I ) )
17561, 158, 174syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  |`  I ) `  <. B ,  C >. )  e.  ran  ( D  |`  I ) )
176173, 175eqeltrd 2531 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( abs `  ( B  -  C )
)  e.  ran  ( D  |`  I ) )
177 ne0i 3776 . . . . . . . . . . . . . . 15  |-  ( ( abs `  ( B  -  C ) )  e.  ran  ( D  |`  I )  ->  ran  ( D  |`  I )  =/=  (/) )
178176, 177syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  ( D  |`  I )  =/=  (/) )
179141, 178eqnetrd 2736 . . . . . . . . . . . . 13  |-  ( ph  ->  R  =/=  (/) )
180 resss 5287 . . . . . . . . . . . . . . . . 17  |-  ( D  |`  I )  C_  D
181 rnss 5221 . . . . . . . . . . . . . . . . 17  |-  ( ( D  |`  I )  C_  D  ->  ran  ( D  |`  I )  C_  ran  D )
182180, 181ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ran  ( D  |`  I )  C_  ran  D
18345rneqi 5219 . . . . . . . . . . . . . . . . 17  |-  ran  D  =  ran  ( abs  o.  -  )
184 rncoss 5253 . . . . . . . . . . . . . . . . . 18  |-  ran  ( abs  o.  -  )  C_  ran  abs
185 frn 5727 . . . . . . . . . . . . . . . . . . 19  |-  ( abs
: CC --> RR  ->  ran 
abs  C_  RR )
18635, 185ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ran  abs  C_  RR
187184, 186sstri 3498 . . . . . . . . . . . . . . . . 17  |-  ran  ( abs  o.  -  )  C_  RR
188183, 187eqsstri 3519 . . . . . . . . . . . . . . . 16  |-  ran  D  C_  RR
189182, 188sstri 3498 . . . . . . . . . . . . . . 15  |-  ran  ( D  |`  I )  C_  RR
19034, 189eqsstri 3519 . . . . . . . . . . . . . 14  |-  R  C_  RR
191190a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  R  C_  RR )
192 fisupcl 7930 . . . . . . . . . . . . 13  |-  ( ( `'  <  Or  RR  /\  ( R  e.  Fin  /\  R  =/=  (/)  /\  R  C_  RR ) )  ->  sup ( R ,  RR ,  `'  <  )  e.  R )
193129, 140, 179, 191, 192syl13anc 1231 . . . . . . . . . . . 12  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  R )
194125, 193sseldd 3490 . . . . . . . . . . 11  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  RR+ )
19533, 194syl5eqel 2535 . . . . . . . . . 10  |-  ( ph  ->  E  e.  RR+ )
196195ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  E  e.  RR+ )
1973, 30, 32, 196lptre2pt 31554 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  E. y  e.  H  E. z  e.  H  ( y  =/=  z  /\  ( abs `  (
y  -  z ) )  <  E ) )
198 simpll 753 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  ph )
19929sselda 3489 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  H )  ->  y  e.  RR )
200199adantrr 716 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  H  /\  z  e.  H ) )  -> 
y  e.  RR )
201200adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  y  e.  RR )
20229sselda 3489 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  H )  ->  z  e.  RR )
203202adantrl 715 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  H  /\  z  e.  H ) )  -> 
z  e.  RR )
204203adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  z  e.  RR )
205 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  y  =/=  z )
206201, 204, 2053jca 1177 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  (
y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )
2078eleq2i 2521 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  H  <->  y  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A }
)
208 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x  +  ( k  x.  T ) )  =  ( y  +  ( k  x.  T
) ) )
209208eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( x  +  ( k  x.  T ) )  e.  A  <->  ( y  +  ( k  x.  T ) )  e.  A ) )
210209rexbidv 2954 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  A
) )
211 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
212211oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  j  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
213212eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
( y  +  ( k  x.  T ) )  e.  A  <->  ( y  +  ( j  x.  T ) )  e.  A ) )
214213cbvrexv 3071 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  A  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
)
215210, 214syl6bb 261 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
) )
216215elrab 3243 . . . . . . . . . . . . . . . . . . 19  |-  ( 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
) )
217207, 216sylbb 197 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  H  ->  (
y  e.  ( X [,] Y )  /\  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  A ) )
218217simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  H  ->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
)
219218adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. j  e.  ZZ  ( y  +  ( j  x.  T ) )  e.  A )
2208eleq2i 2521 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  H  <->  z  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A }
)
221 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
x  +  ( k  x.  T ) )  =  ( z  +  ( k  x.  T
) ) )
222221eleq1d 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( x  +  ( k  x.  T ) )  e.  A  <->  ( z  +  ( k  x.  T ) )  e.  A ) )
223222rexbidv 2954 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
) )
224223elrab 3243 . . . . . . . . . . . . . . . . . . 19  |-  ( 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
) )
225220, 224sylbb 197 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  H  ->  (
z  e.  ( X [,] Y )  /\  E. k  e.  ZZ  (
z  +  ( k  x.  T ) )  e.  A ) )
226225simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  H  ->  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
)
227226adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. k  e.  ZZ  ( z  +  ( k  x.  T ) )  e.  A )
228 reeanv 3011 . . . . . . . . . . . . . . . 16  |-  ( 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 ) )
229219, 227, 228sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) )
230229ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
231 simplll 759 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
232 simpl1 1000 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
y  e.  RR )
233 simpl2 1001 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
z  e.  RR )
234 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
y  <  z )
235232, 233, 2343jca 1177 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
236235adantll 713 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
237236adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
238 simplr 755 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
239 eleq1 2515 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
b  e.  RR  <->  z  e.  RR ) )
240 breq2 4441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
y  <  b  <->  y  <  z ) )
241239, 2403anbi23d 1303 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  (
( y  e.  RR  /\  b  e.  RR  /\  y  <  b )  <->  ( y  e.  RR  /\  z  e.  RR  /\  y  < 
z ) ) )
242241anbi2d 703 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  z  ->  (
( ph  /\  (
y  e.  RR  /\  b  e.  RR  /\  y  <  b ) )  <->  ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) ) ) )
243 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  z  ->  (
b  +  ( k  x.  T ) )  =  ( z  +  ( k  x.  T
) ) )
244243eleq1d 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
( b  +  ( k  x.  T ) )  e.  A  <->  ( z  +  ( k  x.  T ) )  e.  A ) )
245244anbi2d 703 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) )
2462452rexbidv 2961 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) )
247242, 246anbi12d 710 . . . . . . . . . . . . . . . . . 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 ) )  <->  ( ( 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 ) ) ) )
248 oveq2 6289 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  (
y  -  b )  =  ( y  -  z ) )
249248fveq2d 5860 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  z  ->  ( abs `  ( y  -  b ) )  =  ( abs `  (
y  -  z ) ) )
250249breq2d 4449 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  z  ->  ( E  <_  ( abs `  (
y  -  b ) )  <->  E  <_  ( abs `  ( y  -  z
) ) ) )
251247, 250imbi12d 320 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) ) )
252 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
a  e.  RR  <->  y  e.  RR ) )
253 breq1 4440 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
a  <  b  <->  y  <  b ) )
254252, 2533anbi13d 1302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  (
( a  e.  RR  /\  b  e.  RR  /\  a  <  b )  <->  ( y  e.  RR  /\  b  e.  RR  /\  y  < 
b ) ) )
255254anbi2d 703 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  y  ->  (
( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  <->  ( ph  /\  ( y  e.  RR  /\  b  e.  RR  /\  y  <  b ) ) ) )
256 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  y  ->  (
a  +  ( j  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
257256eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
( a  +  ( j  x.  T ) )  e.  A  <->  ( y  +  ( j  x.  T ) )  e.  A ) )
258257anbi1d 704 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) )
2592582rexbidv 2961 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) )
260255, 259anbi12d 710 . . . . . . . . . . . . . . . . . . 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 ) )  <->  ( ( 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 ) ) ) )
261 oveq1 6288 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  (
a  -  b )  =  ( y  -  b ) )
262261fveq2d 5860 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  y  ->  ( abs `  ( a  -  b ) )  =  ( abs `  (
y  -  b ) ) )
263262breq2d 4449 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  y  ->  ( E  <_  ( abs `  (
a  -  b ) )  <->  E  <_  ( abs `  ( y  -  b
) ) ) )
264260, 263imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) )
265 fourierdlem42.15 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) )
266265simprbi 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ps 
->  E. j  e.  ZZ  E. k  e.  ZZ  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )
267265biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 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 ) ) )
268267simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  ( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) ) )
269268simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  ph )
270269, 50syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  B  e.  RR )
271270adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  B  e.  RR )
272269, 51syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  C  e.  RR )
273272adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  C  e.  RR )
274269, 49syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  A  C_  ( B [,] C ) )
275274sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( b  +  ( k  x.  T ) )  e.  A )  ->  (
b  +  ( k  x.  T ) )  e.  ( B [,] C ) )
276275adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( b  +  ( k  x.  T
) )  e.  ( B [,] C ) )
277274sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( a  +  ( j  x.  T ) )  e.  A )  ->  (
a  +  ( j  x.  T ) )  e.  ( B [,] C ) )
278277adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( a  +  ( j  x.  T
) )  e.  ( B [,] C ) )
279271, 273, 276, 278iccsuble 31495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  ( C  -  B )
)
280 fourierdlem42.t . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  T  =  ( C  -  B
)
281279, 280syl6breqr 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T
)
2822813adant2 1016 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 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 )
283282adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 )
284 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  -.  k  <_  j )
285 zre 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ZZ  ->  j  e.  RR )
286285adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  j  e.  RR )
287286ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  j  e.  RR )
288 zre 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ZZ  ->  k  e.  RR )
289288adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  k  e.  RR )
290289ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  k  e.  RR )
291287, 290ltnled 9735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  (
j  <  k  <->  -.  k  <_  j ) )
292284, 291mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  j  <  k )
29351, 50resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( C  -  B
)  e.  RR )
294280, 293syl5eqel 2535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  T  e.  RR )
295269, 294syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  T  e.  RR )
296295ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  e.  RR )
297289adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  e.  RR )
298286adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
j  e.  RR )
299297, 298resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  -  j
)  e.  RR )
300295adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  ->  T  e.  RR )
301299, 300remulcld 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  e.  RR )
302301adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
k  -  j )  x.  T )  e.  RR )
303268simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )
304303simp2d 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  b  e.  RR )
305304adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
b  e.  RR )
306288adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  e.  RR )
307295adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  e.  RR )
308306, 307remulcld 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  RR )
309308adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  x.  T
)  e.  RR )
310305, 309readdcld 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( b  +  ( k  x.  T ) )  e.  RR )
311303simp1d 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  a  e.  RR )
312311adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
a  e.  RR )
313285adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  j  e.  RR )
314295adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  T  e.  RR )
315313, 314remulcld 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  j  e.  ZZ )  ->  (
j  x.  T )  e.  RR )
316315adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  x.  T
)  e.  RR )
317312, 316readdcld 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( a  +  ( j  x.  T ) )  e.  RR )
318310, 317resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  e.  RR )
319318adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) )  e.  RR )
320295recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  T  e.  CC )
321320mulid2d 9617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  ( 1  x.  T
)  =  T )
322321eqcomd 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  T  =  (
1  x.  T ) )
323322ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  =  ( 1  x.  T
) )
324 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  <  k )
325 zltlem1 10923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  <  k  <->  j  <_  ( k  - 
1 ) ) )
326325ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( j  <  k  <->  j  <_  (
k  -  1 ) ) )
327324, 326mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  <_  ( k  -  1 ) )
328286ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  j  e.  RR )
329 peano2rem 9891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  RR  ->  (
k  -  1 )  e.  RR )
330297, 329syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  -  1 )  e.  RR )
331330adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( k  -  1 )  e.  RR )
332 1re 9598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  1  e.  RR
333 resubcl 9888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 1  e.  RR  /\  j  e.  RR )  ->  ( 1  -  j
)  e.  RR )
334332, 328, 333sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( 1  -  j )  e.  RR )
335 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  j  <_  ( k  -  1 ) )
336328, 331, 334, 335leadd1dd 10173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  +  ( 1  -  j ) )  <_ 
( ( k  - 
1 )  +  ( 1  -  j ) ) )
337 zcn 10876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  ZZ  ->  j  e.  CC )
338337adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  j  e.  CC )
339 1cnd 9615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  1  e.  CC )
340338, 339pncan3d 9939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  +  ( 1  -  j ) )  =  1 )
341340ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  +  ( 1  -  j ) )  =  1 )
342 zcn 10876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  ZZ  ->  k  e.  CC )
343342adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  k  e.  CC )
344343, 339, 338npncand 9960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( ( k  - 
1 )  +  ( 1  -  j ) )  =  ( k  -  j ) )
345344ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( (
k  -  1 )  +  ( 1  -  j ) )  =  ( k  -  j
) )
346336, 341, 3453brtr3d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  1  <_  ( k  -  j ) )
347327, 346syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  1  <_  ( k  -  j ) )
348332a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  1  e.  RR )
349299adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( k  -  j )  e.  RR )
35050, 51posdifd 10146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( B  <  C  <->  0  <  ( C  -  B ) ) )
351149, 350mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  0  <  ( C  -  B ) )
352351, 280syl6breqr 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  0  <  T )
353294, 352elrpd 11264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  T  e.  RR+ )
354269, 353syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  T  e.  RR+ )
355354ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  e.  RR+ )
356348, 349, 355lemul1d 11305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( 1  <_  ( k  -  j )  <->  ( 1  x.  T )  <_ 
( ( k  -  j )  x.  T
) ) )
357347, 356mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( 1  x.  T )  <_ 
( ( k  -  j )  x.  T
) )
358323, 357eqbrtrd 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  <_  ( ( k  -  j
)  x.  T ) )
359304, 311resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  ( b  -  a
)  e.  RR )
360303simp3d 1011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ps 
->  a  <  b )
361311, 304posdifd 10146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ps 
->  ( a  <  b  <->  0  <  ( b  -  a ) ) )
362360, 361mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  0  <  ( b  -  a ) )
363359, 362elrpd 11264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  ( b  -  a
)  e.  RR+ )
364363adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( b  -  a
)  e.  RR+ )
365301, 364ltaddrp2d 11296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  <  ( (
b  -  a )  +  ( ( k  -  j )  x.  T ) ) )
366304recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  b  e.  CC )
367366adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
b  e.  CC )
368308recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  CC )
369368adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  x.  T
)  e.  CC )
370311recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  a  e.  CC )
371370adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
a  e.  CC )
372315recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  (
j  x.  T )  e.  CC )
373372adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  x.  T
)  e.  CC )
374367, 369, 371, 373addsub4d 9983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  =  ( ( b  -  a )  +  ( ( k  x.  T )  -  ( j  x.  T
) ) ) )
375342ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  e.  CC )
376337ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
j  e.  CC )
377320adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  ->  T  e.  CC )
378375, 376, 377subdird 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  =  ( ( k  x.  T )  -  ( j  x.  T ) ) )
379378eqcomd 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  x.  T )  -  (
j  x.  T ) )  =  ( ( k  -  j )  x.  T ) )
380379oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  -  a )  +  ( ( k  x.  T
)  -  ( j  x.  T ) ) )  =  ( ( b  -  a )  +  ( ( k  -  j )  x.  T ) ) )
381374, 380eqtr2d 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  -  a )  +  ( ( k  -  j
)  x.  T ) )  =  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) ) )
382365, 381breqtrd 4461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  <  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) ) )
383382adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
k  -  j )  x.  T )  < 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) ) )
384296, 302, 319, 358, 383lelttrd 9743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  <  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) ) )
385296, 319ltnled 9735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 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 ) )
386384, 385mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  -.  (
( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T )
387292, 386syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  -.  ( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  <_  T )
3883873adantl3 1155 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 )
389283, 388condan 794 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  k  <_  j )
390190, 193sseldi 3487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  RR )
39133, 390syl5eqel 2535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  E  e.  RR )
392269, 391syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  E  e.  RR )
3933923ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  e.  RR )
394393ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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 )
3952953ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  T  e.  RR )
396395ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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 )
397286, 289resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  -  k
)  e.  RR )
398397adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  -  k
)  e.  RR )
399398, 300remulcld 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( j  -  k )  x.  T
)  e.  RR )
4003993adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 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 )
401400ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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 )
402 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ph )
403145, 146jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( B  e.  A  /\  C  e.  A
) )
404402, 403, 1493jca 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C ) )
405 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( d  =  C  ->  (
d  e.  A  <->  C  e.  A ) )
406405anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  (
( B  e.  A  /\  d  e.  A
)  <->  ( B  e.  A  /\  C  e.  A ) ) )
407 breq2 4441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  ( B  <  d  <->  B  <  C ) )
408406, 4073anbi23d 1303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( d  =  C  ->  (
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  <-> 
( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C ) ) )
409 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  (
d  -  B )  =  ( C  -  B ) )
410409breq2d 4449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( d  =  C  ->  ( E  <_  ( d  -  B )  <->  E  <_  ( C  -  B ) ) )
411408, 410imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 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 ) ) ) )
412 simp2l 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  B  e.  A )
413 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( c  =  B  ->  (
c  e.  A  <->  B  e.  A ) )
414413anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
( c  e.  A  /\  d  e.  A
)  <->  ( B  e.  A  /\  d  e.  A ) ) )
415 breq1 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
c  <  d  <->  B  <  d ) )
416414, 4153anbi23d 1303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  =  B  ->  (
( ph  /\  (
c  e.  A  /\  d  e.  A )  /\  c  <  d )  <-> 
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d ) ) )
417 oveq2 6289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
d  -  c )  =  ( d  -  B ) )
418417breq2d 4449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  =  B  ->  ( E  <_  ( d  -  c )  <->  E  <_  ( d  -  B ) ) )
419416, 418imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 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 ) ) ) )
420190a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  R  C_  RR )
421 0re 9599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  0  e.  RR
42234eleq2i 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( y  e.  R  <->  y  e.  ran  ( D  |`  I ) )
423422biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  e.  R  ->  y  e.  ran  ( D  |`  I ) )
424423adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  y  e.  ran  ( D  |`  I ) )
42561adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  y  e.  R )  ->  ( D  |`  I )  Fn  I )
426 fvelrnb 5905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( D  |`  I )  Fn  I  ->  ( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )
427425, 426syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  (
y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )
428424, 427mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  y  e.  R )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y )
429121rpge0d 11270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  x  e.  I )  ->  0  <_  ( ( D  |`  I ) `  x
) )
4304293adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  0  <_  (
( D  |`  I ) `
 x ) )
431 simp3 999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  ( ( D  |`  I ) `  x
)  =  y )
432430, 431breqtrd 4461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  0  <_  y
)
4334323exp 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ph  ->  ( x  e.  I  ->  ( ( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
) )
434433adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  (
x  e.  I  -> 
( ( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
) )
435434rexlimdv 2933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  y  e.  R )  ->  ( E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
)
436428, 435mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  y  e.  R )  ->  0  <_  y )
437436ralrimiva 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  A. y  e.  R 
0  <_  y )
438 breq1 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
439438ralbidv 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  =  0  ->  ( A. y  e.  R  x  <_  y  <->  A. y  e.  R  0  <_  y ) )
440439rspcev 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( 0  e.  RR  /\  A. y  e.  R  0  <_  y )  ->  E. x  e.  RR  A. y  e.  R  x  <_  y )
441421, 437, 440sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  E. x  e.  RR  A. y  e.  R  x  <_  y )
4424413ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E. x  e.  RR  A. y  e.  R  x  <_  y
)
443 pm3.22 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( c  e.  A  /\  d  e.  A )  ->  ( d  e.  A  /\  c  e.  A
) )
444 opelxp 5019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( <.
d ,  c >.  e.  ( A  X.  A
)  <->  ( d  e.  A  /\  c  e.  A ) )
445443, 444sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( c  e.  A  /\  d  e.  A )  -> 
<. d ,  c >.  e.  ( A  X.  A
) )
4464453ad2ant2 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  ( A  X.  A ) )
44749, 52sstrd 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ph  ->  A  C_  RR )
448447sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  c  e.  A )  ->  c  e.  RR )
449448adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
c  e.  RR )
4504493adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  e.  RR )
451 simp3 999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  <  d )
452450, 451gtned 9723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  d  =/=  c )
453452neneqd 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  -.  d  =  c )
454 df-br 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( d  _I  c  <->  <. d ,  c >.  e.  _I  )
455 vex 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  c  e. 
_V
456455ideq 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( d  _I  c  <->  d  =  c )
457454, 456bitr3i 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( <.
d ,  c >.  e.  _I  <->  d  =  c )
458453, 457sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  -.  <.
d ,  c >.  e.  _I  )
459446, 458eldifd 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  ( ( A  X.  A
)  \  _I  )
)
460459, 48syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  I
)
461450, 451ltned 9724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  =/=  d )
4621433ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ( D  |`  I )  =  ( ( abs  o.  -  )  |`  I ) )
463462fveq1d 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
( ( abs  o.  -  )  |`  I ) `
 <. d ,  c
>. ) )
4644453ad2ant2 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  ( A  X.  A ) )
465 necom 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( c  =/=  d  <->  d  =/=  c )
466465biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( c  =/=  d  ->  d  =/=  c )
467466neneqd 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( c  =/=  d  ->  -.  d  =  c )
4684673ad2ant3 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  -.  d  =  c )
469468, 457sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  -.  <.
d ,  c >.  e.  _I  )
470464, 469eldifd 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  ( ( A  X.  A
)  \  _I  )
)
471470, 48syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  I
)
472 fvres 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( <.
d ,  c >.  e.  I  ->  ( ( ( abs  o.  -  )  |`  I ) `  <. d ,  c >.
)  =  ( ( abs  o.  -  ) `  <. d ,  c
>. ) )
473471, 472syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( ( abs  o.  -  )  |`  I ) `
 <. d ,  c
>. )  =  (
( abs  o.  -  ) `  <. d ,  c
>. ) )
474 simp1 997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ph )
475474, 471jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ( ph  /\  <. d ,  c
>.  e.  I ) )
476 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  =  <. d ,  c
>.  ->  ( x  e.  I  <->  <. d ,  c
>.  e.  I ) )
477476anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  <. d ,  c
>.  ->  ( ( ph  /\  x  e.  I )  <-> 
( ph  /\  <. d ,  c >.  e.  I
) ) )
478 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  <. d ,  c
>.  ->  ( x  e. 
dom  -  <->  <. d ,  c
>.  e.  dom  -  )
)
479477, 478imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  <. d ,  c
>.  ->  ( ( (
ph  /\  x  e.  I )  ->  x  e.  dom  -  )  <->  ( ( ph  /\  <. d ,  c
>.  e.  I )  ->  <. d ,  c >.  e.  dom  -  ) ) )
480479, 70vtoclg 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( <.
d ,  c >.  e.  I  ->  ( (
ph  /\  <. d ,  c >.  e.  I
)  ->  <. d ,  c >.  e.  dom  -  ) )
481471, 475, 480sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  dom  -  )
482 fvco 5934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( Fun  -  /\  <. d ,  c >.  e.  dom  -  )  ->  ( ( abs  o.  -  ) `  <. d ,  c >.
)  =  ( abs `  (  -  `  <. d ,  c >. )
) )
48367, 481, 482sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( abs  o.  -  ) `  <. d ,  c
>. )  =  ( abs `  (  -  `  <. d ,  c >.
) ) )
484 df-ov 6284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( d  -  c )  =  (  -  `  <. d ,  c >. )
485484eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  (  -  ` 
<. d ,  c >.
)  =  ( d  -  c )
486485fveq2i 5859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( abs `  (  -  `  <. d ,  c >. )
)  =  ( abs `  ( d  -  c
) )
487483, 486syl6eq 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( abs  o.  -  ) `  <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
488463, 473, 4873eqtrd 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
489461, 488syld3an3 1274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
490447sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  d  e.  A )  ->  d  e.  RR )
491490adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
d  e.  RR )
4924913adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  d  e.  RR )
493450, 492, 451ltled 9736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  <_  d )
494450, 492, 493abssubge0d 13244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  ( abs `  ( d  -  c ) )  =  ( d  -  c
) )
495489, 494eqtrd 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
d  -  c ) )
496 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  =  <. d ,  c
>.  ->  ( ( D  |`  I ) `  x
)  =  ( ( D  |`  I ) `  <. d ,  c
>. ) )
497496eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  <. d ,  c
>.  ->  ( ( ( D  |`  I ) `  x )  =  ( d  -  c )  <-> 
( ( D  |`  I ) `  <. d ,  c >. )  =  ( d  -  c ) ) )
498497rspcev 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
<. d ,  c >.  e.  I  /\  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
d  -  c ) )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) )
499460, 495, 498syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) )
500491, 449resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
( d  -  c
)  e.  RR )
501 elex 3104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( d  -  c )  e.  RR  ->  (
d  -  c )  e.  _V )
502500, 501syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
( d  -  c
)  e.  _V )
5035023adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  _V )
504 simp1 997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  ph )
505 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  =  ( d  -  c )  ->  (
y  e.  ran  ( D  |`  I )  <->  ( d  -  c )  e. 
ran  ( D  |`  I ) ) )
506 eqeq2 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( y  =  ( d  -  c )  ->  (
( ( D  |`  I ) `  x
)  =  y  <->  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) )
507506rexbidv 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  =  ( d  -  c )  ->  ( E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) )
508505, 507bibi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( y  =  ( d  -  c )  ->  (
( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y )  <-> 
( ( d  -  c )  e.  ran  ( D  |`  I )  <->  E. x  e.  I 
( ( D  |`  I ) `  x
)  =  ( d  -  c ) ) ) )
509508imbi2d 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( y  =  ( d  -  c )  ->  (
( ph  ->  ( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )  <->  ( ph  ->  ( ( d  -  c )  e.  ran  ( D  |`  I )  <->  E. x  e.  I 
( ( D  |`  I ) `  x
)  =  ( d  -  c ) ) ) ) )
51061, 426syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  ( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y ) )
511509, 510vtoclg 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( d  -  c )  e.  _V  ->  ( ph  ->  ( ( d  -  c )  e. 
ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) ) )
512503, 504, 511sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
( d  -  c
)  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) )
513499, 512mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  ran  ( D  |`  I ) )
514513, 34syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  R )
515 infmrlb 10531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( R  C_  RR  /\  E. x  e.  RR  A. y  e.  R  x  <_  y  /\  ( d  -  c )  e.  R
)  ->  sup ( R ,  RR ,  `'  <  )  <_  (
d  -  c ) )
516420, 442, 514, 515syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  sup ( R ,  RR ,  `'  <  )  <_  (
d  -  c ) )
51733, 516syl5eqbr 4470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E  <_  ( d  -  c
) )
518419, 517vtoclg 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( B  e.  A  ->  (
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  E  <_  (
d  -  B ) ) )
519412, 518mpcom 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  E  <_  ( d  -  B
) )
520411, 519vtoclg 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( C  e.  A  ->  (
( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C )  ->  E  <_  ( C  -  B )
) )
521146, 404, 520sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  E  <_  ( C  -  B ) )
522521, 280syl6breqr 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  E  <_  T )
523269, 522syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  E  <_  T )
5245233ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  T )
525524ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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  <_  T
)
526366adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ps  /\  k  e.  ZZ )  ->  b  e.  CC )
527526, 368pncan2d 9938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( b  +  ( k  x.  T ) )  -  b )  =  ( k  x.  T ) )
528527oveq1d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( ( b  +  ( k  x.  T
) )  -  b
)  /  T )  =  ( ( k  x.  T )  /  T ) )
529342adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  e.  CC )
530320adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  e.  CC )
531421a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  0  e.  RR )
532531, 352gtned 9723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  T  =/=  0 )
533269, 532syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ps 
->  T  =/=  0
)
534533adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  =/=  0 )
535529, 530, 534divcan4d 10333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( k  x.  T
)  /  T )  =  k )
536528, 535eqtr2d 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
537536adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
538537adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T ) ) )  ->  k  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
539 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T
) )  ->  (
( a  +  ( j  x.  T ) )  -  b )  =  ( ( b  +  ( k  x.  T ) )  -  b ) )
540539oveq1d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T
) )  ->  (
( ( a  +  ( j  x.  T
) )  -  b