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 41966
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 12517 . . . . 5 (𝐵 ∈ ℝ*𝐵 ≤ +∞)
31, 2syl 17 . . . 4 (𝜑𝐵 ≤ +∞)
43adantr 484 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ +∞)
5 id 22 . . . . 5 (sup(𝐴, ℝ*, < ) = +∞ → sup(𝐴, ℝ*, < ) = +∞)
65eqcomd 2807 . . . 4 (sup(𝐴, ℝ*, < ) = +∞ → +∞ = sup(𝐴, ℝ*, < ))
76adantl 485 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → +∞ = sup(𝐴, ℝ*, < ))
84, 7breqtrd 5059 . 2 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
9 simpl 486 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝜑)
10 1rp 12385 . . . . . . . 8 1 ∈ ℝ+
11 nfcv 2958 . . . . . . . . . 10 𝑥1
12 supxrgelem.xph . . . . . . . . . . . 12 𝑥𝜑
13 nfv 1915 . . . . . . . . . . . 12 𝑥1 ∈ ℝ+
1412, 13nfan 1900 . . . . . . . . . . 11 𝑥(𝜑 ∧ 1 ∈ ℝ+)
15 nfv 1915 . . . . . . . . . . 11 𝑥𝑦𝐴 𝐵 < (𝑦 +𝑒 1)
1614, 15nfim 1897 . . . . . . . . . 10 𝑥((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
17 eleq1 2880 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈ ℝ+))
1817anbi2d 631 . . . . . . . . . . 11 (𝑥 = 1 → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈ ℝ+)))
19 oveq2 7147 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 1))
2019breq2d 5045 . . . . . . . . . . . 12 (𝑥 = 1 → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 1)))
2120rexbidv 3259 . . . . . . . . . . 11 (𝑥 = 1 → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1)))
2218, 21imbi12d 348 . . . . . . . . . 10 (𝑥 = 1 → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))))
23 supxrgelem.y . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥))
2411, 16, 22, 23vtoclgf 3516 . . . . . . . . 9 (1 ∈ ℝ+ → ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1)))
2510, 24ax-mp 5 . . . . . . . 8 ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
2610, 25mpan2 690 . . . . . . 7 (𝜑 → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
2726adantr 484 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
28 mnfxr 10691 . . . . . . . . . . 11 -∞ ∈ ℝ*
2928a1i 11 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ ∈ ℝ*)
30 supxrgelem.a . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ*)
3130sselda 3918 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ*)
32313adant3 1129 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝑦 ∈ ℝ*)
33 supxrcl 12700 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
3430, 33syl 17 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
35343ad2ant1 1130 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
36 simpl3 1190 . . . . . . . . . . . 12 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → 𝐵 < (𝑦 +𝑒 1))
37 simpr 488 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ < 𝑦)
3831adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*)
39 ngtmnft 12551 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ* → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦))
4038, 39syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦))
4137, 40mpbird 260 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
4241oveq1d 7154 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = (-∞ +𝑒 1))
43 1xr 10693 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
4443a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 1 ∈ ℝ*)
45 1re 10634 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
46 renepnf 10682 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ → 1 ≠ +∞)
4745, 46ax-mp 5 . . . . . . . . . . . . . . . 16 1 ≠ +∞
4847a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 1 ≠ +∞)
49 xaddmnf2 12614 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ* ∧ 1 ≠ +∞) → (-∞ +𝑒 1) = -∞)
5044, 48, 49syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (-∞ +𝑒 1) = -∞)
5142, 50eqtrd 2836 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = -∞)
52513adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = -∞)
5336, 52breqtrd 5059 . . . . . . . . . . 11 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → 𝐵 < -∞)
54 nltmnf 12516 . . . . . . . . . . . . . 14 (𝐵 ∈ ℝ* → ¬ 𝐵 < -∞)
551, 54syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐵 < -∞)
5655adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
57563ad2antl1 1182 . . . . . . . . . . 11 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
5853, 57condan 817 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ < 𝑦)
5930adantr 484 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝐴 ⊆ ℝ*)
60 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦𝐴)
61 supxrub 12709 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ*𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6259, 60, 61syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
63623adant3 1129 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6429, 32, 35, 58, 63xrltletrd 12546 . . . . . . . . 9 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ < sup(𝐴, ℝ*, < ))
65643exp 1116 . . . . . . . 8 (𝜑 → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < ))))
6665adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < ))))
6766rexlimdv 3245 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < )))
6827, 67mpd 15 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → -∞ < sup(𝐴, ℝ*, < ))
69 simpr 488 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ sup(𝐴, ℝ*, < ) = +∞)
70 nltpnft 12549 . . . . . . . . 9 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7134, 70syl 17 . . . . . . . 8 (𝜑 → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7271adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7369, 72mtbid 327 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ ¬ sup(𝐴, ℝ*, < ) < +∞)
7473notnotrd 135 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) < +∞)
7568, 74jca 515 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞))
7634adantr 484 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
77 xrrebnd 12553 . . . . 5 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
7876, 77syl 17 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
7975, 78mpbird 260 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ)
80 simpl 486 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ))
81 simpr 488 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ 𝐵 ≤ sup(𝐴, ℝ*, < ))
8234adantr 484 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
831adantr 484 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → 𝐵 ∈ ℝ*)
84 xrltnle 10701 . . . . . . . 8 ((sup(𝐴, ℝ*, < ) ∈ ℝ*𝐵 ∈ ℝ*) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8582, 83, 84syl2anc 587 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8685adantlr 714 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8781, 86mpbird 260 . . . . 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 12521 . . . . . . . . . . . . . 14 (sup(𝐴, ℝ*, < ) ∈ ℝ* → -∞ ≤ sup(𝐴, ℝ*, < ))
9334, 92syl 17 . . . . . . . . . . . . 13 (𝜑 → -∞ ≤ sup(𝐴, ℝ*, < ))
9493ad2antrr 725 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ ≤ sup(𝐴, ℝ*, < ))
95 simpr 488 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) < 𝐵)
9689, 90, 91, 94, 95xrlelttrd 12545 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ < 𝐵)
97 id 22 . . . . . . . . . . . . . 14 (𝜑𝜑)
9810a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℝ+)
9997, 98, 25syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
10099ad2antrr 725 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
10113ad2ant1 1130 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 ∈ ℝ*)
10243a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 1 ∈ ℝ*)
10332, 102jca 515 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*))
104 xaddcl 12624 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑦 +𝑒 1) ∈ ℝ*)
105103, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ∈ ℝ*)
106 pnfxr 10688 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
107106a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → +∞ ∈ ℝ*)
108 simp3 1135 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 < (𝑦 +𝑒 1))
10931, 43, 104sylancl 589 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐴) → (𝑦 +𝑒 1) ∈ ℝ*)
110 pnfge 12517 . . . . . . . . . . . . . . . . . 18 ((𝑦 +𝑒 1) ∈ ℝ* → (𝑦 +𝑒 1) ≤ +∞)
111109, 110syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴) → (𝑦 +𝑒 1) ≤ +∞)
1121113adant3 1129 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ≤ +∞)
113101, 105, 107, 108, 112xrltletrd 12546 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 < +∞)
1141133exp 1116 . . . . . . . . . . . . . 14 (𝜑 → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞)))
115114rexlimdv 3245 . . . . . . . . . . . . 13 (𝜑 → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞))
11688, 115syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞))
117100, 116mpd 15 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 < +∞)
11896, 117jca 515 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (-∞ < 𝐵𝐵 < +∞))
119 xrrebnd 12553 . . . . . . . . . . 11 (𝐵 ∈ ℝ* → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵𝐵 < +∞)))
12091, 119syl 17 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵𝐵 < +∞)))
121118, 120mpbird 260 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
122 simpr 488 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℝ)
123122adantr 484 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈ ℝ)
124121, 123resubcld 11061 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
12526, 115mpd 15 . . . . . . . . . . . . 13 (𝜑𝐵 < +∞)
126125ad2antrr 725 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 < +∞)
12796, 126jca 515 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (-∞ < 𝐵𝐵 < +∞))
128127, 120mpbird 260 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
129123, 128posdifd 11220 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ 0 < (𝐵 − sup(𝐴, ℝ*, < ))))
13095, 129mpbid 235 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 0 < (𝐵 − sup(𝐴, ℝ*, < )))
131124, 130elrpd 12420 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
132 ovex 7172 . . . . . . . 8 (𝐵 − sup(𝐴, ℝ*, < )) ∈ V
133 nfcv 2958 . . . . . . . . 9 𝑥(𝐵 − sup(𝐴, ℝ*, < ))
134 nfv 1915 . . . . . . . . . . 11 𝑥(𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+
13512, 134nfan 1900 . . . . . . . . . 10 𝑥(𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
136 nfv 1915 . . . . . . . . . 10 𝑥𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))
137135, 136nfim 1897 . . . . . . . . 9 𝑥((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
138 eleq1 2880 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑥 ∈ ℝ+ ↔ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+))
139138anbi2d 631 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)))
140 oveq2 7147 . . . . . . . . . . . 12 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
141140breq2d 5045 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
142141rexbidv 3259 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
143139, 142imbi12d 348 . . . . . . . . 9 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))))
144133, 137, 143, 23vtoclgf 3516 . . . . . . . 8 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ V → ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
145132, 144ax-mp 5 . . . . . . 7 ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
14688, 131, 145syl2anc 587 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
147 ltpnf 12507 . . . . . . . . . . . . 13 (sup(𝐴, ℝ*, < ) ∈ ℝ → sup(𝐴, ℝ*, < ) < +∞)
148147adantr 484 . . . . . . . . . . . 12 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < +∞)
149 id 22 . . . . . . . . . . . . . 14 (𝑦 = +∞ → 𝑦 = +∞)
150149eqcomd 2807 . . . . . . . . . . . . 13 (𝑦 = +∞ → +∞ = 𝑦)
151150adantl 485 . . . . . . . . . . . 12 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → +∞ = 𝑦)
152148, 151breqtrd 5059 . . . . . . . . . . 11 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
153152adantll 713 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
154153ad5ant15 758 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
155 simplll 774 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵))
156 simpl 486 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
15788, 41sylanl1 679 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
158157adantlr 714 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
159 simplr 768 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
160 oveq1 7146 . . . . . . . . . . . . . . . . . 18 (𝑦 = -∞ → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
161160adantl 485 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
162128, 123resubcld 11061 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
163162rexrd 10684 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ*)
164163ad3antrrr 729 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ*)
165 renepnf 10682 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
166124, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
167166ad3antrrr 729 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
168 xaddmnf2 12614 . . . . . . . . . . . . . . . . . 18 (((𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ* ∧ (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
169164, 167, 168syl2anc 587 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
170161, 169eqtrd 2836 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
171159, 170breqtrd 5059 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < -∞)
172156, 158, 171syl2anc 587 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → 𝐵 < -∞)
17355ad5antr 733 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
174172, 173condan 817 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → -∞ < 𝑦)
175174adantr 484 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → -∞ < 𝑦)
176 simp3 1135 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → ¬ 𝑦 = +∞)
177313adant3 1129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*)
178 nltpnft 12549 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ* → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞))
179177, 178syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞))
180176, 179mtbid 327 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → ¬ ¬ 𝑦 < +∞)
181180notnotrd 135 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
1821813adant1r 1174 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
183182ad5ant135 1365 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
184175, 183jca 515 . . . . . . . . . . 11 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → (-∞ < 𝑦𝑦 < +∞))
18531adantlr 714 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦𝐴) → 𝑦 ∈ ℝ*)
186185ad5ant13 756 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*)
187 xrrebnd 12553 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦𝑦 < +∞)))
188186, 187syl 17 . . . . . . . . . . 11 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦𝑦 < +∞)))
189184, 188mpbird 260 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ)
190 simplr 768 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
191121ad2antrr 725 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝐵 ∈ ℝ)
192 simpr 488 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
193124adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
194 rexadd 12617 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))))
195192, 193, 194syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))))
196192, 193readdcld 10663 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
197195, 196eqeltrd 2893 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
198197adantr 484 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
199 simpr 488 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
200191, 198, 191, 199ltsub1dd 11245 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝐵𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵))
201121recnd 10662 . . . . . . . . . . . . . . 15 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℂ)
202201subidd 10978 . . . . . . . . . . . . . 14 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵𝐵) = 0)
203202ad2antrr 725 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝐵𝐵) = 0)
204201adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝐵 ∈ ℂ)
205192recnd 10662 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
206122recnd 10662 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
207206ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
208205, 207subcld 10990 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 − sup(𝐴, ℝ*, < )) ∈ ℂ)
209205, 204, 207addsub12d 11013 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))))
210195, 209eqtrd 2836 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))))
211204, 208, 210mvrladdd 11046 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
212211adantr 484 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
213203, 212breq12d 5046 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → ((𝐵𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) ↔ 0 < (𝑦 − sup(𝐴, ℝ*, < ))))
214200, 213mpbid 235 . . . . . . . . . . 11 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 0 < (𝑦 − sup(𝐴, ℝ*, < )))
215123ad2antrr 725 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) ∈ ℝ)
216 simplr 768 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝑦 ∈ ℝ)
217215, 216posdifd 11220 . . . . . . . . . . 11 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (sup(𝐴, ℝ*, < ) < 𝑦 ↔ 0 < (𝑦 − sup(𝐴, ℝ*, < ))))
218214, 217mpbird 260 . . . . . . . . . 10 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) < 𝑦)
219155, 189, 190, 218syl21anc 836 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
220154, 219pm2.61dan 812 . . . . . . . 8 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) < 𝑦)
221220ex 416 . . . . . . 7 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) → (𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) → sup(𝐴, ℝ*, < ) < 𝑦))
222221reximdva 3236 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦))
223146, 222mpd 15 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
22480, 87, 223syl2anc 587 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
22559, 33syl 17 . . . . . . . . 9 ((𝜑𝑦𝐴) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
22631, 225xrlenltd 10700 . . . . . . . 8 ((𝜑𝑦𝐴) → (𝑦 ≤ sup(𝐴, ℝ*, < ) ↔ ¬ sup(𝐴, ℝ*, < ) < 𝑦))
22762, 226mpbid 235 . . . . . . 7 ((𝜑𝑦𝐴) → ¬ sup(𝐴, ℝ*, < ) < 𝑦)
228227ralrimiva 3152 . . . . . 6 (𝜑 → ∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦)
229 ralnex 3202 . . . . . 6 (∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦 ↔ ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
230228, 229sylib 221 . . . . 5 (𝜑 → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
231230ad2antrr 725 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
232224, 231condan 817 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
2339, 79, 232syl2anc 587 . 2 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
2348, 233pm2.61dan 812 1 (𝜑𝐵 ≤ sup(𝐴, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wnf 1785  wcel 2112  wne 2990  wral 3109  wrex 3110  Vcvv 3444  wss 3884   class class class wbr 5033  (class class class)co 7139  supcsup 8892  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533  +∞cpnf 10665  -∞cmnf 10666  *cxr 10667   < clt 10668  cle 10669  cmin 10863  +crp 12381   +𝑒 cxad 12497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-so 5443  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-1st 7675  df-2nd 7676  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-sup 8894  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-rp 12382  df-xadd 12500
This theorem is referenced by:  supxrge  41967
  Copyright terms: Public domain W3C validator