Step | Hyp | Ref
| Expression |
1 | | infleinf.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
2 | | infxrcl 13066 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ*
→ inf(𝐴,
ℝ*, < ) ∈ ℝ*) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → inf(𝐴, ℝ*, < ) ∈
ℝ*) |
4 | | pnfge 12865 |
. . . . 5
⊢
(inf(𝐴,
ℝ*, < ) ∈ ℝ* → inf(𝐴, ℝ*, < )
≤ +∞) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤
+∞) |
6 | 5 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = ∅) → inf(𝐴, ℝ*, < ) ≤
+∞) |
7 | | infeq1 9213 |
. . . . . 6
⊢ (𝐵 = ∅ → inf(𝐵, ℝ*, < ) =
inf(∅, ℝ*, < )) |
8 | | xrinf0 13071 |
. . . . . . 7
⊢
inf(∅, ℝ*, < ) = +∞ |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (𝐵 = ∅ → inf(∅,
ℝ*, < ) = +∞) |
10 | 7, 9 | eqtrd 2780 |
. . . . 5
⊢ (𝐵 = ∅ → inf(𝐵, ℝ*, < ) =
+∞) |
11 | 10 | eqcomd 2746 |
. . . 4
⊢ (𝐵 = ∅ → +∞ =
inf(𝐵, ℝ*,
< )) |
12 | 11 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = ∅) → +∞ = inf(𝐵, ℝ*, <
)) |
13 | 6, 12 | breqtrd 5105 |
. 2
⊢ ((𝜑 ∧ 𝐵 = ∅) → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, <
)) |
14 | | neqne 2953 |
. . . 4
⊢ (¬
𝐵 = ∅ → 𝐵 ≠ ∅) |
15 | 14 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐵 = ∅) → 𝐵 ≠ ∅) |
16 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ inf(𝐴,
ℝ*, < ) ∈ ℝ*) |
17 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ → 𝑟 ∈
ℝ) |
18 | | 2re 12047 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
19 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ → 2 ∈
ℝ) |
20 | 17, 19 | resubcld 11403 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ → (𝑟 − 2) ∈
ℝ) |
21 | 20 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
∧ 𝑟 ∈ ℝ)
→ (𝑟 − 2) ∈
ℝ) |
22 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ inf(𝐵,
ℝ*, < ) = -∞) |
23 | | infleinf.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆
ℝ*) |
24 | | infxrunb2 42878 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ⊆ ℝ*
→ (∀𝑦 ∈
ℝ ∃𝑥 ∈
𝐵 𝑥 < 𝑦 ↔ inf(𝐵, ℝ*, < ) =
-∞)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑥 ∈ 𝐵 𝑥 < 𝑦 ↔ inf(𝐵, ℝ*, < ) =
-∞)) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ (∀𝑦 ∈
ℝ ∃𝑥 ∈
𝐵 𝑥 < 𝑦 ↔ inf(𝐵, ℝ*, < ) =
-∞)) |
27 | 22, 26 | mpbird 256 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ ∀𝑦 ∈
ℝ ∃𝑥 ∈
𝐵 𝑥 < 𝑦) |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
∧ 𝑟 ∈ ℝ)
→ ∀𝑦 ∈
ℝ ∃𝑥 ∈
𝐵 𝑥 < 𝑦) |
29 | | breq2 5083 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑟 − 2) → (𝑥 < 𝑦 ↔ 𝑥 < (𝑟 − 2))) |
30 | 29 | rexbidv 3228 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑟 − 2) → (∃𝑥 ∈ 𝐵 𝑥 < 𝑦 ↔ ∃𝑥 ∈ 𝐵 𝑥 < (𝑟 − 2))) |
31 | 30 | rspcva 3559 |
. . . . . . . . . . 11
⊢ (((𝑟 − 2) ∈ ℝ ∧
∀𝑦 ∈ ℝ
∃𝑥 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑥 ∈ 𝐵 𝑥 < (𝑟 − 2)) |
32 | 21, 28, 31 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
∧ 𝑟 ∈ ℝ)
→ ∃𝑥 ∈
𝐵 𝑥 < (𝑟 − 2)) |
33 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜑) |
34 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
35 | | 1rp 12733 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ+ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈
ℝ+) |
37 | | 1ex 10972 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
V |
38 | | eleq1 2828 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 1 → (𝑦 ∈ ℝ+ ↔ 1 ∈
ℝ+)) |
39 | 38 | 3anbi3d 1441 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 1 → ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) ↔ (𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 1 ∈
ℝ+))) |
40 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 1 → (𝑥 +𝑒 𝑦) = (𝑥 +𝑒 1)) |
41 | 40 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 1 → (𝑧 ≤ (𝑥 +𝑒 𝑦) ↔ 𝑧 ≤ (𝑥 +𝑒 1))) |
42 | 41 | rexbidv 3228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 1 → (∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 𝑦) ↔ ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 1))) |
43 | 39, 42 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 1 → (((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 𝑦)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 1 ∈ ℝ+) →
∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 1)))) |
44 | | infleinf.c |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 𝑦)) |
45 | 37, 43, 44 | vtocl 3497 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 1 ∈ ℝ+) →
∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 1)) |
46 | 33, 34, 36, 45 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 1)) |
47 | 46 | adantlr 712 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 1)) |
48 | 47 | 3adant3 1131 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) → ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 1)) |
49 | | simp1l 1196 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) → 𝜑) |
50 | 49 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝜑) |
51 | 50, 1 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝐴 ⊆
ℝ*) |
52 | 50, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝐵 ⊆
ℝ*) |
53 | | simp1r 1197 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) → 𝑟 ∈ ℝ) |
54 | 53 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝑟 ∈
ℝ) |
55 | | simp2 1136 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) → 𝑥 ∈ 𝐵) |
56 | 55 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝑥 ∈ 𝐵) |
57 | | simpll3 1213 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝑥 < (𝑟 − 2)) |
58 | | simplr 766 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝑧 ∈ 𝐴) |
59 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝑧 ≤ (𝑥 +𝑒 1)) |
60 | 51, 52, 54, 56, 57, 58, 59 | infleinflem2 42881 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ≤ (𝑥 +𝑒 1)) → 𝑧 < 𝑟) |
61 | 60 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) ∧ 𝑧 ∈ 𝐴) → (𝑧 ≤ (𝑥 +𝑒 1) → 𝑧 < 𝑟)) |
62 | 61 | reximdva 3205 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) → (∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 1) → ∃𝑧 ∈ 𝐴 𝑧 < 𝑟)) |
63 | 48, 62 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 < (𝑟 − 2)) → ∃𝑧 ∈ 𝐴 𝑧 < 𝑟) |
64 | 63 | 3exp 1118 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (𝑥 ∈ 𝐵 → (𝑥 < (𝑟 − 2) → ∃𝑧 ∈ 𝐴 𝑧 < 𝑟))) |
65 | 64 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
∧ 𝑟 ∈ ℝ)
→ (𝑥 ∈ 𝐵 → (𝑥 < (𝑟 − 2) → ∃𝑧 ∈ 𝐴 𝑧 < 𝑟))) |
66 | 65 | rexlimdv 3214 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
∧ 𝑟 ∈ ℝ)
→ (∃𝑥 ∈
𝐵 𝑥 < (𝑟 − 2) → ∃𝑧 ∈ 𝐴 𝑧 < 𝑟)) |
67 | 32, 66 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
∧ 𝑟 ∈ ℝ)
→ ∃𝑧 ∈
𝐴 𝑧 < 𝑟) |
68 | 67 | ralrimiva 3110 |
. . . . . . . 8
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ ∀𝑟 ∈
ℝ ∃𝑧 ∈
𝐴 𝑧 < 𝑟) |
69 | | infxrunb2 42878 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑟 ∈
ℝ ∃𝑧 ∈
𝐴 𝑧 < 𝑟 ↔ inf(𝐴, ℝ*, < ) =
-∞)) |
70 | 1, 69 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑟 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑧 < 𝑟 ↔ inf(𝐴, ℝ*, < ) =
-∞)) |
71 | 70 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ (∀𝑟 ∈
ℝ ∃𝑧 ∈
𝐴 𝑧 < 𝑟 ↔ inf(𝐴, ℝ*, < ) =
-∞)) |
72 | 68, 71 | mpbid 231 |
. . . . . . 7
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ inf(𝐴,
ℝ*, < ) = -∞) |
73 | 72, 22 | eqtr4d 2783 |
. . . . . 6
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ inf(𝐴,
ℝ*, < ) = inf(𝐵, ℝ*, <
)) |
74 | 16, 73 | xreqled 42840 |
. . . . 5
⊢ ((𝜑 ∧ inf(𝐵, ℝ*, < ) = -∞)
→ inf(𝐴,
ℝ*, < ) ≤ inf(𝐵, ℝ*, <
)) |
75 | 74 | adantlr 712 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ inf(𝐵, ℝ*, < ) = -∞)
→ inf(𝐴,
ℝ*, < ) ≤ inf(𝐵, ℝ*, <
)) |
76 | | mnfxr 11033 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
77 | 76 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → -∞ ∈
ℝ*) |
78 | 77 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ ¬ inf(𝐵, ℝ*, < ) =
-∞) → -∞ ∈ ℝ*) |
79 | | infxrcl 13066 |
. . . . . . . 8
⊢ (𝐵 ⊆ ℝ*
→ inf(𝐵,
ℝ*, < ) ∈ ℝ*) |
80 | 23, 79 | syl 17 |
. . . . . . 7
⊢ (𝜑 → inf(𝐵, ℝ*, < ) ∈
ℝ*) |
81 | 80 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ ¬ inf(𝐵, ℝ*, < ) =
-∞) → inf(𝐵,
ℝ*, < ) ∈ ℝ*) |
82 | | mnfle 12869 |
. . . . . . 7
⊢
(inf(𝐵,
ℝ*, < ) ∈ ℝ* → -∞ ≤
inf(𝐵, ℝ*,
< )) |
83 | 81, 82 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ ¬ inf(𝐵, ℝ*, < ) =
-∞) → -∞ ≤ inf(𝐵, ℝ*, <
)) |
84 | | neqne 2953 |
. . . . . . . 8
⊢ (¬
inf(𝐵, ℝ*,
< ) = -∞ → inf(𝐵, ℝ*, < ) ≠
-∞) |
85 | 84 | necomd 3001 |
. . . . . . 7
⊢ (¬
inf(𝐵, ℝ*,
< ) = -∞ → -∞ ≠ inf(𝐵, ℝ*, <
)) |
86 | 85 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ ¬ inf(𝐵, ℝ*, < ) =
-∞) → -∞ ≠ inf(𝐵, ℝ*, <
)) |
87 | 78, 81, 83, 86 | xrleneltd 42833 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ ¬ inf(𝐵, ℝ*, < ) =
-∞) → -∞ < inf(𝐵, ℝ*, <
)) |
88 | 3 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
→ inf(𝐴,
ℝ*, < ) ∈ ℝ*) |
89 | 80 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
→ inf(𝐵,
ℝ*, < ) ∈ ℝ*) |
90 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑏(((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) |
91 | 23 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) → 𝐵 ⊆
ℝ*) |
92 | | simpllr 773 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) → 𝐵 ≠ ∅) |
93 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ -∞ < inf(𝐵, ℝ*, < ))
→ -∞ < inf(𝐵,
ℝ*, < )) |
94 | | infxrbnd2 42879 |
. . . . . . . . . . . 12
⊢ (𝐵 ⊆ ℝ*
→ (∃𝑏 ∈
ℝ ∀𝑥 ∈
𝐵 𝑏 ≤ 𝑥 ↔ -∞ < inf(𝐵, ℝ*, <
))) |
95 | 23, 94 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝐵 𝑏 ≤ 𝑥 ↔ -∞ < inf(𝐵, ℝ*, <
))) |
96 | 95 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ -∞ < inf(𝐵, ℝ*, < ))
→ (∃𝑏 ∈
ℝ ∀𝑥 ∈
𝐵 𝑏 ≤ 𝑥 ↔ -∞ < inf(𝐵, ℝ*, <
))) |
97 | 93, 96 | mpbird 256 |
. . . . . . . . 9
⊢ ((𝜑 ∧ -∞ < inf(𝐵, ℝ*, < ))
→ ∃𝑏 ∈
ℝ ∀𝑥 ∈
𝐵 𝑏 ≤ 𝑥) |
98 | 97 | ad4ant13 748 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝐵 𝑏 ≤ 𝑥) |
99 | | simpr 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) → 𝑤 ∈ ℝ+) |
100 | 99 | rphalfcld 12783 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) → (𝑤 / 2) ∈
ℝ+) |
101 | 90, 91, 92, 98, 100 | infrpge 42861 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) → ∃𝑥 ∈ 𝐵 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) |
102 | | simpll 764 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵) → 𝜑) |
103 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
104 | | rphalfcl 12756 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℝ+
→ (𝑤 / 2) ∈
ℝ+) |
105 | 104 | ad2antlr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵) → (𝑤 / 2) ∈
ℝ+) |
106 | | ovex 7304 |
. . . . . . . . . . . . . 14
⊢ (𝑤 / 2) ∈ V |
107 | | eleq1 2828 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑤 / 2) → (𝑦 ∈ ℝ+ ↔ (𝑤 / 2) ∈
ℝ+)) |
108 | 107 | 3anbi3d 1441 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 / 2) → ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) ↔ (𝜑 ∧ 𝑥 ∈ 𝐵 ∧ (𝑤 / 2) ∈
ℝ+))) |
109 | | oveq2 7279 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑤 / 2) → (𝑥 +𝑒 𝑦) = (𝑥 +𝑒 (𝑤 / 2))) |
110 | 109 | breq2d 5091 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑤 / 2) → (𝑧 ≤ (𝑥 +𝑒 𝑦) ↔ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2)))) |
111 | 110 | rexbidv 3228 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 / 2) → (∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 𝑦) ↔ ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2)))) |
112 | 108, 111 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑤 / 2) → (((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 𝑦)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ (𝑤 / 2) ∈ ℝ+) →
∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))))) |
113 | 106, 112,
44 | vtocl 3497 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ (𝑤 / 2) ∈ ℝ+) →
∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) |
114 | 102, 103,
105, 113 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵) → ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) |
115 | 114 | 3adant3 1131 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) → ∃𝑧 ∈
𝐴 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) |
116 | | simp11l 1283 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → 𝜑) |
117 | 116, 1 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → 𝐴 ⊆
ℝ*) |
118 | 116, 23 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → 𝐵 ⊆
ℝ*) |
119 | | simp11 1202 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → (𝜑 ∧ 𝑤 ∈
ℝ+)) |
120 | 119 | simprd 496 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → 𝑤 ∈ ℝ+) |
121 | | simp12 1203 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → 𝑥 ∈ 𝐵) |
122 | | simp3 1137 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) → 𝑥 ≤
(inf(𝐵,
ℝ*, < ) +𝑒 (𝑤 / 2))) |
123 | 122 | 3ad2ant1 1132 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) |
124 | | simp2 1136 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → 𝑧 ∈ 𝐴) |
125 | | simp3 1137 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) |
126 | 117, 118,
120, 121, 123, 124, 125 | infleinflem1 42880 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2))) → inf(𝐴, ℝ*, < ) ≤
(inf(𝐵,
ℝ*, < ) +𝑒 𝑤)) |
127 | 126 | 3exp 1118 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) → (𝑧 ∈ 𝐴 → (𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2)) → inf(𝐴, ℝ*, < ) ≤
(inf(𝐵,
ℝ*, < ) +𝑒 𝑤)))) |
128 | 127 | rexlimdv 3214 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) → (∃𝑧
∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 (𝑤 / 2)) → inf(𝐴, ℝ*, < ) ≤
(inf(𝐵,
ℝ*, < ) +𝑒 𝑤))) |
129 | 115, 128 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2))) → inf(𝐴,
ℝ*, < ) ≤ (inf(𝐵, ℝ*, < )
+𝑒 𝑤)) |
130 | 129 | 3exp 1118 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑥 ∈ 𝐵 → (𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2)) → inf(𝐴,
ℝ*, < ) ≤ (inf(𝐵, ℝ*, < )
+𝑒 𝑤)))) |
131 | 130 | rexlimdv 3214 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(∃𝑥 ∈ 𝐵 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2)) → inf(𝐴,
ℝ*, < ) ≤ (inf(𝐵, ℝ*, < )
+𝑒 𝑤))) |
132 | 131 | ad4ant14 749 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) → (∃𝑥 ∈ 𝐵 𝑥 ≤ (inf(𝐵, ℝ*, < )
+𝑒 (𝑤 /
2)) → inf(𝐴,
ℝ*, < ) ≤ (inf(𝐵, ℝ*, < )
+𝑒 𝑤))) |
133 | 101, 132 | mpd 15 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
∧ 𝑤 ∈
ℝ+) → inf(𝐴, ℝ*, < ) ≤
(inf(𝐵,
ℝ*, < ) +𝑒 𝑤)) |
134 | 88, 89, 133 | xrlexaddrp 42862 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ -∞ < inf(𝐵, ℝ*, < ))
→ inf(𝐴,
ℝ*, < ) ≤ inf(𝐵, ℝ*, <
)) |
135 | 87, 134 | syldan 591 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ ∅) ∧ ¬ inf(𝐵, ℝ*, < ) =
-∞) → inf(𝐴,
ℝ*, < ) ≤ inf(𝐵, ℝ*, <
)) |
136 | 75, 135 | pm2.61dan 810 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ ∅) → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, <
)) |
137 | 15, 136 | syldan 591 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐵 = ∅) → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, <
)) |
138 | 13, 137 | pm2.61dan 810 |
1
⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, <
)) |