This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑥 𝜑
xralrple2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xralrple2.b ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion xralrple2 ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( ( 1 + 𝑥 ) · 𝐵 ) ) )

Proof

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