Theorem ltasr 9370

Description: Ordering property of addition. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)

Assertion

Ref	Expression
ltasr	|- ( C e. R. -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )

Proof of Theorem ltasr

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

Step	Hyp	Ref	Expression
1		dmaddsr 9355	. 2 |- dom +R = ( R. X. R. )
2		ltrelsr 9341	. 2 |- <R C_ ( R. X. R. )
3		0nsr 9349	. 2 |- -. (/) e. R.
4		df-nr 9330	. . . 4 |- R. = ( ( P. X. P. ) /. ~R )
5		oveq1 6199	. . . . . 6 |- ( [ <. v , u >. ] ~R = C -> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) = ( C +R [ <. x , y >. ] ~R ) )
6		oveq1 6199	. . . . . 6 |- ( [ <. v , u >. ] ~R = C -> ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) = ( C +R [ <. z , w >. ] ~R ) )
7	5, 6	breq12d 4405	. . . . 5 |- ( [ <. v , u >. ] ~R = C -> ( ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) <R ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) <-> ( C +R [ <. x , y >. ] ~R ) <R ( C +R [ <. z , w >. ] ~R ) ) )
8	7	bibi2d 318	. . . 4 |- ( [ <. v , u >. ] ~R = C -> ( ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) <R ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) ) <-> ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> ( C +R [ <. x , y >. ] ~R ) <R ( C +R [ <. z , w >. ] ~R ) ) ) )
9		breq1 4395	. . . . 5 |- ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> A <R [ <. z , w >. ] ~R ) )
10		oveq2 6200	. . . . . 6 |- ( [ <. x , y >. ] ~R = A -> ( C +R [ <. x , y >. ] ~R ) = ( C +R A ) )
11	10	breq1d 4402	. . . . 5 |- ( [ <. x , y >. ] ~R = A -> ( ( C +R [ <. x , y >. ] ~R ) <R ( C +R [ <. z , w >. ] ~R ) <-> ( C +R A ) <R ( C +R [ <. z , w >. ] ~R ) ) )
12	9, 11	bibi12d 321	. . . 4 |- ( [ <. x , y >. ] ~R = A -> ( ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> ( C +R [ <. x , y >. ] ~R ) <R ( C +R [ <. z , w >. ] ~R ) ) <-> ( A <R [ <. z , w >. ] ~R <-> ( C +R A ) <R ( C +R [ <. z , w >. ] ~R ) ) ) )
13		breq2 4396	. . . . 5 |- ( [ <. z , w >. ] ~R = B -> ( A <R [ <. z , w >. ] ~R <-> A <R B ) )
14		oveq2 6200	. . . . . 6 |- ( [ <. z , w >. ] ~R = B -> ( C +R [ <. z , w >. ] ~R ) = ( C +R B ) )
15	14	breq2d 4404	. . . . 5 |- ( [ <. z , w >. ] ~R = B -> ( ( C +R A ) <R ( C +R [ <. z , w >. ] ~R ) <-> ( C +R A ) <R ( C +R B ) ) )
16	13, 15	bibi12d 321	. . . 4 |- ( [ <. z , w >. ] ~R = B -> ( ( A <R [ <. z , w >. ] ~R <-> ( C +R A ) <R ( C +R [ <. z , w >. ] ~R ) ) <-> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) ) )
17		addclpr 9290	. . . . . . 7 |- ( ( v e. P. /\ u e. P. ) -> ( v +P. u ) e. P. )
18	17	3ad2ant1 1009	. . . . . 6 |- ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( v +P. u ) e. P. )
19		ltapr 9317	. . . . . . 7 |- ( ( v +P. u ) e. P. -> ( ( x +P. w ) <P ( y +P. z ) <-> ( ( v +P. u ) +P. ( x +P. w ) ) <P ( ( v +P. u ) +P. ( y +P. z ) ) ) )
20		ltsrpr 9347	. . . . . . 7 |- ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> ( x +P. w ) <P ( y +P. z ) )
21		ltsrpr 9347	. . . . . . . 8 |- ( [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R <R [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R <-> ( ( v +P. x ) +P. ( u +P. w ) ) <P ( ( u +P. y ) +P. ( v +P. z ) ) )
22		vex 3073	. . . . . . . . . 10 |- v e. _V
23		vex 3073	. . . . . . . . . 10 |- x e. _V
24		vex 3073	. . . . . . . . . 10 |- u e. _V
25		addcompr 9293	. . . . . . . . . 10 |- ( y +P. z ) = ( z +P. y )
26		addasspr 9294	. . . . . . . . . 10 |- ( ( y +P. z ) +P. f ) = ( y +P. ( z +P. f ) )
27		vex 3073	. . . . . . . . . 10 |- w e. _V
28	22, 23, 24, 25, 26, 27	caov4 6396	. . . . . . . . 9 |- ( ( v +P. x ) +P. ( u +P. w ) ) = ( ( v +P. u ) +P. ( x +P. w ) )
29		addcompr 9293	. . . . . . . . . 10 |- ( ( u +P. y ) +P. ( v +P. z ) ) = ( ( v +P. z ) +P. ( u +P. y ) )
30		vex 3073	. . . . . . . . . . 11 |- z e. _V
31		addcompr 9293	. . . . . . . . . . 11 |- ( x +P. w ) = ( w +P. x )
32		addasspr 9294	. . . . . . . . . . 11 |- ( ( x +P. w ) +P. f ) = ( x +P. ( w +P. f ) )
33		vex 3073	. . . . . . . . . . 11 |- y e. _V
34	22, 30, 24, 31, 32, 33	caov42 6398	. . . . . . . . . 10 |- ( ( v +P. z ) +P. ( u +P. y ) ) = ( ( v +P. u ) +P. ( y +P. z ) )
35	29, 34	eqtri 2480	. . . . . . . . 9 |- ( ( u +P. y ) +P. ( v +P. z ) ) = ( ( v +P. u ) +P. ( y +P. z ) )
36	28, 35	breq12i 4401	. . . . . . . 8 |- ( ( ( v +P. x ) +P. ( u +P. w ) ) <P ( ( u +P. y ) +P. ( v +P. z ) ) <-> ( ( v +P. u ) +P. ( x +P. w ) ) <P ( ( v +P. u ) +P. ( y +P. z ) ) )
37	21, 36	bitri 249	. . . . . . 7 |- ( [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R <R [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R <-> ( ( v +P. u ) +P. ( x +P. w ) ) <P ( ( v +P. u ) +P. ( y +P. z ) ) )
38	19, 20, 37	3bitr4g 288	. . . . . 6 |- ( ( v +P. u ) e. P. -> ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R <R [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R ) )
39	18, 38	syl 16	. . . . 5 |- ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R <R [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R ) )
40		addsrpr 9345	. . . . . . 7 |- ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) ) -> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) = [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R )
41	40	3adant3 1008	. . . . . 6 |- ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) = [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R )
42		addsrpr 9345	. . . . . . 7 |- ( ( ( v e. P. /\ u e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) = [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R )
43	42	3adant2 1007	. . . . . 6 |- ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) = [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R )
44	41, 43	breq12d 4405	. . . . 5 |- ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) <R ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) <-> [ <. ( v +P. x ) , ( u +P. y ) >. ] ~R <R [ <. ( v +P. z ) , ( u +P. w ) >. ] ~R ) )
45	39, 44	bitr4d 256	. . . 4 |- ( ( ( v e. P. /\ u e. P. ) /\ ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) <R ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) ) )
46	4, 8, 12, 16, 45	3ecoptocl 7294	. . 3 |- ( ( C e. R. /\ A e. R. /\ B e. R. ) -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )
47	46	3coml 1195	. 2 |- ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )
48	1, 2, 3, 47	ndmovord 6355	1 |- ( C e. R. -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   <.cop 3983   class class class wbr 4392  (class class class)co 6192   [cec 7201   P.cnp 9129   +P. cpp 9131   <P cltp 9133   ~R cer 9136   R.cnr 9137   +R cplr 9141   <R cltr 9143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-nul 4521  ax-pow 4570  ax-pr 4631  ax-un 6474  ax-inf2 7950

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3072  df-sbc 3287  df-csb 3389  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-pss 3444  df-nul 3738  df-if 3892  df-pw 3962  df-sn 3978  df-pr 3980  df-tp 3982  df-op 3984  df-uni 4192  df-int 4229  df-iun 4273  df-br 4393  df-opab 4451  df-mpt 4452  df-tr 4486  df-eprel 4732  df-id 4736  df-po 4741  df-so 4742  df-fr 4779  df-we 4781  df-ord 4822  df-on 4823  df-lim 4824  df-suc 4825  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5481  df-fun 5520  df-fn 5521  df-f 5522  df-f1 5523  df-fo 5524  df-f1o 5525  df-fv 5526  df-ov 6195  df-oprab 6196  df-mpt2 6197  df-om 6579  df-1st 6679  df-2nd 6680  df-recs 6934  df-rdg 6968  df-1o 7022  df-oadd 7026  df-omul 7027  df-er 7203  df-ec 7205  df-qs 7209  df-ni 9144  df-pli 9145  df-mi 9146  df-lti 9147  df-plpq 9180  df-mpq 9181  df-ltpq 9182  df-enq 9183  df-nq 9184  df-erq 9185  df-plq 9186  df-mq 9187  df-1nq 9188  df-rq 9189  df-ltnq 9190  df-np 9253  df-plp 9255  df-ltp 9257  df-plpr 9327  df-enr 9329  df-nr 9330  df-plr 9331  df-ltr 9333

This theorem is referenced by:  addgt0sr  9374  sqgt0sr  9376  mappsrpr  9378  ltpsrpr  9379  map2psrpr  9380  supsrlem  9381  axpre-ltadd  9437