Theorem ltasr 9509

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 9494	. 2 |- dom +R = ( R. X. R. )
2		ltrelsr 9477	. 2 |- <R C_ ( R. X. R. )
3		0nsr 9488	. 2 |- -. (/) e. R.
4		df-nr 9466	. . . 4 |- R. = ( ( P. X. P. ) /. ~R )
5		oveq1 6287	. . . . . 6 |- ( [ <. v , u >. ] ~R = C -> ( [ <. v , u >. ] ~R +R [ <. x , y >. ] ~R ) = ( C +R [ <. x , y >. ] ~R ) )
6		oveq1 6287	. . . . . 6 |- ( [ <. v , u >. ] ~R = C -> ( [ <. v , u >. ] ~R +R [ <. z , w >. ] ~R ) = ( C +R [ <. z , w >. ] ~R ) )
7	5, 6	breq12d 4410	. . . . 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 4400	. . . . 5 |- ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> A <R [ <. z , w >. ] ~R ) )
10		oveq2 6288	. . . . . 6 |- ( [ <. x , y >. ] ~R = A -> ( C +R [ <. x , y >. ] ~R ) = ( C +R A ) )
11	10	breq1d 4407	. . . . 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 4401	. . . . 5 |- ( [ <. z , w >. ] ~R = B -> ( A <R [ <. z , w >. ] ~R <-> A <R B ) )
14		oveq2 6288	. . . . . 6 |- ( [ <. z , w >. ] ~R = B -> ( C +R [ <. z , w >. ] ~R ) = ( C +R B ) )
15	14	breq2d 4409	. . . . 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 9428	. . . . . . 7 |- ( ( v e. P. /\ u e. P. ) -> ( v +P. u ) e. P. )
18	17	3ad2ant1 1020	. . . . . 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 9455	. . . . . . 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 9486	. . . . . . 7 |- ( [ <. x , y >. ] ~R <R [ <. z , w >. ] ~R <-> ( x +P. w ) <P ( y +P. z ) )
21		ltsrpr 9486	. . . . . . . 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 3064	. . . . . . . . . 10 |- v e. _V
23		vex 3064	. . . . . . . . . 10 |- x e. _V
24		vex 3064	. . . . . . . . . 10 |- u e. _V
25		addcompr 9431	. . . . . . . . . 10 |- ( y +P. z ) = ( z +P. y )
26		addasspr 9432	. . . . . . . . . 10 |- ( ( y +P. z ) +P. f ) = ( y +P. ( z +P. f ) )
27		vex 3064	. . . . . . . . . 10 |- w e. _V
28	22, 23, 24, 25, 26, 27	caov4 6489	. . . . . . . . 9 |- ( ( v +P. x ) +P. ( u +P. w ) ) = ( ( v +P. u ) +P. ( x +P. w ) )
29		addcompr 9431	. . . . . . . . . 10 |- ( ( u +P. y ) +P. ( v +P. z ) ) = ( ( v +P. z ) +P. ( u +P. y ) )
30		vex 3064	. . . . . . . . . . 11 |- z e. _V
31		addcompr 9431	. . . . . . . . . . 11 |- ( x +P. w ) = ( w +P. x )
32		addasspr 9432	. . . . . . . . . . 11 |- ( ( x +P. w ) +P. f ) = ( x +P. ( w +P. f ) )
33		vex 3064	. . . . . . . . . . 11 |- y e. _V
34	22, 30, 24, 31, 32, 33	caov42 6491	. . . . . . . . . 10 |- ( ( v +P. z ) +P. ( u +P. y ) ) = ( ( v +P. u ) +P. ( y +P. z ) )
35	29, 34	eqtri 2433	. . . . . . . . 9 |- ( ( u +P. y ) +P. ( v +P. z ) ) = ( ( v +P. u ) +P. ( y +P. z ) )
36	28, 35	breq12i 4406	. . . . . . . 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 251	. . . . . . 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 290	. . . . . 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 17	. . . . 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 9484	. . . . . . 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 1019	. . . . . 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 9484	. . . . . . 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 1018	. . . . . 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 4410	. . . . 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 258	. . . 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 7442	. . 3 |- ( ( C e. R. /\ A e. R. /\ B e. R. ) -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )
47	46	3coml 1206	. 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 6448	1 |- ( C e. R. -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )

Syntax hints:   -> wi 4   <-> wb 186   /\ wa 369   /\ w3a 976   = wceq 1407   e. wcel 1844   <.cop 3980   class class class wbr 4397  (class class class)co 6280   [cec 7348   P.cnp 9269   +P. cpp 9271   <P cltp 9273   ~R cer 9274   R.cnr 9275   +R cplr 9279   <R cltr 9281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-inf2 8093

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-int 4230  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-om 6686  df-1st 6786  df-2nd 6787  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-oadd 7173  df-omul 7174  df-er 7350  df-ec 7352  df-qs 7356  df-ni 9282  df-pli 9283  df-mi 9284  df-lti 9285  df-plpq 9318  df-mpq 9319  df-ltpq 9320  df-enq 9321  df-nq 9322  df-erq 9323  df-plq 9324  df-mq 9325  df-1nq 9326  df-rq 9327  df-ltnq 9328  df-np 9391  df-plp 9393  df-ltp 9395  df-enr 9465  df-nr 9466  df-plr 9467  df-ltr 9469

This theorem is referenced by:  addgt0sr  9513  sqgt0sr  9515  mappsrpr  9517  ltpsrpr  9518  map2psrpr  9519  supsrlem  9520  axpre-ltadd  9576