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 ⊢ Ⅎ n φ
xrralrecnnge.a ⊢ φ → A ∈ ℝ
xrralrecnnge.b ⊢ φ → B ∈ ℝ *
Assertion xrralrecnnge ⊢ φ → A ≤ B ↔ ∀ n ∈ ℕ A − 1 n ≤ B

Proof

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