Theorem ltsrpr 9265

Description: Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)

Assertion

Ref	Expression
ltsrpr	|- ( [ <. A , B >. ] ~R <R [ <. C , D >. ] ~R <-> ( A +P. D ) <P ( B +P. C ) )

Proof of Theorem ltsrpr

Dummy variables x y z w v u f are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		enrex 9258	. 2 |- ~R e. _V
2		enrer 9256	. . 3 |- ~R Er ( P. X. P. )
3		erdm 7132	. . 3 |- ( ~R Er ( P. X. P. ) -> dom ~R = ( P. X. P. ) )
4	2, 3	ax-mp 5	. 2 |- dom ~R = ( P. X. P. )
5		df-nr 9248	. 2 |- R. = ( ( P. X. P. ) /. ~R )
6		ltrelsr 9259	. 2 |- <R C_ ( R. X. R. )
7		ltrelpr 9188	. 2 |- <P C_ ( P. X. P. )
8		0npr 9182	. 2 |- -. (/) e. P.
9		dmplp 9202	. 2 |- dom +P. = ( P. X. P. )
10		df-ltr 9251	. . 3 |- <R = { <. x , y >. | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) ) ) }
11		addclpr 9208	. . . . . . 7 |- ( ( w e. P. /\ v e. P. ) -> ( w +P. v ) e. P. )
12	11	ad2ant2lr 747	. . . . . 6 |- ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( w +P. v ) e. P. )
13		addclpr 9208	. . . . . . 7 |- ( ( B e. P. /\ C e. P. ) -> ( B +P. C ) e. P. )
14	13	ad2ant2lr 747	. . . . . 6 |- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( B +P. C ) e. P. )
15	12, 14	anim12ci 567	. . . . 5 |- ( ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) /\ ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) )
16	15	an4s 822	. . . 4 |- ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) )
17		enreceq 9257	. . . . . 6 |- ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) -> ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R <-> ( z +P. B ) = ( w +P. A ) ) )
18		enreceq 9257	. . . . . . 7 |- ( ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. v , u >. ] ~R = [ <. C , D >. ] ~R <-> ( v +P. D ) = ( u +P. C ) ) )
19		eqcom 2445	. . . . . . 7 |- ( ( v +P. D ) = ( u +P. C ) <-> ( u +P. C ) = ( v +P. D ) )
20	18, 19	syl6bb 261	. . . . . 6 |- ( ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. v , u >. ] ~R = [ <. C , D >. ] ~R <-> ( u +P. C ) = ( v +P. D ) ) )
21	17, 20	bi2anan9 868	. . . . 5 |- ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) <-> ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) ) )
22		oveq12 6121	. . . . . 6 |- ( ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) -> ( ( z +P. B ) +P. ( u +P. C ) ) = ( ( w +P. A ) +P. ( v +P. D ) ) )
23		addcompr 9211	. . . . . . . . . 10 |- ( u +P. B ) = ( B +P. u )
24	23	oveq1i 6122	. . . . . . . . 9 |- ( ( u +P. B ) +P. C ) = ( ( B +P. u ) +P. C )
25		addasspr 9212	. . . . . . . . 9 |- ( ( u +P. B ) +P. C ) = ( u +P. ( B +P. C ) )
26		addasspr 9212	. . . . . . . . 9 |- ( ( B +P. u ) +P. C ) = ( B +P. ( u +P. C ) )
27	24, 25, 26	3eqtr3i 2471	. . . . . . . 8 |- ( u +P. ( B +P. C ) ) = ( B +P. ( u +P. C ) )
28	27	oveq2i 6123	. . . . . . 7 |- ( z +P. ( u +P. ( B +P. C ) ) ) = ( z +P. ( B +P. ( u +P. C ) ) )
29		addasspr 9212	. . . . . . 7 |- ( ( z +P. u ) +P. ( B +P. C ) ) = ( z +P. ( u +P. ( B +P. C ) ) )
30		addasspr 9212	. . . . . . 7 |- ( ( z +P. B ) +P. ( u +P. C ) ) = ( z +P. ( B +P. ( u +P. C ) ) )
31	28, 29, 30	3eqtr4i 2473	. . . . . 6 |- ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( z +P. B ) +P. ( u +P. C ) )
32		addcompr 9211	. . . . . . . . . 10 |- ( v +P. A ) = ( A +P. v )
33	32	oveq1i 6122	. . . . . . . . 9 |- ( ( v +P. A ) +P. D ) = ( ( A +P. v ) +P. D )
34		addasspr 9212	. . . . . . . . 9 |- ( ( v +P. A ) +P. D ) = ( v +P. ( A +P. D ) )
35		addasspr 9212	. . . . . . . . 9 |- ( ( A +P. v ) +P. D ) = ( A +P. ( v +P. D ) )
36	33, 34, 35	3eqtr3i 2471	. . . . . . . 8 |- ( v +P. ( A +P. D ) ) = ( A +P. ( v +P. D ) )
37	36	oveq2i 6123	. . . . . . 7 |- ( w +P. ( v +P. ( A +P. D ) ) ) = ( w +P. ( A +P. ( v +P. D ) ) )
38		addasspr 9212	. . . . . . 7 |- ( ( w +P. v ) +P. ( A +P. D ) ) = ( w +P. ( v +P. ( A +P. D ) ) )
39		addasspr 9212	. . . . . . 7 |- ( ( w +P. A ) +P. ( v +P. D ) ) = ( w +P. ( A +P. ( v +P. D ) ) )
40	37, 38, 39	3eqtr4i 2473	. . . . . 6 |- ( ( w +P. v ) +P. ( A +P. D ) ) = ( ( w +P. A ) +P. ( v +P. D ) )
41	22, 31, 40	3eqtr4g 2500	. . . . 5 |- ( ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) -> ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) )
42	21, 41	syl6bi 228	. . . 4 |- ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) -> ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) ) )
43		ovex 6137	. . . . 5 |- ( z +P. u ) e. _V
44		ovex 6137	. . . . 5 |- ( B +P. C ) e. _V
45		ltapr 9235	. . . . 5 |- ( f e. P. -> ( x <P y <-> ( f +P. x ) <P ( f +P. y ) ) )
46		ovex 6137	. . . . 5 |- ( w +P. v ) e. _V
47		addcompr 9211	. . . . 5 |- ( x +P. y ) = ( y +P. x )
48		ovex 6137	. . . . 5 |- ( A +P. D ) e. _V
49	43, 44, 45, 46, 47, 48	caovord3 6297	. . . 4 |- ( ( ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) /\ ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) ) -> ( ( z +P. u ) <P ( w +P. v ) <-> ( A +P. D ) <P ( B +P. C ) ) )
50	16, 42, 49	syl6an 545	. . 3 |- ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) -> ( ( z +P. u ) <P ( w +P. v ) <-> ( A +P. D ) <P ( B +P. C ) ) ) )
51	1, 2, 5, 10, 50	brecop 7214	. 2 |- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R <R [ <. C , D >. ] ~R <-> ( A +P. D ) <P ( B +P. C ) ) )
52	1, 4, 5, 6, 7, 8, 9, 51	brecop2 7215	1 |- ( [ <. A , B >. ] ~R <R [ <. C , D >. ] ~R <-> ( A +P. D ) <P ( B +P. C ) )

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   <.cop 3904   class class class wbr 4313   X. cxp 4859   dom cdm 4861  (class class class)co 6112   Er wer 7119   [cec 7120   P.cnp 9047   +P. cpp 9049   <P cltp 9051   ~R cer 9054   R.cnr 9055   <R cltr 9061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-inf2 7868

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-recs 6853  df-rdg 6887  df-1o 6941  df-oadd 6945  df-omul 6946  df-er 7122  df-ec 7124  df-qs 7128  df-ni 9062  df-pli 9063  df-mi 9064  df-lti 9065  df-plpq 9098  df-mpq 9099  df-ltpq 9100  df-enq 9101  df-nq 9102  df-erq 9103  df-plq 9104  df-mq 9105  df-1nq 9106  df-rq 9107  df-ltnq 9108  df-np 9171  df-plp 9173  df-ltp 9175  df-enr 9247  df-nr 9248  df-ltr 9251

This theorem is referenced by:  gt0srpr  9266  ltsosr  9282  0lt1sr  9283  ltasr  9288  mappsrpr  9296  ltpsrpr  9297  map2psrpr  9298