Metamath Proof Explorer

Theorem xralrple

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Assertion xralrple ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 rpge0 ⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ 𝑥 )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ 𝑥 )
3 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
4 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
5 4 adantl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
6 3 5 addge01d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 0 ≤ 𝑥 ↔ 𝐵 ≤ ( 𝐵 + 𝑥 ) ) )
7 2 6 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ≤ ( 𝐵 + 𝑥 ) )
8 simpll ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ℝ* )
9 3 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ* )
10 3 5 readdcld ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + 𝑥 ) ∈ ℝ )
11 10 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + 𝑥 ) ∈ ℝ* )
12 xrletr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐵 + 𝑥 ) ∈ ℝ* ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ ( 𝐵 + 𝑥 ) ) → 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
13 8 9 11 12 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ ( 𝐵 + 𝑥 ) ) → 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
14 7 13 mpan2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 → 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
15 14 ralrimdva ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 → ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
16 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
17 16 adantl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ* )
18 simpl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ* )
19 qbtwnxr ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 < 𝐴 ) → ∃ 𝑦 ∈ ℚ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) )
20 19 3expia ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐵 < 𝐴 → ∃ 𝑦 ∈ ℚ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) )
21 17 18 20 syl2anc ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 → ∃ 𝑦 ∈ ℚ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) )
22 simprrl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → 𝐵 < 𝑦 )
23 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → 𝐵 ∈ ℝ )
24 qre ⊢ ( 𝑦 ∈ ℚ → 𝑦 ∈ ℝ )
25 24 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → 𝑦 ∈ ℝ )
26 difrp ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐵 < 𝑦 ↔ ( 𝑦 − 𝐵 ) ∈ ℝ+ ) )
27 23 25 26 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ( 𝐵 < 𝑦 ↔ ( 𝑦 − 𝐵 ) ∈ ℝ+ ) )
28 22 27 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ( 𝑦 − 𝐵 ) ∈ ℝ+ )
29 simprrr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → 𝑦 < 𝐴 )
30 25 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → 𝑦 ∈ ℝ* )
31 simpll ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → 𝐴 ∈ ℝ* )
32 xrltnle ⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝑦 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑦 ) )
33 30 31 32 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ( 𝑦 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑦 ) )
34 29 33 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ¬ 𝐴 ≤ 𝑦 )
35 23 recnd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → 𝐵 ∈ ℂ )
36 25 recnd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → 𝑦 ∈ ℂ )
37 35 36 pncan3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ( 𝐵 + ( 𝑦 − 𝐵 ) ) = 𝑦 )
38 37 breq2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ( 𝐴 ≤ ( 𝐵 + ( 𝑦 − 𝐵 ) ) ↔ 𝐴 ≤ 𝑦 ) )
39 34 38 mtbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ¬ 𝐴 ≤ ( 𝐵 + ( 𝑦 − 𝐵 ) ) )
40 oveq2 ⊢ ( 𝑥 = ( 𝑦 − 𝐵 ) → ( 𝐵 + 𝑥 ) = ( 𝐵 + ( 𝑦 − 𝐵 ) ) )
41 40 breq2d ⊢ ( 𝑥 = ( 𝑦 − 𝐵 ) → ( 𝐴 ≤ ( 𝐵 + 𝑥 ) ↔ 𝐴 ≤ ( 𝐵 + ( 𝑦 − 𝐵 ) ) ) )
42 41 notbid ⊢ ( 𝑥 = ( 𝑦 − 𝐵 ) → ( ¬ 𝐴 ≤ ( 𝐵 + 𝑥 ) ↔ ¬ 𝐴 ≤ ( 𝐵 + ( 𝑦 − 𝐵 ) ) ) )
43 42 rspcev ⊢ ( ( ( 𝑦 − 𝐵 ) ∈ ℝ+ ∧ ¬ 𝐴 ≤ ( 𝐵 + ( 𝑦 − 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ+ ¬ 𝐴 ≤ ( 𝐵 + 𝑥 ) )
44 28 39 43 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ∃ 𝑥 ∈ ℝ+ ¬ 𝐴 ≤ ( 𝐵 + 𝑥 ) )
45 rexnal ⊢ ( ∃ 𝑥 ∈ ℝ+ ¬ 𝐴 ≤ ( 𝐵 + 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) )
46 44 45 sylib ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℚ ∧ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) ) ) → ¬ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) )
47 46 rexlimdvaa ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℚ ( 𝐵 < 𝑦 ∧ 𝑦 < 𝐴 ) → ¬ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
48 21 47 syld ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 → ¬ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
49 48 con2d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) → ¬ 𝐵 < 𝐴 ) )
50 xrlenlt ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
51 16 50 sylan2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
52 49 51 sylibrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) → 𝐴 ≤ 𝐵 ) )
53 15 52 impbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )