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

Theorem fourierdlem42OLD 37953
Description: The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of fourierdlem42 37952 as of 29-Sep-2020. ( (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
fourierdlem42OLD.b  |-  ( ph  ->  B  e.  RR )
fourierdlem42OLD.c  |-  ( ph  ->  C  e.  RR )
fourierdlem42OLD.bc  |-  ( ph  ->  B  <  C )
fourierdlem42OLD.t  |-  T  =  ( C  -  B
)
fourierdlem42OLD.a  |-  ( ph  ->  A  C_  ( B [,] C ) )
fourierdlem42OLD.af  |-  ( ph  ->  A  e.  Fin )
fourierdlem42OLD.ba  |-  ( ph  ->  B  e.  A )
fourierdlem42OLD.ca  |-  ( ph  ->  C  e.  A )
fourierdlem42OLD.d  |-  D  =  ( abs  o.  -  )
fourierdlem42OLD.i  |-  I  =  ( ( A  X.  A )  \  _I  )
fourierdlem42OLD.r  |-  R  =  ran  ( D  |`  I )
fourierdlem42OLD.e  |-  E  =  sup ( R ,  RR ,  `'  <  )
fourierdlem42OLD.x  |-  ( ph  ->  X  e.  RR )
fourierdlem42OLD.y  |-  ( ph  ->  Y  e.  RR )
fourierdlem42OLD.j  |-  J  =  ( topGen `  ran  (,) )
fourierdlem42OLD.k  |-  K  =  ( Jt  ( X [,] Y ) )
fourierdlem42OLD.h  |-  H  =  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A }
fourierdlem42OLD.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
fourierdlem42OLD  |-  ( 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 fourierdlem42OLD
Dummy variables  c 
d  i  l  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem42OLD.x . . . . 5  |-  ( ph  ->  X  e.  RR )
2 fourierdlem42OLD.y . . . . 5  |-  ( ph  ->  Y  e.  RR )
3 fourierdlem42OLD.j . . . . . 6  |-  J  =  ( topGen `  ran  (,) )
4 fourierdlem42OLD.k . . . . . 6  |-  K  =  ( Jt  ( X [,] Y ) )
53, 4icccmp 21841 . . . . 5  |-  ( ( X  e.  RR  /\  Y  e.  RR )  ->  K  e.  Comp )
61, 2, 5syl2anc 665 . . . 4  |-  ( ph  ->  K  e.  Comp )
76adantr 466 . . 3  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  K  e.  Comp )
8 fourierdlem42OLD.h . . . . . 6  |-  H  =  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A }
9 ssrab2 3546 . . . . . . 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 3508 . . . . 5  |-  ( ph  ->  H  C_  ( X [,] Y ) )
12 retop 21780 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  e.  Top
133, 12eqeltri 2503 . . . . . . 7  |-  J  e. 
Top
141, 2iccssred 37551 . . . . . . 7  |-  ( ph  ->  ( X [,] Y
)  C_  RR )
15 uniretop 21781 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
163unieqi 4228 . . . . . . . . 9  |-  U. J  =  U. ( topGen `  ran  (,) )
1715, 16eqtr4i 2454 . . . . . . . 8  |-  RR  =  U. J
1817restuni 20176 . . . . . . 7  |-  ( ( J  e.  Top  /\  ( X [,] Y ) 
C_  RR )  -> 
( X [,] Y
)  =  U. ( Jt  ( X [,] Y ) ) )
1913, 14, 18sylancr 667 . . . . . 6  |-  ( ph  ->  ( X [,] Y
)  =  U. ( Jt  ( X [,] Y ) ) )
204unieqi 4228 . . . . . . 7  |-  U. K  =  U. ( Jt  ( X [,] Y ) )
2120eqcomi 2435 . . . . . 6  |-  U. ( Jt  ( X [,] Y ) )  =  U. K
2219, 21syl6eq 2479 . . . . 5  |-  ( ph  ->  ( X [,] Y
)  =  U. K
)
2311, 22sseqtrd 3500 . . . 4  |-  ( ph  ->  H  C_  U. K )
2423adantr 466 . . 3  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  H  C_ 
U. K )
25 simpr 462 . . 3  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  -.  H  e.  Fin )
26 eqid 2422 . . . 4  |-  U. K  =  U. K
2726bwth 20423 . . 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 1264 . 2  |-  ( (
ph  /\  -.  H  e.  Fin )  ->  E. x  e.  U. K x  e.  ( ( limPt `  K
) `  H )
)
2911, 14sstrd 3474 . . . . . . . . . 10  |-  ( ph  ->  H  C_  RR )
3029ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  H  C_  RR )
31 ne0i 3767 . . . . . . . . . 10  |-  ( x  e.  ( ( limPt `  J ) `  H
)  ->  ( ( limPt `  J ) `  H )  =/=  (/) )
3231adantl 467 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  -> 
( ( limPt `  J
) `  H )  =/=  (/) )
33 fourierdlem42OLD.e . . . . . . . . . . 11  |-  E  =  sup ( R ,  RR ,  `'  <  )
34 fourierdlem42OLD.r . . . . . . . . . . . . 13  |-  R  =  ran  ( D  |`  I )
35 absf 13400 . . . . . . . . . . . . . . . . . 18  |-  abs : CC
--> RR
36 ffn 5746 . . . . . . . . . . . . . . . . . 18  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
3735, 36ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  abs  Fn  CC
38 subf 9884 . . . . . . . . . . . . . . . . . 18  |-  -  :
( CC  X.  CC )
--> CC
39 ffn 5746 . . . . . . . . . . . . . . . . . 18  |-  (  -  : ( CC  X.  CC ) --> CC  ->  -  Fn  ( CC  X.  CC ) )
4038, 39ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  -  Fn  ( CC  X.  CC )
41 frn 5752 . . . . . . . . . . . . . . . . . 18  |-  (  -  : ( CC  X.  CC ) --> CC  ->  ran  - 
C_  CC )
4238, 41ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ran  -  C_  CC
43 fnco 5702 . . . . . . . . . . . . . . . . 17  |-  ( ( abs  Fn  CC  /\  -  Fn  ( CC  X.  CC )  /\  ran  -  C_  CC )  ->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) )
4437, 40, 42, 43mp3an 1360 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  Fn  ( CC  X.  CC )
45 fourierdlem42OLD.d . . . . . . . . . . . . . . . . 17  |-  D  =  ( abs  o.  -  )
4645fneq1i 5688 . . . . . . . . . . . . . . . 16  |-  ( D  Fn  ( CC  X.  CC )  <->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) )
4744, 46mpbir 212 . . . . . . . . . . . . . . 15  |-  D  Fn  ( CC  X.  CC )
48 fourierdlem42OLD.i . . . . . . . . . . . . . . . 16  |-  I  =  ( ( A  X.  A )  \  _I  )
49 fourierdlem42OLD.a . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  C_  ( B [,] C ) )
50 fourierdlem42OLD.b . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  RR )
51 fourierdlem42OLD.c . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  RR )
5250, 51iccssred 37551 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( B [,] C
)  C_  RR )
53 ax-resscn 9603 . . . . . . . . . . . . . . . . . . . 20  |-  RR  C_  CC
5452, 53syl6ss 3476 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( B [,] C
)  C_  CC )
5549, 54sstrd 3474 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  C_  CC )
56 xpss12 4959 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  C_  CC  /\  A  C_  CC )  ->  ( A  X.  A )  C_  ( CC  X.  CC ) )
5755, 55, 56syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  X.  A
)  C_  ( CC  X.  CC ) )
5857ssdifssd 3603 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  X.  A )  \  _I  )  C_  ( CC  X.  CC ) )
5948, 58syl5eqss 3508 . . . . . . . . . . . . . . 15  |-  ( ph  ->  I  C_  ( CC  X.  CC ) )
60 fnssres 5707 . . . . . . . . . . . . . . 15  |-  ( ( D  Fn  ( CC 
X.  CC )  /\  I  C_  ( CC  X.  CC ) )  ->  ( D  |`  I )  Fn  I )
6147, 59, 60sylancr 667 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  |`  I )  Fn  I )
62 fvres 5895 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  I  ->  (
( D  |`  I ) `
 x )  =  ( D `  x
) )
6362adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  =  ( D `  x
) )
6445fveq1i 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( D `
 x )  =  ( ( abs  o.  -  ) `  x
)
6564a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  ( D `  x )  =  ( ( abs 
o.  -  ) `  x ) )
66 ffun 5748 . . . . . . . . . . . . . . . . . . . 20  |-  (  -  : ( CC  X.  CC ) --> CC  ->  Fun  -  )
6738, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  Fun  -
6859sselda 3464 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  ( CC  X.  CC ) )
6938fdmi 5751 . . . . . . . . . . . . . . . . . . . 20  |-  dom  -  =  ( CC  X.  CC )
7068, 69syl6eleqr 2518 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  dom  -  )
71 fvco 5957 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  -  /\  x  e.  dom  -  )  -> 
( ( abs  o.  -  ) `  x
)  =  ( abs `  (  -  `  x
) ) )
7267, 70, 71sylancr 667 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (
( abs  o.  -  ) `  x )  =  ( abs `  (  -  `  x ) ) )
7363, 65, 723eqtrd 2467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  =  ( abs `  (  -  `  x ) ) )
7438a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  -  :
( CC  X.  CC )
--> CC )
7574, 68ffvelrnd 6038 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (  -  `  x )  e.  CC )
7675abscld 13497 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  ( abs `  (  -  `  x ) )  e.  RR )
7773, 76eqeltrd 2507 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  e.  RR )
78 elxp2 4871 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( CC  X.  CC )  <->  E. y  e.  CC  E. z  e.  CC  x  =  <. y ,  z
>. )
7968, 78sylib 199 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  E. y  e.  CC  E. z  e.  CC  x  =  <. y ,  z >. )
80 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  <. y ,  z
>.  ->  (  -  `  x )  =  (  -  `  <. y ,  z >. )
)
81803ad2ant3 1028 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  x
)  =  (  -  ` 
<. y ,  z >.
) )
82 df-ov 6308 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  -  z )  =  (  -  `  <. y ,  z >. )
83 simp1l 1029 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  ph )
84 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  x  =  <. y ,  z
>. )
85 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  x  e.  I )
8684, 85eqeltrrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  I  /\  x  =  <. y ,  z >. )  ->  <. y ,  z >.  e.  I
)
8786adantll 718 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  I )  /\  x  =  <. y ,  z
>. )  ->  <. y ,  z >.  e.  I
)
88873adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  -> 
<. y ,  z >.  e.  I )
8955adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  A  C_  CC )
9048eleq2i 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
y ,  z >.  e.  I  <->  <. y ,  z
>.  e.  ( ( A  X.  A )  \  _I  ) )
91 eldif 3446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
y ,  z >.  e.  ( ( A  X.  A )  \  _I  ) 
<->  ( <. y ,  z
>.  e.  ( A  X.  A )  /\  -.  <.
y ,  z >.  e.  _I  ) )
9290, 91sylbb 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( <.
y ,  z >.  e.  I  ->  ( <.
y ,  z >.  e.  ( A  X.  A
)  /\  -.  <. y ,  z >.  e.  _I  ) )
9392simpld 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
y ,  z >.  e.  I  ->  <. y ,  z >.  e.  ( A  X.  A ) )
94 opelxp 4883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
y ,  z >.  e.  ( A  X.  A
)  <->  ( y  e.  A  /\  z  e.  A ) )
9593, 94sylib 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
y ,  z >.  e.  I  ->  ( y  e.  A  /\  z  e.  A ) )
9695adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  ( y  e.  A  /\  z  e.  A ) )
9796simpld 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  e.  A )
9889, 97sseldd 3465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  e.  CC )
9996simprd 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  z  e.  A )
10089, 99sseldd 3465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  z  e.  CC )
10192simprd 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
y ,  z >.  e.  I  ->  -.  <. y ,  z >.  e.  _I  )
102 df-br 4424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  _I  z  <->  <. y ,  z >.  e.  _I  )
103101, 102sylnibr 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
y ,  z >.  e.  I  ->  -.  y  _I  z )
104 vex 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  z  e. 
_V
105104ideq 5006 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  _I  z  <->  y  =  z )
106103, 105sylnib 305 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
y ,  z >.  e.  I  ->  -.  y  =  z )
107106neqned 2623 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
y ,  z >.  e.  I  ->  y  =/=  z )
108107adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  =/=  z )
10998, 100, 108subne0d 10002 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  ( y  -  z )  =/=  0 )
11083, 88, 109syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  ( y  -  z
)  =/=  0 )
11182, 110syl5eqner 2721 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  <. y ,  z >. )  =/=  0 )
11281, 111eqnetrd 2713 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  x
)  =/=  0 )
1131123exp 1204 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  (
( y  e.  CC  /\  z  e.  CC )  ->  ( x  = 
<. y ,  z >.  ->  (  -  `  x
)  =/=  0 ) ) )
114113rexlimdvv 2920 . . . . . . . . . . . . . . . . . . 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 13387 . . . . . . . . . . . . . . . . . . 19  |-  ( (  -  `  x )  e.  CC  ->  (
(  -  `  x
)  =/=  0  <->  0  <  ( abs `  (  -  `  x ) ) ) )
11775, 116syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (
(  -  `  x
)  =/=  0  <->  0  <  ( abs `  (  -  `  x ) ) ) )
118115, 117mpbid 213 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  0  <  ( abs `  (  -  `  x ) ) )
11973eqcomd 2430 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  ( abs `  (  -  `  x ) )  =  ( ( D  |`  I ) `  x
) )
120118, 119breqtrd 4448 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  0  <  ( ( D  |`  I ) `  x
) )
12177, 120elrpd 11345 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  e.  RR+ )
122121ralrimiva 2836 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  I 
( ( D  |`  I ) `  x
)  e.  RR+ )
123 fnfvrnss 6066 . . . . . . . . . . . . . 14  |-  ( ( ( D  |`  I )  Fn  I  /\  A. x  e.  I  (
( D  |`  I ) `
 x )  e.  RR+ )  ->  ran  ( D  |`  I )  C_  RR+ )
