Metamath Proof Explorer

Theorem xralrple3

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses xralrple3.a 
|- ( ph -> A e. RR* )
xralrple3.b 
|- ( ph -> B e. RR )
xralrple3.c 
|- ( ph -> C e. RR )
xralrple3.g 
|- ( ph -> 0 <_ C )
Assertion xralrple3 
|- ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( B + ( C x. x ) ) ) )

Proof

Step Hyp Ref Expression
1 xralrple3.a 
 |-  ( ph -> A e. RR* )
2 xralrple3.b 
 |-  ( ph -> B e. RR )
3 xralrple3.c 
 |-  ( ph -> C e. RR )
4 xralrple3.g 
 |-  ( ph -> 0 <_ C )
5 1 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A e. RR* )
6 2 rexrd 
 |-  ( ph -> B e. RR* )
7 6 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B e. RR* )
8 2 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B e. RR )
9 3 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> C e. RR )
10 rpre 
 |-  ( x e. RR+ -> x e. RR )
11 10 adantl 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> x e. RR )
12 9 11 remulcld 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> ( C x. x ) e. RR )
13 8 12 readdcld 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> ( B + ( C x. x ) ) e. RR )
14 13 rexrd 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> ( B + ( C x. x ) ) e. RR* )
15 simplr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A <_ B )
16 3 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> C e. RR )
17 10 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
18 4 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ C )
19 rpge0 
 |-  ( x e. RR+ -> 0 <_ x )
20 19 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ x )
21 16 17 18 20 mulge0d 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ ( C x. x ) )
22 2 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> B e. RR )
23 16 17 remulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( C x. x ) e. RR )
24 22 23 addge01d 
 |-  ( ( ph /\ x e. RR+ ) -> ( 0 <_ ( C x. x ) <-> B <_ ( B + ( C x. x ) ) ) )
25 21 24 mpbid 
 |-  ( ( ph /\ x e. RR+ ) -> B <_ ( B + ( C x. x ) ) )
26 25 adantlr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B <_ ( B + ( C x. x ) ) )
27 5 7 14 15 26 xrletrd 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A <_ ( B + ( C x. x ) ) )
28 27 ralrimiva 
 |-  ( ( ph /\ A <_ B ) -> A. x e. RR+ A <_ ( B + ( C x. x ) ) )
29 28 ex 
 |-  ( ph -> ( A <_ B -> A. x e. RR+ A <_ ( B + ( C x. x ) ) ) )
30 1rp 
 |-  1 e. RR+
31 oveq2 
 |-  ( x = 1 -> ( C x. x ) = ( C x. 1 ) )
32 31 oveq2d 
 |-  ( x = 1 -> ( B + ( C x. x ) ) = ( B + ( C x. 1 ) ) )
33 32 breq2d 
 |-  ( x = 1 -> ( A <_ ( B + ( C x. x ) ) <-> A <_ ( B + ( C x. 1 ) ) ) )
34 33 rspcva 
 |-  ( ( 1 e. RR+ /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) -> A <_ ( B + ( C x. 1 ) ) )
35 30 34 mpan 
 |-  ( A. x e. RR+ A <_ ( B + ( C x. x ) ) -> A <_ ( B + ( C x. 1 ) ) )
36 35 ad2antlr 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C = 0 ) -> A <_ ( B + ( C x. 1 ) ) )
37 oveq1 
 |-  ( C = 0 -> ( C x. 1 ) = ( 0 x. 1 ) )
38 0cn 
 |-  0 e. CC
39 38 mulid1i 
 |-  ( 0 x. 1 ) = 0
40 39 a1i 
 |-  ( C = 0 -> ( 0 x. 1 ) = 0 )
41 37 40 eqtrd 
 |-  ( C = 0 -> ( C x. 1 ) = 0 )
42 41 oveq2d 
 |-  ( C = 0 -> ( B + ( C x. 1 ) ) = ( B + 0 ) )
43 42 adantl 
 |-  ( ( ph /\ C = 0 ) -> ( B + ( C x. 1 ) ) = ( B + 0 ) )
44 2 recnd 
 |-  ( ph -> B e. CC )
45 44 adantr 
 |-  ( ( ph /\ C = 0 ) -> B e. CC )
46 45 addid1d 
 |-  ( ( ph /\ C = 0 ) -> ( B + 0 ) = B )
47 43 46 eqtrd 
 |-  ( ( ph /\ C = 0 ) -> ( B + ( C x. 1 ) ) = B )
48 47 adantlr 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C = 0 ) -> ( B + ( C x. 1 ) ) = B )
49 36 48 breqtrd 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C = 0 ) -> A <_ B )
50 neqne 
 |-  ( -. C = 0 -> C =/= 0 )
