![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltadd2dd | Structured version Visualization version Unicode version |
Description: Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
Ref | Expression |
---|---|
ltd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
ltd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
letrd.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
ltletrd.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ltadd2dd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltletrd.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ltd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | ltd.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | letrd.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | ltadd2d 9817 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | mpbid 215 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-resscn 9622 ax-addrcl 9626 ax-pre-lttri 9639 ax-pre-ltadd 9641 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-mpt 4477 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-ov 6318 df-er 7389 df-en 7596 df-dom 7597 df-sdom 7598 df-pnf 9703 df-mnf 9704 df-ltxr 9706 |
This theorem is referenced by: ccatrn 12769 eirrlem 14305 prmreclem5 14913 iccntr 21888 icccmplem2 21890 ivthlem2 22452 uniioombllem3 22592 opnmbllem 22608 dvcnvre 23020 cosordlem 23529 efif1olem2 23541 atanlogaddlem 23888 pntibndlem2 24478 pntlemr 24489 dya2icoseg 29148 opnmbllem0 32021 binomcxplemdvbinom 36746 zltlesub 37533 supxrge 37599 ltadd12dd 37604 0ellimcdiv 37768 ioodvbdlimc1lem2 37842 ioodvbdlimc1lem2OLD 37844 stoweidlem11 37909 stoweidlem14 37912 stoweidlem26 37924 stoweidlem44 37943 dirkertrigeqlem3 38000 dirkercncflem1 38003 dirkercncflem2 38004 fourierdlem4 38011 fourierdlem10 38017 fourierdlem28 38035 fourierdlem40 38048 fourierdlem50 38058 fourierdlem57 38065 fourierdlem59 38067 fourierdlem60 38068 fourierdlem61 38069 fourierdlem68 38076 fourierdlem74 38082 fourierdlem75 38083 fourierdlem76 38084 fourierdlem78 38086 fourierdlem79 38087 fourierdlem84 38092 fourierdlem93 38101 fourierdlem111 38119 fouriersw 38133 |
Copyright terms: Public domain | W3C validator |