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 44343
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 11265 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3 pnfxr 11273 . . . . . . 7 +∞ ∈ ℝ*
43a1i 11 . . . . . 6 (𝐵 ∈ ℝ → +∞ ∈ ℝ*)
5 ltpnf 13105 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 < +∞)
62, 4, 5xrltled 13134 . . . . 5 (𝐵 ∈ ℝ → 𝐵 ≤ +∞)
71, 6syl 17 . . . 4 (𝜑𝐵 ≤ +∞)
87adantr 480 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ +∞)
9 id 22 . . . . 5 (sup(𝐴, ℝ*, < ) = +∞ → sup(𝐴, ℝ*, < ) = +∞)
109eqcomd 2737 . . . 4 (sup(𝐴, ℝ*, < ) = +∞ → +∞ = sup(𝐴, ℝ*, < ))
1110adantl 481 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → +∞ = sup(𝐴, ℝ*, < ))
128, 11breqtrd 5175 . 2 ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
13 simpl 482 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝜑)
14 1rp 12983 . . . . . . . 8 1 ∈ ℝ+
15 nfcv 2902 . . . . . . . . . 10 𝑥1
16 supxrgere.xph . . . . . . . . . . . 12 𝑥𝜑
17 nfv 1916 . . . . . . . . . . . 12 𝑥1 ∈ ℝ+
1816, 17nfan 1901 . . . . . . . . . . 11 𝑥(𝜑 ∧ 1 ∈ ℝ+)
19 nfv 1916 . . . . . . . . . . 11 𝑥𝑦𝐴 (𝐵 − 1) < 𝑦
2018, 19nfim 1898 . . . . . . . . . 10 𝑥((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)
21 eleq1 2820 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈ ℝ+))
2221anbi2d 628 . . . . . . . . . . 11 (𝑥 = 1 → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈ ℝ+)))
23 oveq2 7420 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝐵𝑥) = (𝐵 − 1))
2423breq1d 5159 . . . . . . . . . . . 12 (𝑥 = 1 → ((𝐵𝑥) < 𝑦 ↔ (𝐵 − 1) < 𝑦))
2524rexbidv 3177 . . . . . . . . . . 11 (𝑥 = 1 → (∃𝑦𝐴 (𝐵𝑥) < 𝑦 ↔ ∃𝑦𝐴 (𝐵 − 1) < 𝑦))
2622, 25imbi12d 343 . . . . . . . . . 10 (𝑥 = 1 → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 (𝐵𝑥) < 𝑦) ↔ ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)))
27 supxrgere.y . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 (𝐵𝑥) < 𝑦)
2815, 20, 26, 27vtoclgf 3555 . . . . . . . . 9 (1 ∈ ℝ+ → ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦))
2914, 28ax-mp 5 . . . . . . . 8 ((𝜑 ∧ 1 ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)
3014, 29mpan2 688 . . . . . . 7 (𝜑 → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)
3130adantr 480 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ∃𝑦𝐴 (𝐵 − 1) < 𝑦)
32 mnfxr 11276 . . . . . . . . . . 11 -∞ ∈ ℝ*
3332a1i 11 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ ∈ ℝ*)
34 supxrgere.a . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ*)
3534sselda 3983 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ∈ ℝ*)
36353adant3 1131 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → 𝑦 ∈ ℝ*)
37 supxrcl 13299 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
3834, 37syl 17 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
39383ad2ant1 1132 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
40 peano2rem 11532 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
411, 40syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 − 1) ∈ ℝ)
4241rexrd 11269 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 1) ∈ ℝ*)
4342adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) ∈ ℝ*)
44433ad2antl1 1184 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) ∈ ℝ*)
4536adantr 480 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*)
4632a1i 11 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → -∞ ∈ ℝ*)
47 simpl3 1192 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) < 𝑦)
48 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ < 𝑦)
4935adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*)
5032a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → -∞ ∈ ℝ*)
51 xrlenlt 11284 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ* ∧ -∞ ∈ ℝ*) → (𝑦 ≤ -∞ ↔ ¬ -∞ < 𝑦))
5249, 50, 51syl2anc 583 . . . . . . . . . . . . . 14 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 ≤ -∞ ↔ ¬ -∞ < 𝑦))
5348, 52mpbird 256 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ≤ -∞)
54533adantl3 1167 . . . . . . . . . . . 12 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → 𝑦 ≤ -∞)
5544, 45, 46, 47, 54xrltletrd 13145 . . . . . . . . . . 11 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) < -∞)
56 nltmnf 13114 . . . . . . . . . . . . . 14 ((𝐵 − 1) ∈ ℝ* → ¬ (𝐵 − 1) < -∞)
5742, 56syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ (𝐵 − 1) < -∞)
5857adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ -∞ < 𝑦) → ¬ (𝐵 − 1) < -∞)
59583ad2antl1 1184 . . . . . . . . . . 11 (((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → ¬ (𝐵 − 1) < -∞)
6055, 59condan 815 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ < 𝑦)
6134adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝐴 ⊆ ℝ*)
62 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → 𝑦𝐴)
63 supxrub 13308 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ*𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6461, 62, 63syl2anc 583 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
65643adant3 1131 . . . . . . . . . 10 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → 𝑦 ≤ sup(𝐴, ℝ*, < ))
6633, 36, 39, 60, 65xrltletrd 13145 . . . . . . . . 9 ((𝜑𝑦𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ < sup(𝐴, ℝ*, < ))
67663exp 1118 . . . . . . . 8 (𝜑 → (𝑦𝐴 → ((𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, < ))))
6867adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (𝑦𝐴 → ((𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, < ))))
6968rexlimdv 3152 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (∃𝑦𝐴 (𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, < )))
7031, 69mpd 15 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → -∞ < sup(𝐴, ℝ*, < ))
71 simpr 484 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ sup(𝐴, ℝ*, < ) = +∞)
72 nltpnft 13148 . . . . . . . . 9 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7338, 72syl 17 . . . . . . . 8 (𝜑 → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7473adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) < +∞))
7571, 74mtbid 323 . . . . . 6 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → ¬ ¬ sup(𝐴, ℝ*, < ) < +∞)
7675notnotrd 133 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) < +∞)
7770, 76jca 511 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞))
7838adantr 480 . . . . 5 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
79 xrrebnd 13152 . . . . 5 (sup(𝐴, ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
8078, 79syl 17 . . . 4 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧ sup(𝐴, ℝ*, < ) < +∞)))
8177, 80mpbird 256 . . 3 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ)
82 simpl 482 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ))
83 simpr 484 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ 𝐵 ≤ sup(𝐴, ℝ*, < ))
8482simprd 495 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) ∈ ℝ)
851ad2antrr 723 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → 𝐵 ∈ ℝ)
8684, 85ltnled 11366 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )))
8783, 86mpbird 256 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → sup(𝐴, ℝ*, < ) < 𝐵)
88 simpll 764 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 𝜑)
891adantr 480 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ∈ ℝ)
90 simpr 484 . . . . . . . . . 10 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℝ)
9189, 90resubcld 11647 . . . . . . . . 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 11806 . . . . . . . . 9 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ 0 < (𝐵 − sup(𝐴, ℝ*, < ))))
9793, 96mpbid 231 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → 0 < (𝐵 − sup(𝐴, ℝ*, < )))
9892, 97elrpd 13018 . . . . . . 7 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
99 ovex 7445 . . . . . . . 8 (𝐵 − sup(𝐴, ℝ*, < )) ∈ V
100 nfcv 2902 . . . . . . . . 9 𝑥(𝐵 − sup(𝐴, ℝ*, < ))
101 nfv 1916 . . . . . . . . . . 11 𝑥(𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+
10216, 101nfan 1901 . . . . . . . . . 10 𝑥(𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)
103 nfv 1916 . . . . . . . . . 10 𝑥𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦
104102, 103nfim 1898 . . . . . . . . 9 𝑥((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)
105 eleq1 2820 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑥 ∈ ℝ+ ↔ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+))
106105anbi2d 628 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → ((𝜑𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+)))
107 oveq2 7420 . . . . . . . . . . . 12 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝐵𝑥) = (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))))
108107breq1d 5159 . . . . . . . . . . 11 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → ((𝐵𝑥) < 𝑦 ↔ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦))
109108rexbidv 3177 . . . . . . . . . 10 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (∃𝑦𝐴 (𝐵𝑥) < 𝑦 ↔ ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦))
110106, 109imbi12d 343 . . . . . . . . 9 (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (((𝜑𝑥 ∈ ℝ+) → ∃𝑦𝐴 (𝐵𝑥) < 𝑦) ↔ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)))
111100, 104, 110, 27vtoclgf 3555 . . . . . . . 8 ((𝐵 − sup(𝐴, ℝ*, < )) ∈ V → ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦))
11299, 111ax-mp 5 . . . . . . 7 ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈ ℝ+) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)
11388, 98, 112syl2anc 583 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)
1141recnd 11247 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℂ)
115114ad3antrrr 727 . . . . . . . . . . . 12 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → 𝐵 ∈ ℂ)
11690recnd 11247 . . . . . . . . . . . . 13 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈ ℂ)
117116ad2antrr 723 . . . . . . . . . . . 12 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) ∈ ℂ)
118115, 117nncand 11581 . . . . . . . . . . 11 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) = sup(𝐴, ℝ*, < ))
119118eqcomd 2737 . . . . . . . . . 10 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) = (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))))
120 simpr 484 . . . . . . . . . 10 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)
121119, 120eqbrtrd 5171 . . . . . . . . 9 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) < 𝑦)
122121ex 412 . . . . . . . 8 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ((𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → sup(𝐴, ℝ*, < ) < 𝑦))
123122adantr 480 . . . . . . 7 ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦𝐴) → ((𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → sup(𝐴, ℝ*, < ) < 𝑦))
124123reximdva 3167 . . . . . 6 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → (∃𝑦𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦))
125113, 124mpd 15 . . . . 5 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
12682, 87, 125syl2anc 583 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
12761, 37syl 17 . . . . . . . . 9 ((𝜑𝑦𝐴) → sup(𝐴, ℝ*, < ) ∈ ℝ*)
12835, 127xrlenltd 11285 . . . . . . . 8 ((𝜑𝑦𝐴) → (𝑦 ≤ sup(𝐴, ℝ*, < ) ↔ ¬ sup(𝐴, ℝ*, < ) < 𝑦))
12964, 128mpbid 231 . . . . . . 7 ((𝜑𝑦𝐴) → ¬ sup(𝐴, ℝ*, < ) < 𝑦)
130129ralrimiva 3145 . . . . . 6 (𝜑 → ∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦)
131 ralnex 3071 . . . . . 6 (∀𝑦𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦 ↔ ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
132130, 131sylib 217 . . . . 5 (𝜑 → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
133132ad2antrr 723 . . . 4 (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → ¬ ∃𝑦𝐴 sup(𝐴, ℝ*, < ) < 𝑦)
134126, 133condan 815 . . 3 ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
13513, 81, 134syl2anc 583 . 2 ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
13612, 135pm2.61dan 810 1 (𝜑𝐵 ≤ sup(𝐴, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1086   = wceq 1540  wnf 1784  wcel 2105  wral 3060  wrex 3069  Vcvv 3473  wss 3949   class class class wbr 5149  (class class class)co 7412  supcsup 9438  cc 11111  cr 11112  0cc0 11113  1c1 11114  +∞cpnf 11250  -∞cmnf 11251  *cxr 11252   < clt 11253  cle 11254  cmin 11449  +crp 12979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8706  df-en 8943  df-dom 8944  df-sdom 8945  df-sup 9440  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-rp 12980
This theorem is referenced by:  suplesup  44349
  Copyright terms: Public domain W3C validator