Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > lenlt | GIF version |
Description: 'Less than or equal to' expressed in terms of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-May-1999.) |
Ref | Expression |
---|---|
lenlt | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexr 7969 | . 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 7969 | . 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | xrlenlt 7988 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | 1, 2, 3 | syl2an 287 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∈ wcel 2142 class class class wbr 3990 ℝcr 7777 ℝ*cxr 7957 < clt 7958 ≤ cle 7959 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-14 2145 ax-ext 2153 ax-sep 4108 ax-pow 4161 ax-pr 4195 |
This theorem depends on definitions: df-bi 116 df-3an 976 df-tru 1352 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ral 2454 df-rex 2455 df-v 2733 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-br 3991 df-opab 4052 df-xp 4618 df-cnv 4620 df-xr 7962 df-le 7964 |
This theorem is referenced by: letri3 8004 ltleletr 8005 letr 8006 leid 8007 eqlelt 8010 ltle 8011 lelttr 8012 ltletr 8013 lenlti 8024 lenltd 8041 lemul1 8516 msqge0 8539 mulge0 8542 ltleap 8555 recgt0 8770 lediv1 8789 dfinfre 8876 nnge1 8905 nnnlt1 8908 avgle1 9122 avgle2 9123 nn0nlt0 9165 zltnle 9262 zleloe 9263 zdcle 9292 recnz 9309 btwnnz 9310 prime 9315 fznlem 10001 fzonlt0 10127 qltnle 10206 bcval4 10690 resqrexlemgt0 10988 climge0 11292 infpnlem1 12315 efle 13576 logleb 13675 cxple 13716 cxple3 13720 lgsval2lem 13790 lgsneg 13804 lgsdilem 13807 supfz 14185 inffz 14186 |
Copyright terms: Public domain | W3C validator |