51 50 adantl 
 |-  ( ( ph /\ -. C = 0 ) -> C =/= 0 )
52 3 adantr 
 |-  ( ( ph /\ C =/= 0 ) -> C e. RR )
53 0red 
 |-  ( ( ph /\ C =/= 0 ) -> 0 e. RR )
54 4 adantr 
 |-  ( ( ph /\ C =/= 0 ) -> 0 <_ C )
55 simpr 
 |-  ( ( ph /\ C =/= 0 ) -> C =/= 0 )
56 53 52 54 55 leneltd 
 |-  ( ( ph /\ C =/= 0 ) -> 0 < C )
57 52 56 elrpd 
 |-  ( ( ph /\ C =/= 0 ) -> C e. RR+ )
58 51 57 syldan 
 |-  ( ( ph /\ -. C = 0 ) -> C e. RR+ )
59 58 adantlr 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ -. C = 0 ) -> C e. RR+ )
60 simpr 
 |-  ( ( C e. RR+ /\ y e. RR+ ) -> y e. RR+ )
61 simpl 
 |-  ( ( C e. RR+ /\ y e. RR+ ) -> C e. RR+ )
62 60 61 rpdivcld 
 |-  ( ( C e. RR+ /\ y e. RR+ ) -> ( y / C ) e. RR+ )
63 62 adantll 
 |-  ( ( ( A. x e. RR+ A <_ ( B + ( C x. x ) ) /\ C e. RR+ ) /\ y e. RR+ ) -> ( y / C ) e. RR+ )
64 simpll 
 |-  ( ( ( A. x e. RR+ A <_ ( B + ( C x. x ) ) /\ C e. RR+ ) /\ y e. RR+ ) -> A. x e. RR+ A <_ ( B + ( C x. x ) ) )
65 oveq2 
 |-  ( x = ( y / C ) -> ( C x. x ) = ( C x. ( y / C ) ) )
66 65 oveq2d 
 |-  ( x = ( y / C ) -> ( B + ( C x. x ) ) = ( B + ( C x. ( y / C ) ) ) )
67 66 breq2d 
 |-  ( x = ( y / C ) -> ( A <_ ( B + ( C x. x ) ) <-> A <_ ( B + ( C x. ( y / C ) ) ) ) )
68 67 rspcva 
 |-  ( ( ( y / C ) e. RR+ /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) -> A <_ ( B + ( C x. ( y / C ) ) ) )
69 63 64 68 syl2anc 
 |-  ( ( ( A. x e. RR+ A <_ ( B + ( C x. x ) ) /\ C e. RR+ ) /\ y e. RR+ ) -> A <_ ( B + ( C x. ( y / C ) ) ) )
70 69 adantlll 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C e. RR+ ) /\ y e. RR+ ) -> A <_ ( B + ( C x. ( y / C ) ) ) )
71 60 rpcnd 
 |-  ( ( C e. RR+ /\ y e. RR+ ) -> y e. CC )
72 61 rpcnd 
 |-  ( ( C e. RR+ /\ y e. RR+ ) -> C e. CC )
73 61 rpne0d 
 |-  ( ( C e. RR+ /\ y e. RR+ ) -> C =/= 0 )
74 71 72 73 divcan2d 
 |-  ( ( C e. RR+ /\ y e. RR+ ) -> ( C x. ( y / C ) ) = y )
75 74 adantll 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C e. RR+ ) /\ y e. RR+ ) -> ( C x. ( y / C ) ) = y )
76 75 oveq2d 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C e. RR+ ) /\ y e. RR+ ) -> ( B + ( C x. ( y / C ) ) ) = ( B + y ) )
77 70 76 breqtrd 
 |-  ( ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C e. RR+ ) /\ y e. RR+ ) -> A <_ ( B + y ) )
78 77 ralrimiva 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C e. RR+ ) -> A. y e. RR+ A <_ ( B + y ) )
79 xralrple 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
80 1 2 79 syl2anc 
 |-  ( ph -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
81 80 ad2antrr 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C e. RR+ ) -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
82 78 81 mpbird 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ C e. RR+ ) -> A <_ B )
83 59 82 syldan 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) /\ -. C = 0 ) -> A <_ B )
84 49 83 pm2.61dan 
 |-  ( ( ph /\ A. x e. RR+ A <_ ( B + ( C x. x ) ) ) -> A <_ B )
85 84 ex 
 |-  ( ph -> ( A. x e. RR+ A <_ ( B + ( C x. x ) ) -> A <_ B ) )
86 29 85 impbid 
 |-  ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( B + ( C x. x ) ) ) )