Theorem ltasr 9473

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 9458	. 2 |- dom +R = ( R. X. R. )
2		ltrelsr 9441	. 2 |- <R C_ ( R. X. R. )
3		0nsr 9452	. 2 |- -. (/) e. R.
4		df-nr 9430	. . . 4 |- R. = ( ( P. X. P. ) /. ~R )
5		oveq1 6289	. . . . . 6 |- ( [ <. v , u >. ] ~R = C -> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) = ( C +R [ <. x , y >. ] ~R ) )
6		oveq1 6289	. . . . . 6 |- ( [ <. v , u >. ] ~R = C -> ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) = ( C +R [ <. z , w >. ] ~R ) )
7	5, 6	breq12d 4460	. . . . 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 4450	. . . . 5 |- ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> A <R [ <. z , w >. ] ~R ) )
10		oveq2 6290	. . . . . 6 |- ( [ <. x , y >. ] ~R = A -> ( C +R [ <. x , y >. ] ~R ) = ( C +R A ) )
11	10	breq1d 4457	. . . . 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 4451	. . . . 5 |- ( [ <. z , w >. ] ~R = B -> ( A <R [ <. z , w >. ] ~R <-> A <R B ) )
14		oveq2 6290	. . . . . 6 |- ( [ <. z , w >. ] ~R = B -> ( C +R [ <. z , w >. ] ~R ) = ( C +R B ) )
15	14	breq2d 4459	. . . . 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 9392	. . . . . . 7 |- ( ( v e. P. /\ u e. P. ) -> ( v +P. u ) e. P. )
18	17	3ad2ant1 1017	. . . . . 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 9419	. . . . . . 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 9450	. . . . . . 7 |- ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> ( x +P. w ) <P ( y +P. z ) )
21		ltsrpr 9450	. . . . . . . 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 3116	. . . . . . . . . 10 |- v e. _V
23		vex 3116	. . . . . . . . . 10 |- x e. _V
24		vex 3116	. . . . . . . . . 10 |- u e. _V
25		addcompr 9395	. . . . . . . . . 10 |- ( y +P. z ) = ( z +P. y )
26		addasspr 9396	. . . . . . . . . 10 |- ( ( y +P. z ) +P. f ) = ( y +P. ( z +P. f ) )
27		vex 3116	. . . . . . . . . 10 |- w e. _V
28	22, 23, 24, 25, 26, 27	caov4 6488	. . . . . . . . 9 |- ( ( v +P. x ) +P. ( u +P. w ) ) = ( ( v +P. u ) +P. ( x +P. w ) )
29		addcompr 9395	. . . . . . . . . 10 |- ( ( u +P. y ) +P. ( v +P. z ) ) = ( ( v +P. z ) +P. ( u +P. y ) )
30		vex 3116	. . . . . . . . . . 11 |- z e. _V
31		addcompr 9395	. . . . . . . . . . 11 |- ( x +P. w ) = ( w +P. x )
32		addasspr 9396	. . . . . . . . . . 11 |- ( ( x +P. w ) +P. f ) = ( x +P. ( w +P. f ) )
33		vex 3116	. . . . . . . . . . 11 |- y e. _V
34	22, 30, 24, 31, 32, 33	caov42 6490	. . . . . . . . . 10 |- ( ( v +P. z ) +P. ( u +P. y ) ) = ( ( v +P. u ) +P. ( y +P. z ) )
35	29, 34	eqtri 2496	. . . . . . . . 9 |- ( ( u +P. y ) +P. ( v +P. z ) ) = ( ( v +P. u ) +P. ( y +P. z ) )
36	28, 35	breq12i 4456	. . . . . . . 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 9448	. . . . . . 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 1016	. . . . . 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 9448	. . . . . . 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 1015	. . . . . 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 4460	. . . . 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 7400	. . 3 |- ( ( C e. R. /\ A e. R. /\ B e. R. ) -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )
47	46	3coml 1203	. 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 6447	1 |- ( C e. R. -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   <.cop 4033   class class class wbr 4447  (class class class)co 6282   [cec 7306   P.cnp 9233   +P. cpp 9235   <P cltp 9237   ~R cer 9238   R.cnr 9239   +R cplr 9243   <R cltr 9245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-omul 7132  df-er 7308  df-ec 7310  df-qs 7314  df-ni 9246  df-pli 9247  df-mi 9248  df-lti 9249  df-plpq 9282  df-mpq 9283  df-ltpq 9284  df-enq 9285  df-nq 9286  df-erq 9287  df-plq 9288  df-mq 9289  df-1nq 9290  df-rq 9291  df-ltnq 9292  df-np 9355  df-plp 9357  df-ltp 9359  df-enr 9429  df-nr 9430  df-plr 9431  df-ltr 9433

This theorem is referenced by:  addgt0sr  9477  sqgt0sr  9479  mappsrpr  9481  ltpsrpr  9482  map2psrpr  9483  supsrlem  9484  axpre-ltadd  9540