ltsrpr

Description: Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996) (Revised by Mario Carneiro, 12-Aug-2015) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltsrpr	$⊢ [⟨A, B⟩] ~_{𝑹} <_{𝑹} [⟨C, D⟩] ~_{𝑹} \leftrightarrow (A +_{𝑷} D) <_{𝑷} (B +_{𝑷} C)$

Proof

Step	Hyp	Ref	Expression
1		enrer	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷)$
2		erdm	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷) \to dom ~_{𝑹} = 𝑷 \times 𝑷$
3	1 2	ax-mp	$⊢ dom ~_{𝑹} = 𝑷 \times 𝑷$
4		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
5		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
6		ltrelpr	$⊢ <_{𝑷} \subseteq 𝑷 \times 𝑷$
7		0npr	$⊢ \neg \emptyset \in 𝑷$
8		dmplp	$⊢ dom +_{𝑷} = 𝑷 \times 𝑷$
9		enrex	$⊢ ~_{𝑹} \in V$
10		df-ltr	$⊢ <_{𝑹} = \{⟨x, y⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v)))\}$
11		addclpr	$⊢ (w \in 𝑷 \land v \in 𝑷) \to w +_{𝑷} v \in 𝑷$
12	11	ad2ant2lr	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to w +_{𝑷} v \in 𝑷$
13		addclpr	$⊢ (B \in 𝑷 \land C \in 𝑷) \to B +_{𝑷} C \in 𝑷$
14	13	ad2ant2lr	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to B +_{𝑷} C \in 𝑷$
15	12 14	anim12ci	$⊢ (((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \land ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷))) \to (B +_{𝑷} C \in 𝑷 \land w +_{𝑷} v \in 𝑷)$
16	15	an4s	$⊢ (((z \in 𝑷 \land w \in 𝑷) \land (A \in 𝑷 \land B \in 𝑷)) \land ((v \in 𝑷 \land u \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷))) \to (B +_{𝑷} C \in 𝑷 \land w +_{𝑷} v \in 𝑷)$
17		enreceq	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (A \in 𝑷 \land B \in 𝑷)) \to ([⟨z, w⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \leftrightarrow z +_{𝑷} B = w +_{𝑷} A)$
18		enreceq	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ([⟨v, u⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹} \leftrightarrow v +_{𝑷} D = u +_{𝑷} C)$
19		eqcom	$⊢ v +_{𝑷} D = u +_{𝑷} C \leftrightarrow u +_{𝑷} C = v +_{𝑷} D$
20	18 19	bitrdi	$⊢ ((v \in 𝑷 \land u \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ([⟨v, u⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹} \leftrightarrow u +_{𝑷} C = v +_{𝑷} D)$
21	17 20	bi2anan9	$⊢ (((z \in 𝑷 \land w \in 𝑷) \land (A \in 𝑷 \land B \in 𝑷)) \land ((v \in 𝑷 \land u \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷))) \to (([⟨z, w⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \land [⟨v, u⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \leftrightarrow (z +_{𝑷} B = w +_{𝑷} A \land u +_{𝑷} C = v +_{𝑷} D))$
22		oveq12	$⊢ (z +_{𝑷} B = w +_{𝑷} A \land u +_{𝑷} C = v +_{𝑷} D) \to (z +_{𝑷} B) +_{𝑷} (u +_{𝑷} C) = (w +_{𝑷} A) +_{𝑷} (v +_{𝑷} D)$
23		addcompr	$⊢ u +_{𝑷} B = B +_{𝑷} u$
24	23	oveq1i	$⊢ (u +_{𝑷} B) +_{𝑷} C = (B +_{𝑷} u) +_{𝑷} C$
25		addasspr	$⊢ (u +_{𝑷} B) +_{𝑷} C = u +_{𝑷} (B +_{𝑷} C)$
26		addasspr	$⊢ (B +_{𝑷} u) +_{𝑷} C = B +_{𝑷} (u +_{𝑷} C)$
27	24 25 26	3eqtr3i	$⊢ u +_{𝑷} (B +_{𝑷} C) = B +_{𝑷} (u +_{𝑷} C)$
28	27	oveq2i	$⊢ z +_{𝑷} (u +_{𝑷} (B +_{𝑷} C)) = z +_{𝑷} (B +_{𝑷} (u +_{𝑷} C))$
29		addasspr	$⊢ (z +_{𝑷} u) +_{𝑷} (B +_{𝑷} C) = z +_{𝑷} (u +_{𝑷} (B +_{𝑷} C))$
30		addasspr	$⊢ (z +_{𝑷} B) +_{𝑷} (u +_{𝑷} C) = z +_{𝑷} (B +_{𝑷} (u +_{𝑷} C))$
31	28 29 30	3eqtr4i	$⊢ (z +_{𝑷} u) +_{𝑷} (B +_{𝑷} C) = (z +_{𝑷} B) +_{𝑷} (u +_{𝑷} C)$
32		addcompr	$⊢ v +_{𝑷} A = A +_{𝑷} v$
33	32	oveq1i	$⊢ (v +_{𝑷} A) +_{𝑷} D = (A +_{𝑷} v) +_{𝑷} D$
34		addasspr	$⊢ (v +_{𝑷} A) +_{𝑷} D = v +_{𝑷} (A +_{𝑷} D)$
35		addasspr	$⊢ (A +_{𝑷} v) +_{𝑷} D = A +_{𝑷} (v +_{𝑷} D)$
36	33 34 35	3eqtr3i	$⊢ v +_{𝑷} (A +_{𝑷} D) = A +_{𝑷} (v +_{𝑷} D)$
37	36	oveq2i	$⊢ w +_{𝑷} (v +_{𝑷} (A +_{𝑷} D)) = w +_{𝑷} (A +_{𝑷} (v +_{𝑷} D))$
38		addasspr	$⊢ (w +_{𝑷} v) +_{𝑷} (A +_{𝑷} D) = w +_{𝑷} (v +_{𝑷} (A +_{𝑷} D))$
39		addasspr	$⊢ (w +_{𝑷} A) +_{𝑷} (v +_{𝑷} D) = w +_{𝑷} (A +_{𝑷} (v +_{𝑷} D))$
40	37 38 39	3eqtr4i	$⊢ (w +_{𝑷} v) +_{𝑷} (A +_{𝑷} D) = (w +_{𝑷} A) +_{𝑷} (v +_{𝑷} D)$
41	22 31 40	3eqtr4g	$⊢ (z +_{𝑷} B = w +_{𝑷} A \land u +_{𝑷} C = v +_{𝑷} D) \to (z +_{𝑷} u) +_{𝑷} (B +_{𝑷} C) = (w +_{𝑷} v) +_{𝑷} (A +_{𝑷} D)$
42	21 41	biimtrdi	$⊢ (((z \in 𝑷 \land w \in 𝑷) \land (A \in 𝑷 \land B \in 𝑷)) \land ((v \in 𝑷 \land u \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷))) \to (([⟨z, w⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \land [⟨v, u⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \to (z +_{𝑷} u) +_{𝑷} (B +_{𝑷} C) = (w +_{𝑷} v) +_{𝑷} (A +_{𝑷} D))$
43		ovex	$⊢ z +_{𝑷} u \in V$
44		ovex	$⊢ B +_{𝑷} C \in V$
45		ltapr	$⊢ f \in 𝑷 \to (x <_{𝑷} y \leftrightarrow (f +_{𝑷} x) <_{𝑷} (f +_{𝑷} y))$
46		ovex	$⊢ w +_{𝑷} v \in V$
47		addcompr	$⊢ x +_{𝑷} y = y +_{𝑷} x$
48		ovex	$⊢ A +_{𝑷} D \in V$
49	43 44 45 46 47 48	caovord3	$⊢ ((B +_{𝑷} C \in 𝑷 \land w +_{𝑷} v \in 𝑷) \land (z +_{𝑷} u) +_{𝑷} (B +_{𝑷} C) = (w +_{𝑷} v) +_{𝑷} (A +_{𝑷} D)) \to ((z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v) \leftrightarrow (A +_{𝑷} D) <_{𝑷} (B +_{𝑷} C))$
50	16 42 49	syl6an	$⊢ (((z \in 𝑷 \land w \in 𝑷) \land (A \in 𝑷 \land B \in 𝑷)) \land ((v \in 𝑷 \land u \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷))) \to (([⟨z, w⟩] ~_{𝑹} = [⟨A, B⟩] ~_{𝑹} \land [⟨v, u⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹}) \to ((z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v) \leftrightarrow (A +_{𝑷} D) <_{𝑷} (B +_{𝑷} C)))$
51	9 1 4 10 50	brecop	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ([⟨A, B⟩] ~_{𝑹} <_{𝑹} [⟨C, D⟩] ~_{𝑹} \leftrightarrow (A +_{𝑷} D) <_{𝑷} (B +_{𝑷} C))$
52	3 4 5 6 7 8 51	brecop2	$⊢ [⟨A, B⟩] ~_{𝑹} <_{𝑹} [⟨C, D⟩] ~_{𝑹} \leftrightarrow (A +_{𝑷} D) <_{𝑷} (B +_{𝑷} C)$

Metamath Proof Explorer

Theorem ltsrpr

Proof