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 / 𝑛 ) ) ) )