axpre-ltadd

Description: Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axltadd . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd . (Contributed by NM, 11-May-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	axpre-ltadd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A <_{ℝ} B \to C + A <_{ℝ} C + B)$

Proof

Step	Hyp	Ref	Expression
1		elreal	$⊢ A \in ℝ \leftrightarrow \exists x \in 𝑹 ⟨x, 0_{𝑹}⟩ = A$
2		elreal	$⊢ B \in ℝ \leftrightarrow \exists y \in 𝑹 ⟨y, 0_{𝑹}⟩ = B$
3		elreal	$⊢ C \in ℝ \leftrightarrow \exists z \in 𝑹 ⟨z, 0_{𝑹}⟩ = C$
4		breq1	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow A <_{ℝ} ⟨y, 0_{𝑹}⟩)$
5		oveq2	$⊢ ⟨x, 0_{𝑹}⟩ = A \to ⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ + A$
6	5	breq1d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ + A <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩)$
7	4 6	bibi12d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to ((⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩) \leftrightarrow (A <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ + A <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩))$
8		breq2	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (A <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow A <_{ℝ} B)$
9		oveq2	$⊢ ⟨y, 0_{𝑹}⟩ = B \to ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ + B$
10	9	breq2d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (⟨z, 0_{𝑹}⟩ + A <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ + A <_{ℝ} ⟨z, 0_{𝑹}⟩ + B)$
11	8 10	bibi12d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to ((A <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ + A <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩) \leftrightarrow (A <_{ℝ} B \leftrightarrow ⟨z, 0_{𝑹}⟩ + A <_{ℝ} ⟨z, 0_{𝑹}⟩ + B))$
12		oveq1	$⊢ ⟨z, 0_{𝑹}⟩ = C \to ⟨z, 0_{𝑹}⟩ + A = C + A$
13		oveq1	$⊢ ⟨z, 0_{𝑹}⟩ = C \to ⟨z, 0_{𝑹}⟩ + B = C + B$
14	12 13	breq12d	$⊢ ⟨z, 0_{𝑹}⟩ = C \to (⟨z, 0_{𝑹}⟩ + A <_{ℝ} ⟨z, 0_{𝑹}⟩ + B \leftrightarrow C + A <_{ℝ} C + B)$
15	14	bibi2d	$⊢ ⟨z, 0_{𝑹}⟩ = C \to ((A <_{ℝ} B \leftrightarrow ⟨z, 0_{𝑹}⟩ + A <_{ℝ} ⟨z, 0_{𝑹}⟩ + B) \leftrightarrow (A <_{ℝ} B \leftrightarrow C + A <_{ℝ} C + B))$
16		ltasr	$⊢ z \in 𝑹 \to (x <_{𝑹} y \leftrightarrow (z +_{𝑹} x) <_{𝑹} (z +_{𝑹} y))$
17	16	adantr	$⊢ (z \in 𝑹 \land (x \in 𝑹 \land y \in 𝑹)) \to (x <_{𝑹} y \leftrightarrow (z +_{𝑹} x) <_{𝑹} (z +_{𝑹} y))$
18		ltresr	$⊢ ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow x <_{𝑹} y$
19	18	a1i	$⊢ (z \in 𝑹 \land (x \in 𝑹 \land y \in 𝑹)) \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow x <_{𝑹} y)$
20		addresr	$⊢ (z \in 𝑹 \land x \in 𝑹) \to ⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ = ⟨z +_{𝑹} x, 0_{𝑹}⟩$
21		addresr	$⊢ (z \in 𝑹 \land y \in 𝑹) \to ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ = ⟨z +_{𝑹} y, 0_{𝑹}⟩$
22	20 21	breqan12d	$⊢ ((z \in 𝑹 \land x \in 𝑹) \land (z \in 𝑹 \land y \in 𝑹)) \to (⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z +_{𝑹} x, 0_{𝑹}⟩ <_{ℝ} ⟨z +_{𝑹} y, 0_{𝑹}⟩)$
23	22	anandis	$⊢ (z \in 𝑹 \land (x \in 𝑹 \land y \in 𝑹)) \to (⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z +_{𝑹} x, 0_{𝑹}⟩ <_{ℝ} ⟨z +_{𝑹} y, 0_{𝑹}⟩)$
24		ltresr	$⊢ ⟨z +_{𝑹} x, 0_{𝑹}⟩ <_{ℝ} ⟨z +_{𝑹} y, 0_{𝑹}⟩ \leftrightarrow (z +_{𝑹} x) <_{𝑹} (z +_{𝑹} y)$
25	23 24	bitrdi	$⊢ (z \in 𝑹 \land (x \in 𝑹 \land y \in 𝑹)) \to (⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ \leftrightarrow (z +_{𝑹} x) <_{𝑹} (z +_{𝑹} y))$
26	17 19 25	3bitr4d	$⊢ (z \in 𝑹 \land (x \in 𝑹 \land y \in 𝑹)) \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩)$
27	26	ancoms	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land z \in 𝑹) \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩)$
28	27	3impa	$⊢ (x \in 𝑹 \land y \in 𝑹 \land z \in 𝑹) \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ + ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩)$
29	1 2 3 7 11 15 28	3gencl	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A <_{ℝ} B \leftrightarrow C + A <_{ℝ} C + B)$
30	29	biimpd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A <_{ℝ} B \to C + A <_{ℝ} C + B)$

Metamath Proof Explorer

Theorem axpre-ltadd

Proof