12461, 122, 123syl2anc 665 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  ( D  |`  I )  C_  RR+ )
12534, 124syl5eqss 3508 . . . . . . . . . . . 12  |-  ( ph  ->  R  C_  RR+ )
126 ltso 9721 . . . . . . . . . . . . . . 15  |-  <  Or  RR
127126a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  <  Or  RR )
128 cnvso 5394 . . . . . . . . . . . . . 14  |-  (  < 
Or  RR  <->  `'  <  Or  RR )
129127, 128sylib 199 . . . . . . . . . . . . 13  |-  ( ph  ->  `'  <  Or  RR )
130 fourierdlem42OLD.af . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  Fin )
131 xpfi 7851 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  Fin  /\  A  e.  Fin )  ->  ( A  X.  A
)  e.  Fin )
132130, 130, 131syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A  X.  A
)  e.  Fin )
133 diffi 7812 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  X.  A )  e.  Fin  ->  (
( A  X.  A
)  \  _I  )  e.  Fin )
134132, 133syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( A  X.  A )  \  _I  )  e.  Fin )
13548, 134syl5eqel 2511 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  I  e.  Fin )
136 fnfi 7858 . . . . . . . . . . . . . . . 16  |-  ( ( ( D  |`  I )  Fn  I  /\  I  e.  Fin )  ->  ( D  |`  I )  e. 
Fin )
13761, 135, 136syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  |`  I )  e.  Fin )
138 rnfi 7866 . . . . . . . . . . . . . . 15  |-  ( ( D  |`  I )  e.  Fin  ->  ran  ( D  |`  I )  e.  Fin )
139137, 138syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  ( D  |`  I )  e.  Fin )
14034, 139syl5eqel 2511 . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  Fin )
14134a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  =  ran  ( D  |`  I ) )
14245a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  D  =  ( abs 
o.  -  ) )
143142reseq1d 5123 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  |`  I )  =  ( ( abs 
o.  -  )  |`  I ) )
144143fveq1d 5883 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  |`  I ) `  <. B ,  C >. )  =  ( ( ( abs  o.  -  )  |`  I ) `  <. B ,  C >. )
)
145 fourierdlem42OLD.ba . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  A )
146 fourierdlem42OLD.ca . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  A )
147 opelxp 4883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( <. B ,  C >.  e.  ( A  X.  A
)  <->  ( B  e.  A  /\  C  e.  A ) )
148145, 146, 147sylanbrc 668 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
<. B ,  C >.  e.  ( A  X.  A
) )
149 fourierdlem42OLD.bc . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  <  C )
15050, 149ltned 9778 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  =/=  C )
151150neneqd 2621 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  B  =  C )
152 ideqg 5005 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( C  e.  A  ->  ( B  _I  C  <->  B  =  C ) )
153146, 152syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( B  _I  C  <->  B  =  C ) )
154151, 153mtbird 302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  B  _I  C
)
155 df-br 4424 . . . . . . . . . . . . . . . . . . . . 21  |-  ( B  _I  C  <->  <. B ,  C >.  e.  _I  )
156154, 155sylnib 305 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  <. B ,  C >.  e.  _I  )
157148, 156eldifd 3447 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
<. B ,  C >.  e.  ( ( A  X.  A )  \  _I  ) )
158157, 48syl6eleqr 2518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
<. B ,  C >.  e.  I )
159 fvres 5895 . . . . . . . . . . . . . . . . . 18  |-  ( <. B ,  C >.  e.  I  ->  ( (
( abs  o.  -  )  |`  I ) `  <. B ,  C >. )  =  ( ( abs 
o.  -  ) `  <. B ,  C >. ) )
160158, 159syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( abs 
o.  -  )  |`  I ) `
 <. B ,  C >. )  =  ( ( abs  o.  -  ) `  <. B ,  C >. ) )
