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 38291
Description: If an extended real number can be approximated from below by members of a set, then it is smaller 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 11801 . . . . 5 (𝐵 ∈ ℝ*𝐵 ≤ +∞)
31, 2syl 17 . . . 4 (𝜑𝐵 ≤ +∞)
43adantr 479 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ +∞)
5 id 22 . . . . 5 (sup(𝐴, ℝ*, < ) = +∞ → sup(𝐴, ℝ*, < ) = +∞)
65eqcomd 2615 . . . 4 (sup(𝐴, ℝ*, < ) = +∞ → +∞ = sup(𝐴, ℝ*, < ))
76adantl 480 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → +∞ = sup(𝐴, ℝ*, < ))
84, 7breqtrd 4603 . 2 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
9 simpl 471 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝜑)
10 1rp 11668 . . . . . . . 8 1 ∈ ℝ+
11 nfcv 2750 . . . . . . . . . 10 𝑥1
12 supxrgelem.xph . . . . . . . . . . . 12 𝑥𝜑
13 nfv 1829 . . . . . . . . . . . 12 𝑥1 ∈ ℝ+
1412, 13nfan 1815 . . . . . . . . . . 11 𝑥(𝜑 ∧ 1 ∈ ℝ+)
15 nfv 1829 . . . . . . . . . . 11 𝑥𝑦𝐴 𝐵 < (𝑦 +𝑒 1)
1614, 15nfim 1812 . . . . . . . . . 10 𝑥((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
17 eleq1 2675 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈ ℝ+))
1817anbi2d 735 . . . . . . . . . . 11 (𝑥 = 1 → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈ ℝ+)))
19 oveq2 6535 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 1))
2019breq2d 4589 . . . . . . . . . . . 12 (𝑥 = 1 → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 1)))
2120rexbidv 3033 . . . . . . . . . . 11 (𝑥 = 1 → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1)))
2218, 21imbi12d 332 . . . . . . . . . 10 (𝑥 = 1 → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))))
23 supxrgelem.y . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥))
2411, 16, 22, 23vtoclgf 3236 . . . . . . . . 9 (1 ∈ ℝ+ → ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1)))
2510, 24ax-mp 5 . . . . . . . 8 ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
2610, 25mpan2 702 . . . . . . 7 (𝜑 → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
2726adantr 479 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
28 mnfxr 11783 . . . . . . . . . . 11 -∞ ∈ ℝ*
2928a1i 11 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ ∈ ℝ*)
30 supxrgelem.a . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ*)
3130sselda 3567 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ*)
32313adant3 1073 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝑦 ∈ ℝ*)
33 supxrcl 11973 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
3430, 33syl 17 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
35343ad2ant1 1074 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
36 simpl3 1058 . . . . . . . . . . . 12 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → 𝐵 < (𝑦 +𝑒 1))
37 simpr 475 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ < 𝑦)
3831adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*)
39 ngtmnft 11831 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ* → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦))
4038, 39syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦))
4137, 40mpbird 245 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
4241oveq1d 6542 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = (-∞ +𝑒 1))
43 1re 9895 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
4443rexri 9948 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
4544a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 1 ∈ ℝ*)
46 renepnf 9943 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ → 1 ≠ +∞)
4743, 46ax-mp 5 . . . . . . . . . . . . . . . 16 1 ≠ +∞
4847a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 1 ≠ +∞)
49 xaddmnf2 11893 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ* ∧ 1 ≠ +∞) → (-∞ +𝑒 1) = -∞)
5045, 48, 49syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (-∞ +𝑒 1) = -∞)
5142, 50eqtrd 2643 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = -∞)
52513adantl3 1211 . . . . . . . . . . . 12 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = -∞)
5336, 52breqtrd 4603 . . . . . . . . . . 11 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → 𝐵 < -∞)
54 nltmnf 11800 . . . . . . . . . . . . . 14 (𝐵 ∈ ℝ* → ¬ 𝐵 < -∞)
551, 54syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐵 < -∞)
5655adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
57563ad2antl1 1215 . . . . . . . . . . 11 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
5853, 57condan 830 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ < 𝑦)
5930adantr 479 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝐴 ⊆ ℝ*)
60 simpr 475 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦𝐴)
61 supxrub 11982 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ*𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6259, 60, 61syl2anc 690 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
63623adant3 1073 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6429, 32, 35, 58, 63xrltletrd 11827 . . . . . . . . 9 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ < sup(𝐴, ℝ*, < ))
65643exp 1255 . . . . . . . 8 (𝜑 → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < ))))
6665adantr 479 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < ))))
6766rexlimdv 3011 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < )))
6827, 67mpd 15 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → -∞ < sup(𝐴, ℝ*, < ))
69 simpr 475 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ sup(𝐴, ℝ*, < ) = +∞)
70 nltpnft 11830 . . . . . . . . 9 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7134, 70syl 17 . . . . . . . 8 (𝜑 → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7271adantr 479 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7369, 72mtbid 312 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ ¬ sup(𝐴, ℝ*, < ) < +∞)
7473notnotrd 126 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) < +∞)
7568, 74jca 552 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞))
7634adantr 479 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
77 xrrebnd 11832 . . . . 5 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
7876, 77syl 17 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
7975, 78mpbird 245 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ)
80 simpl 471 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ))
81 simpr 475 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ 𝐵 ≤ sup(𝐴, ℝ*, < ))
8234adantr 479 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
831adantr 479 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → 𝐵 ∈ ℝ*)
84 xrltnle 9956 . . . . . . . 8 ((sup(𝐴, ℝ*, < ) ∈ ℝ*𝐵 ∈ ℝ*) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8582, 83, 84syl2anc 690 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8685adantlr 746 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8781, 86mpbird 245 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) < 𝐵)
88 simpll 785 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝜑)
8928a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ ∈ ℝ*)
9088, 34syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
9188, 1syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ*)
92 mnfle 11804 . . . . . . . . . . . . . 14 (sup(𝐴, ℝ*, < ) ∈ ℝ* → -∞ ≤ sup(𝐴, ℝ*, < ))
9334, 92syl 17 . . . . . . . . . . . . 13 (𝜑 → -∞ ≤ sup(𝐴, ℝ*, < ))
9493ad2antrr 757 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ ≤ sup(𝐴, ℝ*, < ))
95 simpr 475 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) < 𝐵)
9689, 90, 91, 94, 95xrlelttrd 11826 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ < 𝐵)
97 id 22 . . . . . . . . . . . . . 14 (𝜑𝜑)
9810a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℝ+)
9997, 98, 25syl2anc 690 . . . . . . . . . . . . 13 (𝜑 → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
10099ad2antrr 757 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
10113ad2ant1 1074 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 ∈ ℝ*)
10244a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 1 ∈ ℝ*)
10332, 102jca 552 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*))
104 xaddcl 11902 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑦 +𝑒 1) ∈ ℝ*)
105103, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ∈ ℝ*)
106 pnfxr 11781 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
107106a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → +∞ ∈ ℝ*)
108 simp3 1055 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 < (𝑦 +𝑒 1))
10931, 44, 104sylancl 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐴) → (𝑦 +𝑒 1) ∈ ℝ*)
110 pnfge 11801 . . . . . . . . . . . . . . . . . 18 ((𝑦 +𝑒 1) ∈ ℝ* → (𝑦 +𝑒 1) ≤ +∞)
111109, 110syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴) → (𝑦 +𝑒 1) ≤ +∞)
1121113adant3 1073 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ≤ +∞)
113101, 105, 107, 108, 112xrltletrd 11827 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 < +∞)
1141133exp 1255 . . . . . . . . . . . . . 14 (𝜑 → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞)))
115114rexlimdv 3011 . . . . . . . . . . . . 13 (𝜑 → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞))
11688, 115syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞))
117100, 116mpd 15 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 < +∞)
11896, 117jca 552 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (-∞ < 𝐵𝐵 < +∞))
119 xrrebnd 11832 . . . . . . . . . . 11 (𝐵 ∈ ℝ* → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵𝐵 < +∞)))
12091, 119syl 17 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵𝐵 < +∞)))
121118, 120mpbird 245 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
122 simpr 475 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℝ)
123122adantr 479 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈ ℝ)
124121, 123resubcld 10309 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
12526, 115mpd 15 . . . . . . . . . . . . 13 (𝜑𝐵 < +∞)
126125ad2antrr 757 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 < +∞)
12796, 126jca 552 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (-∞ < 𝐵𝐵 < +∞))
128127, 120mpbird 245 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
129123, 128posdifd 10463 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ 0 < (𝐵 − sup(𝐴, ℝ*, < ))))
13095, 129mpbid 220 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 0 < (𝐵 − sup(𝐴, ℝ*, < )))
131124, 130elrpd 11701 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
132 ovex 6555 . . . . . . . 8 (𝐵 − sup(𝐴, ℝ*, < )) ∈ V
133 nfcv 2750 . . . . . . . . 9 𝑥(𝐵 − sup(𝐴, ℝ*, < ))
134 nfv 1829 . . . . . . . . . . 11 𝑥(𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+
13512, 134nfan 1815 . . . . . . . . . 10 𝑥(𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
136 nfv 1829 . . . . . . . . . 10 𝑥𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))
137135, 136nfim 1812 . . . . . . . . 9 𝑥((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
138 eleq1 2675 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑥 ∈ ℝ+ ↔ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+))
139138anbi2d 735 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)))
140 oveq2 6535 . . . . . . . . . . . 12 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
141140breq2d 4589 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
142141rexbidv 3033 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
143139, 142imbi12d 332 . . . . . . . . 9 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))))
144133, 137, 143, 23vtoclgf 3236 . . . . . . . 8 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ V → ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
145132, 144ax-mp 5 . . . . . . 7 ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
14688, 131, 145syl2anc 690 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
147 ltpnf 11791 . . . . . . . . . . . . 13 (sup(𝐴, ℝ*, < ) ∈ ℝ → sup(𝐴, ℝ*, < ) < +∞)
148147adantr 479 . . . . . . . . . . . 12 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < +∞)
149 id 22 . . . . . . . . . . . . . 14 (𝑦 = +∞ → 𝑦 = +∞)
150149eqcomd 2615 . . . . . . . . . . . . 13 (𝑦 = +∞ → +∞ = 𝑦)
151150adantl 480 . . . . . . . . . . . 12 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → +∞ = 𝑦)
152148, 151breqtrd 4603 . . . . . . . . . . 11 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
153152adantll 745 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
154153ad5ant15 1294 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
155 simplll 793 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵))
156 simpl 471 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
15788, 41sylanl1 679 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
158157adantlr 746 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
159 simplr 787 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
160 oveq1 6534 . . . . . . . . . . . . . . . . . 18 (𝑦 = -∞ → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
161160adantl 480 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
162128, 123resubcld 10309 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
163162rexrd 9945 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ*)
164163ad3antrrr 761 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ*)
165 renepnf 9943 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
166124, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
167166ad3antrrr 761 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
168 xaddmnf2 11893 . . . . . . . . . . . . . . . . . 18 (((𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ* ∧ (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
169164, 167, 168syl2anc 690 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
170161, 169eqtrd 2643 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
171159, 170breqtrd 4603 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < -∞)
172156, 158, 171syl2anc 690 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → 𝐵 < -∞)
17355ad5antr 765 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
174172, 173condan 830 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → -∞ < 𝑦)
175174adantr 479 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → -∞ < 𝑦)
176 simp3 1055 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → ¬ 𝑦 = +∞)
177313adant3 1073 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*)
178 nltpnft 11830 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ* → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞))
179177, 178syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞))
180176, 179mtbid 312 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → ¬ ¬ 𝑦 < +∞)
181180notnotrd 126 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
1821813adant1r 1310 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
183182ad5ant135 1305 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
184175, 183jca 552 . . . . . . . . . . 11 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → (-∞ < 𝑦𝑦 < +∞))
18531adantlr 746 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦𝐴) → 𝑦 ∈ ℝ*)
186185ad5ant13 1292 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*)
187 xrrebnd 11832 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦𝑦 < +∞)))
188186, 187syl 17 . . . . . . . . . . 11 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦𝑦 < +∞)))
189184, 188mpbird 245 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ)
190 simplr 787 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
191121ad2antrr 757 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝐵 ∈ ℝ)
192 simpr 475 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
193124adantr 479 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
194 rexadd 11896 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))))
195192, 193, 194syl2anc 690 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))))
196192, 193readdcld 9925 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
197195, 196eqeltrd 2687 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
198197adantr 479 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
199 simpr 475 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
200191, 198, 191, 199ltsub1dd 10488 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝐵𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵))
201121recnd 9924 . . . . . . . . . . . . . . 15 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℂ)
202201subidd 10231 . . . . . . . . . . . . . 14 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵𝐵) = 0)
203202ad2antrr 757 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝐵𝐵) = 0)
204192recnd 9924 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
205201adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝐵 ∈ ℂ)
206122recnd 9924 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
207206ad2antrr 757 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
208204, 205, 207addsub12d 10266 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))))
209195, 208eqtrd 2643 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))))
210209oveq1d 6542 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = ((𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))) − 𝐵))
211204, 207subcld 10243 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 − sup(𝐴, ℝ*, < )) ∈ ℂ)
212205, 211pncan2d 10245 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
213210, 212eqtrd 2643 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
214213adantr 479 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
215203, 214breq12d 4590 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → ((𝐵𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) ↔ 0 < (𝑦 − sup(𝐴, ℝ*, < ))))
216200, 215mpbid 220 . . . . . . . . . . 11 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 0 < (𝑦 − sup(𝐴, ℝ*, < )))
217123ad2antrr 757 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) ∈ ℝ)
218 simplr 787 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝑦 ∈ ℝ)
219217, 218posdifd 10463 . . . . . . . . . . 11 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (sup(𝐴, ℝ*, < ) < 𝑦 ↔ 0 < (𝑦 − sup(𝐴, ℝ*, < ))))
220216, 219mpbird 245 . . . . . . . . . 10 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) < 𝑦)
221155, 189, 190, 220syl21anc 1316 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
222154, 221pm2.61dan 827 . . . . . . . 8 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) < 𝑦)
223222ex 448 . . . . . . 7 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) → (𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) → sup(𝐴, ℝ*, < ) < 𝑦))
224223reximdva 2999 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦))
225146, 224mpd 15 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
22680, 87, 225syl2anc 690 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
22759, 33syl 17 . . . . . . . . 9 ((𝜑𝑦𝐴) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
22831, 227xrlenltd 9955 . . . . . . . 8 ((𝜑𝑦𝐴) → (𝑦 ≤ sup(𝐴, ℝ*, < ) ↔ ¬ sup(𝐴, ℝ*, < ) < 𝑦))
22962, 228mpbid 220 . . . . . . 7 ((𝜑𝑦𝐴) → ¬ sup(𝐴, ℝ*, < ) < 𝑦)
230229ralrimiva 2948 . . . . . 6 (𝜑 → ∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦)
231 ralnex 2974 . . . . . 6 (∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦 ↔ ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
232230, 231sylib 206 . . . . 5 (𝜑 → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
233232ad2antrr 757 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
234226, 233condan 830 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
2359, 79, 234syl2anc 690 . 2 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
2368, 235pm2.61dan 827 1 (𝜑𝐵 ≤ sup(𝐴, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wnf 1698  wcel 1976  wne 2779  wral 2895  wrex 2896  Vcvv 3172  wss 3539   class class class wbr 4577  (class class class)co 6527  supcsup 8206  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795  +∞cpnf 9927  -∞cmnf 9928  *cxr 9929   < clt 9930  cle 9931  cmin 10117  +crp 11664   +𝑒 cxad 11776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7036  df-2nd 7037  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-sup 8208  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-rp 11665  df-xadd 11779
This theorem is referenced by:  supxrge  38292
  Copyright terms: Public domain W3C validator