Metamath Proof Explorer

Theorem xralrple2

Description: Show that A is less than B by showing that there is no positive bound on the difference. A variant on xralrple . (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses xralrple2.x 
|- F/ x ph
xralrple2.a 
|- ( ph -> A e. RR* )
xralrple2.b 
|- ( ph -> B e. ( 0 [,) +oo ) )
Assertion xralrple2 
|- ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) )

Proof

Step Hyp Ref Expression
1 xralrple2.x 
 |-  F/ x ph
2 xralrple2.a 
 |-  ( ph -> A e. RR* )
3 xralrple2.b 
 |-  ( ph -> B e. ( 0 [,) +oo ) )
4 nfv 
 |-  F/ x A <_ B
5 1 4 nfan 
 |-  F/ x ( ph /\ A <_ B )
6 2 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A e. RR* )
7 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
8 3 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B e. ( 0 [,) +oo ) )
9 7 8 sseldi 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B e. RR* )
10 1red 
 |-  ( ( ph /\ x e. RR+ ) -> 1 e. RR )
11 rpre 
 |-  ( x e. RR+ -> x e. RR )
12 11 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
13 10 12 readdcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 + x ) e. RR )
14 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
15 14 3 sseldi 
 |-  ( ph -> B e. RR )
16 15 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> B e. RR )
17 13 16 remulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 + x ) x. B ) e. RR )
18 17 rexrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 + x ) x. B ) e. RR* )
19 18 adantlr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> ( ( 1 + x ) x. B ) e. RR* )
20 simplr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A <_ B )
21 15 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B e. RR )
22 1red 
 |-  ( x e. RR+ -> 1 e. RR )
23 22 11 readdcld 
 |-  ( x e. RR+ -> ( 1 + x ) e. RR )
24 23 adantl 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> ( 1 + x ) e. RR )
25 0xr 
 |-  0 e. RR*
26 25 a1i 
 |-  ( B e. ( 0 [,) +oo ) -> 0 e. RR* )
27 pnfxr 
 |-  +oo e. RR*
28 27 a1i 
 |-  ( B e. ( 0 [,) +oo ) -> +oo e. RR* )
29 id 
 |-  ( B e. ( 0 [,) +oo ) -> B e. ( 0 [,) +oo ) )
30 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,) +oo ) ) -> 0 <_ B )
31 26 28 29 30 syl3anc 
 |-  ( B e. ( 0 [,) +oo ) -> 0 <_ B )
32 3 31 syl 
 |-  ( ph -> 0 <_ B )
33 32 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> 0 <_ B )
34 id 
 |-  ( x e. RR+ -> x e. RR+ )
35 22 34 ltaddrpd 
 |-  ( x e. RR+ -> 1 < ( 1 + x ) )
36 22 23 35 ltled 
 |-  ( x e. RR+ -> 1 <_ ( 1 + x ) )
37 36 adantl 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> 1 <_ ( 1 + x ) )
38 21 24 33 37 lemulge12d 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B <_ ( ( 1 + x ) x. B ) )
39 6 9 19 20 38 xrletrd 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A <_ ( ( 1 + x ) x. B ) )
40 39 ex 
 |-  ( ( ph /\ A <_ B ) -> ( x e. RR+ -> A <_ ( ( 1 + x ) x. B ) ) )
41 5 40 ralrimi 
 |-  ( ( ph /\ A <_ B ) -> A. x e. RR+ A <_ ( ( 1 + x ) x. B ) )
42 41 ex 
 |-  ( ph -> ( A <_ B -> A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) )
43 2 ad3antrrr 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B = 0 ) -> A e. RR* )
44 id 
 |-  ( B = 0 -> B = 0 )
45 0red 
 |-  ( B = 0 -> 0 e. RR )
46 44 45 eqeltrd 
 |-  ( B = 0 -> B e. RR )
47 46 adantl 
 |-  ( ( y e. RR+ /\ B = 0 ) -> B e. RR )
48 rpre 
 |-  ( y e. RR+ -> y e. RR )
49 48 adantr 
 |-  ( ( y e. RR+ /\ B = 0 ) -> y e. RR )
50 47 49 readdcld 
 |-  ( ( y e. RR+ /\ B = 0 ) -> ( B + y ) e. RR )
