Metamath Proof Explorer

Theorem xrralrecnnle

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 xrralrecnnle.n ⊢ Ⅎ 𝑛 𝜑
xrralrecnnle.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xrralrecnnle.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion xrralrecnnle ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 xrralrecnnle.n ⊢ Ⅎ 𝑛 𝜑
2 xrralrecnnle.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
3 xrralrecnnle.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 nfv ⊢ Ⅎ 𝑛 𝐴 ≤ 𝐵
5 1 4 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝐴 ≤ 𝐵 )
6 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ* )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ )
8 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
10 7 9 readdcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ )
11 10 rexrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* )
12 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* )
13 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
14 3 13 syl ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ* )
16 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ≤ 𝐵 )
17 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
18 rpreccl ⊢ ( 𝑛 ∈ ℝ+ → ( 1 / 𝑛 ) ∈ ℝ+ )
19 17 18 syl ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
21 7 20 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 < ( 𝐵 + ( 1 / 𝑛 ) ) )
22 21 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 < ( 𝐵 + ( 1 / 𝑛 ) ) )
23 6 15 12 16 22 xrlelttrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐴 < ( 𝐵 + ( 1 / 𝑛 ) ) )
24 6 12 23 xrltled ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) )
25 24 ex ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝑛 ∈ ℕ → 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )
26 5 25 ralrimi ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) )
27 26 ex ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 → ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )
28 rpgtrecnn ⊢ ( 𝑥 ∈ ℝ+ → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝑥 )
29 28 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝑥 )
30 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) )
31 1 30 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) )
32 nfv ⊢ Ⅎ 𝑛 𝑥 ∈ ℝ+
33 31 32 nfan ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ )
34 nfv ⊢ Ⅎ 𝑛 𝐴 ≤ ( 𝐵 + 𝑥 )
35 simpll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝜑 )
36 rspa ⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) )
37 36 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) )
38 35 37 jca ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )
39 38 adantlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )
40 simplr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ+ )
41 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
42 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → 𝐴 ∈ ℝ* )
43 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
44 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
46 43 45 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + 𝑥 ) ∈ ℝ )
47 46 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + 𝑥 ) ∈ ℝ* )
48 47 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → ( 𝐵 + 𝑥 ) ∈ ℝ* )
49 11 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* )
50 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) )
51 8 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → ( 1 / 𝑛 ) ∈ ℝ )
52 45 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → 𝑥 ∈ ℝ )
53 43 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → 𝐵 ∈ ℝ )
54 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → ( 1 / 𝑛 ) < 𝑥 )
55 51 52 53 54 ltadd2dd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → ( 𝐵 + ( 1 / 𝑛 ) ) < ( 𝐵 + 𝑥 ) )
56 55 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → ( 𝐵 + ( 1 / 𝑛 ) ) < ( 𝐵 + 𝑥 ) )
57 42 49 48 50 56 xrlelttrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → 𝐴 < ( 𝐵 + 𝑥 ) )
58 42 48 57 xrltled ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝑥 ) → 𝐴 ≤ ( 𝐵 + 𝑥 ) )
59 58 ex ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1 / 𝑛 ) < 𝑥 → 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
60 39 40 41 59 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1 / 𝑛 ) < 𝑥 → 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
61 60 ex ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑛 ∈ ℕ → ( ( 1 / 𝑛 ) < 𝑥 → 𝐴 ≤ ( 𝐵 + 𝑥 ) ) ) )
62 33 34 61 rexlimd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝑥 → 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
63 29 62 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 + 𝑥 ) )
64 63 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) → ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) )
65 xralrple ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
66 2 3 65 syl2anc ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
68 64 67 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) → 𝐴 ≤ 𝐵 )
69 68 ex ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) → 𝐴 ≤ 𝐵 ) )
70 27 69 impbid ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑛 ∈ ℕ 𝐴 ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )