| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > leloed | Structured version Visualization version GIF version | ||
| Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
| Ref | Expression |
|---|---|
| ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
| Ref | Expression |
|---|---|
| leloed | ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
| 2 | ltd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
| 3 | leloe 11302 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) | |
| 4 | 1, 2, 3 | syl2anc 595 | 1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∨ wo 860 = wceq 1569 ∈ wcel 2142 class class class wbr 5108 ℝcr 11105 < clt 11249 ≤ cle 11250 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-resscn 11163 ax-pre-lttri 11180 |
| This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-br 5109 df-opab 5173 df-mpt 5192 df-id 5555 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 |
| This theorem is used by: mulge0 11738 prodgt0 12068 lemul1 12073 fimaxre 12165 fiminre 12168 supfirege 12208 nn0le2is012 12666 nn0o1gt2 16445 2mulprm 16757 reconnlem1 24995 reconnlem2 24996 ivthle 25626 ivthle2 25627 ovolicc2lem3 25689 itgsplitioo 26008 dvlip 26163 dvge0 26176 dvfsumlem1 26196 dgrco 26443 plydivex 26469 coseq00topi 26678 logreclem 26938 scvxcvx 27161 pntrlog2bndlem5 27756 fzo0opth 33159 dnibndlem13 37107 lcmineqlem23 42846 lcmineqlem 42847 aks4d1p1 42871 sticksstones12a 42952 sticksstones22 42963 elpell1qr2 43627 pellfundex 43641 fmul01lt1lem2 46329 wallispilem3 46809 fourierdlem25 46874 fourierdlem42 46891 chnsubseqwl 47623 lighneallem4b 48389 nprmdvdsfacm1lem2 48401 nn0o1gt2ALTV 48487 stgoldbwt 48569 sbgoldbwt 48570 sbgoldbalt 48574 nnsum3primesle9 48587 bgoldbtbndlem1 48598 |
| Copyright terms: Public domain | W3C validator |