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 xφ
xralrple2.a φA*
xralrple2.b φB0+∞
Assertion xralrple2 φABx+A1+xB

Proof

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