![]() |
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 7435 | . 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 7435 | . 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | xrlenlt 7453 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | 1, 2, 3 | syl2an 283 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 102 ↔ wb 103 ∈ wcel 1434 class class class wbr 3811 ℝcr 7251 ℝ*cxr 7423 < clt 7424 ≤ cle 7425 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3922 ax-pow 3974 ax-pr 3999 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-v 2614 df-dif 2986 df-un 2988 df-in 2990 df-ss 2997 df-pw 3408 df-sn 3428 df-pr 3429 df-op 3431 df-br 3812 df-opab 3866 df-xp 4406 df-cnv 4408 df-xr 7428 df-le 7430 |
This theorem is referenced by: letri3 7468 ltleletr 7469 letr 7470 leid 7471 ltle 7474 lelttr 7475 ltletr 7476 lenlti 7487 lenltd 7503 lemul1 7969 msqge0 7992 mulge0 7995 ltleap 8006 recgt0 8204 lediv1 8223 dfinfre 8310 nnge1 8338 nnnlt1 8341 avgle1 8547 avgle2 8548 nn0nlt0 8590 zltnle 8691 zleloe 8692 zdcle 8718 recnz 8734 btwnnz 8735 prime 8740 fznlem 9349 fzonlt0 9466 qltnle 9545 bcval4 9994 resqrexlemgt0 10279 climge0 10536 |
Copyright terms: Public domain | W3C validator |