Metamath Proof Explorer

Theorem suplesup

Description: If any element of A can be approximated from below by members of B , then the supremum of A is less than or equal to the supremum of B . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses suplesup.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
suplesup.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
suplesup.c ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 𝑦 ) < 𝑧 )
Assertion suplesup ( 𝜑 → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 suplesup.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 suplesup.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
3 suplesup.c ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 𝑦 ) < 𝑧 )
4 ressxr ⊢ ℝ ⊆ ℝ*
5 1 4 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
6 supxrcl ⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
7 5 6 syl ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
8 7 adantr ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
9 eqidd ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → +∞ = +∞ )
10 simpr ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
11 peano2re ⊢ ( 𝑤 ∈ ℝ → ( 𝑤 + 1 ) ∈ ℝ )
12 11 adantl ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) → ( 𝑤 + 1 ) ∈ ℝ )
13 5 adantr ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝐴 ⊆ ℝ* )
14 supxrunb2 ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 < 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
15 13 14 syl ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 < 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
16 10 15 mpbird ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 < 𝑥 )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) → ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 < 𝑥 )
18 breq1 ⊢ ( 𝑟 = ( 𝑤 + 1 ) → ( 𝑟 < 𝑥 ↔ ( 𝑤 + 1 ) < 𝑥 ) )
19 18 rexbidv ⊢ ( 𝑟 = ( 𝑤 + 1 ) → ( ∃ 𝑥 ∈ 𝐴 𝑟 < 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑤 + 1 ) < 𝑥 ) )
20 19 rspcva ⊢ ( ( ( 𝑤 + 1 ) ∈ ℝ ∧ ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 < 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ( 𝑤 + 1 ) < 𝑥 )
21 12 17 20 syl2anc ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑥 ∈ 𝐴 ( 𝑤 + 1 ) < 𝑥 )
22 1rp ⊢ 1 ∈ ℝ+
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 1 ∈ ℝ+ )
24 3 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 𝑦 ) < 𝑧 )
25 oveq2 ⊢ ( 𝑦 = 1 → ( 𝑥 − 𝑦 ) = ( 𝑥 − 1 ) )
26 25 breq1d ⊢ ( 𝑦 = 1 → ( ( 𝑥 − 𝑦 ) < 𝑧 ↔ ( 𝑥 − 1 ) < 𝑧 ) )
27 26 rexbidv ⊢ ( 𝑦 = 1 → ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 𝑦 ) < 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 1 ) < 𝑧 ) )
28 27 rspcva ⊢ ( ( 1 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 𝑦 ) < 𝑧 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 1 ) < 𝑧 )
29 23 24 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 1 ) < 𝑧 )
30 29 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 1 ) < 𝑧 )
31 30 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 1 ) < 𝑧 )
32 nfv ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 )
33 simp11r ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑥 − 1 ) < 𝑧 ) → 𝑤 ∈ ℝ )
34 4 33 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑥 − 1 ) < 𝑧 ) → 𝑤 ∈ ℝ* )
35 1 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
36 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 1 ∈ ℝ )
37 35 36 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 − 1 ) ∈ ℝ )
38 37 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 − 1 ) ∈ ℝ )
39 38 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → ( 𝑥 − 1 ) ∈ ℝ )
40 39 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑥 − 1 ) < 𝑧 ) → ( 𝑥 − 1 ) ∈ ℝ )
41 4 40 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑥 − 1 ) < 𝑧 ) → ( 𝑥 − 1 ) ∈ ℝ* )
42 2 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ℝ* )
43 42 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ℝ* )
44 43 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ℝ* )
45 44 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑥 − 1 ) < 𝑧 ) → 𝑧 ∈ ℝ* )
46 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → ( 𝑤 + 1 ) < 𝑥 )
47 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → 𝑤 ∈ ℝ )
48 1red ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → 1 ∈ ℝ )
49 35 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
50 49 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → 𝑥 ∈ ℝ )
51 47 48 50 ltaddsubd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → ( ( 𝑤 + 1 ) < 𝑥 ↔ 𝑤 < ( 𝑥 − 1 ) ) )
52 46 51 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → 𝑤 < ( 𝑥 − 1 ) )
53 52 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑥 − 1 ) < 𝑧 ) → 𝑤 < ( 𝑥 − 1 ) )
54 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑥 − 1 ) < 𝑧 ) → ( 𝑥 − 1 ) < 𝑧 )
55 34 41 45 53 54 xrlttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑥 − 1 ) < 𝑧 ) → 𝑤 < 𝑧 )
56 55 3exp ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → ( 𝑧 ∈ 𝐵 → ( ( 𝑥 − 1 ) < 𝑧 → 𝑤 < 𝑧 ) ) )
57 32 56 reximdai ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 1 ) < 𝑧 → ∃ 𝑧 ∈ 𝐵 𝑤 < 𝑧 ) )
58 31 57 mpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝑤 + 1 ) < 𝑥 ) → ∃ 𝑧 ∈ 𝐵 𝑤 < 𝑧 )
59 58 3exp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 → ( ( 𝑤 + 1 ) < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 < 𝑧 ) ) )
60 59 adantlr ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 → ( ( 𝑤 + 1 ) < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 < 𝑧 ) ) )
61 60 rexlimdv ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝑤 + 1 ) < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 < 𝑧 ) )
62 21 61 mpd ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑧 ∈ 𝐵 𝑤 < 𝑧 )
63 4 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
64 63 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ* )
65 64 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 < 𝑧 ) → 𝑤 ∈ ℝ* )
66 43 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 < 𝑧 ) → 𝑧 ∈ ℝ* )
67 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 < 𝑧 ) → 𝑤 < 𝑧 )
68 65 66 67 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 < 𝑧 ) → 𝑤 ≤ 𝑧 )
69 68 ex ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑤 < 𝑧 → 𝑤 ≤ 𝑧 ) )
70 69 adantllr ⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑤 < 𝑧 → 𝑤 ≤ 𝑧 ) )
71 70 reximdva ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐵 𝑤 < 𝑧 → ∃ 𝑧 ∈ 𝐵 𝑤 ≤ 𝑧 ) )
72 62 71 mpd ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑧 ∈ 𝐵 𝑤 ≤ 𝑧 )
73 72 ralrimiva ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ∀ 𝑤 ∈ ℝ ∃ 𝑧 ∈ 𝐵 𝑤 ≤ 𝑧 )
74 supxrunb1 ⊢ ( 𝐵 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑧 ∈ 𝐵 𝑤 ≤ 𝑧 ↔ sup ( 𝐵 , ℝ* , < ) = +∞ ) )
75 2 74 syl ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ ℝ ∃ 𝑧 ∈ 𝐵 𝑤 ≤ 𝑧 ↔ sup ( 𝐵 , ℝ* , < ) = +∞ ) )
76 75 adantr ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( ∀ 𝑤 ∈ ℝ ∃ 𝑧 ∈ 𝐵 𝑤 ≤ 𝑧 ↔ sup ( 𝐵 , ℝ* , < ) = +∞ ) )
77 73 76 mpbid ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐵 , ℝ* , < ) = +∞ )
78 9 10 77 3eqtr4d ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) = sup ( 𝐵 , ℝ* , < ) )
79 8 78 xreqled ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )
80 supeq1 ⊢ ( 𝐴 = ∅ → sup ( 𝐴 , ℝ* , < ) = sup ( ∅ , ℝ* , < ) )
81 xrsup0 ⊢ sup ( ∅ , ℝ* , < ) = -∞
82 81 a1i ⊢ ( 𝐴 = ∅ → sup ( ∅ , ℝ* , < ) = -∞ )
83 80 82 eqtrd ⊢ ( 𝐴 = ∅ → sup ( 𝐴 , ℝ* , < ) = -∞ )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) = -∞ )
85 supxrcl ⊢ ( 𝐵 ⊆ ℝ* → sup ( 𝐵 , ℝ* , < ) ∈ ℝ* )
86 2 85 syl ⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) ∈ ℝ* )
87 mnfle ⊢ ( sup ( 𝐵 , ℝ* , < ) ∈ ℝ* → -∞ ≤ sup ( 𝐵 , ℝ* , < ) )
88 86 87 syl ⊢ ( 𝜑 → -∞ ≤ sup ( 𝐵 , ℝ* , < ) )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → -∞ ≤ sup ( 𝐵 , ℝ* , < ) )
90 84 89 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )
91 90 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )
92 simpll ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ ¬ 𝐴 = ∅ ) → 𝜑 )
93 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ⊆ ℝ )
94 neqne ⊢ ( ¬ 𝐴 = ∅ → 𝐴 ≠ ∅ )
95 94 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ≠ ∅ )
96 supxrgtmnf ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → -∞ < sup ( 𝐴 , ℝ* , < ) )
97 93 95 96 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → -∞ < sup ( 𝐴 , ℝ* , < ) )
98 97 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ ¬ 𝐴 = ∅ ) → -∞ < sup ( 𝐴 , ℝ* , < ) )
99 simpr ⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ¬ sup ( 𝐴 , ℝ* , < ) = +∞ )
100 simpl ⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝜑 )
101 nltpnft ⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
102 100 7 101 3syl ⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
103 99 102 mtbid ⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ¬ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ )
104 notnotr ⊢ ( ¬ ¬ sup ( 𝐴 , ℝ* , < ) < +∞ → sup ( 𝐴 , ℝ* , < ) < +∞ )
105 103 104 syl ⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) < +∞ )
106 105 adantr ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) < +∞ )
107 98 106 jca ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ ¬ 𝐴 = ∅ ) → ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) )
108 92 7 syl ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
109 xrrebnd ⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
110 108 109 syl ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ ¬ 𝐴 = ∅ ) → ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ* , < ) ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) ) )
111 107 110 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
112 nfv ⊢ Ⅎ 𝑤 ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
113 2 adantr ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) → 𝐵 ⊆ ℝ* )
114 simpr ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
115 114 adantr ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
116 simpr ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ )
117 116 rphalfcld ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 / 2 ) ∈ ℝ+ )
118 115 117 ltsubrpd ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < sup ( 𝐴 , ℝ* , < ) )
119 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → 𝐴 ⊆ ℝ* )
120 rpre ⊢ ( 𝑤 ∈ ℝ+ → 𝑤 ∈ ℝ )
121 2re ⊢ 2 ∈ ℝ
122 121 a1i ⊢ ( 𝑤 ∈ ℝ+ → 2 ∈ ℝ )
123 2ne0 ⊢ 2 ≠ 0
124 123 a1i ⊢ ( 𝑤 ∈ ℝ+ → 2 ≠ 0 )
125 120 122 124 redivcld ⊢ ( 𝑤 ∈ ℝ+ → ( 𝑤 / 2 ) ∈ ℝ )
126 125 adantl ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 / 2 ) ∈ ℝ )
127 115 126 resubcld ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) ∈ ℝ )
128 4 127 sselid ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) ∈ ℝ* )
129 supxrlub ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) ∈ ℝ* ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < sup ( 𝐴 , ℝ* , < ) ↔ ∃ 𝑥 ∈ 𝐴 ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) )
130 119 128 129 syl2anc ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < sup ( 𝐴 , ℝ* , < ) ↔ ∃ 𝑥 ∈ 𝐴 ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) )
131 118 130 mpbid ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝐴 ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 )
132 rphalfcl ⊢ ( 𝑤 ∈ ℝ+ → ( 𝑤 / 2 ) ∈ ℝ+ )
133 132 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 / 2 ) ∈ ℝ+ )
134 24 3adant2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 𝑦 ) < 𝑧 )
135 oveq2 ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( 𝑥 − 𝑦 ) = ( 𝑥 − ( 𝑤 / 2 ) ) )
136 135 breq1d ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( ( 𝑥 − 𝑦 ) < 𝑧 ↔ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) )
137 136 rexbidv ⊢ ( 𝑦 = ( 𝑤 / 2 ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 𝑦 ) < 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) )
138 137 rspcva ⊢ ( ( ( 𝑤 / 2 ) ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ 𝐵 ( 𝑥 − 𝑦 ) < 𝑧 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 )
139 133 134 138 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 )
140 139 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 )
141 recn ⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ → sup ( 𝐴 , ℝ* , < ) ∈ ℂ )
142 141 adantr ⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℂ )
143 120 recnd ⊢ ( 𝑤 ∈ ℝ+ → 𝑤 ∈ ℂ )
144 143 adantl ⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℂ )
145 144 halfcld ⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 / 2 ) ∈ ℂ )
146 142 145 145 subsub4d ⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+ ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) = ( sup ( 𝐴 , ℝ* , < ) − ( ( 𝑤 / 2 ) + ( 𝑤 / 2 ) ) ) )
147 143 2halvesd ⊢ ( 𝑤 ∈ ℝ+ → ( ( 𝑤 / 2 ) + ( 𝑤 / 2 ) ) = 𝑤 )
148 147 oveq2d ⊢ ( 𝑤 ∈ ℝ+ → ( sup ( 𝐴 , ℝ* , < ) − ( ( 𝑤 / 2 ) + ( 𝑤 / 2 ) ) ) = ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) )
149 148 adantl ⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+ ) → ( sup ( 𝐴 , ℝ* , < ) − ( ( 𝑤 / 2 ) + ( 𝑤 / 2 ) ) ) = ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) )
150 146 149 eqtr2d ⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ ∧ 𝑤 ∈ ℝ+ ) → ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) = ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) )
151 150 adantll ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) = ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) )
152 151 adantr ⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) = ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) )
153 152 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) = ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) )
154 127 126 resubcld ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) ∈ ℝ )
155 154 adantr ⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) ∈ ℝ )
156 155 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) ∈ ℝ )
157 4 156 sselid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) ∈ ℝ* )
158 120 49 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
159 125 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 / 2 ) ∈ ℝ )
160 158 159 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 − ( 𝑤 / 2 ) ) ∈ ℝ )
161 160 adantllr ⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 − ( 𝑤 / 2 ) ) ∈ ℝ )
162 161 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( 𝑥 − ( 𝑤 / 2 ) ) ∈ ℝ )
163 4 162 sselid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( 𝑥 − ( 𝑤 / 2 ) ) ∈ ℝ* )
164 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → 𝜑 )
165 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → 𝑧 ∈ 𝐵 )
166 164 165 42 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → 𝑧 ∈ ℝ* )
167 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
168 120 ad5antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → 𝑤 ∈ ℝ )
169 168 rehalfcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( 𝑤 / 2 ) ∈ ℝ )
170 167 169 resubcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) ∈ ℝ )
171 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → 𝑥 ∈ 𝐴 )
172 164 171 35 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → 𝑥 ∈ ℝ )
173 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 )
174 170 172 169 173 ltsub1dd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) < ( 𝑥 − ( 𝑤 / 2 ) ) )
175 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 )
176 157 163 166 174 175 xrlttrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) − ( 𝑤 / 2 ) ) < 𝑧 )
177 153 176 eqbrtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 ) → ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) < 𝑧 )
178 177 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 → ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) < 𝑧 ) )
179 178 reximdva ⊢ ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 − ( 𝑤 / 2 ) ) < 𝑧 → ∃ 𝑧 ∈ 𝐵 ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) < 𝑧 ) )
180 140 179 mpd ⊢ ( ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 ) → ∃ 𝑧 ∈ 𝐵 ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) < 𝑧 )
181 180 rexlimdva2 ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑥 ∈ 𝐴 ( sup ( 𝐴 , ℝ* , < ) − ( 𝑤 / 2 ) ) < 𝑥 → ∃ 𝑧 ∈ 𝐵 ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) < 𝑧 ) )
182 131 181 mpd ⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐵 ( sup ( 𝐴 , ℝ* , < ) − 𝑤 ) < 𝑧 )
183 112 113 114 182 supxrgere ⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ* , < ) ∈ ℝ ) → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )
184 92 111 183 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )
185 91 184 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ* , < ) = +∞ ) → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )
186 79 185 pm2.61dan ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )