Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xrlenltd | Structured version Visualization version GIF version |
Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
xrlenltd.a | ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
xrlenltd.b | ⊢ (𝜑 → 𝐵 ∈ ℝ*) |
Ref | Expression |
---|---|
xrlenltd | ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrlenltd.a | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ*) | |
2 | xrlenltd.b | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ*) | |
3 | xrlenlt 11041 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∈ wcel 2110 class class class wbr 5079 ℝ*cxr 11009 < clt 11010 ≤ cle 11011 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 ax-sep 5227 ax-nul 5234 ax-pr 5356 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-ral 3071 df-rex 3072 df-rab 3075 df-v 3433 df-dif 3895 df-un 3897 df-nul 4263 df-if 4466 df-sn 4568 df-pr 4570 df-op 4574 df-br 5080 df-opab 5142 df-xp 5596 df-cnv 5598 df-le 11016 |
This theorem is referenced by: xrnltled 11044 supxrleub 13059 infxrgelb 13068 ixxub 13099 ixxlb 13100 icodisj 13207 supicclub2 13235 bldisj 23549 icombl 24726 ioorcl2 24734 ply1divmo 25298 ig1peu 25334 psercnlem1 25582 infxrge0gelb 31085 supxrgere 42843 supxrgelem 42847 lenelioc 43045 iccdificc 43048 limsupub 43216 fge0iccico 43879 sge0sn 43888 sge0rpcpnf 43930 pimltmnf2 44206 pimconstlt0 44209 pimgtpnf2 44212 pimdecfgtioo 44222 pimincfltioo 44223 |
Copyright terms: Public domain | W3C validator |