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

Theorem supxrgere 45344
Description: If a 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
supxrgere.xph 𝑥𝜑
supxrgere.a (𝜑𝐴 ⊆ ℝ*)
supxrgere.b (𝜑𝐵 ∈ ℝ)
supxrgere.y ((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 (𝐵𝑥) < 𝑦)
Assertion
Ref Expression
supxrgere (𝜑𝐵 ≤ sup(𝐴, ℝ*, < ))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem supxrgere
StepHypRef Expression
1 supxrgere.b . . . . 5 (𝜑𝐵 ∈ ℝ)
2 rexr 11307 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3 pnfxr 11315 . . . . . . 7 +∞ ∈ ℝ*
43a1i 11 . . . . . 6 (𝐵 ∈ ℝ → +∞ ∈ ℝ*)
5 ltpnf 13162 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 < +∞)
62, 4, 5xrltled 13192 . . . . 5 (𝐵 ∈ ℝ → 𝐵 ≤ +∞)
71, 6syl 17 . . . 4 (𝜑𝐵 ≤ +∞)
87adantr 480 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ +∞)
9 id 22 . . . . 5 (sup(𝐴, ℝ*, < ) = +∞ → sup(𝐴, ℝ*, < ) = +∞)
109eqcomd 2743 . . . 4 (sup(𝐴, ℝ*, < ) = +∞ → +∞ = sup(𝐴, ℝ*, < ))
1110adantl 481 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → +∞ = sup(𝐴, ℝ*, < ))
128, 11breqtrd 5169 . 2 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
13 simpl 482 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝜑)
14 1rp 13038 . . . . . . . 8 1 ∈ ℝ+
15 nfcv 2905 . . . . . . . . . 10 𝑥1
16 supxrgere.xph . . . . . . . . . . . 12 𝑥𝜑
17 nfv 1914 . . . . . . . . . . . 12 𝑥1 ∈ ℝ+
1816, 17nfan 1899 . . . . . . . . . . 11 𝑥(𝜑 ∧ 1 ∈ ℝ+)
19 nfv 1914 . . . . . . . . . . 11 𝑥𝑦𝐴 (𝐵 − 1) < 𝑦
2018, 19nfim 1896 . . . . . . . . . 10 𝑥((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)
21 eleq1 2829 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈ ℝ+))
2221anbi2d 630 . . . . . . . . . . 11 (𝑥 = 1 → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈ ℝ+)))
23 oveq2 7439 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝐵𝑥) = (𝐵 − 1))
2423breq1d 5153 . . . . . . . . . . . 12 (𝑥 = 1 → ((𝐵𝑥) < 𝑦 ↔ (𝐵 − 1) < 𝑦))
2524rexbidv 3179 . . . . . . . . . . 11 (𝑥 = 1 → (∃𝑦𝐴 (𝐵𝑥) < 𝑦 ↔ ∃𝑦𝐴 (𝐵 − 1) < 𝑦))
2622, 25imbi12d 344 . . . . . . . . . 10 (𝑥 = 1 → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 (𝐵𝑥) < 𝑦) ↔ ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)))
27 supxrgere.y . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 (𝐵𝑥) < 𝑦)
2815, 20, 26, 27vtoclgf 3569 . . . . . . . . 9 (1 ∈ ℝ+ → ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦))
2914, 28ax-mp 5 . . . . . . . 8 ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)
3014, 29mpan2 691 . . . . . . 7 (𝜑 → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)
3130adantr 480 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)
32 mnfxr 11318 . . . . . . . . . . 11 -∞ ∈ ℝ*
3332a1i 11 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ ∈ ℝ*)
34 supxrgere.a . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ*)
3534sselda 3983 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ*)
36353adant3 1133 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → 𝑦 ∈ ℝ*)
37 supxrcl 13357 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
3834, 37syl 17 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
39383ad2ant1 1134 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
40 peano2rem 11576 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
411, 40syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 − 1) ∈ ℝ)
4241rexrd 11311 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 1) ∈ ℝ*)
4342adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) ∈ ℝ*)
44433ad2antl1 1186 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) ∈ ℝ*)
4536adantr 480 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*)
4632a1i 11 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → -∞ ∈ ℝ*)
47 simpl3 1194 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) < 𝑦)
48 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ < 𝑦)
4935adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*)
5032a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → -∞ ∈ ℝ*)
51 xrlenlt 11326 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ* ∧ -∞ ∈ ℝ*) → (𝑦 ≤ -∞ ↔ ¬ -∞ < 𝑦))
5249, 50, 51syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 ≤ -∞ ↔ ¬ -∞ < 𝑦))
5348, 52mpbird 257 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ≤ -∞)
54533adantl3 1169 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → 𝑦 ≤ -∞)
5544, 45, 46, 47, 54xrltletrd 13203 . . . . . . . . . . 11 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) < -∞)
56 nltmnf 13171 . . . . . . . . . . . . . 14 ((𝐵 − 1) ∈ ℝ* → ¬ (𝐵 − 1) < -∞)
5742, 56syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ (𝐵 − 1) < -∞)
5857adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ -∞ < 𝑦) → ¬ (𝐵 − 1) < -∞)
59583ad2antl1 1186 . . . . . . . . . . 11 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → ¬ (𝐵 − 1) < -∞)
6055, 59condan 818 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ < 𝑦)
6134adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝐴 ⊆ ℝ*)
62 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦𝐴)
63 supxrub 13366 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ*𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6461, 62, 63syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
65643adant3 1133 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6633, 36, 39, 60, 65xrltletrd 13203 . . . . . . . . 9 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ < sup(𝐴, ℝ*, < ))
67663exp 1120 . . . . . . . 8 (𝜑 → (𝑦𝐴 → ((𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, < ))))
6867adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (𝑦𝐴 → ((𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, < ))))
6968rexlimdv 3153 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (∃𝑦𝐴 (𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, < )))
7031, 69mpd 15 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → -∞ < sup(𝐴, ℝ*, < ))
71 simpr 484 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ sup(𝐴, ℝ*, < ) = +∞)
72 nltpnft 13206 . . . . . . . . 9 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7338, 72syl 17 . . . . . . . 8 (𝜑 → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7473adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7571, 74mtbid 324 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ ¬ sup(𝐴, ℝ*, < ) < +∞)
7675notnotrd 133 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) < +∞)
7770, 76jca 511 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞))
7838adantr 480 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
79 xrrebnd 13210 . . . . 5 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
8078, 79syl 17 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
8177, 80mpbird 257 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ)
82 simpl 482 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ))
83 simpr 484 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ 𝐵 ≤ sup(𝐴, ℝ*, < ))
8482simprd 495 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) ∈ ℝ)
851ad2antrr 726 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → 𝐵 ∈ ℝ)
8684, 85ltnled 11408 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8783, 86mpbird 257 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) < 𝐵)
88 simpll 767 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝜑)
891adantr 480 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ∈ ℝ)
90 simpr 484 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℝ)
9189, 90resubcld 11691 . . . . . . . . 9 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
9291adantr 480 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ)
93 simpr 484 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) < 𝐵)
9490adantr 480 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈ ℝ)
9588, 1syl 17 . . . . . . . . . 10 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ)
9694, 95posdifd 11850 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ 0 < (𝐵 − sup(𝐴, ℝ*, < ))))
9793, 96mpbid 232 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 0 < (𝐵 − sup(𝐴, ℝ*, < )))
9892, 97elrpd 13074 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
99 ovex 7464 . . . . . . . 8 (𝐵 − sup(𝐴, ℝ*, < )) ∈ V
100 nfcv 2905 . . . . . . . . 9 𝑥(𝐵 − sup(𝐴, ℝ*, < ))
101 nfv 1914 . . . . . . . . . . 11 𝑥(𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+
10216, 101nfan 1899 . . . . . . . . . 10 𝑥(𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
103 nfv 1914 . . . . . . . . . 10 𝑥𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦
104102, 103nfim 1896 . . . . . . . . 9 𝑥((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)
105 eleq1 2829 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑥 ∈ ℝ+ ↔ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+))
106105anbi2d 630 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)))
107 oveq2 7439 . . . . . . . . . . . 12 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝐵𝑥) = (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))))
108107breq1d 5153 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → ((𝐵𝑥) < 𝑦 ↔ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦))
109108rexbidv 3179 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (∃𝑦𝐴 (𝐵𝑥) < 𝑦 ↔ ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦))
110106, 109imbi12d 344 . . . . . . . . 9 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 (𝐵𝑥) < 𝑦) ↔ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)))
111100, 104, 110, 27vtoclgf 3569 . . . . . . . 8 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ V → ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦))
11299, 111ax-mp 5 . . . . . . 7 ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)
11388, 98, 112syl2anc 584 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)
1141recnd 11289 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℂ)
115114ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → 𝐵 ∈ ℂ)
11690recnd 11289 . . . . . . . . . . . . 13 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
117116ad2antrr 726 . . . . . . . . . . . 12 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) ∈ ℂ)
118115, 117nncand 11625 . . . . . . . . . . 11 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) = sup(𝐴, ℝ*, < ))
119118eqcomd 2743 . . . . . . . . . 10 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) = (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))))
120 simpr 484 . . . . . . . . . 10 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)
121119, 120eqbrtrd 5165 . . . . . . . . 9 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) < 𝑦)
122121ex 412 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ((𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → sup(𝐴, ℝ*, < ) < 𝑦))
123122adantr 480 . . . . . . 7 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) → ((𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → sup(𝐴, ℝ*, < ) < 𝑦))
124123reximdva 3168 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦))
125113, 124mpd 15 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
12682, 87, 125syl2anc 584 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
12761, 37syl 17 . . . . . . . . 9 ((𝜑𝑦𝐴) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
12835, 127xrlenltd 11327 . . . . . . . 8 ((𝜑𝑦𝐴) → (𝑦 ≤ sup(𝐴, ℝ*, < ) ↔ ¬ sup(𝐴, ℝ*, < ) < 𝑦))
12964, 128mpbid 232 . . . . . . 7 ((𝜑𝑦𝐴) → ¬ sup(𝐴, ℝ*, < ) < 𝑦)
130129ralrimiva 3146 . . . . . 6 (𝜑 → ∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦)
131 ralnex 3072 . . . . . 6 (∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦 ↔ ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
132130, 131sylib 218 . . . . 5 (𝜑 → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
133132ad2antrr 726 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
134126, 133condan 818 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
13513, 81, 134syl2anc 584 . 2 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
13612, 135pm2.61dan 813 1 (𝜑𝐵 ≤ sup(𝐴, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wnf 1783  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  wss 3951   class class class wbr 5143  (class class class)co 7431  supcsup 9480  cc 11153  cr 11154  0cc0 11155  1c1 11156  +∞cpnf 11292  -∞cmnf 11293  *cxr 11294   < clt 11295  cle 11296  cmin 11492  +crp 13034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-sup 9482  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-rp 13035
This theorem is referenced by:  suplesup  45350
  Copyright terms: Public domain W3C validator