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

Theorem supxrgelem 39866
 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 12002 . . . . 5 (𝐵 ∈ ℝ*𝐵 ≤ +∞)
31, 2syl 17 . . . 4 (𝜑𝐵 ≤ +∞)
43adantr 480 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ +∞)
5 id 22 . . . . 5 (sup(𝐴, ℝ*, < ) = +∞ → sup(𝐴, ℝ*, < ) = +∞)
65eqcomd 2657 . . . 4 (sup(𝐴, ℝ*, < ) = +∞ → +∞ = sup(𝐴, ℝ*, < ))
76adantl 481 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → +∞ = sup(𝐴, ℝ*, < ))
84, 7breqtrd 4711 . 2 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
9 simpl 472 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝜑)
10 1rp 11874 . . . . . . . 8 1 ∈ ℝ+
11 nfcv 2793 . . . . . . . . . 10 𝑥1
12 supxrgelem.xph . . . . . . . . . . . 12 𝑥𝜑
13 nfv 1883 . . . . . . . . . . . 12 𝑥1 ∈ ℝ+
1412, 13nfan 1868 . . . . . . . . . . 11 𝑥(𝜑 ∧ 1 ∈ ℝ+)
15 nfv 1883 . . . . . . . . . . 11 𝑥𝑦𝐴 𝐵 < (𝑦 +𝑒 1)
1614, 15nfim 1865 . . . . . . . . . 10 𝑥((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
17 eleq1 2718 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈ ℝ+))
1817anbi2d 740 . . . . . . . . . . 11 (𝑥 = 1 → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈ ℝ+)))
19 oveq2 6698 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 1))
2019breq2d 4697 . . . . . . . . . . . 12 (𝑥 = 1 → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 1)))
2120rexbidv 3081 . . . . . . . . . . 11 (𝑥 = 1 → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1)))
2218, 21imbi12d 333 . . . . . . . . . 10 (𝑥 = 1 → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))))
23 supxrgelem.y . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥))
2411, 16, 22, 23vtoclgf 3295 . . . . . . . . 9 (1 ∈ ℝ+ → ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1)))
2510, 24ax-mp 5 . . . . . . . 8 ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
2610, 25mpan2 707 . . . . . . 7 (𝜑 → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
2726adantr 480 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
28 mnfxr 10134 . . . . . . . . . . 11 -∞ ∈ ℝ*
2928a1i 11 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ ∈ ℝ*)
30 supxrgelem.a . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ*)
3130sselda 3636 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ*)
32313adant3 1101 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝑦 ∈ ℝ*)
33 supxrcl 12183 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
3430, 33syl 17 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
35343ad2ant1 1102 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
36 simpl3 1086 . . . . . . . . . . . 12 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → 𝐵 < (𝑦 +𝑒 1))
37 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ < 𝑦)
3831adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*)
39 ngtmnft 12035 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ* → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦))
4038, 39syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦))
4137, 40mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
4241oveq1d 6705 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = (-∞ +𝑒 1))
43 1re 10077 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
4443rexri 10135 . . . . . . . . . . . . . . . 16 1 ∈ ℝ*
4544a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 1 ∈ ℝ*)
46 renepnf 10125 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ → 1 ≠ +∞)
4743, 46ax-mp 5 . . . . . . . . . . . . . . . 16 1 ≠ +∞
4847a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 1 ≠ +∞)
49 xaddmnf2 12098 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ* ∧ 1 ≠ +∞) → (-∞ +𝑒 1) = -∞)
5045, 48, 49syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (-∞ +𝑒 1) = -∞)
5142, 50eqtrd 2685 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = -∞)
52513adantl3 1239 . . . . . . . . . . . 12 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = -∞)
5336, 52breqtrd 4711 . . . . . . . . . . 11 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → 𝐵 < -∞)
54 nltmnf 12001 . . . . . . . . . . . . . 14 (𝐵 ∈ ℝ* → ¬ 𝐵 < -∞)
551, 54syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐵 < -∞)
5655adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
57563ad2antl1 1243 . . . . . . . . . . 11 (((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
5853, 57condan 852 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ < 𝑦)
5930adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝐴 ⊆ ℝ*)
60 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦𝐴)
61 supxrub 12192 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ*𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6259, 60, 61syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
63623adant3 1101 . . . . . . . . . 10 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6429, 32, 35, 58, 63xrltletrd 12030 . . . . . . . . 9 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → -∞ < sup(𝐴, ℝ*, < ))
65643exp 1283 . . . . . . . 8 (𝜑 → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < ))))
6665adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < ))))
6766rexlimdv 3059 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → -∞ < sup(𝐴, ℝ*, < )))
6827, 67mpd 15 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → -∞ < sup(𝐴, ℝ*, < ))
69 simpr 476 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ sup(𝐴, ℝ*, < ) = +∞)
70 nltpnft 12033 . . . . . . . . 9 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7134, 70syl 17 . . . . . . . 8 (𝜑 → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7271adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7369, 72mtbid 313 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ ¬ sup(𝐴, ℝ*, < ) < +∞)
7473notnotrd 128 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) < +∞)
7568, 74jca 553 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞))
7634adantr 480 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
77 xrrebnd 12037 . . . . 5 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
7876, 77syl 17 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
7975, 78mpbird 247 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ)
80 simpl 472 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ))
81 simpr 476 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ 𝐵 ≤ sup(𝐴, ℝ*, < ))
8234adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
831adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → 𝐵 ∈ ℝ*)
84 xrltnle 10143 . . . . . . . 8 ((sup(𝐴, ℝ*, < ) ∈ ℝ*𝐵 ∈ ℝ*) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8582, 83, 84syl2anc 694 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8685adantlr 751 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8781, 86mpbird 247 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) < 𝐵)
88 simpll 805 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝜑)
8928a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ ∈ ℝ*)
9088, 34syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
9188, 1syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ*)
92 mnfle 12007 . . . . . . . . . . . . . 14 (sup(𝐴, ℝ*, < ) ∈ ℝ* → -∞ ≤ sup(𝐴, ℝ*, < ))
9334, 92syl 17 . . . . . . . . . . . . 13 (𝜑 → -∞ ≤ sup(𝐴, ℝ*, < ))
9493ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ ≤ sup(𝐴, ℝ*, < ))
95 simpr 476 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) < 𝐵)
9689, 90, 91, 94, 95xrlelttrd 12029 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → -∞ < 𝐵)
97 id 22 . . . . . . . . . . . . . 14 (𝜑𝜑)
9810a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℝ+)
9997, 98, 25syl2anc 694 . . . . . . . . . . . . 13 (𝜑 → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
10099ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1))
10113ad2ant1 1102 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 ∈ ℝ*)
10244a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 1 ∈ ℝ*)
10332, 102jca 553 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*))
104 xaddcl 12108 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑦 +𝑒 1) ∈ ℝ*)
105103, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ∈ ℝ*)
106 pnfxr 10130 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
107106a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → +∞ ∈ ℝ*)
108 simp3 1083 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 < (𝑦 +𝑒 1))
10931, 44, 104sylancl 695 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐴) → (𝑦 +𝑒 1) ∈ ℝ*)
110 pnfge 12002 . . . . . . . . . . . . . . . . . 18 ((𝑦 +𝑒 1) ∈ ℝ* → (𝑦 +𝑒 1) ≤ +∞)
111109, 110syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴) → (𝑦 +𝑒 1) ≤ +∞)
1121113adant3 1101 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ≤ +∞)
113101, 105, 107, 108, 112xrltletrd 12030 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴𝐵 < (𝑦 +𝑒 1)) → 𝐵 < +∞)
1141133exp 1283 . . . . . . . . . . . . . 14 (𝜑 → (𝑦𝐴 → (𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞)))
115114rexlimdv 3059 . . . . . . . . . . . . 13 (𝜑 → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞))
11688, 115syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 < +∞))
117100, 116mpd 15 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 < +∞)
11896, 117jca 553 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (-∞ < 𝐵𝐵 < +∞))
119 xrrebnd 12037 . . . . . . . . . . 11 (𝐵 ∈ ℝ* → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵𝐵 < +∞)))
12091, 119syl 17 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵𝐵 < +∞)))
121118, 120mpbird 247 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
122 simpr 476 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℝ)
123122adantr 480 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈ ℝ)
124121, 123resubcld 10496 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
12526, 115mpd 15 . . . . . . . . . . . . 13 (𝜑𝐵 < +∞)
126125ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 < +∞)
12796, 126jca 553 . . . . . . . . . . 11 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (-∞ < 𝐵𝐵 < +∞))
128127, 120mpbird 247 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
129123, 128posdifd 10652 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ 0 < (𝐵 − sup(𝐴, ℝ*, < ))))
13095, 129mpbid 222 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 0 < (𝐵 − sup(𝐴, ℝ*, < )))
131124, 130elrpd 11907 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
132 ovex 6718 . . . . . . . 8 (𝐵 − sup(𝐴, ℝ*, < )) ∈ V
133 nfcv 2793 . . . . . . . . 9 𝑥(𝐵 − sup(𝐴, ℝ*, < ))
134 nfv 1883 . . . . . . . . . . 11 𝑥(𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+
13512, 134nfan 1868 . . . . . . . . . 10 𝑥(𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
136 nfv 1883 . . . . . . . . . 10 𝑥𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))
137135, 136nfim 1865 . . . . . . . . 9 𝑥((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
138 eleq1 2718 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑥 ∈ ℝ+ ↔ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+))
139138anbi2d 740 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)))
140 oveq2 6698 . . . . . . . . . . . 12 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
141140breq2d 4697 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
142141rexbidv 3081 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
143139, 142imbi12d 333 . . . . . . . . 9 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))))
144133, 137, 143, 23vtoclgf 3295 . . . . . . . 8 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ V → ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
145132, 144ax-mp 5 . . . . . . 7 ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
14688, 131, 145syl2anc 694 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
147 ltpnf 11992 . . . . . . . . . . . . 13 (sup(𝐴, ℝ*, < ) ∈ ℝ → sup(𝐴, ℝ*, < ) < +∞)
148147adantr 480 . . . . . . . . . . . 12 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < +∞)
149 id 22 . . . . . . . . . . . . . 14 (𝑦 = +∞ → 𝑦 = +∞)
150149eqcomd 2657 . . . . . . . . . . . . 13 (𝑦 = +∞ → +∞ = 𝑦)
151150adantl 481 . . . . . . . . . . . 12 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → +∞ = 𝑦)
152148, 151breqtrd 4711 . . . . . . . . . . 11 ((sup(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
153152adantll 750 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
154153ad5ant15 1336 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
155 simplll 813 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵))
156 simpl 472 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))))
15788, 41sylanl1 683 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
158157adantlr 751 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞)
159 simplr 807 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
160 oveq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑦 = -∞ → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
161160adantl 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
162128, 123resubcld 10496 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
163162rexrd 10127 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ*)
164163ad3antrrr 766 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ*)
165 renepnf 10125 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
166124, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
167166ad3antrrr 766 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞)
168 xaddmnf2 12098 . . . . . . . . . . . . . . . . . 18 (((𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ* ∧ (𝐵 − sup(𝐴, ℝ*, < )) ≠ +∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
169164, 167, 168syl2anc 694 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
170161, 169eqtrd 2685 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = -∞)
171159, 170breqtrd 4711 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < -∞)
172156, 158, 171syl2anc 694 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → 𝐵 < -∞)
17355ad5antr 773 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞)
174172, 173condan 852 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → -∞ < 𝑦)
175174adantr 480 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → -∞ < 𝑦)
176 simp3 1083 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → ¬ 𝑦 = +∞)
177313adant3 1101 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*)
178 nltpnft 12033 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ* → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞))
179177, 178syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞))
180176, 179mtbid 313 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → ¬ ¬ 𝑦 < +∞)
181180notnotrd 128 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
1821813adant1r 1359 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
183182ad5ant135 1354 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞)
184175, 183jca 553 . . . . . . . . . . 11 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → (-∞ < 𝑦𝑦 < +∞))
18531adantlr 751 . . . . . . . . . . . . 13 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ 𝑦𝐴) → 𝑦 ∈ ℝ*)
186185ad5ant13 1332 . . . . . . . . . . . 12 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*)
187 xrrebnd 12037 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦𝑦 < +∞)))
188186, 187syl 17 . . . . . . . . . . 11 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦𝑦 < +∞)))
189184, 188mpbird 247 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ)
190 simplr 807 . . . . . . . . . 10 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
191121ad2antrr 762 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝐵 ∈ ℝ)
192 simpr 476 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
193124adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
194 rexadd 12101 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))))
195192, 193, 194syl2anc 694 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))))
196192, 193readdcld 10107 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
197195, 196eqeltrd 2730 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
198197adantr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈ ℝ)
199 simpr 476 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))))
200191, 198, 191, 199ltsub1dd 10677 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝐵𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵))
201121recnd 10106 . . . . . . . . . . . . . . 15 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℂ)
202201subidd 10418 . . . . . . . . . . . . . 14 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵𝐵) = 0)
203202ad2antrr 762 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (𝐵𝐵) = 0)
204192recnd 10106 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
205201adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝐵 ∈ ℂ)
206122recnd 10106 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
207206ad2antrr 762 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
208204, 205, 207addsub12d 10453 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))))
209195, 208eqtrd 2685 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))))
210209oveq1d 6705 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = ((𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))) − 𝐵))
211204, 207subcld 10430 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 − sup(𝐴, ℝ*, < )) ∈ ℂ)
212205, 211pncan2d 10432 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝐵 + (𝑦 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
213210, 212eqtrd 2685 . . . . . . . . . . . . . 14 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
214213adantr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) = (𝑦 − sup(𝐴, ℝ*, < )))
215203, 214breq12d 4698 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → ((𝐵𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) − 𝐵) ↔ 0 < (𝑦 − sup(𝐴, ℝ*, < ))))
216200, 215mpbid 222 . . . . . . . . . . 11 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 0 < (𝑦 − sup(𝐴, ℝ*, < )))
217123ad2antrr 762 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) ∈ ℝ)
218 simplr 807 . . . . . . . . . . . 12 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 𝑦 ∈ ℝ)
219217, 218posdifd 10652 . . . . . . . . . . 11 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → (sup(𝐴, ℝ*, < ) < 𝑦 ↔ 0 < (𝑦 − sup(𝐴, ℝ*, < ))))
220216, 219mpbird 247 . . . . . . . . . 10 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) < 𝑦)
221155, 189, 190, 220syl21anc 1365 . . . . . . . . 9 ((((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦)
222154, 221pm2.61dan 849 . . . . . . . 8 (((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → sup(𝐴, ℝ*, < ) < 𝑦)
223222ex 449 . . . . . . 7 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) → (𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) → sup(𝐴, ℝ*, < ) < 𝑦))
224223reximdva 3046 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦))
225146, 224mpd 15 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
22680, 87, 225syl2anc 694 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
22759, 33syl 17 . . . . . . . . 9 ((𝜑𝑦𝐴) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
22831, 227xrlenltd 10142 . . . . . . . 8 ((𝜑𝑦𝐴) → (𝑦 ≤ sup(𝐴, ℝ*, < ) ↔ ¬ sup(𝐴, ℝ*, < ) < 𝑦))
22962, 228mpbid 222 . . . . . . 7 ((𝜑𝑦𝐴) → ¬ sup(𝐴, ℝ*, < ) < 𝑦)
230229ralrimiva 2995 . . . . . 6 (𝜑 → ∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦)
231 ralnex 3021 . . . . . 6 (∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦 ↔ ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
232230, 231sylib 208 . . . . 5 (𝜑 → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
233232ad2antrr 762 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
234226, 233condan 852 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
2359, 79, 234syl2anc 694 . 2 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
2368, 235pm2.61dan 849 1 (𝜑𝐵 ≤ sup(𝐴, ℝ*, < ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523  Ⅎwnf 1748   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ⊆ wss 3607   class class class wbr 4685  (class class class)co 6690  supcsup 8387  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977  +∞cpnf 10109  -∞cmnf 10110  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  ℝ+crp 11870   +𝑒 cxad 11982 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-sup 8389  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-rp 11871  df-xadd 11985 This theorem is referenced by:  supxrge  39867
 Copyright terms: Public domain W3C validator