ltapr

Description: Ordering property of addition. Proposition 9-3.5(v) of Gleason p. 123. (Contributed by NM, 8-Apr-1996) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dmplp	$⊢ dom +_{𝑷} = 𝑷 \times 𝑷$
2		ltrelpr	$⊢ <_{𝑷} \subseteq 𝑷 \times 𝑷$
3		0npr	$⊢ \neg \emptyset \in 𝑷$
4		ltaprlem	$⊢ C \in 𝑷 \to (A <_{𝑷} B \to (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B))$
5	4	adantr	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to (A <_{𝑷} B \to (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B))$
6		olc	$⊢ (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B) \to (C +_{𝑷} B = C +_{𝑷} A \lor (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B))$
7		ltaprlem	$⊢ C \in 𝑷 \to (B <_{𝑷} A \to (C +_{𝑷} B) <_{𝑷} (C +_{𝑷} A))$
8	7	adantr	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to (B <_{𝑷} A \to (C +_{𝑷} B) <_{𝑷} (C +_{𝑷} A))$
9		ltsopr	$⊢ <_{𝑷} Or 𝑷$
10		sotric	$⊢ (<_{𝑷} Or 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to (B <_{𝑷} A \leftrightarrow \neg (B = A \lor A <_{𝑷} B))$
11	9 10	mpan	$⊢ (B \in 𝑷 \land A \in 𝑷) \to (B <_{𝑷} A \leftrightarrow \neg (B = A \lor A <_{𝑷} B))$
12	11	adantl	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to (B <_{𝑷} A \leftrightarrow \neg (B = A \lor A <_{𝑷} B))$
13		addclpr	$⊢ (C \in 𝑷 \land B \in 𝑷) \to C +_{𝑷} B \in 𝑷$
14		addclpr	$⊢ (C \in 𝑷 \land A \in 𝑷) \to C +_{𝑷} A \in 𝑷$
15	13 14	anim12dan	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to (C +_{𝑷} B \in 𝑷 \land C +_{𝑷} A \in 𝑷)$
16		sotric	$⊢ (<_{𝑷} Or 𝑷 \land (C +_{𝑷} B \in 𝑷 \land C +_{𝑷} A \in 𝑷)) \to ((C +_{𝑷} B) <_{𝑷} (C +_{𝑷} A) \leftrightarrow \neg (C +_{𝑷} B = C +_{𝑷} A \lor (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B)))$
17	9 15 16	sylancr	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to ((C +_{𝑷} B) <_{𝑷} (C +_{𝑷} A) \leftrightarrow \neg (C +_{𝑷} B = C +_{𝑷} A \lor (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B)))$
18	8 12 17	3imtr3d	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to (\neg (B = A \lor A <_{𝑷} B) \to \neg (C +_{𝑷} B = C +_{𝑷} A \lor (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B)))$
19	18	con4d	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to ((C +_{𝑷} B = C +_{𝑷} A \lor (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B)) \to (B = A \lor A <_{𝑷} B))$
20	6 19	syl5	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to ((C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B) \to (B = A \lor A <_{𝑷} B))$
21		df-or	$⊢ (B = A \lor A <_{𝑷} B) \leftrightarrow (\neg B = A \to A <_{𝑷} B)$
22	20 21	imbitrdi	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to ((C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B) \to (\neg B = A \to A <_{𝑷} B))$
23	22	com23	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to (\neg B = A \to ((C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B) \to A <_{𝑷} B))$
24	9 2	soirri	$⊢ \neg (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} A)$
25		oveq2	$⊢ B = A \to C +_{𝑷} B = C +_{𝑷} A$
26	25	breq2d	$⊢ B = A \to ((C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B) \leftrightarrow (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} A))$
27	24 26	mtbiri	$⊢ B = A \to \neg (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B)$
28	27	pm2.21d	$⊢ B = A \to ((C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B) \to A <_{𝑷} B)$
29	23 28	pm2.61d2	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to ((C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B) \to A <_{𝑷} B)$
30	5 29	impbid	$⊢ (C \in 𝑷 \land (B \in 𝑷 \land A \in 𝑷)) \to (A <_{𝑷} B \leftrightarrow (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B))$
31	30	3impb	$⊢ (C \in 𝑷 \land B \in 𝑷 \land A \in 𝑷) \to (A <_{𝑷} B \leftrightarrow (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B))$
32	31	3com13	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to (A <_{𝑷} B \leftrightarrow (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B))$
33	1 2 3 32	ndmovord	$⊢ C \in 𝑷 \to (A <_{𝑷} B \leftrightarrow (C +_{𝑷} A) <_{𝑷} (C +_{𝑷} B))$

Metamath Proof Explorer

Theorem ltapr

Proof