MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltasr Structured version   Visualization version   GIF version

Theorem ltasr 9772
Description: Ordering property of addition. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
Assertion
Ref Expression
ltasr (𝐶R → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))

Proof of Theorem ltasr
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmaddsr 9757 . 2 dom +R = (R × R)
2 ltrelsr 9740 . 2 <R ⊆ (R × R)
3 0nsr 9751 . 2 ¬ ∅ ∈ R
4 df-nr 9729 . . . 4 R = ((P × P) / ~R )
5 oveq1 6529 . . . . . 6 ([⟨𝑣, 𝑢⟩] ~R = 𝐶 → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) = (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ))
6 oveq1 6529 . . . . . 6 ([⟨𝑣, 𝑢⟩] ~R = 𝐶 → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) = (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ))
75, 6breq12d 4585 . . . . 5 ([⟨𝑣, 𝑢⟩] ~R = 𝐶 → (([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) <R ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) ↔ (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R )))
87bibi2d 330 . . . 4 ([⟨𝑣, 𝑢⟩] ~R = 𝐶 → (([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) <R ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R )) ↔ ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ))))
9 breq1 4575 . . . . 5 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R𝐴 <R [⟨𝑧, 𝑤⟩] ~R ))
10 oveq2 6530 . . . . . 6 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) = (𝐶 +R 𝐴))
1110breq1d 4582 . . . . 5 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → ((𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ) ↔ (𝐶 +R 𝐴) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R )))
129, 11bibi12d 333 . . . 4 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → (([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R )) ↔ (𝐴 <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝐶 +R 𝐴) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ))))
13 breq2 4576 . . . . 5 ([⟨𝑧, 𝑤⟩] ~R = 𝐵 → (𝐴 <R [⟨𝑧, 𝑤⟩] ~R𝐴 <R 𝐵))
14 oveq2 6530 . . . . . 6 ([⟨𝑧, 𝑤⟩] ~R = 𝐵 → (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ) = (𝐶 +R 𝐵))
1514breq2d 4584 . . . . 5 ([⟨𝑧, 𝑤⟩] ~R = 𝐵 → ((𝐶 +R 𝐴) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ) ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
1613, 15bibi12d 333 . . . 4 ([⟨𝑧, 𝑤⟩] ~R = 𝐵 → ((𝐴 <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝐶 +R 𝐴) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R )) ↔ (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵))))
17 addclpr 9691 . . . . . . 7 ((𝑣P𝑢P) → (𝑣 +P 𝑢) ∈ P)
18173ad2ant1 1074 . . . . . 6 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → (𝑣 +P 𝑢) ∈ P)
19 ltapr 9718 . . . . . . 7 ((𝑣 +P 𝑢) ∈ P → ((𝑥 +P 𝑤)<P (𝑦 +P 𝑧) ↔ ((𝑣 +P 𝑢) +P (𝑥 +P 𝑤))<P ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧))))
20 ltsrpr 9749 . . . . . . 7 ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝑥 +P 𝑤)<P (𝑦 +P 𝑧))
21 ltsrpr 9749 . . . . . . . 8 ([⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R <R [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R ↔ ((𝑣 +P 𝑥) +P (𝑢 +P 𝑤))<P ((𝑢 +P 𝑦) +P (𝑣 +P 𝑧)))
22 vex 3170 . . . . . . . . . 10 𝑣 ∈ V
23 vex 3170 . . . . . . . . . 10 𝑥 ∈ V
24 vex 3170 . . . . . . . . . 10 𝑢 ∈ V
25 addcompr 9694 . . . . . . . . . 10 (𝑦 +P 𝑧) = (𝑧 +P 𝑦)
26 addasspr 9695 . . . . . . . . . 10 ((𝑦 +P 𝑧) +P 𝑓) = (𝑦 +P (𝑧 +P 𝑓))
27 vex 3170 . . . . . . . . . 10 𝑤 ∈ V
2822, 23, 24, 25, 26, 27caov4 6735 . . . . . . . . 9 ((𝑣 +P 𝑥) +P (𝑢 +P 𝑤)) = ((𝑣 +P 𝑢) +P (𝑥 +P 𝑤))
29 addcompr 9694 . . . . . . . . . 10 ((𝑢 +P 𝑦) +P (𝑣 +P 𝑧)) = ((𝑣 +P 𝑧) +P (𝑢 +P 𝑦))
30 vex 3170 . . . . . . . . . . 11 𝑧 ∈ V
31 addcompr 9694 . . . . . . . . . . 11 (𝑥 +P 𝑤) = (𝑤 +P 𝑥)
32 addasspr 9695 . . . . . . . . . . 11 ((𝑥 +P 𝑤) +P 𝑓) = (𝑥 +P (𝑤 +P 𝑓))
33 vex 3170 . . . . . . . . . . 11 𝑦 ∈ V
3422, 30, 24, 31, 32, 33caov42 6737 . . . . . . . . . 10 ((𝑣 +P 𝑧) +P (𝑢 +P 𝑦)) = ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧))
3529, 34eqtri 2626 . . . . . . . . 9 ((𝑢 +P 𝑦) +P (𝑣 +P 𝑧)) = ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧))
3628, 35breq12i 4581 . . . . . . . 8 (((𝑣 +P 𝑥) +P (𝑢 +P 𝑤))<P ((𝑢 +P 𝑦) +P (𝑣 +P 𝑧)) ↔ ((𝑣 +P 𝑢) +P (𝑥 +P 𝑤))<P ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧)))
3721, 36bitri 262 . . . . . . 7 ([⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R <R [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R ↔ ((𝑣 +P 𝑢) +P (𝑥 +P 𝑤))<P ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧)))
3819, 20, 373bitr4g 301 . . . . . 6 ((𝑣 +P 𝑢) ∈ P → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ [⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R <R [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R ))
3918, 38syl 17 . . . . 5 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ [⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R <R [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R ))
40 addsrpr 9747 . . . . . . 7 (((𝑣P𝑢P) ∧ (𝑥P𝑦P)) → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) = [⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R )
41403adant3 1073 . . . . . 6 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) = [⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R )
42 addsrpr 9747 . . . . . . 7 (((𝑣P𝑢P) ∧ (𝑧P𝑤P)) → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) = [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R )
43423adant2 1072 . . . . . 6 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) = [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R )
4441, 43breq12d 4585 . . . . 5 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → (([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) <R ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) ↔ [⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R <R [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R ))
4539, 44bitr4d 269 . . . 4 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) <R ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R )))
464, 8, 12, 16, 453ecoptocl 7698 . . 3 ((𝐶R𝐴R𝐵R) → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
47463coml 1263 . 2 ((𝐴R𝐵R𝐶R) → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
481, 2, 3, 47ndmovord 6694 1 (𝐶R → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1975  cop 4125   class class class wbr 4572  (class class class)co 6522  [cec 7599  Pcnp 9532   +P cpp 9534  <P cltp 9536   ~R cer 9537  Rcnr 9538   +R cplr 9542   <R cltr 9544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819  ax-inf2 8393
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-ral 2895  df-rex 2896  df-reu 2897  df-rmo 2898  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-pss 3550  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-tp 4124  df-op 4126  df-uni 4362  df-int 4400  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-tr 4670  df-eprel 4934  df-id 4938  df-po 4944  df-so 4945  df-fr 4982  df-we 4984  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-pred 5578  df-ord 5624  df-on 5625  df-lim 5626  df-suc 5627  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-om 6930  df-1st 7031  df-2nd 7032  df-wrecs 7266  df-recs 7327  df-rdg 7365  df-1o 7419  df-oadd 7423  df-omul 7424  df-er 7601  df-ec 7603  df-qs 7607  df-ni 9545  df-pli 9546  df-mi 9547  df-lti 9548  df-plpq 9581  df-mpq 9582  df-ltpq 9583  df-enq 9584  df-nq 9585  df-erq 9586  df-plq 9587  df-mq 9588  df-1nq 9589  df-rq 9590  df-ltnq 9591  df-np 9654  df-plp 9656  df-ltp 9658  df-enr 9728  df-nr 9729  df-plr 9730  df-ltr 9732
This theorem is referenced by:  addgt0sr  9776  sqgt0sr  9778  mappsrpr  9780  ltpsrpr  9781  map2psrpr  9782  supsrlem  9783  axpre-ltadd  9839
  Copyright terms: Public domain W3C validator