ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prarloc Unicode version
Theorem prarloc 7820
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 7821 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 7794 . . . . . . 7 |- ( <. L , U >. e. P. -> E. x e. Q. x e. L )
2 df-rex 2528 . . . . . . 7 |- ( E. x e. Q. x e. L <-> E. x ( x e. Q. /\ x e. L ) )
31, 2sylib 122 . . . . . 6 |- ( <. L , U >. e. P. -> E. x ( x e. Q. /\ x e. L ) )
43adantr 276 . . . . 5 |- ( ( <. L , U >. e. P. /\ P e. Q. ) -> E. x ( x e. Q. /\ x e. L ) )
5 prmu 7795 . . . . . . 7 |- ( <. L , U >. e. P. -> E. y e. Q. y e. U )
6 df-rex 2528 . . . . . . 7 |- ( E. y e. Q. y e. U <-> E. y ( y e. Q. /\ y e. U ) )
75, 6sylib 122 . . . . . 6 |- ( <. L , U >. e. P. -> E. y ( y e. Q. /\ y e. U ) )
87adantr 276 . . . . 5 |- ( ( <. L , U >. e. P. /\ P e. Q. ) -> E. y ( y e. Q. /\ y e. U ) )
9 subhalfnqq 7731 . . . . . . . . 9 |- ( P e. Q. -> E. q e. Q. ( q +Q q ) <Q P )
109adantl 277 . . . . . . . 8 |- ( ( <. L , U >. e. P. /\ P e. Q. ) -> E. q e. Q. ( q +Q q ) <Q P )
11 df-rex 2528 . . . . . . . 8 |- ( E. q e. Q. ( q +Q q ) <Q P <-> E. q ( q e. Q. /\ ( q +Q q ) <Q P ) )
1210, 11sylib 122 . . . . . . 7 |- ( ( <. L , U >. e. P. /\ P e. Q. ) -> E. q ( q e. Q. /\ ( q +Q q ) <Q P ) )
1312ancli 323 . . . . . 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 1958 . . . . . 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 134 . . . . 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 1989 . . . . 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 1208 . . . 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 7736 . . . . . . . . . . . . . 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 2528 . . . . . . . . . . . . . 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 122 . . . . . . . . . . . . 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 1234 . . . . . . . . . . . 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 1258 . . . . . . . . . . 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 1260 . . . . . . . . . 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 1262 . . . . . . . . 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 1261 . . . . . . . 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 323 . . . . . . 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 1958 . . . . . . 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 134 . . . . . 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 1650 . . . . 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 1649 . . . 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 1075 . . . . . . . . . 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 1097 . . . . . . . . . . 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 276 . . . . . . . . . 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 1098 . . . . . . . . . . 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 276 . . . . . . . . . 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 1204 . . . . . . . . 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 1095 . . . . . . . . . . . 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 276 . . . . . . . . . . 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 1076 . . . . . . . . . . 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 531 . . . . . . . . . . 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 541 . . . . . . . . . . 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 542 . . . . . . . . . . . 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 1078 . . . . . . . . . . . . 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 7802 . . . . . . . . . . . . 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 411 . . . . . . . . . . . 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 7818 . . . . . . . . . . 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 1294 . . . . . . . . . 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 2528 . . . . . . . . . 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 122 . . . . . . . . 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 306 . . . . . . . 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 1958 . . . . . . . 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 134 . . . . . . 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 541 . . . . . . . . . . . 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 2297 . . . . . . . . . . . . . . . . 17 |- ( a = ( x +Q0 ( [ <. m , 1o >. ] ~Q0 ·Q0 q ) ) -> ( a e. L <-> ( x +Q0 ( [ <. m , 1o >. ] ~Q0 ·Q0 q ) ) e. L ) )
5655anbi1d 465 . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . 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 2948 . . . . . . . . . . . . 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 160 . . . . . . . . . . . 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 542 . . . . . . . . . . 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 2297 . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . 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 1874 . . . . . . . . . . . . 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 2948 . . . . . . . . . . . 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 160 . . . . . . . . . . 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 1958 . . . . . . . . . . 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 1654 . . . . . . . . . 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 134 . . . . . . . . 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 541 . . . . . . . . . . . . . 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 277 . . . . . . . . . . . . 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 542 . . . . . . . . . . . . . . 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 277 . . . . . . . . . . . . . 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 109 . . . . . . . . . . . . . . 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 1070 . . . . . . . . . . . . . . . 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 1071 . . . . . . . . . . . . . . . 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 306 . . . . . . . . . . . . . . 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 1069 . . . . . . . . . . . . . . . 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 541 . . . . . . . . . . . . . . . 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 306 . . . . . . . . . . . . . . 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 7819 . . . . . . . . . . . . . . 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 1272 . . . . . . . . . . . . . 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 306 . . . . . . . . . . . . 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 306 . . . . . . . . . . . 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 571 . . . . . . . . . . 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 399 . . . . . . . . . 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 1650 . . . . . . . . 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 1647 . . . . . . 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 1948 . . . . 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 1948 . . . 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 1712 . . 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 122 . 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 1958 . . . . 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 2528 . . . . . 6 |- ( E. b e. U b <Q ( a +Q P ) <-> E. b ( b e. U /\ b <Q ( a +Q P ) ) )
103102anbi2i 457 . . . . 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 187 . . . 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 1654 . . 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 2528 . . 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 187 . 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 122 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 104   /\ w3a 1005   = wceq 1398   E.wex 1541   e. wcel 2205   E.wrex 2523   <.cop 3694   class class class wbr 4111   omcom 4714  (class class class)co 6052   1oc1o 6642   2oc2o 6643   +o coa 6646   [cec 6767   N.cnpi 7589   <N clti 7592   ~Q ceq 7596   Q.cnq 7597   +Q cplq 7599   .Q cmq 7600   <Q cltq 7602   ~Q0 ceq0 7603   +Q0 cplq0 7606   ·Q0 cmq0 7607   P.cnp 7608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-coll 4227  ax-sep 4230  ax-nul 4238  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-iinf 4712
This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3045  df-csb 3141  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-nul 3511  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-int 3952  df-iun 3995  df-br 4112  df-opab 4174  df-mpt 4175  df-tr 4211  df-eprel 4412  df-id 4416  df-po 4419  df-iso 4420  df-iord 4489  df-on 4491  df-suc 4494  df-iom 4715  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-res 4763  df-ima 4764  df-iota 5314  df-fun 5356  df-fn 5357  df-f 5358  df-f1 5359  df-fo 5360  df-f1o 5361  df-fv 5362  df-ov 6055  df-oprab 6056  df-mpo 6057  df-1st 6336  df-2nd 6337  df-recs 6538  df-irdg 6603  df-1o 6649  df-2o 6650  df-oadd 6653  df-omul 6654  df-er 6769  df-ec 6771  df-qs 6775  df-ni 7621  df-pli 7622  df-mi 7623  df-lti 7624  df-plpq 7661  df-mpq 7662  df-enq 7664  df-nqqs 7665  df-plqqs 7666  df-mqqs 7667  df-1nqqs 7668  df-rq 7669  df-ltnqqs 7670  df-enq0 7741  df-nq0 7742  df-0nq0 7743  df-plq0 7744  df-mq0 7745  df-inp 7783
This theorem is referenced by:  prarloc2  7821  addlocpr  7853  prmuloc  7883  ltaddpr  7914  ltexprlemloc  7924  ltexprlemrl  7927  ltexprlemru  7929
  Copyright terms: Public domain W3C validator