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