![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lensymd | Structured version Visualization version GIF version |
Description: 'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
lensymd.3 | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Ref | Expression |
---|---|
lensymd | ⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lensymd.3 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵) | |
2 | ltd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
3 | ltd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
4 | 2, 3 | lenltd 11405 | . 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
5 | 1, 4 | mpbid 232 | 1 ⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2106 class class class wbr 5148 ℝcr 11152 < clt 11293 ≤ cle 11294 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-br 5149 df-opab 5211 df-xp 5695 df-cnv 5697 df-xr 11297 df-le 11299 |
This theorem is referenced by: lbinf 12219 supaddc 12233 supmul1 12235 zsupss 12977 prodge0rd 13140 infmrp1 13383 fzdisj 13588 uzdisj 13634 fzouzdisj 13732 addmodlteq 13984 seqf1olem1 14079 seqf1olem2 14080 seqcoll 14500 seqcoll2 14501 ccatalpha 14628 rlimcld2 15611 rlimno1 15687 smupvallem 16517 lcmgcdlem 16640 4sqlem11 16989 ramcl2lem 17043 psdmul 22188 recld2 24850 nmoleub2lem3 25162 ivthlem3 25502 ovolicopnf 25573 dvferm1lem 26037 dvferm2lem 26039 dgrlb 26290 dgreq0 26320 aaliou3lem9 26407 radcnvle 26478 abelthlem2 26491 dvlog2lem 26709 lgsval2lem 27366 pntlem3 27668 irredminply 33722 unblimceq0lem 36489 unblimceq0 36490 mblfinlem2 37645 imo72b2 44162 climisp 45702 stoweidlem52 46008 fourierdlem10 46073 fourierdlem12 46075 fourierdlem20 46083 fourierdlem50 46112 fourierdlem54 46116 fourierdlem103 46165 fouriersw 46187 etransclem35 46225 etransc 46239 |
Copyright terms: Public domain | W3C validator |