This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltasr

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

Ref Expression
Assertion ltasr ( 𝐶 ∈ R → ( 𝐴 <R 𝐵 ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dmaddsr ⊢ dom +R = ( R × R )
2 ltrelsr ⊢ <R ⊆ ( R × R )
3 0nsr ⊢ ¬ ∅ ∈ R
4 df-nr ⊢ R = ( ( P × P ) / ~R )
5 oveq1 ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = 𝐶 → ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) = ( 𝐶 +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) )
6 oveq1 ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = 𝐶 → ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) )
7 5 6 breq12d ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = 𝐶 → ( ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) <R ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ ( 𝐶 +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) )
8 7 bibi2d ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = 𝐶 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) <R ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ↔ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( 𝐶 +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ) )
9 breq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ 𝐴 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) )
10 oveq2 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( 𝐶 +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) = ( 𝐶 +R 𝐴 ) )
11 10 breq1d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( 𝐶 +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) )
12 9 11 bibi12d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( 𝐶 +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ↔ ( 𝐴 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ) )
13 breq2 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( 𝐴 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ 𝐴 <R 𝐵 ) )
14 oveq2 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐶 +R 𝐵 ) )
15 14 breq2d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R 𝐵 ) ) )
16 13 15 bibi12d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( ( 𝐴 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ↔ ( 𝐴 <R 𝐵 ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R 𝐵 ) ) ) )
17 addclpr ⊢ ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) → ( 𝑣 +P 𝑢 ) ∈ P )
18 17 3ad2ant1 ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( 𝑣 +P 𝑢 ) ∈ P )
19 ltapr ⊢ ( ( 𝑣 +P 𝑢 ) ∈ P → ( ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) ↔ ( ( 𝑣 +P 𝑢 ) +P ( 𝑥 +P 𝑤 ) ) <P ( ( 𝑣 +P 𝑢 ) +P ( 𝑦 +P 𝑧 ) ) ) )
20 ltsrpr ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) )
21 ltsrpr ⊢ ( [ ⟨ ( 𝑣 +P 𝑥 ) , ( 𝑢 +P 𝑦 ) ⟩ ] ~R <R [ ⟨ ( 𝑣 +P 𝑧 ) , ( 𝑢 +P 𝑤 ) ⟩ ] ~R ↔ ( ( 𝑣 +P 𝑥 ) +P ( 𝑢 +P 𝑤 ) ) <P ( ( 𝑢 +P 𝑦 ) +P ( 𝑣 +P 𝑧 ) ) )
22 vex ⊢ 𝑣 ∈ V
23 vex ⊢ 𝑥 ∈ V
24 vex ⊢ 𝑢 ∈ V
25 addcompr ⊢ ( 𝑦 +P 𝑧 ) = ( 𝑧 +P 𝑦 )
26 addasspr ⊢ ( ( 𝑦 +P 𝑧 ) +P 𝑓 ) = ( 𝑦 +P ( 𝑧 +P 𝑓 ) )
27 vex ⊢ 𝑤 ∈ V
28 22 23 24 25 26 27 caov4 ⊢ ( ( 𝑣 +P 𝑥 ) +P ( 𝑢 +P 𝑤 ) ) = ( ( 𝑣 +P 𝑢 ) +P ( 𝑥 +P 𝑤 ) )
29 addcompr ⊢ ( ( 𝑢 +P 𝑦 ) +P ( 𝑣 +P 𝑧 ) ) = ( ( 𝑣 +P 𝑧 ) +P ( 𝑢 +P 𝑦 ) )
30 vex ⊢ 𝑧 ∈ V
31 addcompr ⊢ ( 𝑥 +P 𝑤 ) = ( 𝑤 +P 𝑥 )
32 addasspr ⊢ ( ( 𝑥 +P 𝑤 ) +P 𝑓 ) = ( 𝑥 +P ( 𝑤 +P 𝑓 ) )
33 vex ⊢ 𝑦 ∈ V
34 22 30 24 31 32 33 caov42 ⊢ ( ( 𝑣 +P 𝑧 ) +P ( 𝑢 +P 𝑦 ) ) = ( ( 𝑣 +P 𝑢 ) +P ( 𝑦 +P 𝑧 ) )
35 29 34 eqtri ⊢ ( ( 𝑢 +P 𝑦 ) +P ( 𝑣 +P 𝑧 ) ) = ( ( 𝑣 +P 𝑢 ) +P ( 𝑦 +P 𝑧 ) )
36 28 35 breq12i ⊢ ( ( ( 𝑣 +P 𝑥 ) +P ( 𝑢 +P 𝑤 ) ) <P ( ( 𝑢 +P 𝑦 ) +P ( 𝑣 +P 𝑧 ) ) ↔ ( ( 𝑣 +P 𝑢 ) +P ( 𝑥 +P 𝑤 ) ) <P ( ( 𝑣 +P 𝑢 ) +P ( 𝑦 +P 𝑧 ) ) )
37 21 36 bitri ⊢ ( [ ⟨ ( 𝑣 +P 𝑥 ) , ( 𝑢 +P 𝑦 ) ⟩ ] ~R <R [ ⟨ ( 𝑣 +P 𝑧 ) , ( 𝑢 +P 𝑤 ) ⟩ ] ~R ↔ ( ( 𝑣 +P 𝑢 ) +P ( 𝑥 +P 𝑤 ) ) <P ( ( 𝑣 +P 𝑢 ) +P ( 𝑦 +P 𝑧 ) ) )
38 19 20 37 3bitr4g ⊢ ( ( 𝑣 +P 𝑢 ) ∈ P → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ [ ⟨ ( 𝑣 +P 𝑥 ) , ( 𝑢 +P 𝑦 ) ⟩ ] ~R <R [ ⟨ ( 𝑣 +P 𝑧 ) , ( 𝑢 +P 𝑤 ) ⟩ ] ~R ) )
39 18 38 syl ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ [ ⟨ ( 𝑣 +P 𝑥 ) , ( 𝑢 +P 𝑦 ) ⟩ ] ~R <R [ ⟨ ( 𝑣 +P 𝑧 ) , ( 𝑢 +P 𝑤 ) ⟩ ] ~R ) )
40 addsrpr ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) → ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) = [ ⟨ ( 𝑣 +P 𝑥 ) , ( 𝑢 +P 𝑦 ) ⟩ ] ~R )
41 40 3adant3 ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) = [ ⟨ ( 𝑣 +P 𝑥 ) , ( 𝑢 +P 𝑦 ) ⟩ ] ~R )
42 addsrpr ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( 𝑣 +P 𝑧 ) , ( 𝑢 +P 𝑤 ) ⟩ ] ~R )
43 42 3adant2 ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( 𝑣 +P 𝑧 ) , ( 𝑢 +P 𝑤 ) ⟩ ] ~R )
44 41 43 breq12d ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) <R ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ [ ⟨ ( 𝑣 +P 𝑥 ) , ( 𝑢 +P 𝑦 ) ⟩ ] ~R <R [ ⟨ ( 𝑣 +P 𝑧 ) , ( 𝑢 +P 𝑤 ) ⟩ ] ~R ) )
45 39 44 bitr4d ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) <R ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) )
46 4 8 12 16 45 3ecoptocl ⊢ ( ( 𝐶 ∈ R ∧ 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 <R 𝐵 ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R 𝐵 ) ) )
47 46 3coml ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R ) → ( 𝐴 <R 𝐵 ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R 𝐵 ) ) )
48 1 2 3 47 ndmovord ⊢ ( 𝐶 ∈ R → ( 𝐴 <R 𝐵 ↔ ( 𝐶 +R 𝐴 ) <R ( 𝐶 +R 𝐵 ) ) )