51 50 rexrd 
 |-  ( ( y e. RR+ /\ B = 0 ) -> ( B + y ) e. RR* )
52 51 adantll 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B = 0 ) -> ( B + y ) e. RR* )
53 25 a1i 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B = 0 ) -> 0 e. RR* )
54 1rp 
 |-  1 e. RR+
55 54 a1i 
 |-  ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) -> 1 e. RR+ )
56 id 
 |-  ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) -> A. x e. RR+ A <_ ( ( 1 + x ) x. B ) )
57 oveq2 
 |-  ( x = 1 -> ( 1 + x ) = ( 1 + 1 ) )
58 57 oveq1d 
 |-  ( x = 1 -> ( ( 1 + x ) x. B ) = ( ( 1 + 1 ) x. B ) )
59 58 breq2d 
 |-  ( x = 1 -> ( A <_ ( ( 1 + x ) x. B ) <-> A <_ ( ( 1 + 1 ) x. B ) ) )
60 59 rspcva 
 |-  ( ( 1 e. RR+ /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) -> A <_ ( ( 1 + 1 ) x. B ) )
61 55 56 60 syl2anc 
 |-  ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) -> A <_ ( ( 1 + 1 ) x. B ) )
62 1p1e2 
 |-  ( 1 + 1 ) = 2
63 62 a1i 
 |-  ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) -> ( 1 + 1 ) = 2 )
64 63 oveq1d 
 |-  ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) -> ( ( 1 + 1 ) x. B ) = ( 2 x. B ) )
65 61 64 breqtrd 
 |-  ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) -> A <_ ( 2 x. B ) )
66 65 adantr 
 |-  ( ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) /\ B = 0 ) -> A <_ ( 2 x. B ) )
67 simpr 
 |-  ( ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) /\ B = 0 ) -> B = 0 )
68 simpl 
 |-  ( ( A <_ ( 2 x. B ) /\ B = 0 ) -> A <_ ( 2 x. B ) )
69 oveq2 
 |-  ( B = 0 -> ( 2 x. B ) = ( 2 x. 0 ) )
70 2cnd 
 |-  ( B = 0 -> 2 e. CC )
71 70 mul01d 
 |-  ( B = 0 -> ( 2 x. 0 ) = 0 )
72 69 71 eqtrd 
 |-  ( B = 0 -> ( 2 x. B ) = 0 )
73 72 adantl 
 |-  ( ( A <_ ( 2 x. B ) /\ B = 0 ) -> ( 2 x. B ) = 0 )
74 68 73 breqtrd 
 |-  ( ( A <_ ( 2 x. B ) /\ B = 0 ) -> A <_ 0 )
75 66 67 74 syl2anc 
 |-  ( ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) /\ B = 0 ) -> A <_ 0 )
76 75 ad4ant24 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B = 0 ) -> A <_ 0 )
77 rpgt0 
 |-  ( y e. RR+ -> 0 < y )
78 77 adantr 
 |-  ( ( y e. RR+ /\ B = 0 ) -> 0 < y )
79 oveq1 
 |-  ( B = 0 -> ( B + y ) = ( 0 + y ) )
80 79 adantl 
 |-  ( ( y e. RR+ /\ B = 0 ) -> ( B + y ) = ( 0 + y ) )
81 48 recnd 
 |-  ( y e. RR+ -> y e. CC )
82 81 adantr 
 |-  ( ( y e. RR+ /\ B = 0 ) -> y e. CC )
83 82 addid2d 
 |-  ( ( y e. RR+ /\ B = 0 ) -> ( 0 + y ) = y )
84 80 83 eqtr2d 
 |-  ( ( y e. RR+ /\ B = 0 ) -> y = ( B + y ) )
85 78 84 breqtrd 
 |-  ( ( y e. RR+ /\ B = 0 ) -> 0 < ( B + y ) )
86 85 adantll 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B = 0 ) -> 0 < ( B + y ) )
87 43 53 52 76 86 xrlelttrd 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B = 0 ) -> A < ( B + y ) )
88 43 52 87 xrltled 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B = 0 ) -> A <_ ( B + y ) )
89 simpl 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ -. B = 0 ) -> ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) )
90 15 adantr 
 |-  ( ( ph /\ -. B = 0 ) -> B e. RR )
91 0red 
 |-  ( ( ph /\ -. B = 0 ) -> 0 e. RR )
