Metamath Proof Explorer

Theorem xralrple

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Assertion xralrple 
|- ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )

Proof

Step Hyp Ref Expression
1 rpge0 
 |-  ( x e. RR+ -> 0 <_ x )
2 1 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> 0 <_ x )
3 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> B e. RR )
4 rpre 
 |-  ( x e. RR+ -> x e. RR )
5 4 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> x e. RR )
6 3 5 addge01d 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> ( 0 <_ x <-> B <_ ( B + x ) ) )
7 2 6 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> B <_ ( B + x ) )
8 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> A e. RR* )
9 3 rexrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> B e. RR* )
10 3 5 readdcld 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> ( B + x ) e. RR )
11 10 rexrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> ( B + x ) e. RR* )
12 xrletr 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( B + x ) e. RR* ) -> ( ( A <_ B /\ B <_ ( B + x ) ) -> A <_ ( B + x ) ) )
13 8 9 11 12 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> ( ( A <_ B /\ B <_ ( B + x ) ) -> A <_ ( B + x ) ) )
14 7 13 mpan2d 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ x e. RR+ ) -> ( A <_ B -> A <_ ( B + x ) ) )
15 14 ralrimdva 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B -> A. x e. RR+ A <_ ( B + x ) ) )
16 rexr 
 |-  ( B e. RR -> B e. RR* )
17 16 adantl 
 |-  ( ( A e. RR* /\ B e. RR ) -> B e. RR* )
18 simpl 
 |-  ( ( A e. RR* /\ B e. RR ) -> A e. RR* )
19 qbtwnxr 
 |-  ( ( B e. RR* /\ A e. RR* /\ B < A ) -> E. y e. QQ ( B < y /\ y < A ) )
20 19 3expia 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B < A -> E. y e. QQ ( B < y /\ y < A ) ) )
21 17 18 20 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( B < A -> E. y e. QQ ( B < y /\ y < A ) ) )
22 simprrl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> B < y )
23 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> B e. RR )
24 qre 
 |-  ( y e. QQ -> y e. RR )
25 24 ad2antrl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> y e. RR )
26 difrp 
 |-  ( ( B e. RR /\ y e. RR ) -> ( B < y <-> ( y - B ) e. RR+ ) )
27 23 25 26 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> ( B < y <-> ( y - B ) e. RR+ ) )
28 22 27 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> ( y - B ) e. RR+ )
29 simprrr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> y < A )
30 25 rexrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> y e. RR* )
31 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> A e. RR* )
32 xrltnle 
 |-  ( ( y e. RR* /\ A e. RR* ) -> ( y < A <-> -. A <_ y ) )
33 30 31 32 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> ( y < A <-> -. A <_ y ) )
34 29 33 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> -. A <_ y )
35 23 recnd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> B e. CC )
36 25 recnd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> y e. CC )
37 35 36 pncan3d 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> ( B + ( y - B ) ) = y )
38 37 breq2d 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> ( A <_ ( B + ( y - B ) ) <-> A <_ y ) )
39 34 38 mtbird 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> -. A <_ ( B + ( y - B ) ) )
40 oveq2 
 |-  ( x = ( y - B ) -> ( B + x ) = ( B + ( y - B ) ) )
41 40 breq2d 
 |-  ( x = ( y - B ) -> ( A <_ ( B + x ) <-> A <_ ( B + ( y - B ) ) ) )
42 41 notbid 
 |-  ( x = ( y - B ) -> ( -. A <_ ( B + x ) <-> -. A <_ ( B + ( y - B ) ) ) )
43 42 rspcev 
 |-  ( ( ( y - B ) e. RR+ /\ -. A <_ ( B + ( y - B ) ) ) -> E. x e. RR+ -. A <_ ( B + x ) )
44 28 39 43 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> E. x e. RR+ -. A <_ ( B + x ) )
45 rexnal 
 |-  ( E. x e. RR+ -. A <_ ( B + x ) <-> -. A. x e. RR+ A <_ ( B + x ) )
46 44 45 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. QQ /\ ( B < y /\ y < A ) ) ) -> -. A. x e. RR+ A <_ ( B + x ) )
47 46 rexlimdvaa 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( E. y e. QQ ( B < y /\ y < A ) -> -. A. x e. RR+ A <_ ( B + x ) ) )
48 21 47 syld 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( B < A -> -. A. x e. RR+ A <_ ( B + x ) ) )
49 48 con2d 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A. x e. RR+ A <_ ( B + x ) -> -. B < A ) )
50 xrlenlt 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
51 16 50 sylan2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
52 49 51 sylibrd 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A. x e. RR+ A <_ ( B + x ) -> A <_ B ) )
53 15 52 impbid 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )