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 45289
Description: If any element of 𝐴 can be approximated from below by members of 𝐵, then the supremum of 𝐴 is less than 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 11303 . . . . . 6 ℝ ⊆ ℝ*
31, 2sstrdi 4008 . . . . 5 (𝜑𝐴 ⊆ ℝ*)
4 supxrcl 13354 . . . . 5 (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
53, 4syl 17 . . . 4 (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
65adantr 480 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
7 eqidd 2736 . . . 4 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → +∞ = +∞)
8 simpr 484 . . . 4 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) = +∞)
9 peano2re 11432 . . . . . . . . . 10 (𝑤 ∈ ℝ → (𝑤 + 1) ∈ ℝ)
109adantl 481 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → (𝑤 + 1) ∈ ℝ)
113adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐴 ⊆ ℝ*)
12 supxrunb2 13359 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ* → (∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥 ↔ sup(𝐴, ℝ*, < ) = +∞))
1311, 12syl 17 . . . . . . . . . . 11 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → (∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥 ↔ sup(𝐴, ℝ*, < ) = +∞))
148, 13mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → ∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥)
1514adantr 480 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → ∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥)
16 breq1 5151 . . . . . . . . . . 11 (𝑟 = (𝑤 + 1) → (𝑟 < 𝑥 ↔ (𝑤 + 1) < 𝑥))
1716rexbidv 3177 . . . . . . . . . 10 (𝑟 = (𝑤 + 1) → (∃𝑥𝐴 𝑟 < 𝑥 ↔ ∃𝑥𝐴 (𝑤 + 1) < 𝑥))
1817rspcva 3620 . . . . . . . . 9 (((𝑤 + 1) ∈ ℝ ∧ ∀𝑟 ∈ ℝ ∃𝑥𝐴 𝑟 < 𝑥) → ∃𝑥𝐴 (𝑤 + 1) < 𝑥)
1910, 15, 18syl2anc 584 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → ∃𝑥𝐴 (𝑤 + 1) < 𝑥)
20 1rp 13036 . . . . . . . . . . . . . . . 16 1 ∈ ℝ+
2120a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 1 ∈ ℝ+)
22 suplesup.c . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥𝐴𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧)
2322r19.21bi 3249 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → ∀𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧)
24 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑦 = 1 → (𝑥𝑦) = (𝑥 − 1))
2524breq1d 5158 . . . . . . . . . . . . . . . . 17 (𝑦 = 1 → ((𝑥𝑦) < 𝑧 ↔ (𝑥 − 1) < 𝑧))
2625rexbidv 3177 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → (∃𝑧𝐵 (𝑥𝑦) < 𝑧 ↔ ∃𝑧𝐵 (𝑥 − 1) < 𝑧))
2726rspcva 3620 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧) → ∃𝑧𝐵 (𝑥 − 1) < 𝑧)
2821, 23, 27syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → ∃𝑧𝐵 (𝑥 − 1) < 𝑧)
2928adantlr 715 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴) → ∃𝑧𝐵 (𝑥 − 1) < 𝑧)
30293adant3 1131 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → ∃𝑧𝐵 (𝑥 − 1) < 𝑧)
31 nfv 1912 . . . . . . . . . . . . 13 𝑧((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥)
32 simp11r 1284 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑤 ∈ ℝ)
332, 32sselid 3993 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑤 ∈ ℝ*)
341sselda 3995 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 𝑥 ∈ ℝ)
35 1red 11260 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐴) → 1 ∈ ℝ)
3634, 35resubcld 11689 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → (𝑥 − 1) ∈ ℝ)
3736adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴) → (𝑥 − 1) ∈ ℝ)
38373adant3 1131 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → (𝑥 − 1) ∈ ℝ)
39383ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → (𝑥 − 1) ∈ ℝ)
402, 39sselid 3993 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → (𝑥 − 1) ∈ ℝ*)
41 suplesup.b . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ⊆ ℝ*)
4241sselda 3995 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐵) → 𝑧 ∈ ℝ*)
4342adantlr 715 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) → 𝑧 ∈ ℝ*)
44433ad2antl1 1184 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵) → 𝑧 ∈ ℝ*)
45443adant3 1131 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑧 ∈ ℝ*)
46 simp3 1137 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → (𝑤 + 1) < 𝑥)
47 simp1r 1197 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → 𝑤 ∈ ℝ)
48 1red 11260 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → 1 ∈ ℝ)
4934adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
50493adant3 1131 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → 𝑥 ∈ ℝ)
5147, 48, 50ltaddsubd 11861 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → ((𝑤 + 1) < 𝑥𝑤 < (𝑥 − 1)))
5246, 51mpbid 232 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → 𝑤 < (𝑥 − 1))
53523ad2ant1 1132 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑤 < (𝑥 − 1))
54 simp3 1137 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → (𝑥 − 1) < 𝑧)
5533, 40, 45, 53, 54xrlttrd 13198 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) ∧ 𝑧𝐵 ∧ (𝑥 − 1) < 𝑧) → 𝑤 < 𝑧)
56553exp 1118 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → (𝑧𝐵 → ((𝑥 − 1) < 𝑧𝑤 < 𝑧)))
5731, 56reximdai 3259 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → (∃𝑧𝐵 (𝑥 − 1) < 𝑧 → ∃𝑧𝐵 𝑤 < 𝑧))
5830, 57mpd 15 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ℝ) ∧ 𝑥𝐴 ∧ (𝑤 + 1) < 𝑥) → ∃𝑧𝐵 𝑤 < 𝑧)
59583exp 1118 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ) → (𝑥𝐴 → ((𝑤 + 1) < 𝑥 → ∃𝑧𝐵 𝑤 < 𝑧)))
6059adantlr 715 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → (𝑥𝐴 → ((𝑤 + 1) < 𝑥 → ∃𝑧𝐵 𝑤 < 𝑧)))
6160rexlimdv 3151 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → (∃𝑥𝐴 (𝑤 + 1) < 𝑥 → ∃𝑧𝐵 𝑤 < 𝑧))
6219, 61mpd 15 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → ∃𝑧𝐵 𝑤 < 𝑧)
632a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ⊆ ℝ*)
6463sselda 3995 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ) → 𝑤 ∈ ℝ*)
6564ad2antrr 726 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) ∧ 𝑤 < 𝑧) → 𝑤 ∈ ℝ*)
6643adantr 480 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) ∧ 𝑤 < 𝑧) → 𝑧 ∈ ℝ*)
67 simpr 484 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) ∧ 𝑤 < 𝑧) → 𝑤 < 𝑧)
6865, 66, 67xrltled 13189 . . . . . . . . . 10 ((((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) ∧ 𝑤 < 𝑧) → 𝑤𝑧)
6968ex 412 . . . . . . . . 9 (((𝜑𝑤 ∈ ℝ) ∧ 𝑧𝐵) → (𝑤 < 𝑧𝑤𝑧))
7069adantllr 719 . . . . . . . 8 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) ∧ 𝑧𝐵) → (𝑤 < 𝑧𝑤𝑧))
7170reximdva 3166 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → (∃𝑧𝐵 𝑤 < 𝑧 → ∃𝑧𝐵 𝑤𝑧))
7262, 71mpd 15 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝑤 ∈ ℝ) → ∃𝑧𝐵 𝑤𝑧)
7372ralrimiva 3144 . . . . 5 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → ∀𝑤 ∈ ℝ ∃𝑧𝐵 𝑤𝑧)
74 supxrunb1 13358 . . . . . . 7 (𝐵 ⊆ ℝ* → (∀𝑤 ∈ ℝ ∃𝑧𝐵 𝑤𝑧 ↔ sup(𝐵, ℝ*, < ) = +∞))
7541, 74syl 17 . . . . . 6 (𝜑 → (∀𝑤 ∈ ℝ ∃𝑧𝐵 𝑤𝑧 ↔ sup(𝐵, ℝ*, < ) = +∞))
7675adantr 480 . . . . 5 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → (∀𝑤 ∈ ℝ ∃𝑧𝐵 𝑤𝑧 ↔ sup(𝐵, ℝ*, < ) = +∞))
7773, 76mpbid 232 . . . 4 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐵, ℝ*, < ) = +∞)
787, 8, 773eqtr4d 2785 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) = sup(𝐵, ℝ*, < ))
796, 78xreqled 45280 . 2 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
80 supeq1 9483 . . . . . . 7 (𝐴 = ∅ → sup(𝐴, ℝ*, < ) = sup(∅, ℝ*, < ))
81 xrsup0 13362 . . . . . . . 8 sup(∅, ℝ*, < ) = -∞
8281a1i 11 . . . . . . 7 (𝐴 = ∅ → sup(∅, ℝ*, < ) = -∞)
8380, 82eqtrd 2775 . . . . . 6 (𝐴 = ∅ → sup(𝐴, ℝ*, < ) = -∞)
8483adantl 481 . . . . 5 ((𝜑𝐴 = ∅) → sup(𝐴, ℝ*, < ) = -∞)
85 supxrcl 13354 . . . . . . . 8 (𝐵 ⊆ ℝ* → sup(𝐵, ℝ*, < ) ∈ ℝ*)
8641, 85syl 17 . . . . . . 7 (𝜑 → sup(𝐵, ℝ*, < ) ∈ ℝ*)
87 mnfle 13174 . . . . . . 7 (sup(𝐵, ℝ*, < ) ∈ ℝ* → -∞ ≤ sup(𝐵, ℝ*, < ))
8886, 87syl 17 . . . . . 6 (𝜑 → -∞ ≤ sup(𝐵, ℝ*, < ))
8988adantr 480 . . . . 5 ((𝜑𝐴 = ∅) → -∞ ≤ sup(𝐵, ℝ*, < ))
9084, 89eqbrtrd 5170 . . . 4 ((𝜑𝐴 = ∅) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
9190adantlr 715 . . 3 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
92 simpll 767 . . . 4 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → 𝜑)
931adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ⊆ ℝ)
94 neqne 2946 . . . . . . . . 9 𝐴 = ∅ → 𝐴 ≠ ∅)
9594adantl 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ≠ ∅)
96 supxrgtmnf 13368 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → -∞ < sup(𝐴, ℝ*, < ))
9793, 95, 96syl2anc 584 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → -∞ < sup(𝐴, ℝ*, < ))
9897adantlr 715 . . . . . 6 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → -∞ < sup(𝐴, ℝ*, < ))
99 simpr 484 . . . . . . . . 9 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ sup(𝐴, ℝ*, < ) = +∞)
100 simpl 482 . . . . . . . . . 10 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝜑)
101 nltpnft 13203 . . . . . . . . . 10 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
102100, 5, 1013syl 18 . . . . . . . . 9 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
10399, 102mtbid 324 . . . . . . . 8 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ ¬ sup(𝐴, ℝ*, < ) < +∞)
104 notnotr 130 . . . . . . . 8 (¬ ¬ sup(𝐴, ℝ*, < ) < +∞ → sup(𝐴, ℝ*, < ) < +∞)
105103, 104syl 17 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) < +∞)
106105adantr 480 . . . . . 6 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) < +∞)
10798, 106jca 511 . . . . 5 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞))
10892, 5syl 17 . . . . . 6 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
109 xrrebnd 13207 . . . . . 6 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
110108, 109syl 17 . . . . 5 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
111107, 110mpbird 257 . . . 4 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) ∈ ℝ)
112 nfv 1912 . . . . 5 𝑤(𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ)
11341adantr 480 . . . . 5 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ⊆ ℝ*)
114 simpr 484 . . . . 5 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℝ)
115114adantr 480 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → sup(𝐴, ℝ*, < ) ∈ ℝ)
116 simpr 484 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
117116rphalfcld 13087 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) ∈ ℝ+)
118115, 117ltsubrpd 13107 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < sup(𝐴, ℝ*, < ))
1193ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → 𝐴 ⊆ ℝ*)
120 rpre 13041 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+𝑤 ∈ ℝ)
121 2re 12338 . . . . . . . . . . . . 13 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+ → 2 ∈ ℝ)
123 2ne0 12368 . . . . . . . . . . . . 13 2 ≠ 0
124123a1i 11 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+ → 2 ≠ 0)
125120, 122, 124redivcld 12093 . . . . . . . . . . 11 (𝑤 ∈ ℝ+ → (𝑤 / 2) ∈ ℝ)
126125adantl 481 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) ∈ ℝ)
127115, 126resubcld 11689 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) ∈ ℝ)
1282, 127sselid 3993 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) ∈ ℝ*)
129 supxrlub 13364 . . . . . . . 8 ((𝐴 ⊆ ℝ* ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) ∈ ℝ*) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < sup(𝐴, ℝ*, < ) ↔ ∃𝑥𝐴 (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥))
130119, 128, 129syl2anc 584 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < sup(𝐴, ℝ*, < ) ↔ ∃𝑥𝐴 (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥))
131118, 130mpbid 232 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → ∃𝑥𝐴 (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥)
132 rphalfcl 13060 . . . . . . . . . . 11 (𝑤 ∈ ℝ+ → (𝑤 / 2) ∈ ℝ+)
1331323ad2ant2 1133 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+𝑥𝐴) → (𝑤 / 2) ∈ ℝ+)
134233adant2 1130 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+𝑥𝐴) → ∀𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧)
135 oveq2 7439 . . . . . . . . . . . . 13 (𝑦 = (𝑤 / 2) → (𝑥𝑦) = (𝑥 − (𝑤 / 2)))
136135breq1d 5158 . . . . . . . . . . . 12 (𝑦 = (𝑤 / 2) → ((𝑥𝑦) < 𝑧 ↔ (𝑥 − (𝑤 / 2)) < 𝑧))
137136rexbidv 3177 . . . . . . . . . . 11 (𝑦 = (𝑤 / 2) → (∃𝑧𝐵 (𝑥𝑦) < 𝑧 ↔ ∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧))
138137rspcva 3620 . . . . . . . . . 10 (((𝑤 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑧𝐵 (𝑥𝑦) < 𝑧) → ∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧)
139133, 134, 138syl2anc 584 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+𝑥𝐴) → ∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧)
140139ad5ant134 1366 . . . . . . . 8 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) → ∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧)
141 recn 11243 . . . . . . . . . . . . . . . . 17 (sup(𝐴, ℝ*, < ) ∈ ℝ → sup(𝐴, ℝ*, < ) ∈ ℂ)
142141adantr 480 . . . . . . . . . . . . . . . 16 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → sup(𝐴, ℝ*, < ) ∈ ℂ)
143120recnd 11287 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℝ+𝑤 ∈ ℂ)
144143adantl 481 . . . . . . . . . . . . . . . . 17 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℂ)
145144halfcld 12509 . . . . . . . . . . . . . . . 16 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) ∈ ℂ)
146142, 145, 145subsub4d 11649 . . . . . . . . . . . . . . 15 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) = (sup(𝐴, ℝ*, < ) − ((𝑤 / 2) + (𝑤 / 2))))
1471432halvesd 12510 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℝ+ → ((𝑤 / 2) + (𝑤 / 2)) = 𝑤)
148147oveq2d 7447 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ+ → (sup(𝐴, ℝ*, < ) − ((𝑤 / 2) + (𝑤 / 2))) = (sup(𝐴, ℝ*, < ) − 𝑤))
149148adantl 481 . . . . . . . . . . . . . . 15 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − ((𝑤 / 2) + (𝑤 / 2))) = (sup(𝐴, ℝ*, < ) − 𝑤))
150146, 149eqtr2d 2776 . . . . . . . . . . . . . 14 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − 𝑤) = ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)))
151150adantll 714 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (sup(𝐴, ℝ*, < ) − 𝑤) = ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)))
152151adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → (sup(𝐴, ℝ*, < ) − 𝑤) = ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)))
153152ad3antrrr 730 . . . . . . . . . . 11 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (sup(𝐴, ℝ*, < ) − 𝑤) = ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)))
154127, 126resubcld 11689 . . . . . . . . . . . . . . 15 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) ∈ ℝ)
155154adantr 480 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) ∈ ℝ)
156155ad3antrrr 730 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) ∈ ℝ)
1572, 156sselid 3993 . . . . . . . . . . . 12 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) ∈ ℝ*)
158120, 49sylanl2 681 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
159125ad2antlr 727 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → (𝑤 / 2) ∈ ℝ)
160158, 159resubcld 11689 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → (𝑥 − (𝑤 / 2)) ∈ ℝ)
161160adantllr 719 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) → (𝑥 − (𝑤 / 2)) ∈ ℝ)
162161ad3antrrr 730 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (𝑥 − (𝑤 / 2)) ∈ ℝ)
1632, 162sselid 3993 . . . . . . . . . . . 12 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (𝑥 − (𝑤 / 2)) ∈ ℝ*)
164 simp-6l 787 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝜑)
165 simplr 769 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑧𝐵)
166164, 165, 42syl2anc 584 . . . . . . . . . . . 12 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑧 ∈ ℝ*)
167 simp-6r 788 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → sup(𝐴, ℝ*, < ) ∈ ℝ)
168120ad5antlr 735 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑤 ∈ ℝ)
169168rehalfcld 12511 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (𝑤 / 2) ∈ ℝ)
170167, 169resubcld 11689 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) ∈ ℝ)
171 simp-4r 784 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑥𝐴)
172164, 171, 34syl2anc 584 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → 𝑥 ∈ ℝ)
173 simpllr 776 . . . . . . . . . . . . 13 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥)
174170, 172, 169, 173ltsub1dd 11873 . . . . . . . . . . . 12 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) < (𝑥 − (𝑤 / 2)))
175 simpr 484 . . . . . . . . . . . 12 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (𝑥 − (𝑤 / 2)) < 𝑧)
176157, 163, 166, 174, 175xrlttrd 13198 . . . . . . . . . . 11 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → ((sup(𝐴, ℝ*, < ) − (𝑤 / 2)) − (𝑤 / 2)) < 𝑧)
177153, 176eqbrtrd 5170 . . . . . . . . . 10 (((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) ∧ (𝑥 − (𝑤 / 2)) < 𝑧) → (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧)
178177ex 412 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) ∧ 𝑧𝐵) → ((𝑥 − (𝑤 / 2)) < 𝑧 → (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧))
179178reximdva 3166 . . . . . . . 8 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) → (∃𝑧𝐵 (𝑥 − (𝑤 / 2)) < 𝑧 → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧))
180140, 179mpd 15 . . . . . . 7 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) ∧ 𝑥𝐴) ∧ (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥) → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧)
181180rexlimdva2 3155 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → (∃𝑥𝐴 (sup(𝐴, ℝ*, < ) − (𝑤 / 2)) < 𝑥 → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧))
182131, 181mpd 15 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑤 ∈ ℝ+) → ∃𝑧𝐵 (sup(𝐴, ℝ*, < ) − 𝑤) < 𝑧)
183112, 113, 114, 182supxrgere 45283 . . . 4 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
18492, 111, 183syl2anc 584 . . 3 (((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
18591, 184pm2.61dan 813 . 2 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
18679, 185pm2.61dan 813 1 (𝜑 → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wral 3059  wrex 3068  wss 3963  c0 4339   class class class wbr 5148  (class class class)co 7431  supcsup 9478  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156  +∞cpnf 11290  -∞cmnf 11291  *cxr 11292   < clt 11293  cle 11294  cmin 11490   / cdiv 11918  2c2 12319  +crp 13032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-sup 9480  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-2 12327  df-rp 13033
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator