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

Theorem fourierdlem42 37799
Description: The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
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  = inf ( 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 21820 . . . . 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 fourierdlem42.h . . . . . 6  |-  H  =  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  A }
9 ssrab2 3543 . . . . . . 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 3505 . . . . 5  |-  ( ph  ->  H  C_  ( X [,] Y ) )
12 retop 21759 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  e.  Top
133, 12eqeltri 2504 . . . . . . 7  |-  J  e. 
Top
141, 2iccssred 37402 . . . . . . 7  |-  ( ph  ->  ( X [,] Y
)  C_  RR )
15 uniretop 21760 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
163unieqi 4222 . . . . . . . . 9  |-  U. J  =  U. ( topGen `  ran  (,) )
1715, 16eqtr4i 2452 . . . . . . . 8  |-  RR  =  U. J
1817restuni 20155 . . . . . . 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 4222 . . . . . . 7  |-  U. K  =  U. ( Jt  ( X [,] Y ) )
2120eqcomi 2433 . . . . . 6  |-  U. ( Jt  ( X [,] Y ) )  =  U. K
2219, 21syl6eq 2477 . . . . 5  |-  ( ph  ->  ( X [,] Y
)  =  U. K
)
2311, 22sseqtrd 3497 . . . 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 2420 . . . 4  |-  U. K  =  U. K
2726bwth 20402 . . 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 3471 . . . . . . . . . 10  |-  ( ph  ->  H  C_  RR )
3029ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  H  C_  RR )
31 ne0i 3764 . . . . . . . . . 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 fourierdlem42.e . . . . . . . . . . 11  |-  E  = inf ( R ,  RR ,  <  )
34 fourierdlem42.r . . . . . . . . . . . . 13  |-  R  =  ran  ( D  |`  I )
35 absf 13379 . . . . . . . . . . . . . . . . . 18  |-  abs : CC
--> RR
36 ffn 5738 . . . . . . . . . . . . . . . . . 18  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
3735, 36ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  abs  Fn  CC
38 subf 9873 . . . . . . . . . . . . . . . . . 18  |-  -  :
( CC  X.  CC )
--> CC
39 ffn 5738 . . . . . . . . . . . . . . . . . 18  |-  (  -  : ( CC  X.  CC ) --> CC  ->  -  Fn  ( CC  X.  CC ) )
4038, 39ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  -  Fn  ( CC  X.  CC )
41 frn 5744 . . . . . . . . . . . . . . . . . 18  |-  (  -  : ( CC  X.  CC ) --> CC  ->  ran  - 
C_  CC )
4238, 41ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ran  -  C_  CC
43 fnco 5694 . . . . . . . . . . . . . . . . 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 fourierdlem42.d . . . . . . . . . . . . . . . . 17  |-  D  =  ( abs  o.  -  )
4645fneq1i 5680 . . . . . . . . . . . . . . . 16  |-  ( D  Fn  ( CC  X.  CC )  <->  ( abs  o.  -  )  Fn  ( CC  X.  CC ) )
4744, 46mpbir 212 . . . . . . . . . . . . . . 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 37402 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( B [,] C
)  C_  RR )
53 ax-resscn 9592 . . . . . . . . . . . . . . . . . . . 20  |-  RR  C_  CC
5452, 53syl6ss 3473 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( B [,] C
)  C_  CC )
5549, 54sstrd 3471 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  C_  CC )
56 xpss12 4952 . . . . . . . . . . . . . . . . . 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 3600 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  X.  A )  \  _I  )  C_  ( CC  X.  CC ) )
5948, 58syl5eqss 3505 . . . . . . . . . . . . . . 15  |-  ( ph  ->  I  C_  ( CC  X.  CC ) )
60 fnssres 5699 . . . . . . . . . . . . . . 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 5887 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  I  ->  (
( D  |`  I ) `
 x )  =  ( D `  x
) )
6362adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  =  ( D `  x
) )
6445fveq1i 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( D `
 x )  =  ( ( abs  o.  -  ) `  x
)
6564a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  ( D `  x )  =  ( ( abs 
o.  -  ) `  x ) )
66 ffun 5740 . . . . . . . . . . . . . . . . . . . 20  |-  (  -  : ( CC  X.  CC ) --> CC  ->  Fun  -  )
6738, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  Fun  -
6859sselda 3461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  ( CC  X.  CC ) )
6938fdmi 5743 . . . . . . . . . . . . . . . . . . . 20  |-  dom  -  =  ( CC  X.  CC )
7068, 69syl6eleqr 2519 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  dom  -  )
71 fvco 5949 . . . . . . . . . . . . . . . . . . 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 2465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  =  ( abs `  (  -  `  x ) ) )
7438a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  I )  ->  -  :
( CC  X.  CC )
--> CC )
7574, 68ffvelrnd 6030 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  (  -  `  x )  e.  CC )
7675abscld 13476 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  ( abs `  (  -  `  x ) )  e.  RR )
7773, 76eqeltrd 2508 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  e.  RR )
78 elxp2 4864 . . . . . . . . . . . . . . . . . . . 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 5873 . . . . . . . . . . . . . . . . . . . . . . 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 6300 . . . . . . . . . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( <.
y ,  z >.  e.  I  <->  <. y ,  z
>.  e.  ( ( A  X.  A )  \  _I  ) )
91 eldif 3443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  e.  CC )
9996simprd 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  z  e.  A )
10089, 99sseldd 3462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  z  e.  CC )
10192simprd 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
y ,  z >.  e.  I  ->  -.  <. y ,  z >.  e.  _I  )
102 df-br 4418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  _I  z  <->  <. y ,  z >.  e.  _I  )
103101, 102sylnibr 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
y ,  z >.  e.  I  ->  -.  y  _I  z )
104 vex 3081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  z  e. 
_V
105104ideq 4999 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  _I  z  <->  y  =  z )
106103, 105sylnib 305 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( <.
y ,  z >.  e.  I  ->  -.  y  =  z )
107106neqned 2625 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
y ,  z >.  e.  I  ->  y  =/=  z )
108107adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  <. y ,  z >.  e.  I
)  ->  y  =/=  z )
10998, 100, 108subne0d 9991 . . . . . . . . . . . . . . . . . . . . . . . 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 2723 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  I )  /\  (
y  e.  CC  /\  z  e.  CC )  /\  x  =  <. y ,  z >. )  ->  (  -  `  <. y ,  z >. )  =/=  0 )
11281, 111eqnetrd 2715 . . . . . . . . . . . . . . . . . . . . 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 2921 . . . . . . . . . . . . . . . . . . 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 13366 . . . . . . . . . . . . . . . . . . 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 2428 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  I )  ->  ( abs `  (  -  `  x ) )  =  ( ( D  |`  I ) `  x
) )
120118, 119breqtrd 4442 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  0  <  ( ( D  |`  I ) `  x
) )
12177, 120elrpd 11334 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  (
( D  |`  I ) `
 x )  e.  RR+ )
122121ralrimiva 2837 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  I 
( ( D  |`  I ) `  x
)  e.  RR+ )
123 fnfvrnss 6058 . . . . . . . . . . . . . 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 3505 . . . . . . . . . . . 12  |-  ( ph  ->  R  C_  RR+ )
126 ltso 9710 . . . . . . . . . . . . . 14  |-  <  Or  RR
127126a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  <  Or  RR )
128 fourierdlem42.af . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  Fin )
129 xpfi 7840 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  Fin  /\  A  e.  Fin )  ->  ( A  X.  A
)  e.  Fin )
130128, 128, 129syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A  X.  A
)  e.  Fin )
131 diffi 7801 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  X.  A )  e.  Fin  ->  (
( A  X.  A
)  \  _I  )  e.  Fin )
132130, 131syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( A  X.  A )  \  _I  )  e.  Fin )
13348, 132syl5eqel 2512 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  I  e.  Fin )
134 fnfi 7847 . . . . . . . . . . . . . . . 16  |-  ( ( ( D  |`  I )  Fn  I  /\  I  e.  Fin )  ->  ( D  |`  I )  e. 
Fin )
13561, 133, 134syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  |`  I )  e.  Fin )
136 rnfi 7855 . . . . . . . . . . . . . . 15  |-  ( ( D  |`  I )  e.  Fin  ->  ran  ( D  |`  I )  e.  Fin )
137135, 136syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  ( D  |`  I )  e.  Fin )
13834, 137syl5eqel 2512 . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  Fin )
13934a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  =  ran  ( D  |`  I ) )
14045a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  D  =  ( abs 
o.  -  ) )
141140reseq1d 5116 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  |`  I )  =  ( ( abs 
o.  -  )  |`  I ) )
142141fveq1d 5875 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  |`  I ) `  <. B ,  C >. )  =  ( ( ( abs  o.  -  )  |`  I ) `  <. B ,  C >. )
)
143 fourierdlem42.ba . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  A )
144 fourierdlem42.ca . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  A )
145 opelxp 4876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( <. B ,  C >.  e.  ( A  X.  A
)  <->  ( B  e.  A  /\  C  e.  A ) )
146143, 144, 145sylanbrc 668 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
<. B ,  C >.  e.  ( A  X.  A
) )
147 fourierdlem42.bc . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  <  C )
14850, 147ltned 9767 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  =/=  C )
149148neneqd 2623 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  B  =  C )
150 ideqg 4998 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( C  e.  A  ->  ( B  _I  C  <->  B  =  C ) )
151144, 150syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( B  _I  C  <->  B  =  C ) )
152149, 151mtbird 302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  B  _I  C
)
153 df-br 4418 . . . . . . . . . . . . . . . . . . . . 21  |-  ( B  _I  C  <->  <. B ,  C >.  e.  _I  )
154152, 153sylnib 305 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  <. B ,  C >.  e.  _I  )
155146, 154eldifd 3444 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
<. B ,  C >.  e.  ( ( A  X.  A )  \  _I  ) )
156155, 48syl6eleqr 2519 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
<. B ,  C >.  e.  I )
157 fvres 5887 . . . . . . . . . . . . . . . . . 18  |-  ( <. B ,  C >.  e.  I  ->  ( (
( abs  o.  -  )  |`  I ) `  <. B ,  C >. )  =  ( ( abs 
o.  -  ) `  <. B ,  C >. ) )
158156, 157syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( abs 
o.  -  )  |`  I ) `
 <. B ,  C >. )  =  ( ( abs  o.  -  ) `  <. B ,  C >. ) )
15950recnd 9665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  CC )
16051recnd 9665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  CC )
161 opelxp 4876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( <. B ,  C >.  e.  ( CC  X.  CC ) 
<->  ( B  e.  CC  /\  C  e.  CC ) )
162159, 160, 161sylanbrc 668 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
<. B ,  C >.  e.  ( CC  X.  CC ) )
163162, 69syl6eleqr 2519 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
<. B ,  C >.  e. 
dom  -  )
164 fvco 5949 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  -  /\  <. B ,  C >.  e.  dom  -  )  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  (  -  `  <. B ,  C >. ) ) )
16567, 163, 164sylancr 667 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  (  -  `  <. B ,  C >. ) ) )
166 df-ov 6300 . . . . . . . . . . . . . . . . . . . . 21  |-  ( B  -  C )  =  (  -  `  <. B ,  C >. )
167166eqcomi 2433 . . . . . . . . . . . . . . . . . . . 20  |-  (  -  ` 
<. B ,  C >. )  =  ( B  -  C )
168167a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  (  -  `  <. B ,  C >. )  =  ( B  -  C ) )
169168fveq2d 5877 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  (  -  `  <. B ,  C >. ) )  =  ( abs `  ( B  -  C ) ) )
170165, 169eqtrd 2461 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs  o.  -  ) `  <. B ,  C >. )  =  ( abs `  ( B  -  C )
) )
171142, 158, 1703eqtrrd 2466 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( abs `  ( B  -  C )
)  =  ( ( D  |`  I ) `  <. B ,  C >. ) )
172 fnfvelrn 6026 . . . . . . . . . . . . . . . . 17  |-  ( ( ( D  |`  I )  Fn  I  /\  <. B ,  C >.  e.  I
)  ->  ( ( D  |`  I ) `  <. B ,  C >. )  e.  ran  ( D  |`  I ) )
17361, 156, 172syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  |`  I ) `  <. B ,  C >. )  e.  ran  ( D  |`  I ) )
174171, 173eqeltrd 2508 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( abs `  ( B  -  C )
)  e.  ran  ( D  |`  I ) )
175 ne0i 3764 . . . . . . . . . . . . . . 15  |-  ( ( abs `  ( B  -  C ) )  e.  ran  ( D  |`  I )  ->  ran  ( D  |`  I )  =/=  (/) )
176174, 175syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  ( D  |`  I )  =/=  (/) )
177139, 176eqnetrd 2715 . . . . . . . . . . . . 13  |-  ( ph  ->  R  =/=  (/) )
178 resss 5140 . . . . . . . . . . . . . . . . 17  |-  ( D  |`  I )  C_  D
179 rnss 5075 . . . . . . . . . . . . . . . . 17  |-  ( ( D  |`  I )  C_  D  ->  ran  ( D  |`  I )  C_  ran  D )
180178, 179ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ran  ( D  |`  I )  C_  ran  D
18145rneqi 5073 . . . . . . . . . . . . . . . . 17  |-  ran  D  =  ran  ( abs  o.  -  )
182 rncoss 5107 . . . . . . . . . . . . . . . . . 18  |-  ran  ( abs  o.  -  )  C_  ran  abs
183 frn 5744 . . . . . . . . . . . . . . . . . . 19  |-  ( abs
: CC --> RR  ->  ran 
abs  C_  RR )
18435, 183ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ran  abs  C_  RR
185182, 184sstri 3470 . . . . . . . . . . . . . . . . 17  |-  ran  ( abs  o.  -  )  C_  RR
186181, 185eqsstri 3491 . . . . . . . . . . . . . . . 16  |-  ran  D  C_  RR
187180, 186sstri 3470 . . . . . . . . . . . . . . 15  |-  ran  ( D  |`  I )  C_  RR
18834, 187eqsstri 3491 . . . . . . . . . . . . . 14  |-  R  C_  RR
189188a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  R  C_  RR )
190 fiinfcl 8015 . . . . . . . . . . . . 13  |-  ( (  <  Or  RR  /\  ( R  e.  Fin  /\  R  =/=  (/)  /\  R  C_  RR ) )  -> inf ( R ,  RR ,  <  )  e.  R )
191127, 138, 177, 189, 190syl13anc 1266 . . . . . . . . . . . 12  |-  ( ph  -> inf ( R ,  RR ,  <  )  e.  R
)
192125, 191sseldd 3462 . . . . . . . . . . 11  |-  ( ph  -> inf ( R ,  RR ,  <  )  e.  RR+ )
19333, 192syl5eqel 2512 . . . . . . . . . 10  |-  ( ph  ->  E  e.  RR+ )
194193ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  U. K )  /\  x  e.  ( ( limPt `  J ) `  H ) )  ->  E  e.  RR+ )
1953, 30, 32, 194lptre2pt 37507 . . . . . . . 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 ) )
196 simpll 758 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  ph )
19729sselda 3461 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  H )  ->  y  e.  RR )
198197adantrr 721 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  H  /\  z  e.  H ) )  -> 
y  e.  RR )
199198adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  y  e.  RR )
20029sselda 3461 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  H )  ->  z  e.  RR )
201200adantrl 720 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  H  /\  z  e.  H ) )  -> 
z  e.  RR )
202201adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  z  e.  RR )
203 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  y  =/=  z )
204199, 202, 2033jca 1185 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
y  e.  H  /\  z  e.  H )
)  /\  y  =/=  z )  ->  (
y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )
2058eleq2i 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  H  <->  y  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A }
)
206 oveq1 6304 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x  +  ( k  x.  T ) )  =  ( y  +  ( k  x.  T
) ) )
207206eleq1d 2489 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( x  +  ( k  x.  T ) )  e.  A  <->  ( y  +  ( k  x.  T ) )  e.  A ) )
208207rexbidv 2937 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  A
) )
209 oveq1 6304 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
210209oveq2d 6313 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  j  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
211210eleq1d 2489 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
( y  +  ( k  x.  T ) )  e.  A  <->  ( y  +  ( j  x.  T ) )  e.  A ) )
212211cbvrexv 3054 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  A  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
)
213208, 212syl6bb 264 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
) )
214213elrab 3226 . . . . . . . . . . . . . . . . . . 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
) )
215205, 214sylbb 200 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  H  ->  (
y  e.  ( X [,] Y )  /\  E. j  e.  ZZ  (
y  +  ( j  x.  T ) )  e.  A ) )
216215simprd 464 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  H  ->  E. j  e.  ZZ  ( y  +  ( j  x.  T
) )  e.  A
)
217216adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. j  e.  ZZ  ( y  +  ( j  x.  T ) )  e.  A )
2188eleq2i 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  H  <->  z  e.  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A }
)
219 oveq1 6304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
x  +  ( k  x.  T ) )  =  ( z  +  ( k  x.  T
) ) )
220219eleq1d 2489 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( x  +  ( k  x.  T ) )  e.  A  <->  ( z  +  ( k  x.  T ) )  e.  A ) )
221220rexbidv 2937 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  A  <->  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
) )
222221elrab 3226 . . . . . . . . . . . . . . . . . . 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
) )
223218, 222sylbb 200 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  H  ->  (
z  e.  ( X [,] Y )  /\  E. k  e.  ZZ  (
z  +  ( k  x.  T ) )  e.  A ) )
224223simprd 464 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  H  ->  E. k  e.  ZZ  ( z  +  ( k  x.  T
) )  e.  A
)
225224adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  H  /\  z  e.  H )  ->  E. k  e.  ZZ  ( z  +  ( k  x.  T ) )  e.  A )
226 reeanv 2994 . . . . . . . . . . . . . . . 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 ) )
227217, 225, 226sylanbrc 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 ) )
228227ad2antlr 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 ) )
229 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 )
230 simpl1 1008 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
y  e.  RR )
231 simpl2 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
z  e.  RR )
232 simpr 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
y  <  z )
233230, 231, 2323jca 1185 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  RR  /\  z  e.  RR  /\  y  =/=  z )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
234233adantll 718 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
y  e.  RR  /\  z  e.  RR  /\  y  =/=  z ) )  /\  y  <  z )  -> 
( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) )
235234adantlr 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 ) )
236 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 ) )
237 eleq1 2492 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
b  e.  RR  <->  z  e.  RR ) )
238 breq2 4421 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
y  <  b  <->  y  <  z ) )
239237, 2383anbi23d 1338 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  (
( y  e.  RR  /\  b  e.  RR  /\  y  <  b )  <->  ( y  e.  RR  /\  z  e.  RR  /\  y  < 
z ) ) )
240239anbi2d 708 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  z  ->  (
( ph  /\  (
y  e.  RR  /\  b  e.  RR  /\  y  <  b ) )  <->  ( ph  /\  ( y  e.  RR  /\  z  e.  RR  /\  y  <  z ) ) ) )
241 oveq1 6304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  z  ->  (
b  +  ( k  x.  T ) )  =  ( z  +  ( k  x.  T
) ) )
242241eleq1d 2489 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  z  ->  (
( b  +  ( k  x.  T ) )  e.  A  <->  ( z  +  ( k  x.  T ) )  e.  A ) )
243242anbi2d 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 ) ) )
2442432rexbidv 2944 . . . . . . . . . . . . . . . . . . 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 ) ) )
245240, 244anbi12d 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 ) ) ) )
246 oveq2 6305 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  z  ->  (
y  -  b )  =  ( y  -  z ) )
247246fveq2d 5877 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  z  ->  ( abs `  ( y  -  b ) )  =  ( abs `  (
y  -  z ) ) )
248247breq2d 4429 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  z  ->  ( E  <_  ( abs `  (
y  -  b ) )  <->  E  <_  ( abs `  ( y  -  z
) ) ) )
249245, 248imbi12d 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 ) ) ) ) )
250 eleq1 2492 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
a  e.  RR  <->  y  e.  RR ) )
251 breq1 4420 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
a  <  b  <->  y  <  b ) )
252250, 2513anbi13d 1337 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  (
( a  e.  RR  /\  b  e.  RR  /\  a  <  b )  <->  ( y  e.  RR  /\  b  e.  RR  /\  y  < 
b ) ) )
253252anbi2d 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  y  ->  (
( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )  <->  ( ph  /\  ( y  e.  RR  /\  b  e.  RR  /\  y  <  b ) ) ) )
254 oveq1 6304 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  y  ->  (
a  +  ( j  x.  T ) )  =  ( y  +  ( j  x.  T
) ) )
255254eleq1d 2489 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  y  ->  (
( a  +  ( j  x.  T ) )  e.  A  <->  ( y  +  ( j  x.  T ) )  e.  A ) )
256255anbi1d 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 ) ) )
2572562rexbidv 2944 . . . . . . . . . . . . . . . . . . . 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 ) ) )
258253, 257anbi12d 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 ) ) ) )
259 oveq1 6304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  y  ->  (
a  -  b )  =  ( y  -  b ) )
260259fveq2d 5877 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  y  ->  ( abs `  ( a  -  b ) )  =  ( abs `  (
y  -  b ) ) )
261260breq2d 4429 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  y  ->  ( E  <_  ( abs `  (
a  -  b ) )  <->  E  <_  ( abs `  ( y  -  b
) ) ) )
262258, 261imbi12d 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 ) ) ) ) )
263 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 ) ) )
264263simprbi 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ps 
->  E. j  e.  ZZ  E. k  e.  ZZ  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )
265263biimpi 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 ) ) )
266265simpld 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  ( ph  /\  (
a  e.  RR  /\  b  e.  RR  /\  a  <  b ) ) )
267266simpld 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  ph )
268267, 50syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  B  e.  RR )
269268adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  B  e.  RR )
270267, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  C  e.  RR )
271270adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  C  e.  RR )
272267, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  A  C_  ( B [,] C ) )
273272sselda 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( b  +  ( k  x.  T ) )  e.  A )  ->  (
b  +  ( k  x.  T ) )  e.  ( B [,] C ) )
274273adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( b  +  ( k  x.  T
) )  e.  ( B [,] C ) )
275272sselda 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( a  +  ( j  x.  T ) )  e.  A )  ->  (
a  +  ( j  x.  T ) )  e.  ( B [,] C ) )
276275adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( a  +  ( j  x.  T
) )  e.  ( B [,] C ) )
277269, 271, 274, 276iccsuble 37420 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  ( C  -  B )
)
278 fourierdlem42.t . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  T  =  ( C  -  B
)
279277, 278syl6breqr 4458 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ps  /\  ( ( a  +  ( j  x.  T ) )  e.  A  /\  (
b  +  ( k  x.  T ) )  e.  A ) )  ->  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T
)
2802793adant2 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 )
281280adantr 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 )
282 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  -.  k  <_  j )
283 zre 10937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ZZ  ->  j  e.  RR )
284283adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  j  e.  RR )
285284ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  j  e.  RR )
286 zre 10937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ZZ  ->  k  e.  RR )
287286adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  k  e.  RR )
288287ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  k  e.  RR )
289285, 288ltnled 9778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  (
j  <  k  <->  -.  k  <_  j ) )
290282, 289mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  j  <  k )
29151, 50resubcld 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( C  -  B
)  e.  RR )
292278, 291syl5eqel 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  T  e.  RR )
293267, 292syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ps 
->  T  e.  RR )
294293ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  e.  RR )
295287adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  e.  RR )
296284adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
j  e.  RR )
297295, 296resubcld 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  -  j
)  e.  RR )
298293adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  ->  T  e.  RR )
299297, 298remulcld 9667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  e.  RR )
300299adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
k  -  j )  x.  T )  e.  RR )
301266simprd 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) )
302301simp2d 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  b  e.  RR )
303302adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
b  e.  RR )
304286adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  e.  RR )
305293adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  e.  RR )
306304, 305remulcld 9667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  RR )
307306adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  x.  T
)  e.  RR )
308303, 307readdcld 9666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( b  +  ( k  x.  T ) )  e.  RR )
309301simp1d 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  a  e.  RR )
310309adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
a  e.  RR )
311283adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  j  e.  RR )
312293adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  T  e.  RR )
313311, 312remulcld 9667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  j  e.  ZZ )  ->  (
j  x.  T )  e.  RR )
314313adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  x.  T
)  e.  RR )
315310, 314readdcld 9666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( a  +  ( j  x.  T ) )  e.  RR )
316308, 315resubcld 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  e.  RR )
317316adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) )  e.  RR )
318293recnd 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  T  e.  CC )
319318mulid2d 9657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  ( 1  x.  T
)  =  T )
320319eqcomd 2428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ps 
->  T  =  (
1  x.  T ) )
321320ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  =  ( 1  x.  T
) )
322 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  <  k )
323 zltlem1 10985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  <  k  <->  j  <_  ( k  - 
1 ) ) )
324323ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( j  <  k  <->  j  <_  (
k  -  1 ) ) )
325322, 324mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  j  <_  ( k  -  1 ) )
326284ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  j  e.  RR )
327 peano2rem 9937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  RR  ->  (
k  -  1 )  e.  RR )
328295, 327syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  -  1 )  e.  RR )
329328adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( k  -  1 )  e.  RR )
330 1re 9638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  1  e.  RR
331 resubcl 9934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 1  e.  RR  /\  j  e.  RR )  ->  ( 1  -  j
)  e.  RR )
332330, 326, 331sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( 1  -  j )  e.  RR )
333 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  j  <_  ( k  -  1 ) )
334326, 329, 332, 333leadd1dd 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  +  ( 1  -  j ) )  <_ 
( ( k  - 
1 )  +  ( 1  -  j ) ) )
335 zcn 10938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  ZZ  ->  j  e.  CC )
336335adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  j  e.  CC )
337 1cnd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  1  e.  CC )
338336, 337pncan3d 9985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  +  ( 1  -  j ) )  =  1 )
339338ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( j  +  ( 1  -  j ) )  =  1 )
340 zcn 10938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  ZZ  ->  k  e.  CC )
341340adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  k  e.  CC )
342341, 337, 336npncand 10006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( ( k  - 
1 )  +  ( 1  -  j ) )  =  ( k  -  j ) )
343342ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  ( (
k  -  1 )  +  ( 1  -  j ) )  =  ( k  -  j
) )
344334, 339, 3433brtr3d 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <_  ( k  -  1 ) )  ->  1  <_  ( k  -  j ) )
345325, 344syldan 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  1  <_  ( k  -  j ) )
346330a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  1  e.  RR )
347297adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( k  -  j )  e.  RR )
34850, 51posdifd 10196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( B  <  C  <->  0  <  ( C  -  B ) ) )
349147, 348mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  0  <  ( C  -  B ) )
350349, 278syl6breqr 4458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  0  <  T )
351292, 350elrpd 11334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  T  e.  RR+ )
352267, 351syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  T  e.  RR+ )
353352ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  e.  RR+ )
354346, 347, 353lemul1d 11377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( 1  <_  ( k  -  j )  <->  ( 1  x.  T )  <_ 
( ( k  -  j )  x.  T
) ) )
355345, 354mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( 1  x.  T )  <_ 
( ( k  -  j )  x.  T
) )
356321, 355eqbrtrd 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  <_  ( ( k  -  j
)  x.  T ) )
357302, 309resubcld 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  ( b  -  a
)  e.  RR )
358301simp3d 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ps 
->  a  <  b )
359309, 302posdifd 10196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ps 
->  ( a  <  b  <->  0  <  ( b  -  a ) ) )
360358, 359mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  0  <  ( b  -  a ) )
361357, 360elrpd 11334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ps 
->  ( b  -  a
)  e.  RR+ )
362361adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( b  -  a
)  e.  RR+ )
363299, 362ltaddrp2d 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  <  ( (
b  -  a )  +  ( ( k  -  j )  x.  T ) ) )
364302recnd 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  b  e.  CC )
365364adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
b  e.  CC )
366306recnd 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  CC )
367366adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( k  x.  T
)  e.  CC )
368309recnd 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ps 
->  a  e.  CC )
369368adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
a  e.  CC )
370313recnd 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  j  e.  ZZ )  ->  (
j  x.  T )  e.  CC )
371370adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  x.  T
)  e.  CC )
372365, 367, 369, 371addsub4d 10029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  =  ( ( b  -  a )  +  ( ( k  x.  T )  -  ( j  x.  T
) ) ) )
373340ad2antll 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  e.  CC )
374335ad2antrl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
j  e.  CC )
375318adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  ->  T  e.  CC )
376373, 374, 375subdird 10071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  =  ( ( k  x.  T )  -  ( j  x.  T ) ) )
377376eqcomd 2428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  x.  T )  -  (
j  x.  T ) )  =  ( ( k  -  j )  x.  T ) )
378377oveq2d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  -  a )  +  ( ( k  x.  T
)  -  ( j  x.  T ) ) )  =  ( ( b  -  a )  +  ( ( k  -  j )  x.  T ) ) )
379372, 378eqtr2d 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( b  -  a )  +  ( ( k  -  j
)  x.  T ) )  =  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) ) )
380363, 379breqtrd 4442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( k  -  j )  x.  T
)  <  ( (
b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T
) ) ) )
381380adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  ( (
k  -  j )  x.  T )  < 
( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) ) )
382294, 300, 317, 356, 381lelttrd 9789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  T  <  ( ( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) ) )
383294, 317ltnled 9778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
384382, 383mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  j  <  k )  ->  -.  (
( b  +  ( k  x.  T ) )  -  ( a  +  ( j  x.  T ) ) )  <_  T )
385290, 384syldan 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  -.  k  <_  j )  ->  -.  ( ( b  +  ( k  x.  T
) )  -  (
a  +  ( j  x.  T ) ) )  <_  T )
3863853adantl3 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 )
387281, 386condan 801 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  k  <_  j )
388188, 191sseldi 3459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  -> inf ( R ,  RR ,  <  )  e.  RR )
38933, 388syl5eqel 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  E  e.  RR )
390267, 389syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  E  e.  RR )
3913903ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  e.  RR )
392391ad2antrr 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 )
3932933ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  T  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 ) ) )  ->  T  e.  RR )
395284, 287resubcld 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( j  e.  ZZ  /\  k  e.  ZZ )  ->  ( j  -  k
)  e.  RR )
396395adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( j  -  k
)  e.  RR )
397396, 298remulcld 9667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
( ( j  -  k )  x.  T
)  e.  RR )
3983973adant3 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 )
399398ad2antrr 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 )
400 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ph )
401143, 144jca 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( B  e.  A  /\  C  e.  A
) )
402400, 401, 1473jca 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C ) )
403 eleq1 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( d  =  C  ->  (
d  e.  A  <->  C  e.  A ) )
404403anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  (
( B  e.  A  /\  d  e.  A
)  <->  ( B  e.  A  /\  C  e.  A ) ) )
405 breq2 4421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  ( B  <  d  <->  B  <  C ) )
406404, 4053anbi23d 1338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( d  =  C  ->  (
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  <-> 
( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C ) ) )
407 oveq1 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  =  C  ->  (
d  -  B )  =  ( C  -  B ) )
408407breq2d 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( d  =  C  ->  ( E  <_  ( d  -  B )  <->  E  <_  ( C  -  B ) ) )
409406, 408imbi12d 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 ) ) ) )
410 simp2l 1031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  B  e.  A )
411 eleq1 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( c  =  B  ->  (
c  e.  A  <->  B  e.  A ) )
412411anbi1d 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
( c  e.  A  /\  d  e.  A
)  <->  ( B  e.  A  /\  d  e.  A ) ) )
413 breq1 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
c  <  d  <->  B  <  d ) )
414412, 4133anbi23d 1338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  =  B  ->  (
( ph  /\  (
c  e.  A  /\  d  e.  A )  /\  c  <  d )  <-> 
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d ) ) )
415 oveq2 6305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  =  B  ->  (
d  -  c )  =  ( d  -  B ) )
416415breq2d 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  =  B  ->  ( E  <_  ( d  -  c )  <->  E  <_  ( d  -  B ) ) )
417414, 416imbi12d 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 ) ) ) )
418188a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  R  C_  RR )
419 0re 9639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  0  e.  RR
42034eleq2i 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( y  e.  R  <->  y  e.  ran  ( D  |`  I ) )
421420biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  e.  R  ->  y  e.  ran  ( D  |`  I ) )
422421adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  y  e.  ran  ( D  |`  I ) )
42361adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  y  e.  R )  ->  ( D  |`  I )  Fn  I )
424 fvelrnb 5920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( D  |`  I )  Fn  I  ->  ( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )
425423, 424syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  (
y  e.  ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y ) )
426422, 425mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  y  e.  R )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  y )
427121rpge0d 11341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  x  e.  I )  ->  0  <_  ( ( D  |`  I ) `  x
) )
4284273adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  0  <_  (
( D  |`  I ) `
 x ) )
