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

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 mulridi ⊢ ( 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 addridd ⊢ ( ( 𝜑 ∧ 𝐶 = 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 ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) )