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

Theorem eliccnelico 44228
Description: An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
eliccnelico.1 (𝜑𝐴 ∈ ℝ*)
eliccnelico.b (𝜑𝐵 ∈ ℝ*)
eliccnelico.c (𝜑𝐶 ∈ (𝐴[,]𝐵))
eliccnelico.nel (𝜑 → ¬ 𝐶 ∈ (𝐴[,)𝐵))
Assertion
Ref Expression
eliccnelico (𝜑𝐶 = 𝐵)

Proof of Theorem eliccnelico
StepHypRef Expression
1 eliccnelico.c . . 3 (𝜑𝐶 ∈ (𝐴[,]𝐵))
2 eliccxr 13408 . . 3 (𝐶 ∈ (𝐴[,]𝐵) → 𝐶 ∈ ℝ*)
31, 2syl 17 . 2 (𝜑𝐶 ∈ ℝ*)
4 eliccnelico.b . 2 (𝜑𝐵 ∈ ℝ*)
5 eliccnelico.1 . . 3 (𝜑𝐴 ∈ ℝ*)
6 iccleub 13375 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,]𝐵)) → 𝐶𝐵)
75, 4, 1, 6syl3anc 1371 . 2 (𝜑𝐶𝐵)
85adantr 481 . . . 4 ((𝜑 ∧ ¬ 𝐵𝐶) → 𝐴 ∈ ℝ*)
94adantr 481 . . . 4 ((𝜑 ∧ ¬ 𝐵𝐶) → 𝐵 ∈ ℝ*)
103adantr 481 . . . 4 ((𝜑 ∧ ¬ 𝐵𝐶) → 𝐶 ∈ ℝ*)
11 iccgelb 13376 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ (𝐴[,]𝐵)) → 𝐴𝐶)
125, 4, 1, 11syl3anc 1371 . . . . 5 (𝜑𝐴𝐶)
1312adantr 481 . . . 4 ((𝜑 ∧ ¬ 𝐵𝐶) → 𝐴𝐶)
14 simpr 485 . . . . 5 ((𝜑 ∧ ¬ 𝐵𝐶) → ¬ 𝐵𝐶)
15 xrltnle 11277 . . . . . . 7 ((𝐶 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐶 < 𝐵 ↔ ¬ 𝐵𝐶))
163, 4, 15syl2anc 584 . . . . . 6 (𝜑 → (𝐶 < 𝐵 ↔ ¬ 𝐵𝐶))
1716adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐵𝐶) → (𝐶 < 𝐵 ↔ ¬ 𝐵𝐶))
1814, 17mpbird 256 . . . 4 ((𝜑 ∧ ¬ 𝐵𝐶) → 𝐶 < 𝐵)
198, 9, 10, 13, 18elicod 13370 . . 3 ((𝜑 ∧ ¬ 𝐵𝐶) → 𝐶 ∈ (𝐴[,)𝐵))
20 eliccnelico.nel . . . 4 (𝜑 → ¬ 𝐶 ∈ (𝐴[,)𝐵))
2120adantr 481 . . 3 ((𝜑 ∧ ¬ 𝐵𝐶) → ¬ 𝐶 ∈ (𝐴[,)𝐵))
2219, 21condan 816 . 2 (𝜑𝐵𝐶)
233, 4, 7, 22xrletrid 13130 1 (𝜑𝐶 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106   class class class wbr 5147  (class class class)co 7405  *cxr 11243   < clt 11244  cle 11245  [,)cico 13322  [,]cicc 13323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-ico 13326  df-icc 13327
This theorem is referenced by:  sge0f1o  45084
  Copyright terms: Public domain W3C validator