92 32 adantr 
 |-  ( ( ph /\ -. B = 0 ) -> 0 <_ B )
93 44 necon3bi 
 |-  ( -. B = 0 -> B =/= 0 )
94 93 adantl 
 |-  ( ( ph /\ -. B = 0 ) -> B =/= 0 )
95 91 90 92 94 leneltd 
 |-  ( ( ph /\ -. B = 0 ) -> 0 < B )
96 90 95 elrpd 
 |-  ( ( ph /\ -. B = 0 ) -> B e. RR+ )
97 96 ad4ant14 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ -. B = 0 ) -> B e. RR+ )
98 simplr 
 |-  ( ( ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) /\ y e. RR+ ) /\ B e. RR+ ) -> y e. RR+ )
99 simpr 
 |-  ( ( ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) /\ y e. RR+ ) /\ B e. RR+ ) -> B e. RR+ )
100 98 99 rpdivcld 
 |-  ( ( ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) /\ y e. RR+ ) /\ B e. RR+ ) -> ( y / B ) e. RR+ )
101 simpll 
 |-  ( ( ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) /\ y e. RR+ ) /\ B e. RR+ ) -> A. x e. RR+ A <_ ( ( 1 + x ) x. B ) )
102 oveq2 
 |-  ( x = ( y / B ) -> ( 1 + x ) = ( 1 + ( y / B ) ) )
103 102 oveq1d 
 |-  ( x = ( y / B ) -> ( ( 1 + x ) x. B ) = ( ( 1 + ( y / B ) ) x. B ) )
104 103 breq2d 
 |-  ( x = ( y / B ) -> ( A <_ ( ( 1 + x ) x. B ) <-> A <_ ( ( 1 + ( y / B ) ) x. B ) ) )
105 104 rspcva 
 |-  ( ( ( y / B ) e. RR+ /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) -> A <_ ( ( 1 + ( y / B ) ) x. B ) )
106 100 101 105 syl2anc 
 |-  ( ( ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) /\ y e. RR+ ) /\ B e. RR+ ) -> A <_ ( ( 1 + ( y / B ) ) x. B ) )
107 106 adantlll 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B e. RR+ ) -> A <_ ( ( 1 + ( y / B ) ) x. B ) )
108 1cnd 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> 1 e. CC )
109 81 adantr 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> y e. CC )
110 rpcn 
 |-  ( B e. RR+ -> B e. CC )
111 110 adantl 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> B e. CC )
112 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
113 112 adantl 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> B =/= 0 )
114 109 111 113 divcld 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> ( y / B ) e. CC )
115 108 114 111 adddird 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> ( ( 1 + ( y / B ) ) x. B ) = ( ( 1 x. B ) + ( ( y / B ) x. B ) ) )
116 111 mulid2d 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> ( 1 x. B ) = B )
117 109 111 113 divcan1d 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> ( ( y / B ) x. B ) = y )
118 116 117 oveq12d 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> ( ( 1 x. B ) + ( ( y / B ) x. B ) ) = ( B + y ) )
119 eqidd 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> ( B + y ) = ( B + y ) )
120 115 118 119 3eqtrd 
 |-  ( ( y e. RR+ /\ B e. RR+ ) -> ( ( 1 + ( y / B ) ) x. B ) = ( B + y ) )
121 120 adantll 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B e. RR+ ) -> ( ( 1 + ( y / B ) ) x. B ) = ( B + y ) )
122 107 121 breqtrd 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ B e. RR+ ) -> A <_ ( B + y ) )
123 89 97 122 syl2anc 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) /\ -. B = 0 ) -> A <_ ( B + y ) )
124 88 123 pm2.61dan 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) /\ y e. RR+ ) -> A <_ ( B + y ) )
125 124 ralrimiva 
 |-  ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) -> A. y e. RR+ A <_ ( B + y ) )
126 xralrple 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
127 2 15 126 syl2anc 
 |-  ( ph -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
128 127 adantr 
 |-  ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
129 125 128 mpbird 
 |-  ( ( ph /\ A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) -> A <_ B )
130 129 ex 
 |-  ( ph -> ( A. x e. RR+ A <_ ( ( 1 + x ) x. B ) -> A <_ B ) )
131 42 130 impbid 
 |-  ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) )