Metamath Proof Explorer

Theorem xrralrecnnge

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses xrralrecnnge.n ⊢ Ⅎ 𝑛 𝜑
xrralrecnnge.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
xrralrecnnge.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
Assertion xrralrecnnge ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xrralrecnnge.n ⊢ Ⅎ 𝑛 𝜑
2 xrralrecnnge.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 xrralrecnnge.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
4 nfv ⊢ Ⅎ 𝑛 𝐴 ≤ 𝐵
5 1 4 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝐴 ≤ 𝐵 )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ )
7 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
9 6 8 resubcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 − ( 1 / 𝑛 ) ) ∈ ℝ )
10 9 rexrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 − ( 1 / 𝑛 ) ) ∈ ℝ* )
11 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 − ( 1 / 𝑛 ) ) ∈ ℝ* )
12 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ* )
13 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
14 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ* )
15 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
16 15 rpreccld ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
18 6 17 ltsubrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 − ( 1 / 𝑛 ) ) < 𝐴 )
19 18 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 − ( 1 / 𝑛 ) ) < 𝐴 )
20 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ≤ 𝐵 )
21 11 14 12 19 20 xrltletrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 − ( 1 / 𝑛 ) ) < 𝐵 )
22 11 12 21 xrltled ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 )
23 22 ex ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝑛 ∈ ℕ → ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
24 5 23 ralrimi ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 )
25 24 ex ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 → ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
26 pnfxr ⊢ +∞ ∈ ℝ*
27 26 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
28 2 ltpnfd ⊢ ( 𝜑 → 𝐴 < +∞ )
29 13 27 28 xrltled ⊢ ( 𝜑 → 𝐴 ≤ +∞ )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ 𝐵 = +∞ ) → 𝐴 ≤ +∞ )
31 id ⊢ ( 𝐵 = +∞ → 𝐵 = +∞ )
32 31 eqcomd ⊢ ( 𝐵 = +∞ → +∞ = 𝐵 )
33 32 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ 𝐵 = +∞ ) → +∞ = 𝐵 )
34 30 33 breqtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ 𝐵 = +∞ ) → 𝐴 ≤ 𝐵 )
35 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ∈ ℝ* )
36 1nn ⊢ 1 ∈ ℕ
37 36 a1i ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 → 1 ∈ ℕ )
38 id ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 → ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 )
39 oveq2 ⊢ ( 𝑛 = 1 → ( 1 / 𝑛 ) = ( 1 / 1 ) )
40 39 oveq2d ⊢ ( 𝑛 = 1 → ( 𝐴 − ( 1 / 𝑛 ) ) = ( 𝐴 − ( 1 / 1 ) ) )
41 40 breq1d ⊢ ( 𝑛 = 1 → ( ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ↔ ( 𝐴 − ( 1 / 1 ) ) ≤ 𝐵 ) )
42 41 rspcva ⊢ ( ( 1 ∈ ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) → ( 𝐴 − ( 1 / 1 ) ) ≤ 𝐵 )
43 37 38 42 syl2anc ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 → ( 𝐴 − ( 1 / 1 ) ) ≤ 𝐵 )
44 43 adantr ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ∧ 𝐵 = -∞ ) → ( 𝐴 − ( 1 / 1 ) ) ≤ 𝐵 )
45 simpr ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ∧ 𝐵 = -∞ ) → 𝐵 = -∞ )
46 44 45 breqtrd ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ∧ 𝐵 = -∞ ) → ( 𝐴 − ( 1 / 1 ) ) ≤ -∞ )
47 46 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ 𝐵 = -∞ ) → ( 𝐴 − ( 1 / 1 ) ) ≤ -∞ )
48 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
49 ax-1ne0 ⊢ 1 ≠ 0
50 49 a1i ⊢ ( 𝜑 → 1 ≠ 0 )
51 48 48 50 redivcld ⊢ ( 𝜑 → ( 1 / 1 ) ∈ ℝ )
52 2 51 resubcld ⊢ ( 𝜑 → ( 𝐴 − ( 1 / 1 ) ) ∈ ℝ )
53 52 mnfltd ⊢ ( 𝜑 → -∞ < ( 𝐴 − ( 1 / 1 ) ) )
54 mnfxr ⊢ -∞ ∈ ℝ*
55 54 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
56 52 rexrd ⊢ ( 𝜑 → ( 𝐴 − ( 1 / 1 ) ) ∈ ℝ* )
57 55 56 xrltnled ⊢ ( 𝜑 → ( -∞ < ( 𝐴 − ( 1 / 1 ) ) ↔ ¬ ( 𝐴 − ( 1 / 1 ) ) ≤ -∞ ) )
58 53 57 mpbid ⊢ ( 𝜑 → ¬ ( 𝐴 − ( 1 / 1 ) ) ≤ -∞ )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ 𝐵 = -∞ ) → ¬ ( 𝐴 − ( 1 / 1 ) ) ≤ -∞ )
60 47 59 pm2.65da ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) → ¬ 𝐵 = -∞ )
61 60 neqned ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) → 𝐵 ≠ -∞ )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ≠ -∞ )
63 neqne ⊢ ( ¬ 𝐵 = +∞ → 𝐵 ≠ +∞ )
64 63 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ≠ +∞ )
65 35 62 64 xrred ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ∈ ℝ )
66 nfv ⊢ Ⅎ 𝑛 𝐵 ∈ ℝ
67 1 66 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝐵 ∈ ℝ )
68 13 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ* )
69 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
70 67 68 69 xrralrecnnle ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )
71 6 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ )
72 7 adantl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
73 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ )
74 71 72 73 lesubaddd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )
75 74 bicomd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ↔ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
76 67 75 ralbida ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
77 70 76 bitr2d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ↔ 𝐴 ≤ 𝐵 ) )
78 77 biimpd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 → 𝐴 ≤ 𝐵 ) )
79 78 imp ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
80 79 an32s ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ 𝐵 ∈ ℝ ) → 𝐴 ≤ 𝐵 )
81 65 80 syldan ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) ∧ ¬ 𝐵 = +∞ ) → 𝐴 ≤ 𝐵 )
82 34 81 pm2.61dan ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
83 82 ex ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 → 𝐴 ≤ 𝐵 ) )
84 25 83 impbid ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )