ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prarloc Unicode version

Theorem prarloc 7279
Description: A Dedekind cut is arithmetically located. Part of Proposition 11.15 of [BauerTaylor], p. 52, slightly modified. It states that given a tolerance  P, there are elements of the lower and upper cut which are within that tolerance of each other.

Usually, proofs will be shorter if they use prarloc2 7280 instead. (Contributed by Jim Kingdon, 22-Oct-2019.)

Assertion
Ref Expression
prarloc  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. a  e.  L  E. b  e.  U  b  <Q  ( a  +Q  P ) )
Distinct variable groups:    L, a, b    P, a, b    U, a, b

Proof of Theorem prarloc
Dummy variables  m  n  q  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prml 7253 . . . . . . 7  |-  ( <. L ,  U >.  e. 
P.  ->  E. x  e.  Q.  x  e.  L )
2 df-rex 2399 . . . . . . 7  |-  ( E. x  e.  Q.  x  e.  L  <->  E. x ( x  e.  Q.  /\  x  e.  L ) )
31, 2sylib 121 . . . . . 6  |-  ( <. L ,  U >.  e. 
P.  ->  E. x ( x  e.  Q.  /\  x  e.  L ) )
43adantr 274 . . . . 5  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. x
( x  e.  Q.  /\  x  e.  L ) )
5 prmu 7254 . . . . . . 7  |-  ( <. L ,  U >.  e. 
P.  ->  E. y  e.  Q.  y  e.  U )
6 df-rex 2399 . . . . . . 7  |-  ( E. y  e.  Q.  y  e.  U  <->  E. y ( y  e.  Q.  /\  y  e.  U ) )
75, 6sylib 121 . . . . . 6  |-  ( <. L ,  U >.  e. 
P.  ->  E. y ( y  e.  Q.  /\  y  e.  U ) )
87adantr 274 . . . . 5  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. y
( y  e.  Q.  /\  y  e.  U ) )
9 subhalfnqq 7190 . . . . . . . . 9  |-  ( P  e.  Q.  ->  E. q  e.  Q.  ( q  +Q  q )  <Q  P )
109adantl 275 . . . . . . . 8  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. q  e.  Q.  ( q  +Q  q )  <Q  P )
11 df-rex 2399 . . . . . . . 8  |-  ( E. q  e.  Q.  (
q  +Q  q ) 
<Q  P  <->  E. q ( q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P ) )
1210, 11sylib 121 . . . . . . 7  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. q
( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) )
1312ancli 321 . . . . . 6  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  /\  E. q
( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )
14 19.42v 1862 . . . . . 6  |-  ( E. q ( ( <. L ,  U >.  e. 
P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) )  <-> 
( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  E. q ( q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P ) ) )
1513, 14sylibr 133 . . . . 5  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. q
( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )
16 eeeanv 1885 . . . . 5  |-  ( E. x E. y E. q ( ( x  e.  Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  <->  ( E. x
( x  e.  Q.  /\  x  e.  L )  /\  E. y ( y  e.  Q.  /\  y  e.  U )  /\  E. q ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) ) )
174, 8, 15, 16syl3anbrc 1150 . . . 4  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. x E. y E. q ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) ) )
18 prarloclemarch2 7195 . . . . . . . . . . . . . 14  |-  ( ( y  e.  Q.  /\  x  e.  Q.  /\  q  e.  Q. )  ->  E. n  e.  N.  ( 1o  <N  n  /\  y  <Q  (
x  +Q  ( [
<. n ,  1o >. ]  ~Q  .Q  q ) ) ) )
19 df-rex 2399 . . . . . . . . . . . . . 14  |-  ( E. n  e.  N.  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) )  <->  E. n
( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q ) ) ) ) )
2018, 19sylib 121 . . . . . . . . . . . . 13  |-  ( ( y  e.  Q.  /\  x  e.  Q.  /\  q  e.  Q. )  ->  E. n
( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q ) ) ) ) )
21203com12 1170 . . . . . . . . . . . 12  |-  ( ( x  e.  Q.  /\  y  e.  Q.  /\  q  e.  Q. )  ->  E. n
( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q ) ) ) ) )
22213adant1r 1194 . . . . . . . . . . 11  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  y  e.  Q.  /\  q  e.  Q. )  ->  E. n ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )
23223adant2r 1196 . . . . . . . . . 10  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  q  e.  Q. )  ->  E. n
( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q ) ) ) ) )
24233adant3r 1198 . . . . . . . . 9  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) )  ->  E. n ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )
25243adant3l 1197 . . . . . . . 8  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  ->  E. n
( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q ) ) ) ) )
2625ancli 321 . . . . . . 7  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  ->  ( (
( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  E. n
( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q ) ) ) ) ) )
27 19.42v 1862 . . . . . . 7  |-  ( E. n ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e. 
P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  <->  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e. 
P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  E. n
( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q ) ) ) ) ) )
2826, 27sylibr 133 . . . . . 6  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  ->  E. n
( ( ( x  e.  Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) ) )
29282eximi 1565 . . . . 5  |-  ( E. y E. q ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  ->  E. y E. q E. n ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) ) )
3029eximi 1564 . . . 4  |-  ( E. x E. y E. q ( ( x  e.  Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  ->  E. x E. y E. q E. n ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e. 
P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) ) )
31 simpl1l 1017 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  x  e.  Q. )
32 simp3rl 1039 . . . . . . . . . . 11  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  ->  q  e.  Q. )
3332adantr 274 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  q  e.  Q. )
34 simp3rr 1040 . . . . . . . . . . 11  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  ->  ( q  +Q  q )  <Q  P )
3534adantr 274 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  ( q  +Q  q )  <Q  P )
3631, 33, 353jca 1146 . . . . . . . . 9  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  ( x  e.  Q.  /\  q  e. 
Q.  /\  ( q  +Q  q )  <Q  P ) )
37 simp3ll 1037 . . . . . . . . . . . 12  |-  ( ( ( x  e.  Q.  /\  x  e.  L )  /\  ( y  e. 
Q.  /\  y  e.  U )  /\  (
( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  (
q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  ->  <. L ,  U >.  e.  P. )
3837adantr 274 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  <. L ,  U >.  e.  P. )
39 simpl1r 1018 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  x  e.  L )
40 simprl 505 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  n  e.  N. )
41 simprrl 513 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  1o  <N  n )
42 simprrr 514 . . . . . . . . . . . 12  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  y  <Q  ( x  +Q  ( [
<. n ,  1o >. ]  ~Q  .Q  q ) ) )
43 simpl2r 1020 . . . . . . . . . . . . 13  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  y  e.  U )
44 prcunqu 7261 . . . . . . . . . . . . 13  |-  ( (
<. L ,  U >.  e. 
P.  /\  y  e.  U )  ->  (
y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) )  ->  (
x  +Q  ( [
<. n ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) )
4538, 43, 44syl2anc 408 . . . . . . . . . . . 12  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  ( y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) )  ->  (
x  +Q  ( [
<. n ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) )
4642, 45mpd 13 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q ) )  e.  U )
47 prarloclem 7277 . . . . . . . . . . 11  |-  ( ( ( <. L ,  U >.  e.  P.  /\  x  e.  L )  /\  (
n  e.  N.  /\  q  e.  Q.  /\  1o  <N  n )  /\  (
x  +Q  ( [
<. n ,  1o >. ]  ~Q  .Q  q ) )  e.  U )  ->  E. m  e.  om  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) )
4838, 39, 40, 33, 41, 46, 47syl231anc 1221 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  E. m  e.  om  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) )
49 df-rex 2399 . . . . . . . . . 10  |-  ( E. m  e.  om  (
( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U )  <->  E. m ( m  e. 
om  /\  ( (
x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )
5048, 49sylib 121 . . . . . . . . 9  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  E. m
( m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )
5136, 50jca 304 . . . . . . . 8  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  E. m ( m  e. 
om  /\  ( (
x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) )
52 19.42v 1862 . . . . . . . 8  |-  ( E. m ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q )  <Q  P )  /\  (
m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  <->  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  E. m ( m  e. 
om  /\  ( (
x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) )
5351, 52sylibr 133 . . . . . . 7  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  E. m
( ( x  e. 
Q.  /\  q  e.  Q.  /\  ( q  +Q  q )  <Q  P )  /\  ( m  e. 
om  /\  ( (
x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) )
54 simprrl 513 . . . . . . . . . . . 12  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  ->  (
x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  e.  L )
55 eleq1 2180 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  ->  ( a  e.  L  <->  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L ) )
5655anbi1d 460 . . . . . . . . . . . . . . . 16  |-  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  ->  ( (
a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U )  <-> 
( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )
5756anbi2d 459 . . . . . . . . . . . . . . 15  |-  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  ->  ( (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) )  <->  ( m  e. 
om  /\  ( (
x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) )
5857anbi2d 459 . . . . . . . . . . . . . 14  |-  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  ->  ( (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  <->  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) ) )
5958ceqsexgv 2788 . . . . . . . . . . . . 13  |-  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  e.  L  -> 
( E. a ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) )  <->  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) ) )
6059biimprcd 159 . . . . . . . . . . . 12  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  ->  (
( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  ->  E. a ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) ) ) )
6154, 60mpd 13 . . . . . . . . . . 11  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  ->  E. a
( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) ) )
62 simprrr 514 . . . . . . . . . . 11  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  ->  (
x  +Q  ( [
<. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U )
63 eleq1 2180 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  ->  ( b  e.  U  <->  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) )
6463anbi2d 459 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  ->  ( (
a  e.  L  /\  b  e.  U )  <->  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )
6564anbi2d 459 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  ->  ( (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) )  <->  ( m  e.  om  /\  ( a  e.  L  /\  (
x  +Q  ( [
<. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) )
6665anbi2d 459 . . . . . . . . . . . . . . 15  |-  ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  ->  ( (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) )  <->  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) ) )
6766anbi2d 459 . . . . . . . . . . . . . 14  |-  ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  ->  ( (
a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  <-> 
( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) ) ) )
6867exbidv 1781 . . . . . . . . . . . . 13  |-  ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  ->  ( E. a ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  <->  E. a ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) ) ) )
6968ceqsexgv 2788 . . . . . . . . . . . 12  |-  ( ( x  +Q  ( [
<. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U  ->  ( E. b ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  E. a
( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) )  <->  E. a ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) ) ) )
7069biimprcd 159 . . . . . . . . . . 11  |-  ( E. a ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) ) )  -> 
( ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U  ->  E. b ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  E. a
( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) ) ) )
7161, 62, 70sylc 62 . . . . . . . . . 10  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  ->  E. b
( b  =  ( x  +Q  ( [
<. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  E. a ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) ) )
72 19.42v 1862 . . . . . . . . . . 11  |-  ( E. a ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) )  <->  ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  E. a
( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) ) )
7372exbii 1569 . . . . . . . . . 10  |-  ( E. b E. a ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) )  <->  E. b ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  E. a
( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) ) )
7471, 73sylibr 133 . . . . . . . . 9  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  ->  E. b E. a ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) ) )
75 simprrl 513 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) )  -> 
a  e.  L )
7675adantl 275 . . . . . . . . . . . . 13  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  a  e.  L
)
77 simprrr 514 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) )  -> 
b  e.  U )
7877adantl 275 . . . . . . . . . . . . . 14  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  b  e.  U
)
79 simpl 108 . . . . . . . . . . . . . . 15  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) ) )
80 simprl2 1012 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  q  e.  Q. )
81 simprl3 1013 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  ( q  +Q  q )  <Q  P )
8280, 81jca 304 . . . . . . . . . . . . . . 15  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  ( q  e. 
Q.  /\  ( q  +Q  q )  <Q  P ) )
83 simprl1 1011 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  x  e.  Q. )
84 simprrl 513 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  m  e.  om )
8583, 84jca 304 . . . . . . . . . . . . . . 15  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  ( x  e. 
Q.  /\  m  e.  om ) )
86 prarloclemcalc 7278 . . . . . . . . . . . . . . 15  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( x  e.  Q.  /\  m  e.  om )
) )  ->  b  <Q  ( a  +Q  P
) )
8779, 82, 85, 86syl12anc 1199 . . . . . . . . . . . . . 14  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  b  <Q  (
a  +Q  P ) )
8878, 87jca 304 . . . . . . . . . . . . 13  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  ( b  e.  U  /\  b  <Q 
( a  +Q  P
) ) )
8976, 88jca 304 . . . . . . . . . . . 12  |-  ( ( ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) ) )  /\  (
( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
9089ancom1s 543 . . . . . . . . . . 11  |-  ( ( ( b  =  ( x  +Q  ( [
<. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  a  =  ( x +Q0  ( [
<. m ,  1o >. ] ~Q0 ·Q0 
q ) ) )  /\  ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q )  <Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) )  ->  ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
9190anasss 396 . . . . . . . . . 10  |-  ( ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) )  ->  ( a  e.  L  /\  (
b  e.  U  /\  b  <Q  ( a  +Q  P ) ) ) )
92912eximi 1565 . . . . . . . . 9  |-  ( E. b E. a ( b  =  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  /\  ( a  =  ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q )
)  /\  ( (
x  e.  Q.  /\  q  e.  Q.  /\  (
q  +Q  q ) 
<Q  P )  /\  (
m  e.  om  /\  ( a  e.  L  /\  b  e.  U
) ) ) ) )  ->  E. b E. a ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
9374, 92syl 14 . . . . . . . 8  |-  ( ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q
)  <Q  P )  /\  ( m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  ->  E. b E. a ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
9493exlimiv 1562 . . . . . . 7  |-  ( E. m ( ( x  e.  Q.  /\  q  e.  Q.  /\  ( q  +Q  q )  <Q  P )  /\  (
m  e.  om  /\  ( ( x +Q0  ( [ <. m ,  1o >. ] ~Q0 ·Q0  q ) )  e.  L  /\  ( x  +Q  ( [ <. ( m  +o  2o ) ,  1o >. ]  ~Q  .Q  q ) )  e.  U ) ) )  ->  E. b E. a ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
9553, 94syl 14 . . . . . 6  |-  ( ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  E. b E. a ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
9695exlimivv 1852 . . . . 5  |-  ( E. q E. n ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  E. b E. a ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
9796exlimivv 1852 . . . 4  |-  ( E. x E. y E. q E. n ( ( ( x  e. 
Q.  /\  x  e.  L )  /\  (
y  e.  Q.  /\  y  e.  U )  /\  ( ( <. L ,  U >.  e.  P.  /\  P  e.  Q. )  /\  ( q  e.  Q.  /\  ( q  +Q  q
)  <Q  P ) ) )  /\  ( n  e.  N.  /\  ( 1o  <N  n  /\  y  <Q  ( x  +Q  ( [ <. n ,  1o >. ]  ~Q  .Q  q
) ) ) ) )  ->  E. b E. a ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
9817, 30, 973syl 17 . . 3  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. b E. a ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
99 excom 1627 . . 3  |-  ( E. b E. a ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P ) ) )  <->  E. a E. b
( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P ) ) ) )
10098, 99sylib 121 . 2  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. a E. b ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) ) )
101 19.42v 1862 . . . . 5  |-  ( E. b ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) )  <->  ( a  e.  L  /\  E. b
( b  e.  U  /\  b  <Q  ( a  +Q  P ) ) ) )
102 df-rex 2399 . . . . . 6  |-  ( E. b  e.  U  b 
<Q  ( a  +Q  P
)  <->  E. b ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) )
103102anbi2i 452 . . . . 5  |-  ( ( a  e.  L  /\  E. b  e.  U  b 
<Q  ( a  +Q  P
) )  <->  ( a  e.  L  /\  E. b
( b  e.  U  /\  b  <Q  ( a  +Q  P ) ) ) )
104101, 103bitr4i 186 . . . 4  |-  ( E. b ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P
) ) )  <->  ( a  e.  L  /\  E. b  e.  U  b  <Q  ( a  +Q  P ) ) )
105104exbii 1569 . . 3  |-  ( E. a E. b ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P ) ) )  <->  E. a ( a  e.  L  /\  E. b  e.  U  b  <Q  ( a  +Q  P
) ) )
106 df-rex 2399 . . 3  |-  ( E. a  e.  L  E. b  e.  U  b  <Q  ( a  +Q  P
)  <->  E. a ( a  e.  L  /\  E. b  e.  U  b  <Q  ( a  +Q  P
) ) )
107105, 106bitr4i 186 . 2  |-  ( E. a E. b ( a  e.  L  /\  ( b  e.  U  /\  b  <Q  ( a  +Q  P ) ) )  <->  E. a  e.  L  E. b  e.  U  b  <Q  ( a  +Q  P ) )
108100, 107sylib 121 1  |-  ( (
<. L ,  U >.  e. 
P.  /\  P  e.  Q. )  ->  E. a  e.  L  E. b  e.  U  b  <Q  ( a  +Q  P ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 947    = wceq 1316   E.wex 1453    e. wcel 1465   E.wrex 2394   <.cop 3500   class class class wbr 3899   omcom 4474  (class class class)co 5742   1oc1o 6274   2oc2o 6275    +o coa 6278   [cec 6395   N.cnpi 7048    <N clti 7051    ~Q ceq 7055   Q.cnq 7056    +Q cplq 7058    .Q cmq 7059    <Q cltq 7061   ~Q0 ceq0 7062   +Q0 cplq0 7065   ·Q0 cmq0 7066   P.cnp 7067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-ral 2398  df-rex 2399  df-reu 2400  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-eprel 4181  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-irdg 6235  df-1o 6281  df-2o 6282  df-oadd 6285  df-omul 6286  df-er 6397  df-ec 6399  df-qs 6403  df-ni 7080  df-pli 7081  df-mi 7082  df-lti 7083  df-plpq 7120  df-mpq 7121  df-enq 7123  df-nqqs 7124  df-plqqs 7125  df-mqqs 7126  df-1nqqs 7127  df-rq 7128  df-ltnqqs 7129  df-enq0 7200  df-nq0 7201  df-0nq0 7202  df-plq0 7203  df-mq0 7204  df-inp 7242
This theorem is referenced by:  prarloc2  7280  addlocpr  7312  prmuloc  7342  ltaddpr  7373  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388
  Copyright terms: Public domain W3C validator