Theorem iooltub 40251

Description: An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
iooltub	⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 < 𝐵)

Proof of Theorem iooltub

Step	Hyp	Ref	Expression
1		elioo2 12420	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
2		simp3 1132	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) → 𝐶 < 𝐵)
3	1, 2	syl6bi 243	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) → 𝐶 < 𝐵))
4	3	3impia 1109	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 < 𝐵)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071   ∈ wcel 2145   class class class wbr 4786  (class class class)co 6792  ℝcr 10136  ℝ^*cxr 10274   < clt 10275  (,)cioo 12379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7095  ax-cnex 10193  ax-resscn 10194  ax-pre-lttri 10211  ax-pre-lttrn 10212

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-1st 7314  df-2nd 7315  df-er 7895  df-en 8109  df-dom 8110  df-sdom 8111  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-ioo 12383

This theorem is referenced by:  iooshift  40263  icoopn  40266  iooiinicc  40283  iooltubd  40285  iooiinioc  40297  lptre2pt  40386  limcresiooub  40388  limcresioolb  40389  sinaover2ne0  40593  dvbdfbdioolem1  40657  dvbdfbdioolem2  40658  ioodvbdlimc1lem1  40660  ioodvbdlimc2lem  40663  fourierdlem27  40864  fourierdlem28  40865  fourierdlem40  40877  fourierdlem41  40878  fourierdlem46  40882  fourierdlem48  40884  fourierdlem49  40885  fourierdlem57  40893  fourierdlem59  40895  fourierdlem60  40896  fourierdlem61  40897  fourierdlem62  40898  fourierdlem64  40900  fourierdlem68  40904  fourierdlem73  40909  fourierdlem76  40912  fourierdlem78  40914  fourierdlem84  40920  fourierdlem90  40926  fourierdlem92  40928  fourierdlem97  40933  fourierdlem103  40939  fourierdlem104  40940  fourierdlem111  40947  sqwvfoura  40958  sqwvfourb  40959  fouriersw  40961  etransclem23  40987  qndenserrnbllem  41027  ioorrnopnlem  41037  ioorrnopnxrlem  41039  hspdifhsp  41346  hoiqssbllem1  41352  hoiqssbllem2  41353  hspmbllem2  41357  iunhoiioolem  41405  pimiooltgt  41437  pimdecfgtioo  41443  pimincfltioo  41444  smfaddlem1  41487  smfmullem1  41514  smfmullem2  41515