16150recnd 9676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  CC )
16251recnd 9676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  CC )
163 opelxp 4883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( <. B ,  C >.  e.  ( CC  X.  CC ) 
<->  ( B  e.  CC  /\  C  e.  CC ) )
164161, 162, 163sylanbrc 668 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
<. B ,  C >.  e.  ( CC  X.  CC ) )
165164, 69syl6eleqr 2518 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
<. B ,  C >.  e. 
dom  -  )
166 fvco 5957 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  -  /\  <. B ,  C >.  e.  dom  -  )  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  (  -  `  <. B ,  C >. ) ) )
16767, 165, 166sylancr 667 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  (  -  `  <. B ,  C >. ) ) )
168 df-ov 6308 . . . . . . . . . . . . . . . . . . . . 21  |-  ( B  -  C )  =  (  -  `  <. B ,  C >. )
169168eqcomi 2435 . . . . . . . . . . . . . . . . . . . 20  |-  (  -  ` 
<. B ,  C >. )  =  ( B  -  C )
170169a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  (  -  `  <. B ,  C >. )  =  ( B  -  C ) )
171170fveq2d 5885 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  (  -  `  <. B ,  C >. ) )  =  ( abs `  ( B  -  C ) ) )
172167, 171eqtrd 2463 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  ( B  -  C )
) )
173144, 160, 1723eqtrrd 2468 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( abs `  ( B  -  C )
)  =  ( ( D  |`  I ) `  <. B ,  C >. ) )
174 fnfvelrn 6034 . . . . . . . . . . . . . . . . 17  |-  ( ( ( D  |`  I )  Fn  I  /\  <. B ,  C >.  e.  I
)  ->  ( ( D  |`  I ) `  <. B ,  C >. )  e.  ran  ( D  |`  I ) )
17561, 158, 174syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  |`  I ) `  <. B ,  C >. )  e.  ran  ( D  |`  I ) )
176173, 175eqeltrd 2507 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( abs `  ( B  -  C )
)  e.  ran  ( D  |`  I ) )
177 ne0i 3767 . . . . . . . . . . . . . . 15  |-  ( ( abs `  ( B  -  C ) )  e.  ran  ( D  |`  I )  ->  ran  ( D  |`  I )  =/=  (/) )
178176, 177syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  ( D  |`  I )  =/=  (/) )
179141, 178eqnetrd 2713 . . . . . . . . . . . . 13  |-  ( ph  ->  R  =/=  (/) )
180 resss 5147 . . . . . . . . . . . . . . . . 17  |-  ( D  |`  I )  C_  D
181 rnss 5082 . . . . . . . . . . . . . . . . 17  |-  ( ( D  |`  I )  C_  D  ->  ran  ( D  |`  I )  C_  ran  D )
182180, 181ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ran  ( D  |`  I )  C_  ran  D
18345rneqi 5080 . . . . . . . . . . . . . . . . 17  |-  ran  D  =  ran  ( abs  o.  -  )
184 rncoss 5114 . . . . . . . . . . . . . . . . . 18  |-  ran  ( abs  o.  -  )  C_  ran  abs
185 frn 5752 . . . . . . . . . . . . . . . . . . 19  |-  ( abs
: CC --> RR  ->  ran 
abs  C_  RR )
18635, 185ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ran  abs  C_  RR
187184, 186sstri 3473 . . . . . . . . . . . . . . . . 17  |-  ran  ( abs  o.  -  )  C_  RR
188183, 187eqsstri 3494 . . . . . . . . . . . . . . . 16  |-  ran  D  C_  RR
189182, 188sstri 3473 . . . . . . . . . . . . . . 15  |-  ran  ( D  |`  I )  C_  RR
19034, 189eqsstri 3494 . . . . . . . . . . . . . 14  |-  R  C_  RR
191190a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  R  C_  RR )
192 fisupcl 7994 . . . . . . . . . . . . 13  |-  ( ( `'  <  Or  RR  /\  ( R  e.  Fin  /\  R  =/=  (/)  /\  R  C_  RR ) )  ->  sup ( R ,  RR ,  `'  <  )  e.  R )
193129, 140, 179, 191, 192syl13anc 1266 . . . . . . . . . . . 12  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  R )
194125, 193sseldd 3465 . . . . . . . . . . 11  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  RR+ )
19533, 194syl5eqel 2511 . . . . . . . . . 10  |-  ( ph  ->  E  e.  RR+ )
196195ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  E  e.  RR+ )
1973, 30, 32, 196lptre2pt 37660 . . . . . . . 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 758 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  ph )
19929sselda 3464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  H )  ->  y  e.  RR )
200199adantrr 721 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  H  /\  z  e.  H ) )  -> 
y  e.  RR )
201200adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  y  e.  RR )
20229sselda 3464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  H )  ->  z  e.  RR )
203202adantrl 720 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  H  /\  z  e.  H ) )  -> 
z  e.  RR )
204203adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  z  e.  RR )
205 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  y  =/=  z )
206201, 204, 2053jca 1185 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  (
y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )
2078eleq2i 2499 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  H  <->  y  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A }
)
208 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x  +  ( k  x.  T ) )  =  ( y  +  ( k  x.  T
) ) )
209208eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( x  +  ( k  x.  T ) )  e.  A  <->  ( y  +  ( k  x.  T ) )  e.  A ) )
210209rexbidv 2936 . . . . . . . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
212211oveq2d 6321 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  j  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
213212eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
( y  +  ( k  x.  T ) )  e.  A  <->  ( y  +  ( j  x.  T ) )  e.  A ) )
214213cbvrexv 3055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  A  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
)
215210, 214syl6bb 264 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
) )
216215elrab 3228 . . . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  H  ->  (
y  e.  ( X [,] Y )  /\  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  A ) )
218217simprd 464 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  H  ->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
)
219218adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. j  e.  ZZ  ( y  +  ( j  x.  T ) )  e.  A )
2208eleq2i 2499 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  H  <->  z  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A }
)
221 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
x  +  ( k  x.  T ) )  =  ( z  +  ( k  x.  T
) ) )
222221eleq1d 2491 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( x  +  ( k  x.  T ) )  e.  A  <->  ( z  +  ( k  x.  T ) )  e.  A ) )
223222rexbidv 2936 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
) )
224223elrab 3228 . . . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  H  ->  (
z  e.  ( X [,] Y )  /\  E. k  e.  ZZ  (
z  +  ( k  x.  T ) )  e.  A ) )
226225simprd 464 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  H  ->  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
)
227226adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. k  e.  ZZ  ( z  +  ( k  x.  T ) )  e.  A )
228 reeanv 2993 . . . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . 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 766 . . . . . . . . . . . . . . . 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 1008 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
y  e.  RR )
233 simpl2 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
z  e.  RR )
234 simpr 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
y  <  z )
235232, 233, 2343jca 1185 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
236235adantll 718 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
237236adantlr 719 . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
b  e.  RR  <->  z  e.  RR ) )
240 breq2 4427 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
y  <  b  <->  y  <  z ) )
241239, 2403anbi23d 1338 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  (
( y  e.  RR  /\  b  e.  RR  /\  y  <  b )  <->  ( y  e.  RR  /\  z  e.  RR  /\  y  < 
z ) ) )
242241anbi2d 708 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  z  ->  (
( ph  /\  (
y  e.  RR  /\  b  e.  RR  /\  y  <  b ) )  <->  ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) ) ) )
243 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  z  ->  (
b  +  ( k  x.  T ) )  =  ( z  +  ( k  x.  T
) ) )
244243eleq1d 2491 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
( b  +  ( k  x.  T ) )  e.  A  <->  ( z  +  ( k  x.  T ) )  e.  A ) )
245244anbi2d 708 . . . . . . . . . . . . . . . . . . . 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 2943 . . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . 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 6313 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  (
y  -  b )  =  ( y  -  z ) )
249248fveq2d 5885 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  z  ->  ( abs `  ( y  -  b ) )  =  ( abs `  (
y  -  z ) ) )
250249breq2d 4435 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  z  ->  ( E  <_  ( abs `  (
y  -  b ) )  <->  E  <_  ( abs `  ( y  -  z
) ) ) )
251247, 250imbi12d 321 . . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
a  e.  RR  <->  y  e.  RR ) )
253 breq1 4426 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
a  <  b  <->  y  <  b ) )
254252, 2533anbi13d 1337 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  (
( a  e.  RR  /\  b  e.  RR  /\  a  <  b )  <->  ( y  e.  RR  /\  b  e.  RR  /\  y  < 
b ) ) )
255254anbi2d 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  y  ->  (
( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  <->  ( ph  /\  ( y  e.  RR  /\  b  e.  RR  /\  y  <  b ) ) ) )
256 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  y  ->  (
a  +  ( j  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
257256eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
( a  +  ( j  x.  T ) )  e.  A  <->  ( y  +  ( j  x.  T ) )  e.  A ) )
258257anbi1d 709 . . . . . . . . . . . . . . . . . . . . 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 2943 . . . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  (
a  -  b )  =  ( y  -  b ) )
262261fveq2d 5885 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  y  ->  ( abs `  ( a  -  b ) )  =  ( abs `  (
y  -  b ) ) )
263262breq2d 4435 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  y  ->  ( E  <_  ( abs `  (
a  -  b ) )  <->  E  <_  ( abs `  ( y  -  b
) ) ) )
264260, 263imbi12d 321 . . . . . . . . . . . . . . . . . 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 fourierdlem42OLD.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 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ps 
->  E. j  e.  ZZ  E. k  e.  ZZ  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )
267265biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  ( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) ) )
269268simpld 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  ph )
270269, 50syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  B  e.  RR )
271270adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  B  e.  RR )
272269, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  C  e.  RR )
273272adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  C  e.  RR )
274269, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  A  C_  ( B [,] C ) )
275274sselda 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( b  +  ( k  x.  T ) )  e.  A )  ->  (
b  +  ( k  x.  T ) )  e.  ( B [,] C ) )
276275adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( b  +  ( k  x.  T
) )  e.  ( B [,] C ) )
277274sselda 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( a  +  ( j  x.  T ) )  e.  A )  ->  (
a  +  ( j  x.  T ) )  e.  ( B [,] C ) )
278277adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 37569 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 fourierdlem42OLD.t . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  T  =  ( C  -  B
)
281279, 280syl6breqr 4464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T
)
2822813adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  -.  k  <_  j )
285 zre 10948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ZZ  ->  j  e.  RR )
286285adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  j  e.  RR )
287286ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  j  e.  RR )
288 zre 10948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ZZ  ->  k  e.  RR )
289288adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  k  e.  RR )
290289ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  k  e.  RR )
291287, 290ltnled 9789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  (
j  <  k  <->  -.  k  <_  j ) )
292284, 291mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  j  <  k )
29351, 50resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( C  -  B
)  e.  RR )
294280, 293syl5eqel 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  T  e.  RR )
295269, 294syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  T  e.  RR )
296295ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  e.  RR )
297289adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  e.  RR )
298286adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
j  e.  RR )
299297, 298resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  -  j
)  e.  RR )
300295adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  ->  T  e.  RR )
301299, 300remulcld 9678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  e.  RR )
302301adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
k  -  j )  x.  T )  e.  RR )
303268simprd 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )
304303simp2d 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  b  e.  RR )
305304adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
b  e.  RR )
306288adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  e.  RR )
307295adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  e.  RR )
308306, 307remulcld 9678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  RR )
309308adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  x.  T
)  e.  RR )
310305, 309readdcld 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( b  +  ( k  x.  T ) )  e.  RR )
311303simp1d 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  a  e.  RR )
312311adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
a  e.  RR )
313285adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  j  e.  RR )
314295adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  T  e.  RR )
315313, 314remulcld 9678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  j  e.  ZZ )  ->  (
j  x.  T )  e.  RR )
316315adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  x.  T
)  e.  RR )
317312, 316readdcld 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( a  +  ( j  x.  T ) )  e.  RR )
318310, 317resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  e.  RR )
319318adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) )  e.  RR )
320295recnd 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  T  e.  CC )
321320mulid2d 9668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  ( 1  x.  T
)  =  T )
322321eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  T  =  (
1  x.  T ) )
323322ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  =  ( 1  x.  T
) )
324 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  <  k )
325 zltlem1 10996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  <  k  <->  j  <_  ( k  - 
1 ) ) )
326325ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( j  <  k  <->  j  <_  (
k  -  1 ) ) )
327324, 326mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  <_  ( k  -  1 ) )
328286ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  j  e.  RR )
329 peano2rem 9948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  RR  ->  (
k  -  1 )  e.  RR )
330297, 329syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  -  1 )  e.  RR )
331330adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( k  -  1 )  e.  RR )
332 1re 9649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  1  e.  RR
333 resubcl 9945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 1  e.  RR  /\  j  e.  RR )  ->  ( 1  -  j
)  e.  RR )
334332, 328, 333sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( 1  -  j )  e.  RR )
335 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  j  <_  ( k  -  1 ) )
336328, 331, 334, 335leadd1dd 10234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  +  ( 1  -  j ) )  <_ 
( ( k  - 
1 )  +  ( 1  -  j ) ) )
337 zcn 10949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  ZZ  ->  j  e.  CC )
338337adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  j  e.  CC )
339 1cnd 9666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  1  e.  CC )
340338, 339pncan3d 9996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  +  ( 1  -  j ) )  =  1 )
341340ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  +  ( 1  -  j ) )  =  1 )
342 zcn 10949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  ZZ  ->  k  e.  CC )
343342adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  k  e.  CC )
344343, 339, 338npncand 10017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( ( k  - 
1 )  +  ( 1  -  j ) )  =  ( k  -  j ) )
345344ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( (
k  -  1 )  +  ( 1  -  j ) )  =  ( k  -  j
) )
346336, 341, 3453brtr3d 4453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  1  <_  ( k  -  j ) )
347327, 346syldan 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( k  -  j )  e.  RR )
35050, 51posdifd 10207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( B  <  C  <->  0  <  ( C  -  B ) ) )
351149, 350mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  0  <  ( C  -  B ) )
352351, 280syl6breqr 4464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  0  <  T )
353294, 352elrpd 11345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  T  e.  RR+ )
354269, 353syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  T  e.  RR+ )
355354ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  e.  RR+ )
356348, 349, 355lemul1d 11388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( 1  <_  ( k  -  j )  <->  ( 1  x.  T )  <_ 
( ( k  -  j )  x.  T
) ) )
357347, 356mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( 1  x.  T )  <_ 
( ( k  -  j )  x.  T
) )
358323, 357eqbrtrd 4444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  <_  ( ( k  -  j
)  x.  T ) )
359304, 311resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  ( b  -  a
)  e.  RR )
360303simp3d 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ps 
->  a  <  b )
361311, 304posdifd 10207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ps 
->  ( a  <  b  <->  0  <  ( b  -  a ) ) )
362360, 361mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  0  <  ( b  -  a ) )
363359, 362elrpd 11345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  ( b  -  a
)  e.  RR+ )
364363adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( b  -  a
)  e.  RR+ )
365301, 364ltaddrp2d 11379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  <  ( (
b  -  a )  +  ( ( k  -  j )  x.  T ) ) )
366304recnd 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  b  e.  CC )
367366adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
b  e.  CC )
368308recnd 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  CC )
369368adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  x.  T
)  e.  CC )
370311recnd 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  a  e.  CC )
371370adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
a  e.  CC )
372315recnd 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  (
j  x.  T )  e.  CC )
373372adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  x.  T
)  e.  CC )
374367, 369, 371, 373addsub4d 10040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  e.  CC )
376337ad2antrl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
j  e.  CC )
377320adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  ->  T  e.  CC )
378375, 376, 377subdird 10082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  =  ( ( k  x.  T )  -  ( j  x.  T ) ) )
379378eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  x.  T )  -  (
j  x.  T ) )  =  ( ( k  -  j )  x.  T ) )
380379oveq2d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  -  a )  +  ( ( k  x.  T
)  -  ( j  x.  T ) ) )  =  ( ( b  -  a )  +  ( ( k  -  j )  x.  T ) ) )
381374, 380eqtr2d 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  -  a )  +  ( ( k  -  j
)  x.  T ) )  =  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) ) )
382365, 381breqtrd 4448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  <  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) ) )
383382adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  <  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) ) )
385296, 319ltnled 9789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  -.  (
( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T )
387292, 386syldan 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  -.  ( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  <_  T )
3883873adantl3 1163 . . . . . . . . . . . . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  k  <_  j )
390190, 193sseldi 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  e.  RR )
39133, 390syl5eqel 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  E  e.  RR )
392269, 391syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  E  e.  RR )
3933923ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  e.  RR )
394393ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  T  e.  RR )
396395ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  -  k
)  e.  RR )
398397adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  -  k
)  e.  RR )
399398, 300remulcld 9678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( j  -  k )  x.  T
)  e.  RR )
4003993adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( B  e.  A  /\  C  e.  A
) )
404402, 403, 1493jca 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C ) )
405 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( d  =  C  ->  (
d  e.  A  <->  C  e.  A ) )
406405anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  (
( B  e.  A  /\  d  e.  A
)  <->  ( B  e.  A  /\  C  e.  A ) ) )
407 breq2 4427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  ( B  <  d  <->  B  <  C ) )
408406, 4073anbi23d 1338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( d  =  C  ->  (
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  <-> 
( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C ) ) )
409 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  (
d  -  B )  =  ( C  -  B ) )
410409breq2d 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( d  =  C  ->  ( E  <_  ( d  -  B )  <->  E  <_  ( C  -  B ) ) )
411408, 410imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  B  e.  A )
413 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( c  =  B  ->  (
c  e.  A  <->  B  e.  A ) )
414413anbi1d 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
( c  e.  A  /\  d  e.  A
)  <->  ( B  e.  A  /\  d  e.  A ) ) )
415 breq1 4426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
c  <  d  <->  B  <  d ) )
416414, 4153anbi23d 1338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  =  B  ->  (
( ph  /\  (
c  e.  A  /\  d  e.  A )  /\  c  <  d )  <-> 
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d ) ) )
417 oveq2 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
d  -  c )  =  ( d  -  B ) )
418417breq2d 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  =  B  ->  ( E  <_  ( d  -  c )  <->  E  <_  ( d  -  B ) ) )
419416, 418imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  0  e.  RR
42234eleq2i 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( y  e.  R  <->  y  e.  ran  ( D  |`  I ) )
423422biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  e.  R  ->  y  e.  ran  ( D  |`  I ) )
424423adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  y  e.  ran  ( D  |`  I ) )
42561adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  y  e.  R )  ->  ( D  |`  I )  Fn  I )
426 fvelrnb 5928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( D  |`  I )  Fn  I  ->  ( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )
427425, 426syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  (
y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )
428424, 427mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  y  e.  R )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y )
429121rpge0d 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  x  e.  I )  ->  0  <_  ( ( D  |`  I ) `  x
) )
4304293adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  0  <_  (
( D  |`  I ) `
 x ) )
431 simp3 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  ( ( D  |`  I ) `  x
)  =  y )
432430, 431breqtrd 4448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  0  <_  y
)
4334323exp 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ph  ->  ( x  e.  I  ->  ( ( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
) )
434433adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  (
x  e.  I  -> 
( ( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
) )
435434rexlimdv 2912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  A. y  e.  R 
0  <_  y )
438 breq1 4426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
439438ralbidv 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  =  0  ->  ( A. y  e.  R  x  <_  y  <->  A. y  e.  R  0  <_  y ) )
440439rspcev 3182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( 0  e.  RR  /\  A. y  e.  R  0  <_  y )  ->  E. x  e.  RR  A. y  e.  R  x  <_  y )
441421, 437, 440sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  E. x  e.  RR  A. y  e.  R  x  <_  y )
4424413ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E. x  e.  RR  A. y  e.  R  x  <_  y
)
443 pm3.22 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( c  e.  A  /\  d  e.  A )  ->  ( d  e.  A  /\  c  e.  A
) )
444 opelxp 4883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( <.
d ,  c >.  e.  ( A  X.  A
)  <->  ( d  e.  A  /\  c  e.  A ) )
445443, 444sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( c  e.  A  /\  d  e.  A )  -> 
<. d ,  c >.  e.  ( A  X.  A
) )
4464453ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  ( A  X.  A ) )
44749, 52sstrd 3474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ph  ->  A  C_  RR )
448447sselda 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  c  e.  A )  ->  c  e.  RR )
449448adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
c  e.  RR )
4504493adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  e.  RR )
451 simp3 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  <  d )
452450, 451gtned 9777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  d  =/=  c )
453452neneqd 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  -.  d  =  c )
454 df-br 4424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( d  _I  c  <->  <. d ,  c >.  e.  _I  )
455 vex 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  c  e. 
_V
456455ideq 5006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( d  _I  c  <->  d  =  c )
457454, 456bitr3i 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( <.
d ,  c >.  e.  _I  <->  d  =  c )
458453, 457sylnibr 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  -.  <.
d ,  c >.  e.  _I  )
459446, 458eldifd 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  ( ( A  X.  A
)  \  _I  )
)
460459, 48syl6eleqr 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  I
)
461450, 451ltned 9778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  =/=  d )
4621433ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ( D  |`  I )  =  ( ( abs  o.  -  )  |`  I ) )
463462fveq1d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
( ( abs  o.  -  )  |`  I ) `
 <. d ,  c
>. ) )
4644453ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  ( A  X.  A ) )
465 necom 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( c  =/=  d  <->  d  =/=  c )
466465biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( c  =/=  d  ->  d  =/=  c )
467466neneqd 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( c  =/=  d  ->  -.  d  =  c )
4684673ad2ant3 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  -.  d  =  c )
469468, 457sylnibr 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  -.  <.
d ,  c >.  e.  _I  )
470464, 469eldifd 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  ( ( A  X.  A
)  \  _I  )
)
471470, 48syl6eleqr 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  I
)
472 fvres 5895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( <.
d ,  c >.  e.  I  ->  ( ( ( abs  o.  -  )  |`  I ) `  <. d ,  c >.
)  =  ( ( abs  o.  -  ) `  <. d ,  c
>. ) )
473471, 472syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( ( abs  o.  -  )  |`  I ) `
 <. d ,  c
>. )  =  (
( abs  o.  -  ) `  <. d ,  c
>. ) )
474 simp1 1005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ph )
475474, 471jca 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ( ph  /\  <. d ,  c
>.  e.  I ) )
476 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  =  <. d ,  c
>.  ->  ( x  e.  I  <->  <. d ,  c
>.  e.  I ) )
477476anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  <. d ,  c
>.  ->  ( ( ph  /\  x  e.  I )  <-> 
( ph  /\  <. d ,  c >.  e.  I
) ) )
478 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  <. d ,  c
>.  ->  ( x  e. 
dom  -  <->  <. d ,  c
>.  e.  dom  -  )
)
479477, 478imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  <. d ,  c
>.  ->  ( ( (
ph  /\  x  e.  I )  ->  x  e.  dom  -  )  <->  ( ( ph  /\  <. d ,  c
>.  e.  I )  ->  <. d ,  c >.  e.  dom  -  ) ) )
480479, 70vtoclg 3139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( <.
d ,  c >.  e.  I  ->  ( (
ph  /\  <. d ,  c >.  e.  I
)  ->  <. d ,  c >.  e.  dom  -  ) )
481471, 475, 480sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  dom  -  )
482 fvco 5957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( Fun  -  /\  <. d ,  c >.  e.  dom  -  )  ->  ( ( abs  o.  -  ) `  <. d ,  c >.
)  =  ( abs `  (  -  `  <. d ,  c >. )
) )
48367, 481, 482sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( abs  o.  -  ) `  <. d ,  c
>. )  =  ( abs `  (  -  `  <. d ,  c >.
) ) )
484 df-ov 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( d  -  c )  =  (  -  `  <. d ,  c >. )
485484eqcomi 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  (  -  ` 
<. d ,  c >.
)  =  ( d  -  c )
486485fveq2i 5884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( abs `  (  -  `  <. d ,  c >. )
)  =  ( abs `  ( d  -  c
) )
487483, 486syl6eq 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( abs  o.  -  ) `  <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
488463, 473, 4873eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
489461, 488syld3an3 1309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
490447sselda 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  d  e.  A )  ->  d  e.  RR )
491490adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
d  e.  RR )
4924913adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  d  e.  RR )
493450, 492, 451ltled 9790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  <_  d )
494450, 492, 493abssubge0d 13493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  ( abs `  ( d  -  c ) )  =  ( d  -  c
) )
495489, 494eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
d  -  c ) )
496 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  =  <. d ,  c
>.  ->  ( ( D  |`  I ) `  x
)  =  ( ( D  |`  I ) `  <. d ,  c
>. ) )
497496eqeq1d 2424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  <. d ,  c
>.  ->  ( ( ( D  |`  I ) `  x )  =  ( d  -  c )  <-> 
( ( D  |`  I ) `  <. d ,  c >. )  =  ( d  -  c ) ) )
498497rspcev 3182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
<. d ,  c >.  e.  I  /\  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
d  -  c ) )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) )
499460, 495, 498syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) )
500491, 449resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
( d  -  c
)  e.  RR )
501 elex 3089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( d  -  c )  e.  RR  ->  (
d  -  c )  e.  _V )
502500, 501syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
( d  -  c
)  e.  _V )
5035023adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  _V )
504 simp1 1005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  ph )
505 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  =  ( d  -  c )  ->  (
y  e.  ran  ( D  |`  I )  <->  ( d  -  c )  e. 
ran  ( D  |`  I ) ) )
506 eqeq2 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( y  =  ( d  -  c )  ->  (
( ( D  |`  I ) `  x
)  =  y  <->  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) )
507506rexbidv 2936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  =  ( d  -  c )  ->  ( E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) )
508505, 507bibi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  ( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y ) )
511509, 510vtoclg 3139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( d  -  c )  e.  _V  ->  ( ph  ->  ( ( d  -  c )  e. 
ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) ) )
512503, 504, 511sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  ran  ( D  |`  I ) )
514513, 34syl6eleqr 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  R )
515 infmrlbOLD 10604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  sup ( R ,  RR ,  `'  <  )  <_  (
d  -  c ) )
51733, 516syl5eqbr 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E  <_  ( d  -  c
) )
518419, 517vtoclg 3139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( B  e.  A  ->  (
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  E  <_  (
d  -  B ) ) )
519412, 518mpcom 37 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  E  <_  ( d  -  B
) )
520411, 519vtoclg 3139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( C  e.  A  ->  (
( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C )  ->  E  <_  ( C  -  B )
) )
521146, 404, 520sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  E  <_  ( C  -  B ) )
522521, 280syl6breqr 4464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  E  <_  T )
523269, 522syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  E  <_  T )
5245233ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  T )
525524ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ps  /\  k  e.  ZZ )  ->  b  e.  CC )
527526, 368pncan2d 9995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( b  +  ( k  x.  T ) )  -  b )  =  ( k  x.  T ) )
528527oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( ( b  +  ( k  x.  T
) )  -  b
)  /  T )  =  ( ( k  x.  T )  /  T ) )
529342adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  e.  CC )
530320adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  e.  CC )
531421a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  0  e.  RR )
532531, 352gtned 9777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  T  =/=  0 )
533269, 532syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ps 
->  T  =/=  0
)
534533adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  =/=  0 )
535529, 530, 534divcan4d 10396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( k  x.  T
)  /  T )  =  k )
536528, 535eqtr2d 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
537536adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
538537adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T
) )  ->  (
( a  +  ( j  x.  T ) )  -  b )  =  ( ( b  +  ( k  x.  T ) )  -  b ) )
540539oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T
) )  ->  (
( ( a  +  ( j