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 ( 𝜑𝐴 ∈ ℝ* )
xralrple3.b ( 𝜑𝐵 ∈ ℝ )
xralrple3.c ( 𝜑𝐶 ∈ ℝ )
xralrple3.g ( 𝜑 → 0 ≤ 𝐶 )
Assertion xralrple3 ( 𝜑 → ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) )

Proof

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