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

Theorem supxrgelem 45353
Description: If an extended real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
supxrgelem.xph 𝑥𝜑
supxrgelem.a (𝜑𝐴 ⊆ ℝ*)
supxrgelem.b (𝜑𝐵 ∈ ℝ*)
supxrgelem.y ((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥))
Assertion
Ref Expression
supxrgelem (𝜑𝐵 ≤ sup(𝐴, ℝ*, < ))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem supxrgelem
StepHypRef Expression
1 supxrgelem.b . . . . 5 (𝜑𝐵 ∈ ℝ*)
2 pnfge 13173 . . . . 5 (𝐵 ∈ ℝ*𝐵 ≤ +∞)
31, 2syl 17 . . . 4 (𝜑𝐵 ≤ +∞)
43adantr 480 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ +∞)
5 id 22 . . . . 5 (sup(𝐴, ℝ*, < ) = +∞ → sup(𝐴, ℝ*, < ) = +∞)
65eqcomd 2742 . . . 4 (sup(𝐴, ℝ*, < ) = +∞ → +∞ = sup(𝐴, ℝ*, < ))
76adantl 481 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → +∞ = sup(𝐴, ℝ*, < ))
84, 7breqtrd 5168 . 2 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
9 simpl 482 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝜑)
10 1rp 13039 . . . . . . . 8 1 ∈ ℝ+
11 nfcv 2904 . . . . . . . . . 10 𝑥1
12 supxrgelem.xph . . . . . . . . . . . 12 𝑥𝜑
13 nfv 1913 . . . . . . . . . . . 12 𝑥1 ∈ ℝ+
1412, 13nfan 1898 . . . . . . . . . . 11 𝑥(𝜑 ∧ 1 ∈ ℝ+)
15 nfv 1913 . . . . . . . . . . 11 𝑥𝑦𝐴 𝐵 < (𝑦 +𝑒 1)
1614, 15nfim 1895 . . . . . . . . . 10 𝑥((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
17 eleq1 2828 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈ ℝ+))
1817anbi2d 630 . . . . . . . . . . 11 (𝑥 = 1 → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈ ℝ+)))
19 oveq2 7440 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 1))
2019breq2d 5154 . . . . . . . . . . . 12 (𝑥 = 1 → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 1)))
2120rexbidv 3178 . . . . . . . . . . 11 (𝑥 = 1 → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1)))
2218, 21imbi12d 344 . . . . . . . . . 10 (𝑥 = 1 → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))))
23 supxrgelem.y . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥))
2411, 16, 22, 23vtoclgf 3568 . . . . . . . . 9 (1 ∈ ℝ+ → ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1)))
2510, 24ax-mp 5 . . . . . . . 8 ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
2610, 25mpan2 691 . . . . . . 7 (𝜑 → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
2726adantr 480 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
28 mnfxr 11319 . . . . . . . . . . 11 -∞ ∈ ℝ*
2928a1i 11 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ ∈ ℝ*)
30 supxrgelem.a . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ*)
3130sselda 3982 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ*)
32313adant3 1132 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝑦 ∈ ℝ*)
33 supxrcl 13358 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
3430, 33syl 17 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
35343ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
36 simpl3 1193 . . . . . . . . . . . 12 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → 𝐵 < (𝑦 +𝑒 1))
37 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ < 𝑦)
3831adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*)
39 ngtmnft 13209 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ* → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦))
4038, 39syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦))
4137, 40mpbird 257 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
4241oveq1d 7447 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = (-∞ +𝑒 1))
43 1xr 11321 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
4443a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 1 ∈ ℝ*)
45 1re 11262 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
46 renepnf 11310 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ → 1 ≠ +∞)
4745, 46ax-mp 5 . . . . . . . . . . . . . . . 16 1 ≠ +∞
4847a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 1 ≠ +∞)
49 xaddmnf2 13272 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ* ∧ 1 ≠ +∞) → (-∞ +𝑒 1) = -∞)
5044, 48, 49syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (-∞ +𝑒 1) = -∞)
5142, 50eqtrd 2776 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = -∞)
52513adantl3 1168 . . . . . . . . . . . 12 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = -∞)
5336, 52breqtrd 5168 . . . . . . . . . . 11 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → 𝐵 < -∞)
54 nltmnf 13172 . . . . . . . . . . . . . 14 (𝐵 ∈ ℝ* → ¬ 𝐵 < -∞)
551, 54syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐵 < -∞)
5655adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
57563ad2antl1 1185 . . . . . . . . . . 11 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
5853, 57condan 817 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ < 𝑦)
5930adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝐴 ⊆ ℝ*)
60 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦𝐴)
61 supxrub 13367 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ*𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6259, 60, 61syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
63623adant3 1132 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6429, 32, 35, 58, 63xrltletrd 13204 . . . . . . . . 9 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ < sup(𝐴, ℝ*, < ))
65643exp 1119 . . . . . . . 8 (𝜑 → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < ))))
6665adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < ))))
6766rexlimdv 3152 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < )))
6827, 67mpd 15 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → -∞ < sup(𝐴, ℝ*, < ))
69 simpr 484 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ sup(𝐴, ℝ*, < ) = +∞)
70 nltpnft 13207 . . . . . . . . 9 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7134, 70syl 17 . . . . . . . 8 (𝜑 → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7271adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7369, 72mtbid 324 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ ¬ sup(𝐴, ℝ*, < ) < +∞)
7473notnotrd 133 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) < +∞)
7568, 74jca 511 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞))
7634adantr 480 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
77 xrrebnd 13211 . . . . 5 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
7876, 77syl 17 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
7975, 78mpbird 257 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ)
80 simpl 482 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ))
81 simpr 484 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ 𝐵 ≤ sup(𝐴, ℝ*, < ))
8234adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
831adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → 𝐵 ∈ ℝ*)
84 xrltnle 11329 . . . . . . . 8 ((sup(𝐴, ℝ*, < ) ∈ ℝ*𝐵 ∈ ℝ*) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8582, 83, 84syl2anc 584 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8685adantlr 715 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8781, 86mpbird 257 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) < 𝐵)
88 simpll 766 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝜑)
8928a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ ∈ ℝ*)
9088, 34syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
9188, 1syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ*)
92 mnfle 13178 . . . . . . . . . . . . . 14 (sup(𝐴, ℝ*, < ) ∈ ℝ* → -∞ ≤ sup(𝐴, ℝ*, < ))
9334, 92syl 17 . . . . . . . . . . . . 13 (𝜑 → -∞ ≤ sup(𝐴, ℝ*, < ))
9493ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ ≤ sup(𝐴, ℝ*, < ))
95 simpr 484 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) < 𝐵)
9689, 90, 91, 94, 95xrlelttrd 13203 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ < 𝐵)
97 id 22 . . . . . . . . . . . . . 14 (𝜑𝜑)
9810a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℝ+)
9997, 98, 25syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
10099ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
10113ad2ant1 1133 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 ∈ ℝ*)
10243a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 1 ∈ ℝ*)
10332, 102jca 511 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*))
104 xaddcl 13282 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑦 +𝑒 1) ∈ ℝ*)
105103, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ∈ ℝ*)
106 pnfxr 11316 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
107106a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → +∞ ∈ ℝ*)
108 simp3 1138 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 < (𝑦 +𝑒 1))
10931, 43, 104sylancl 586 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐴) → (𝑦 +𝑒 1) ∈ ℝ*)
110 pnfge 13173 . . . . . . . . . . . . . . . . . 18 ((𝑦 +𝑒 1) ∈ ℝ* → (𝑦 +𝑒 1) ≤ +∞)
111109, 110syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴) → (𝑦 +𝑒 1) ≤ +∞)
1121113adant3 1132 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ≤ +∞)
113101, 105, 107, 108, 112xrltletrd 13204 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 < +∞)
1141133exp 1119 . . . . . . . . . . . . . 14 (𝜑 → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞)))
115114rexlimdv 3152 . . . . . . . . . . . . 13 (𝜑 → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞))
11688, 115syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞))
117100, 116mpd 15 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 < +∞)
11896, 117jca 511 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (-∞ < 𝐵𝐵 < +∞))
119 xrrebnd 13211 . . . . . . . . . . 11 (𝐵 ∈ ℝ* → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵𝐵 < +∞)))
12091, 119syl 17 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵𝐵 < +∞)))
121118, 120mpbird 257 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
122 simpr 484 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℝ)
123122adantr 480 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈ ℝ)
124121, 123resubcld 11692 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
12526, 115mpd 15 . . . . . . . . . . . . 13 (𝜑𝐵 < +∞)
126125ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 < +∞)
12796, 126jca 511 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (-∞ < 𝐵𝐵 < +∞))
128127, 120mpbird 257 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
129123, 128posdifd 11851 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ 0 < (𝐵 − sup(𝐴, ℝ*, < ))))
13095, 129mpbid 232 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 0 < (𝐵 − sup(𝐴, ℝ*, < )))
131124, 130elrpd 13075 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
132 ovex 7465 . . . . . . . 8 (𝐵 − sup(𝐴, ℝ*, < )) ∈ V
133 nfcv 2904 . . . . . . . . 9 𝑥(𝐵 − sup(𝐴, ℝ*, < ))
134 nfv 1913 . . . . . . . . . . 11 𝑥(𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+
13512, 134nfan 1898 . . . . . . . . . 10 𝑥(𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
136 nfv 1913 . . . . . . . . . 10 𝑥𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))
137135, 136nfim 1895 . . . . . . . . 9 𝑥((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
138 eleq1 2828 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑥 ∈ ℝ+ ↔ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+))
139138anbi2d 630 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)))
140 oveq2 7440 . . . . . . . . . . . 12 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
141140breq2d 5154 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
142141rexbidv 3178 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
143139, 142imbi12d 344 . . . . . . . . 9 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))))
144133, 137, 143, 23vtoclgf 3568 . . . . . . . 8 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ V → ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
145132, 144ax-mp 5 . . . . . . 7 ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
14688, 131, 145syl2anc 584 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
147 ltpnf 13163 . . . . . . . . . . . . 13 (sup(𝐴, ℝ*, < ) ∈ ℝ → sup(𝐴, ℝ*, < ) < +∞)
148147adantr 480 . . . . . . . . . . . 12 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < +∞)
149 id 22 . . . . . . . . . . . . . 14 (𝑦 = +∞ → 𝑦 = +∞)
150149eqcomd 2742 . . . . . . . . . . . . 13 (𝑦 = +∞ → +∞ = 𝑦)
151150adantl 481 . . . . . . . . . . . 12 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → +∞ = 𝑦)
152148, 151breqtrd 5168 . . . . . . . . . . 11 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
153152adantll 714 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
154153ad5ant15 758 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
155 simplll 774 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵))
156 simpl 482 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
15788, 41sylanl1 680 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
158157adantlr 715 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
159 simplr 768 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
160 oveq1 7439 . . . . . . . . . . . . . . . . . 18 (𝑦 = -∞ → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
161160adantl 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
162128, 123resubcld 11692 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
163162rexrd 11312 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ*)
164163ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ*)
165 renepnf 11310 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
166124, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
167166ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
168 xaddmnf2 13272 . . . . . . . . . . . . . . . . . 18 (((𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ* ∧ (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
169164, 167, 168syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
170161, 169eqtrd 2776 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
171159, 170breqtrd 5168 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < -∞)
172156, 158, 171syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → 𝐵 < -∞)
17355ad5antr 734 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
174172, 173condan 817 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → -∞ < 𝑦)
175174adantr 480 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → -∞ < 𝑦)
176 simp3 1138 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → ¬ 𝑦 = +∞)
177313adant3 1132 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*)
178 nltpnft 13207 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ* → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞))
179177, 178syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞))
180176, 179mtbid 324 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → ¬ ¬ 𝑦 < +∞)
181180notnotrd 133 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
1821813adant1r 1177 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
183182ad5ant135 1369 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
184175, 183jca 511 . . . . . . . . . . 11 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → (-∞ < 𝑦𝑦 < +∞))
18531adantlr 715 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦𝐴) → 𝑦 ∈ ℝ*)
186185ad5ant13 756 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*)
187 xrrebnd 13211 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦𝑦 < +∞)))
188186, 187syl 17 . . . . . . . . . . 11 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦𝑦 < +∞)))
189184, 188mpbird 257 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ)
190 simplr 768 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
191121ad2antrr 726 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝐵 ∈ ℝ)
192 simpr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
193124adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
194 rexadd 13275 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))))
195192, 193, 194syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))))
196192, 193readdcld 11291 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
197195, 196eqeltrd 2840 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
198197adantr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
199 simpr 484 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
200191, 198, 191, 199ltsub1dd 11876 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝐵𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵))
201121recnd 11290 . . . . . . . . . . . . . . 15 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℂ)
202201subidd 11609 . . . . . . . . . . . . . 14 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵𝐵) = 0)
203202ad2antrr 726 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝐵𝐵) = 0)
204201adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝐵 ∈ ℂ)
205192recnd 11290 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
206122recnd 11290 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
207206ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
208205, 207subcld 11621 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 − sup(𝐴, ℝ*, < )) ∈ ℂ)
209205, 204, 207addsub12d 11644 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))))
210195, 209eqtrd 2776 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))))
211204, 208, 210mvrladdd 11677 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
212211adantr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
213203, 212breq12d 5155 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → ((𝐵𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) ↔ 0 < (𝑦 − sup(𝐴, ℝ*, < ))))
214200, 213mpbid 232 . . . . . . . . . . 11 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 0 < (𝑦 − sup(𝐴, ℝ*, < )))
215123ad2antrr 726 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) ∈ ℝ)
216 simplr 768 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝑦 ∈ ℝ)
217215, 216posdifd 11851 . . . . . . . . . . 11 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (sup(𝐴, ℝ*, < ) < 𝑦 ↔ 0 < (𝑦 − sup(𝐴, ℝ*, < ))))
218214, 217mpbird 257 . . . . . . . . . 10 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) < 𝑦)
219155, 189, 190, 218syl21anc 837 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
220154, 219pm2.61dan 812 . . . . . . . 8 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) < 𝑦)
221220ex 412 . . . . . . 7 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) → (𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) → sup(𝐴, ℝ*, < ) < 𝑦))
222221reximdva 3167 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦))
223146, 222mpd 15 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
22480, 87, 223syl2anc 584 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
22559, 33syl 17 . . . . . . . . 9 ((𝜑𝑦𝐴) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
22631, 225xrlenltd 11328 . . . . . . . 8 ((𝜑𝑦𝐴) → (𝑦 ≤ sup(𝐴, ℝ*, < ) ↔ ¬ sup(𝐴, ℝ*, < ) < 𝑦))
22762, 226mpbid 232 . . . . . . 7 ((𝜑𝑦𝐴) → ¬ sup(𝐴, ℝ*, < ) < 𝑦)
228227ralrimiva 3145 . . . . . 6 (𝜑 → ∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦)
229 ralnex 3071 . . . . . 6 (∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦 ↔ ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
230228, 229sylib 218 . . . . 5 (𝜑 → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
231230ad2antrr 726 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
232224, 231condan 817 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
2339, 79, 232syl2anc 584 . 2 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
2348, 233pm2.61dan 812 1 (𝜑𝐵 ≤ sup(𝐴, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wnf 1782  wcel 2107  wne 2939  wral 3060  wrex 3069  Vcvv 3479  wss 3950   class class class wbr 5142  (class class class)co 7432  supcsup 9481  cc 11154  cr 11155  0cc0 11156  1c1 11157   + caddc 11159  +∞cpnf 11293  -∞cmnf 11294  *cxr 11295   < clt 11296  cle 11297  cmin 11493  +crp 13035   +𝑒 cxad 13153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-po 5591  df-so 5592  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-er 8746  df-en 8987  df-dom 8988  df-sdom 8989  df-sup 9483  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-rp 13036  df-xadd 13156
This theorem is referenced by:  supxrge  45354
  Copyright terms: Public domain W3C validator