429 simp3 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  ( ( D  |`  I ) `  x
)  =  y )
430428, 429breqtrd 4442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  x  e.  I  /\  ( ( D  |`  I ) `  x
)  =  y )  ->  0  <_  y
)
4314303exp 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ph  ->  ( x  e.  I  ->  ( ( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
) )
432431adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  y  e.  R )  ->  (
x  e.  I  -> 
( ( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
) )
433432rexlimdv 2913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  y  e.  R )  ->  ( E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y  -> 
0  <_  y )
)
434426, 433mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  y  e.  R )  ->  0  <_  y )
435434ralrimiva 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  A. y  e.  R 
0  <_  y )
436 breq1 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
437436ralbidv 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  =  0  ->  ( A. y  e.  R  x  <_  y  <->  A. y  e.  R  0  <_  y ) )
438437rspcev 3179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( 0  e.  RR  /\  A. y  e.  R  0  <_  y )  ->  E. x  e.  RR  A. y  e.  R  x  <_  y )
439419, 435, 438sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  E. x  e.  RR  A. y  e.  R  x  <_  y )
4404393ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E. x  e.  RR  A. y  e.  R  x  <_  y
)
441 pm3.22 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( c  e.  A  /\  d  e.  A )  ->  ( d  e.  A  /\  c  e.  A
) )
442 opelxp 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( <.
d ,  c >.  e.  ( A  X.  A
)  <->  ( d  e.  A  /\  c  e.  A ) )
443441, 442sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( c  e.  A  /\  d  e.  A )  -> 
<. d ,  c >.  e.  ( A  X.  A
) )
4444433ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  ( A  X.  A ) )
44549, 52sstrd 3471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ph  ->  A  C_  RR )
446445sselda 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  c  e.  A )  ->  c  e.  RR )
447446adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
c  e.  RR )
4484473adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  e.  RR )
449 simp3 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  <  d )
450448, 449gtned 9766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  d  =/=  c )
451450neneqd 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  -.  d  =  c )
452 df-br 4418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( d  _I  c  <->  <. d ,  c >.  e.  _I  )
453 vex 3081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  c  e. 
_V
454453ideq 4999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( d  _I  c  <->  d  =  c )
455452, 454bitr3i 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( <.
d ,  c >.  e.  _I  <->  d  =  c )
456451, 455sylnibr 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  -.  <.
d ,  c >.  e.  _I  )
457444, 456eldifd 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  ( ( A  X.  A
)  \  _I  )
)
458457, 48syl6eleqr 2519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  <. d ,  c >.  e.  I
)
459448, 449ltned 9767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  =/=  d )
4601413ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ( D  |`  I )  =  ( ( abs  o.  -  )  |`  I ) )
461460fveq1d 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
( ( abs  o.  -  )  |`  I ) `
 <. d ,  c
>. ) )
4624433ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  ( A  X.  A ) )
463 necom 2691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( c  =/=  d  <->  d  =/=  c )
464463biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( c  =/=  d  ->  d  =/=  c )
465464neneqd 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( c  =/=  d  ->  -.  d  =  c )
4664653ad2ant3 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  -.  d  =  c )
467466, 455sylnibr 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  -.  <.
d ,  c >.  e.  _I  )
468462, 467eldifd 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  ( ( A  X.  A
)  \  _I  )
)
469468, 48syl6eleqr 2519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  I
)
470 fvres 5887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( <.
d ,  c >.  e.  I  ->  ( ( ( abs  o.  -  )  |`  I ) `  <. d ,  c >.
)  =  ( ( abs  o.  -  ) `  <. d ,  c
>. ) )
471469, 470syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( ( abs  o.  -  )  |`  I ) `
 <. d ,  c
>. )  =  (
( abs  o.  -  ) `  <. d ,  c
>. ) )
472 simp1 1005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ph )
473472, 469jca 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  ( ph  /\  <. d ,  c
>.  e.  I ) )
474 eleq1 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  =  <. d ,  c
>.  ->  ( x  e.  I  <->  <. d ,  c
>.  e.  I ) )
475474anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  <. d ,  c
>.  ->  ( ( ph  /\  x  e.  I )  <-> 
( ph  /\  <. d ,  c >.  e.  I
) ) )
476 eleq1 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( x  =  <. d ,  c
>.  ->  ( x  e. 
dom  -  <->  <. d ,  c
>.  e.  dom  -  )
)
477475, 476imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( x  =  <. d ,  c
>.  ->  ( ( (
ph  /\  x  e.  I )  ->  x  e.  dom  -  )  <->  ( ( ph  /\  <. d ,  c
>.  e.  I )  ->  <. d ,  c >.  e.  dom  -  ) ) )
478477, 70vtoclg 3136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( <.
d ,  c >.  e.  I  ->  ( (
ph  /\  <. d ,  c >.  e.  I
)  ->  <. d ,  c >.  e.  dom  -  ) )
479469, 473, 478sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  <. d ,  c >.  e.  dom  -  )
480 fvco 5949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( Fun  -  /\  <. d ,  c >.  e.  dom  -  )  ->  ( ( abs  o.  -  ) `  <. d ,  c >.
)  =  ( abs `  (  -  `  <. d ,  c >. )
) )
48167, 479, 480sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( abs  o.  -  ) `  <. d ,  c
>. )  =  ( abs `  (  -  `  <. d ,  c >.
) ) )
482 df-ov 6300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( d  -  c )  =  (  -  `  <. d ,  c >. )
483482eqcomi 2433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  (  -  ` 
<. d ,  c >.
)  =  ( d  -  c )
484483fveq2i 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( abs `  (  -  `  <. d ,  c >. )
)  =  ( abs `  ( d  -  c
) )
485481, 484syl6eq 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( abs  o.  -  ) `  <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
486461, 471, 4853eqtrd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  =/=  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
487459, 486syld3an3 1309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  ( abs `  ( d  -  c ) ) )
488445sselda 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  d  e.  A )  ->  d  e.  RR )
489488adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
d  e.  RR )
4904893adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  d  e.  RR )
491448, 490, 449ltled 9779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  c  <_  d )
492448, 490, 491abssubge0d 13472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  ( abs `  ( d  -  c ) )  =  ( d  -  c
) )
493487, 492eqtrd 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
d  -  c ) )
494 fveq2 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  =  <. d ,  c
>.  ->  ( ( D  |`  I ) `  x
)  =  ( ( D  |`  I ) `  <. d ,  c
>. ) )
495494eqeq1d 2422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  =  <. d ,  c
>.  ->  ( ( ( D  |`  I ) `  x )  =  ( d  -  c )  <-> 
( ( D  |`  I ) `  <. d ,  c >. )  =  ( d  -  c ) ) )
496495rspcev 3179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
<. d ,  c >.  e.  I  /\  (
( D  |`  I ) `
 <. d ,  c
>. )  =  (
d  -  c ) )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) )
497458, 493, 496syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) )
498489, 447resubcld 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
( d  -  c
)  e.  RR )
499 elex 3087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( d  -  c )  e.  RR  ->  (
d  -  c )  e.  _V )
500498, 499syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A ) )  -> 
( d  -  c
)  e.  _V )
5015003adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  _V )
502 simp1 1005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  ph )
503 eleq1 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  =  ( d  -  c )  ->  (
y  e.  ran  ( D  |`  I )  <->  ( d  -  c )  e. 
ran  ( D  |`  I ) ) )
504 eqeq2 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( y  =  ( d  -  c )  ->  (
( ( D  |`  I ) `  x
)  =  y  <->  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) )
505504rexbidv 2937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( y  =  ( d  -  c )  ->  ( E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) )
506503, 505bibi12d 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 ) ) ) )
507506imbi2d 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 ) ) ) ) )
50861, 424syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  ( y  e.  ran  ( D  |`  I )  <->  E. x  e.  I 
( ( D  |`  I ) `  x
)  =  y ) )
509507, 508vtoclg 3136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( d  -  c )  e.  _V  ->  ( ph  ->  ( ( d  -  c )  e. 
ran  ( D  |`  I )  <->  E. x  e.  I  ( ( D  |`  I ) `  x )  =  ( d  -  c ) ) ) )
510501, 502, 509sylc 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 ) ) )
511497, 510mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  ran  ( D  |`  I ) )
512511, 34syl6eleqr 2519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  (
d  -  c )  e.  R )
513 infrelb 10592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( R  C_  RR  /\  E. x  e.  RR  A. y  e.  R  x  <_  y  /\  ( d  -  c )  e.  R
)  -> inf ( R ,  RR ,  <  )  <_  ( d  -  c
) )
514418, 440, 512, 513syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  -> inf ( R ,  RR ,  <  )  <_  ( d  -  c ) )
51533, 514syl5eqbr 4451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( c  e.  A  /\  d  e.  A )  /\  c  <  d )  ->  E  <_  ( d  -  c
) )
516417, 515vtoclg 3136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( B  e.  A  ->  (
( ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  E  <_  (
d  -  B ) ) )
517410, 516mpcom 37 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( B  e.  A  /\  d  e.  A )  /\  B  <  d )  ->  E  <_  ( d  -  B
) )
518409, 517vtoclg 3136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( C  e.  A  ->  (
( ph  /\  ( B  e.  A  /\  C  e.  A )  /\  B  <  C )  ->  E  <_  ( C  -  B )
) )
519144, 402, 518sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  E  <_  ( C  -  B ) )
520519, 278syl6breqr 4458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  E  <_  T )
521267, 520syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ps 
->  E  <_  T )
5225213ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ )  /\  (
( a  +  ( j  x.  T ) )  e.  A  /\  ( b  +  ( k  x.  T ) )  e.  A ) )  ->  E  <_  T )
523522ad2antrr 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
)
524364adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ps  /\  k  e.  ZZ )  ->  b  e.  CC )
525524, 366pncan2d 9984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( b  +  ( k  x.  T ) )  -  b )  =  ( k  x.  T ) )
526525oveq1d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( ( b  +  ( k  x.  T
) )  -  b
)  /  T )  =  ( ( k  x.  T )  /  T ) )
527340adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  e.  CC )
528318adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  e.  CC )
529419a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  0  e.  RR )
530529, 350gtned 9766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  T  =/=  0 )
531267, 530syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ps 
->  T  =/=  0
)
532531adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ps  /\  k  e.  ZZ )  ->  T  =/=  0 )
533527, 528, 532divcan4d 10385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ps  /\  k  e.  ZZ )  ->  (
( k  x.  T
)  /  T )  =  k )
534526, 533eqtr2d 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ps  /\  k  e.  ZZ )  ->  k  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
535534adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ps  /\  ( j  e.  ZZ  /\  k  e.  ZZ ) )  -> 
k  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
536535adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T ) ) )  ->  k  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
537 oveq1 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T
) )  ->  (
( a  +  ( j  x.  T ) )  -  b )  =  ( ( b  +  ( k  x.  T ) )  -  b ) )
538537oveq1d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( a  +  ( j  x.  T ) )  =  ( b  +  ( k  x.  T
) )  ->  (
( ( a  +  ( j  x.  T
) )  -  b
)  /  T )  =  ( ( ( b  +  ( k  x.  T ) )  -  b )  /  T ) )
539538adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ps  /\  (
j  e.  ZZ  /\  k  e.  ZZ )
)  /\  ( a  +  (