Theorem leltadd 10094

Description: Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)

Assertion

Ref	Expression
leltadd	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( A + B ) < ( C + D ) ) )

Proof of Theorem leltadd

Step	Hyp	Ref	Expression
1		ltleadd 10093	. . . . 5 |- ( ( ( B e. RR /\ A e. RR ) /\ ( D e. RR /\ C e. RR ) ) -> ( ( B < D /\ A <_ C ) -> ( B + A ) < ( D + C ) ) )
2	1	ancomsd 455	. . . 4 |- ( ( ( B e. RR /\ A e. RR ) /\ ( D e. RR /\ C e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( B + A ) < ( D + C ) ) )
3	2	ancom2s 809	. . 3 |- ( ( ( B e. RR /\ A e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( B + A ) < ( D + C ) ) )
4	3	ancom1s 812	. 2 |- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( B + A ) < ( D + C ) ) )
5		recn 9625	. . . 4 |- ( A e. RR -> A e. CC )
6		recn 9625	. . . 4 |- ( B e. RR -> B e. CC )
7		addcom 9815	. . . 4 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
8	5, 6, 7	syl2an 479	. . 3 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
9		recn 9625	. . . 4 |- ( C e. RR -> C e. CC )
10		recn 9625	. . . 4 |- ( D e. RR -> D e. CC )
11		addcom 9815	. . . 4 |- ( ( C e. CC /\ D e. CC ) -> ( C + D ) = ( D + C ) )
12	9, 10, 11	syl2an 479	. . 3 |- ( ( C e. RR /\ D e. RR ) -> ( C + D ) = ( D + C ) )
13	8, 12	breqan12d 4433	. 2 |- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + B ) < ( C + D ) <-> ( B + A ) < ( D + C ) ) )
14	4, 13	sylibrd 237	1 |- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( A + B ) < ( C + D ) ) )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1867   class class class wbr 4417  (class class class)co 6297   CCcc 9533   RRcr 9534   + caddc 9538   < clt 9671   <_ cle 9672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589  ax-resscn 9592  ax-1cn 9593  ax-icn 9594  ax-addcl 9595  ax-addrcl 9596  ax-mulcl 9597  ax-mulrcl 9598  ax-mulcom 9599  ax-addass 9600  ax-mulass 9601  ax-distr 9602  ax-i2m1 9603  ax-1ne0 9604  ax-1rid 9605  ax-rnegex 9606  ax-rrecex 9607  ax-cnre 9608  ax-pre-lttri 9609  ax-pre-lttrn 9610  ax-pre-ltadd 9611

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4477  df-mpt 4478  df-id 4761  df-po 4767  df-so 4768  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6300  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9673  df-mnf 9674  df-xr 9675  df-ltxr 9676  df-le 9677

This theorem is referenced by:  lt2add  10095  addgegt0  10097  leltaddd  10231  fldiv  12080