ltasr

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

		Ref	Expression
	Assertion	ltasr	$⊢ C \in 𝑹 \to (A <_{𝑹} B \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} B))$

Proof

Step	Hyp	Ref	Expression
1		dmaddsr	$⊢ dom +_{𝑹} = 𝑹 \times 𝑹$
2		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
3		0nsr	$⊢ \neg \emptyset \in 𝑹$
4		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
5		oveq1	$⊢ [⟨v, u⟩] ~_{𝑹} = C \to [⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨x, y⟩] ~_{𝑹} = C +_{𝑹} [⟨x, y⟩] ~_{𝑹}$
6		oveq1	$⊢ [⟨v, u⟩] ~_{𝑹} = C \to [⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹} = C +_{𝑹} [⟨z, w⟩] ~_{𝑹}$
7	5 6	breq12d	$⊢ [⟨v, u⟩] ~_{𝑹} = C \to (([⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨x, y⟩] ~_{𝑹}) <_{𝑹} ([⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹}) \leftrightarrow (C +_{𝑹} [⟨x, y⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨z, w⟩] ~_{𝑹}))$
8	7	bibi2d	$⊢ [⟨v, u⟩] ~_{𝑹} = C \to (([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow ([⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨x, y⟩] ~_{𝑹}) <_{𝑹} ([⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹})) \leftrightarrow ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow (C +_{𝑹} [⟨x, y⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨z, w⟩] ~_{𝑹})))$
9		breq1	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow A <_{𝑹} [⟨z, w⟩] ~_{𝑹})$
10		oveq2	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to C +_{𝑹} [⟨x, y⟩] ~_{𝑹} = C +_{𝑹} A$
11	10	breq1d	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to ((C +_{𝑹} [⟨x, y⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨z, w⟩] ~_{𝑹}) \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} [⟨z, w⟩] ~_{𝑹}))$
12	9 11	bibi12d	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to (([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow (C +_{𝑹} [⟨x, y⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨z, w⟩] ~_{𝑹})) \leftrightarrow (A <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} [⟨z, w⟩] ~_{𝑹})))$
13		breq2	$⊢ [⟨z, w⟩] ~_{𝑹} = B \to (A <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow A <_{𝑹} B)$
14		oveq2	$⊢ [⟨z, w⟩] ~_{𝑹} = B \to C +_{𝑹} [⟨z, w⟩] ~_{𝑹} = C +_{𝑹} B$
15	14	breq2d	$⊢ [⟨z, w⟩] ~_{𝑹} = B \to ((C +_{𝑹} A) <_{𝑹} (C +_{𝑹} [⟨z, w⟩] ~_{𝑹}) \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} B))$
16	13 15	bibi12d	$⊢ [⟨z, w⟩] ~_{𝑹} = B \to ((A <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} [⟨z, w⟩] ~_{𝑹})) \leftrightarrow (A <_{𝑹} B \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} B)))$
17		addclpr	$⊢ (v \in 𝑷 \land u \in 𝑷) \to v +_{𝑷} u \in 𝑷$
18	17	3ad2ant1	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to v +_{𝑷} u \in 𝑷$
19		ltapr	$⊢ v +_{𝑷} u \in 𝑷 \to ((x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z) \leftrightarrow ((v +_{𝑷} u) +_{𝑷} (x +_{𝑷} w)) <_{𝑷} ((v +_{𝑷} u) +_{𝑷} (y +_{𝑷} z)))$
20		ltsrpr	$⊢ [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow (x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z)$
21		ltsrpr	$⊢ [⟨v +_{𝑷} x, u +_{𝑷} y⟩] ~_{𝑹} <_{𝑹} [⟨v +_{𝑷} z, u +_{𝑷} w⟩] ~_{𝑹} \leftrightarrow ((v +_{𝑷} x) +_{𝑷} (u +_{𝑷} w)) <_{𝑷} ((u +_{𝑷} y) +_{𝑷} (v +_{𝑷} z))$
22		vex	$⊢ v \in V$
23		vex	$⊢ x \in V$
24		vex	$⊢ u \in V$
25		addcompr	$⊢ y +_{𝑷} z = z +_{𝑷} y$
26		addasspr	$⊢ (y +_{𝑷} z) +_{𝑷} f = y +_{𝑷} (z +_{𝑷} f)$
27		vex	$⊢ w \in V$
28	22 23 24 25 26 27	caov4	$⊢ (v +_{𝑷} x) +_{𝑷} (u +_{𝑷} w) = (v +_{𝑷} u) +_{𝑷} (x +_{𝑷} w)$
29		addcompr	$⊢ (u +_{𝑷} y) +_{𝑷} (v +_{𝑷} z) = (v +_{𝑷} z) +_{𝑷} (u +_{𝑷} y)$
30		vex	$⊢ z \in V$
31		addcompr	$⊢ x +_{𝑷} w = w +_{𝑷} x$
32		addasspr	$⊢ (x +_{𝑷} w) +_{𝑷} f = x +_{𝑷} (w +_{𝑷} f)$
33		vex	$⊢ y \in V$
34	22 30 24 31 32 33	caov42	$⊢ (v +_{𝑷} z) +_{𝑷} (u +_{𝑷} y) = (v +_{𝑷} u) +_{𝑷} (y +_{𝑷} z)$
35	29 34	eqtri	$⊢ (u +_{𝑷} y) +_{𝑷} (v +_{𝑷} z) = (v +_{𝑷} u) +_{𝑷} (y +_{𝑷} z)$
36	28 35	breq12i	$⊢ ((v +_{𝑷} x) +_{𝑷} (u +_{𝑷} w)) <_{𝑷} ((u +_{𝑷} y) +_{𝑷} (v +_{𝑷} z)) \leftrightarrow ((v +_{𝑷} u) +_{𝑷} (x +_{𝑷} w)) <_{𝑷} ((v +_{𝑷} u) +_{𝑷} (y +_{𝑷} z))$
37	21 36	bitri	$⊢ [⟨v +_{𝑷} x, u +_{𝑷} y⟩] ~_{𝑹} <_{𝑹} [⟨v +_{𝑷} z, u +_{𝑷} w⟩] ~_{𝑹} \leftrightarrow ((v +_{𝑷} u) +_{𝑷} (x +_{𝑷} w)) <_{𝑷} ((v +_{𝑷} u) +_{𝑷} (y +_{𝑷} z))$
38	19 20 37	3bitr4g	$⊢ v +_{𝑷} u \in 𝑷 \to ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow [⟨v +_{𝑷} x, u +_{𝑷} y⟩] ~_{𝑹} <_{𝑹} [⟨v +_{𝑷} z, u +_{𝑷} w⟩] ~_{𝑹})$
39	18 38	syl	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow [⟨v +_{𝑷} x, u +_{𝑷} y⟩] ~_{𝑹} <_{𝑹} [⟨v +_{𝑷} z, u +_{𝑷} w⟩] ~_{𝑹})$
40		addsrpr	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷)) \to [⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨x, y⟩] ~_{𝑹} = [⟨v +_{𝑷} x, u +_{𝑷} y⟩] ~_{𝑹}$
41	40	3adant3	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to [⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨x, y⟩] ~_{𝑹} = [⟨v +_{𝑷} x, u +_{𝑷} y⟩] ~_{𝑹}$
42		addsrpr	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to [⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹} = [⟨v +_{𝑷} z, u +_{𝑷} w⟩] ~_{𝑹}$
43	42	3adant2	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to [⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹} = [⟨v +_{𝑷} z, u +_{𝑷} w⟩] ~_{𝑹}$
44	41 43	breq12d	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (([⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨x, y⟩] ~_{𝑹}) <_{𝑹} ([⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹}) \leftrightarrow [⟨v +_{𝑷} x, u +_{𝑷} y⟩] ~_{𝑹} <_{𝑹} [⟨v +_{𝑷} z, u +_{𝑷} w⟩] ~_{𝑹})$
45	39 44	bitr4d	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow ([⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨x, y⟩] ~_{𝑹}) <_{𝑹} ([⟨v, u⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹}))$
46	4 8 12 16 45	3ecoptocl	$⊢ (C \in 𝑹 \land A \in 𝑹 \land B \in 𝑹) \to (A <_{𝑹} B \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} B))$
47	46	3coml	$⊢ (A \in 𝑹 \land B \in 𝑹 \land C \in 𝑹) \to (A <_{𝑹} B \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} B))$
48	1 2 3 47	ndmovord	$⊢ C \in 𝑹 \to (A <_{𝑹} B \leftrightarrow (C +_{𝑹} A) <_{𝑹} (C +_{𝑹} B))$

Metamath Proof Explorer

Theorem ltasr

Proof