Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  suplesup Structured version   Visualization version   GIF version

Theorem suplesup 40071
Description: If any element of 𝐴 can be approximated from below by members of 𝐵, then the supremum of 𝐴 is smaller or equal to the supremum of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
suplesup.a (𝜑𝐴 ⊆ ℝ)
suplesup.b (𝜑𝐵 ⊆ ℝ*)
suplesup.c (𝜑 → ∀𝑥𝐴𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧)
Assertion
Ref Expression
suplesup (𝜑 → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
Distinct variable groups:   𝑥,𝐴,𝑧   𝑥,𝐵,𝑦,𝑧   𝜑,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)

Proof of Theorem suplesup
Dummy variables 𝑟 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suplesup.a . . . . . 6 (𝜑𝐴 ⊆ ℝ)
2 ressxr 10295 . . . . . 6 ℝ ⊆ ℝ*
31, 2syl6ss 3756 . . . . 5 (𝜑𝐴 ⊆ ℝ*)
4 supxrcl 12358 . . . . 5 (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
53, 4syl 17 . . . 4 (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
65adantr 472 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
7 eqidd 2761 . . . 4 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → +∞ = +∞)
8 simpr 479 . . . 4 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) = +∞)
9 peano2re 10421 . . . . . . . . . 10 (𝑤 ∈ ℝ → (𝑤 + 1) ∈ ℝ)
109adantl 473 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → (𝑤 + 1) ∈ ℝ)
113adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐴 ⊆ ℝ*)
12 supxrunb2 12363 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ* → (∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥 ↔ sup(𝐴, ℝ*, < ) = +∞))
1311, 12syl 17 . . . . . . . . . . 11 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → (∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥 ↔ sup(𝐴, ℝ*, < ) = +∞))
148, 13mpbird 247 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → ∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥)
1514adantr 472 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → ∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥)
16 breq1 4807 . . . . . . . . . . 11 (𝑟 = (𝑤 + 1) → (𝑟 < 𝑥 ↔ (𝑤 + 1) < 𝑥))
1716rexbidv 3190 . . . . . . . . . 10 (𝑟 = (𝑤 + 1) → (∃𝑥𝐴 𝑟 < 𝑥 ↔ ∃𝑥𝐴 (𝑤 + 1) < 𝑥))
1817rspcva 3447 . . . . . . . . 9 (((𝑤 + 1) ∈ ℝ ∧ ∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥) → ∃𝑥𝐴 (𝑤 + 1) < 𝑥)
1910, 15, 18syl2anc 696 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → ∃𝑥𝐴 (𝑤 + 1) < 𝑥)
20 1rp 12049 . . . . . . . . . . . . . . . 16 1 ∈ ℝ+
2120a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 1 ∈ ℝ+)
22 suplesup.c . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥𝐴𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧)
2322r19.21bi 3070 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → ∀𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧)
24 oveq2 6822 . . . . . . . . . . . . . . . . . 18 (𝑦 = 1 → (𝑥𝑦) = (𝑥 − 1))
2524breq1d 4814 . . . . . . . . . . . . . . . . 17 (𝑦 = 1 → ((𝑥𝑦) < 𝑧 ↔ (𝑥 − 1) < 𝑧))
2625rexbidv 3190 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → (∃𝑧𝐵 (𝑥𝑦) < 𝑧 ↔ ∃𝑧𝐵 (𝑥 − 1) < 𝑧))
2726rspcva 3447 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧) → ∃𝑧𝐵 (𝑥 − 1) < 𝑧)
2821, 23, 27syl2anc 696 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → ∃𝑧𝐵 (𝑥 − 1) < 𝑧)
2928adantlr 753 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴) → ∃𝑧𝐵 (𝑥 − 1) < 𝑧)
30293adant3 1127 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → ∃𝑧𝐵 (𝑥 − 1) < 𝑧)
31 nfv 1992 . . . . . . . . . . . . 13 𝑧((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥)
32 simp11r 1370 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑤 ∈ ℝ)
332, 32sseldi 3742 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑤 ∈ ℝ*)
341sselda 3744 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 𝑥 ∈ ℝ)
35 1red 10267 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 1 ∈ ℝ)
3634, 35resubcld 10670 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝑥 − 1) ∈ ℝ)
3736adantlr 753 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴) → (𝑥 − 1) ∈ ℝ)
38373adant3 1127 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → (𝑥 − 1) ∈ ℝ)
39383ad2ant1 1128 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → (𝑥 − 1) ∈ ℝ)
402, 39sseldi 3742 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → (𝑥 − 1) ∈ ℝ*)
41 suplesup.b . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ⊆ ℝ*)
4241sselda 3744 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐵) → 𝑧 ∈ ℝ*)
4342adantlr 753 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) → 𝑧 ∈ ℝ*)
44433ad2antl1 1201 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵) → 𝑧 ∈ ℝ*)
45443adant3 1127 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑧 ∈ ℝ*)
46 simp3 1133 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → (𝑤 + 1) < 𝑥)
47 simp1r 1241 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → 𝑤 ∈ ℝ)
48 1red 10267 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → 1 ∈ ℝ)
4934adantlr 753 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
50493adant3 1127 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → 𝑥 ∈ ℝ)
5147, 48, 50ltaddsubd 10839 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → ((𝑤 + 1) < 𝑥𝑤 < (𝑥 − 1)))
5246, 51mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → 𝑤 < (𝑥 − 1))
53523ad2ant1 1128 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑤 < (𝑥 − 1))
54 simp3 1133 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → (𝑥 − 1) < 𝑧)
5533, 40, 45, 53, 54xrlttrd 12203 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑤 < 𝑧)
56553exp 1113 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → (𝑧𝐵 → ((𝑥 − 1) < 𝑧𝑤 < 𝑧)))
5731, 56reximdai 3150 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → (∃𝑧𝐵 (𝑥 − 1) < 𝑧 → ∃𝑧𝐵 𝑤 < 𝑧))
5830, 57mpd 15 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → ∃𝑧𝐵 𝑤 < 𝑧)
59583exp 1113 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ) → (𝑥𝐴 → ((𝑤 + 1) < 𝑥 → ∃𝑧𝐵 𝑤 < 𝑧)))
6059adantlr 753 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → (𝑥𝐴 → ((𝑤 + 1) < 𝑥 → ∃𝑧𝐵 𝑤 < 𝑧)))
6160rexlimdv 3168 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → (∃𝑥𝐴 (𝑤 + 1) < 𝑥 → ∃𝑧𝐵 𝑤 < 𝑧))
6219, 61mpd 15 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → ∃𝑧𝐵 𝑤 < 𝑧)
632a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ⊆ ℝ*)
6463sselda 3744 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ) → 𝑤 ∈ ℝ*)
6564ad2antrr 764 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) ∧ 𝑤 < 𝑧) → 𝑤 ∈ ℝ*)
6643adantr 472 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) ∧ 𝑤 < 𝑧) → 𝑧 ∈ ℝ*)
67 simpr 479 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) ∧ 𝑤 < 𝑧) → 𝑤 < 𝑧)
6865, 66, 67xrltled 40003 . . . . . . . . . 10 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) ∧ 𝑤 < 𝑧) → 𝑤𝑧)
6968ex 449 . . . . . . . . 9 (((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) → (𝑤 < 𝑧𝑤𝑧))
7069adantllr 757 . . . . . . . 8 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) ∧ 𝑧𝐵) → (𝑤 < 𝑧𝑤𝑧))
7170reximdva 3155 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → (∃𝑧𝐵 𝑤 < 𝑧 → ∃𝑧𝐵 𝑤𝑧))
7262, 71mpd 15 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → ∃𝑧𝐵 𝑤𝑧)
7372ralrimiva 3104 . . . . 5 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → ∀𝑤 ∈ ℝ ∃𝑧𝐵 𝑤𝑧)
74 supxrunb1 12362 . . . . . . 7 (𝐵 ⊆ ℝ* → (∀𝑤 ∈ ℝ ∃𝑧𝐵 𝑤𝑧 ↔ sup(𝐵, ℝ*, < ) = +∞))
7541, 74syl 17 . . . . . 6 (𝜑 → (∀𝑤 ∈ ℝ ∃𝑧𝐵 𝑤𝑧 ↔ sup(𝐵, ℝ*, < ) = +∞))
7675adantr 472 . . . . 5 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → (∀𝑤 ∈ ℝ ∃𝑧𝐵 𝑤𝑧 ↔ sup(𝐵, ℝ*, < ) = +∞))
7773, 76mpbid 222 . . . 4 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐵, ℝ*, < ) = +∞)
787, 8, 773eqtr4d 2804 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) = sup(𝐵, ℝ*, < ))
796, 78xreqled 40062 . 2 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
80 supeq1 8518 . . . . . . 7 (𝐴 = ∅ → sup(𝐴, ℝ*, < ) = sup(∅, ℝ*, < ))
81 xrsup0 12366 . . . . . . . 8 sup(∅, ℝ*, < ) = -∞
8281a1i 11 . . . . . . 7 (𝐴 = ∅ → sup(∅, ℝ*, < ) = -∞)
8380, 82eqtrd 2794 . . . . . 6 (𝐴 = ∅ → sup(𝐴, ℝ*, < ) = -∞)
8483adantl 473 . . . . 5 ((𝜑𝐴 = ∅) → sup(𝐴, ℝ*, < ) = -∞)
85 supxrcl 12358 . . . . . . . 8 (𝐵 ⊆ ℝ* → sup(𝐵, ℝ*, < ) ∈ ℝ*)
8641, 85syl 17 . . . . . . 7 (𝜑 → sup(𝐵, ℝ*, < ) ∈ ℝ*)
87 mnfle 12182 . . . . . . 7 (sup(𝐵, ℝ*, < ) ∈ ℝ* → -∞ ≤ sup(𝐵, ℝ*, < ))
8886, 87syl 17 . . . . . 6 (𝜑 → -∞ ≤ sup(𝐵, ℝ*, < ))
8988adantr 472 . . . . 5 ((𝜑𝐴 = ∅) → -∞ ≤ sup(𝐵, ℝ*, < ))
9084, 89eqbrtrd 4826 . . . 4 ((𝜑𝐴 = ∅) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
9190adantlr 753 . . 3 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
92 simpll 807 . . . 4 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → 𝜑)
931adantr 472 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ⊆ ℝ)
94 neqne 2940 . . . . . . . . 9 𝐴 = ∅ → 𝐴 ≠ ∅)
9594adantl 473 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ≠ ∅)
96 supxrgtmnf 12372 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → -∞ < sup(𝐴, ℝ*, < ))
9793, 95, 96syl2anc 696 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → -∞ < sup(𝐴, ℝ*, < ))
9897adantlr 753 . . . . . 6 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → -∞ < sup(𝐴, ℝ*, < ))
99 simpr 479 . . . . . . . . 9 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ sup(𝐴, ℝ*, < ) = +∞)
100 simpl 474 . . . . . . . . . 10 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝜑)
101 nltpnft 12208 . . . . . . . . . 10 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
102100, 5, 1013syl 18 . . . . . . . . 9 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
10399, 102mtbid 313 . . . . . . . 8 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ ¬ sup(𝐴, ℝ*, < ) < +∞)
104 notnotr 125 . . . . . . . 8 (¬ ¬ sup(𝐴, ℝ*, < ) < +∞ → sup(𝐴, ℝ*, < ) < +∞)
105103, 104syl 17 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) < +∞)
106105adantr 472 . . . . . 6 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) < +∞)
10798, 106jca 555 . . . . 5 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞))
10892, 5syl 17 . . . . . 6 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
109 xrrebnd 12212 . . . . . 6 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
110108, 109syl 17 . . . . 5 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
111107, 110mpbird 247 . . . 4 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) ∈ ℝ)
112 nfv 1992 . . . . 5 𝑤(𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ)
11341adantr 472 . . . . 5 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ⊆ ℝ*)
114 simpr 479 . . . . 5 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℝ)
115114adantr 472 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → sup(𝐴, ℝ*, < ) ∈ ℝ)
116 simpr 479 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
117116rphalfcld 12097 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) ∈ ℝ+)
118115, 117ltsubrpd 12117 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < sup(𝐴, ℝ*, < ))
1193ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → 𝐴 ⊆ ℝ*)
120 rpre 12052 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+𝑤 ∈ ℝ)
121 2re 11302 . . . . . . . . . . . . 13 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+ → 2 ∈ ℝ)
123 2ne0 11325 . . . . . . . . . . . . 13 2 ≠ 0
124123a1i 11 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+ → 2 ≠ 0)
125120, 122, 124redivcld 11065 . . . . . . . . . . 11 (𝑤 ∈ ℝ+ → (𝑤 / 2) ∈ ℝ)
126125adantl 473 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) ∈ ℝ)
127115, 126resubcld 10670 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) ∈ ℝ)
1282, 127sseldi 3742 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) ∈ ℝ*)
129 supxrlub 12368 . . . . . . . 8 ((𝐴 ⊆ ℝ* ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) ∈ ℝ*) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < sup(𝐴, ℝ*, < ) ↔ ∃𝑥𝐴 (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥))
130119, 128, 129syl2anc 696 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < sup(𝐴, ℝ*, < ) ↔ ∃𝑥𝐴 (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥))
131118, 130mpbid 222 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → ∃𝑥𝐴 (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥)
132 rphalfcl 12071 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+ → (𝑤 / 2) ∈ ℝ+)
1331323ad2ant2 1129 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+𝑥𝐴) → (𝑤 / 2) ∈ ℝ+)
134233adant2 1126 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+𝑥𝐴) → ∀𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧)
135 oveq2 6822 . . . . . . . . . . . . . 14 (𝑦 = (𝑤 / 2) → (𝑥𝑦) = (𝑥 − (𝑤 / 2)))
136135breq1d 4814 . . . . . . . . . . . . 13 (𝑦 = (𝑤 / 2) → ((𝑥𝑦) < 𝑧 ↔ (𝑥 − (𝑤 / 2)) < 𝑧))
137136rexbidv 3190 . . . . . . . . . . . 12 (𝑦 = (𝑤 / 2) → (∃𝑧𝐵 (𝑥𝑦) < 𝑧 ↔ ∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧))
138137rspcva 3447 . . . . . . . . . . 11 (((𝑤 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧) → ∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧)
139133, 134, 138syl2anc 696 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+𝑥𝐴) → ∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧)
140139ad5ant134 1467 . . . . . . . . 9 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) → ∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧)
141 recn 10238 . . . . . . . . . . . . . . . . . 18 (sup(𝐴, ℝ*, < ) ∈ ℝ → sup(𝐴, ℝ*, < ) ∈ ℂ)
142141adantr 472 . . . . . . . . . . . . . . . . 17 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → sup(𝐴, ℝ*, < ) ∈ ℂ)
143120recnd 10280 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℝ+𝑤 ∈ ℂ)
144143adantl 473 . . . . . . . . . . . . . . . . . 18 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℂ)
145144halfcld 11489 . . . . . . . . . . . . . . . . 17 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) ∈ ℂ)
146142, 145, 145subsub4d 10635 . . . . . . . . . . . . . . . 16 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) = (sup(𝐴, ℝ*, < ) − ((𝑤 / 2) + (𝑤 / 2))))
1471432halvesd 11490 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℝ+ → ((𝑤 / 2) + (𝑤 / 2)) = 𝑤)
148147oveq2d 6830 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℝ+ → (sup(𝐴, ℝ*, < ) − ((𝑤 / 2) + (𝑤 / 2))) = (sup(𝐴, ℝ*, < ) − 𝑤))
149148adantl 473 . . . . . . . . . . . . . . . 16 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − ((𝑤 / 2) + (𝑤 / 2))) = (sup(𝐴, ℝ*, < ) − 𝑤))
150146, 149eqtr2d 2795 . . . . . . . . . . . . . . 15 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − 𝑤) = ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)))
151150adantll 752 . . . . . . . . . . . . . 14 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − 𝑤) = ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)))
152151adantr 472 . . . . . . . . . . . . 13 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → (sup(𝐴, ℝ*, < ) − 𝑤) = ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)))
153152ad3antrrr 768 . . . . . . . . . . . 12 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (sup(𝐴, ℝ*, < ) − 𝑤) = ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)))
154127, 126resubcld 10670 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) ∈ ℝ)
155154adantr 472 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) ∈ ℝ)
156155ad3antrrr 768 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) ∈ ℝ)
1572, 156sseldi 3742 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) ∈ ℝ*)
158120, 49sylanl2 686 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
159125ad2antlr 765 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → (𝑤 / 2) ∈ ℝ)
160158, 159resubcld 10670 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → (𝑥 − (𝑤 / 2)) ∈ ℝ)
161160adantllr 757 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → (𝑥 − (𝑤 / 2)) ∈ ℝ)
162161ad3antrrr 768 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (𝑥 − (𝑤 / 2)) ∈ ℝ)
1632, 162sseldi 3742 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (𝑥 − (𝑤 / 2)) ∈ ℝ*)
164 simp-6l 833 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝜑)
165 simplr 809 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑧𝐵)
166164, 165, 42syl2anc 696 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑧 ∈ ℝ*)
167 simp-6r 835 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → sup(𝐴, ℝ*, < ) ∈ ℝ)
168120ad5antlr 777 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑤 ∈ ℝ)
169168rehalfcld 11491 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (𝑤 / 2) ∈ ℝ)
170167, 169resubcld 10670 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) ∈ ℝ)
171 simp-4r 827 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑥𝐴)
172164, 171, 34syl2anc 696 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑥 ∈ ℝ)
173 simpllr 817 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥)
174170, 172, 169, 173ltsub1dd 10851 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) < (𝑥 − (𝑤 / 2)))
175 simpr 479 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (𝑥 − (𝑤 / 2)) < 𝑧)
176157, 163, 166, 174, 175xrlttrd 12203 . . . . . . . . . . . 12 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) < 𝑧)
177153, 176eqbrtrd 4826 . . . . . . . . . . 11 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧)
178177ex 449 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) → ((𝑥 − (𝑤 / 2)) < 𝑧 → (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧))
179178reximdva 3155 . . . . . . . . 9 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) → (∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧 → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧))
180140, 179mpd 15 . . . . . . . 8 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧)
181180ex 449 . . . . . . 7 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥 → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧))
182181rexlimdva 3169 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (∃𝑥𝐴 (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥 → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧))
183131, 182mpd 15 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧)
184112, 113, 114, 183supxrgere 40065 . . . 4 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
18592, 111, 184syl2anc 696 . . 3 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
18691, 185pm2.61dan 867 . 2 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
18779, 186pm2.61dan 867 1 (𝜑 → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  wss 3715  c0 4058   class class class wbr 4804  (class class class)co 6814  supcsup 8513  cc 10146  cr 10147  0cc0 10148  1c1 10149   + caddc 10151  +∞cpnf 10283  -∞cmnf 10284  *cxr 10285   < clt 10286  cle 10287  cmin 10478   / cdiv 10896  2c2 11282  +crp 12045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-sup 8515  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-2 11291  df-rp 12046
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator