![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lenltd | 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 |
---|---|
lenltd | ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | ltd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
3 | lenlt 10572 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∈ wcel 2083 class class class wbr 4968 ℝcr 10389 < clt 10528 ≤ cle 10529 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pr 5228 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-br 4969 df-opab 5031 df-xp 5456 df-cnv 5458 df-xr 10532 df-le 10534 |
This theorem is referenced by: ltnsymd 10642 nltled 10643 lensymd 10644 leadd1 10962 leord1 11021 lediv1 11359 lemuldiv 11374 lerec 11377 le2msq 11394 suprleub 11461 infregelb 11479 suprfinzcl 11951 uzinfi 12181 rpnnen1lem5 12234 nn0disj 12877 fleqceilz 13076 modsumfzodifsn 13166 addmodlteq 13168 leexp2 13389 expnngt1 13456 hashf1 13667 ccatsymb 13784 swrdccatin2 13931 isercoll 14862 ruclem3 15423 sadcaddlem 15643 pcfac 16068 sylow1lem1 18457 fvmptnn04if 21145 chfacfisf 21150 chfacfisfcpmat 21151 ivthlem2 23740 ioorcl2 23860 itg1ge0a 23999 mbfi1fseqlem4 24006 itg2monolem1 24038 itg2cnlem1 24049 mdegmullem 24359 quotcan 24585 logdivle 24890 cxple 24963 gausslemma2dlem1a 25627 padicabv 25892 upgrewlkle2 27075 pthdlem1 27233 ssnnssfz 30194 smattr 30675 smatbl 30676 smatbr 30677 esumpcvgval 30950 eulerpartlems 31231 dstfrvunirn 31345 ballotlemodife 31368 erdszelem7 32054 erdszelem8 32055 unbdqndv2lem1 33459 poimirlem2 34446 poimirlem7 34451 poimirlem10 34454 poimirlem11 34455 areacirc 34539 frlmvscadiccat 38693 rencldnfilem 38923 irrapxlem1 38925 monotoddzzfi 39045 radcnvrat 40205 reclt0d 41220 reclt0 41225 sqrlearg 41392 dvnxpaek 41790 volico 41832 sublevolico 41833 fourierdlem12 41968 fourierdlem42 41998 elaa2lem 42082 iundjiun 42306 hoidmvval0 42433 hoidmv1lelem2 42438 hoidmv1lelem3 42439 hoidmvlelem4 42444 hspdifhsp 42462 volico2 42487 ovolval2lem 42489 vonioo 42528 smfconst 42590 fzopredsuc 43061 stgoldbwt 43445 nnsum3primesle9 43463 bgoldbtbndlem1 43474 ssnn0ssfz 43897 |
Copyright terms: Public domain | W3C validator |