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

Theorem ltasr 9906
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 9891 . 2 dom +R = (R × R)
2 ltrelsr 9874 . 2 <R ⊆ (R × R)
3 0nsr 9885 . 2 ¬ ∅ ∈ R
4 df-nr 9863 . . . 4 R = ((P × P) / ~R )
5 oveq1 6642 . . . . . 6 ([⟨𝑣, 𝑢⟩] ~R = 𝐶 → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) = (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ))
6 oveq1 6642 . . . . . 6 ([⟨𝑣, 𝑢⟩] ~R = 𝐶 → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) = (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ))
75, 6breq12d 4657 . . . . 5 ([⟨𝑣, 𝑢⟩] ~R = 𝐶 → (([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) <R ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) ↔ (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R )))
87bibi2d 332 . . . 4 ([⟨𝑣, 𝑢⟩] ~R = 𝐶 → (([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) <R ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R )) ↔ ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ))))
9 breq1 4647 . . . . 5 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R𝐴 <R [⟨𝑧, 𝑤⟩] ~R ))
10 oveq2 6643 . . . . . 6 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) = (𝐶 +R 𝐴))
1110breq1d 4654 . . . . 5 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → ((𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ) ↔ (𝐶 +R 𝐴) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R )))
129, 11bibi12d 335 . . . 4 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → (([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝐶 +R [⟨𝑥, 𝑦⟩] ~R ) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R )) ↔ (𝐴 <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝐶 +R 𝐴) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ))))
13 breq2 4648 . . . . 5 ([⟨𝑧, 𝑤⟩] ~R = 𝐵 → (𝐴 <R [⟨𝑧, 𝑤⟩] ~R𝐴 <R 𝐵))
14 oveq2 6643 . . . . . 6 ([⟨𝑧, 𝑤⟩] ~R = 𝐵 → (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ) = (𝐶 +R 𝐵))
1514breq2d 4656 . . . . 5 ([⟨𝑧, 𝑤⟩] ~R = 𝐵 → ((𝐶 +R 𝐴) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R ) ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
1613, 15bibi12d 335 . . . 4 ([⟨𝑧, 𝑤⟩] ~R = 𝐵 → ((𝐴 <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝐶 +R 𝐴) <R (𝐶 +R [⟨𝑧, 𝑤⟩] ~R )) ↔ (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵))))
17 addclpr 9825 . . . . . . 7 ((𝑣P𝑢P) → (𝑣 +P 𝑢) ∈ P)
18173ad2ant1 1080 . . . . . 6 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → (𝑣 +P 𝑢) ∈ P)
19 ltapr 9852 . . . . . . 7 ((𝑣 +P 𝑢) ∈ P → ((𝑥 +P 𝑤)<P (𝑦 +P 𝑧) ↔ ((𝑣 +P 𝑢) +P (𝑥 +P 𝑤))<P ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧))))
20 ltsrpr 9883 . . . . . . 7 ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝑥 +P 𝑤)<P (𝑦 +P 𝑧))
21 ltsrpr 9883 . . . . . . . 8 ([⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R <R [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R ↔ ((𝑣 +P 𝑥) +P (𝑢 +P 𝑤))<P ((𝑢 +P 𝑦) +P (𝑣 +P 𝑧)))
22 vex 3198 . . . . . . . . . 10 𝑣 ∈ V
23 vex 3198 . . . . . . . . . 10 𝑥 ∈ V
24 vex 3198 . . . . . . . . . 10 𝑢 ∈ V
25 addcompr 9828 . . . . . . . . . 10 (𝑦 +P 𝑧) = (𝑧 +P 𝑦)
26 addasspr 9829 . . . . . . . . . 10 ((𝑦 +P 𝑧) +P 𝑓) = (𝑦 +P (𝑧 +P 𝑓))
27 vex 3198 . . . . . . . . . 10 𝑤 ∈ V
2822, 23, 24, 25, 26, 27caov4 6850 . . . . . . . . 9 ((𝑣 +P 𝑥) +P (𝑢 +P 𝑤)) = ((𝑣 +P 𝑢) +P (𝑥 +P 𝑤))
29 addcompr 9828 . . . . . . . . . 10 ((𝑢 +P 𝑦) +P (𝑣 +P 𝑧)) = ((𝑣 +P 𝑧) +P (𝑢 +P 𝑦))
30 vex 3198 . . . . . . . . . . 11 𝑧 ∈ V
31 addcompr 9828 . . . . . . . . . . 11 (𝑥 +P 𝑤) = (𝑤 +P 𝑥)
32 addasspr 9829 . . . . . . . . . . 11 ((𝑥 +P 𝑤) +P 𝑓) = (𝑥 +P (𝑤 +P 𝑓))
33 vex 3198 . . . . . . . . . . 11 𝑦 ∈ V
3422, 30, 24, 31, 32, 33caov42 6852 . . . . . . . . . 10 ((𝑣 +P 𝑧) +P (𝑢 +P 𝑦)) = ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧))
3529, 34eqtri 2642 . . . . . . . . 9 ((𝑢 +P 𝑦) +P (𝑣 +P 𝑧)) = ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧))
3628, 35breq12i 4653 . . . . . . . 8 (((𝑣 +P 𝑥) +P (𝑢 +P 𝑤))<P ((𝑢 +P 𝑦) +P (𝑣 +P 𝑧)) ↔ ((𝑣 +P 𝑢) +P (𝑥 +P 𝑤))<P ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧)))
3721, 36bitri 264 . . . . . . 7 ([⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R <R [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R ↔ ((𝑣 +P 𝑢) +P (𝑥 +P 𝑤))<P ((𝑣 +P 𝑢) +P (𝑦 +P 𝑧)))
3819, 20, 373bitr4g 303 . . . . . 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 9881 . . . . . . 7 (((𝑣P𝑢P) ∧ (𝑥P𝑦P)) → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) = [⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R )
41403adant3 1079 . . . . . 6 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) = [⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R )
42 addsrpr 9881 . . . . . . 7 (((𝑣P𝑢P) ∧ (𝑧P𝑤P)) → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) = [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R )
43423adant2 1078 . . . . . 6 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) = [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R )
4441, 43breq12d 4657 . . . . 5 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → (([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) <R ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R ) ↔ [⟨(𝑣 +P 𝑥), (𝑢 +P 𝑦)⟩] ~R <R [⟨(𝑣 +P 𝑧), (𝑢 +P 𝑤)⟩] ~R ))
4539, 44bitr4d 271 . . . 4 (((𝑣P𝑢P) ∧ (𝑥P𝑦P) ∧ (𝑧P𝑤P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑥, 𝑦⟩] ~R ) <R ([⟨𝑣, 𝑢⟩] ~R +R [⟨𝑧, 𝑤⟩] ~R )))
464, 8, 12, 16, 453ecoptocl 7824 . . 3 ((𝐶R𝐴R𝐵R) → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
47463coml 1270 . 2 ((𝐴R𝐵R𝐶R) → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
481, 2, 3, 47ndmovord 6809 1 (𝐶R → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  cop 4174   class class class wbr 4644  (class class class)co 6635  [cec 7725  Pcnp 9666   +P cpp 9668  <P cltp 9670   ~R cer 9671  Rcnr 9672   +R cplr 9676   <R cltr 9678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-omul 7550  df-er 7727  df-ec 7729  df-qs 7733  df-ni 9679  df-pli 9680  df-mi 9681  df-lti 9682  df-plpq 9715  df-mpq 9716  df-ltpq 9717  df-enq 9718  df-nq 9719  df-erq 9720  df-plq 9721  df-mq 9722  df-1nq 9723  df-rq 9724  df-ltnq 9725  df-np 9788  df-plp 9790  df-ltp 9792  df-enr 9862  df-nr 9863  df-plr 9864  df-ltr 9866
This theorem is referenced by:  addgt0sr  9910  sqgt0sr  9912  mappsrpr  9914  ltpsrpr  9915  map2psrpr  9916  supsrlem  9917  axpre-ltadd  9973
  Copyright terms: Public domain W3C validator