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

Metamath Proof Explorer

Theorem ltpsrpr

Description: Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ltpsrpr.3	$⊢ C \in 𝑹$
	Assertion	ltpsrpr	$⊢ (C +_{𝑹} [⟨A, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨B, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow A <_{𝑷} B$

Proof

Step	Hyp	Ref	Expression
1		ltpsrpr.3	$⊢ C \in 𝑹$
2		ltasr	$⊢ C \in 𝑹 \to ([⟨A, 1_{𝑷}⟩] ~_{𝑹} <_{𝑹} [⟨B, 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow (C +_{𝑹} [⟨A, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨B, 1_{𝑷}⟩] ~_{𝑹}))$
3	1 2	ax-mp	$⊢ [⟨A, 1_{𝑷}⟩] ~_{𝑹} <_{𝑹} [⟨B, 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow (C +_{𝑹} [⟨A, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨B, 1_{𝑷}⟩] ~_{𝑹})$
4		addcompr	$⊢ A +_{𝑷} 1_{𝑷} = 1_{𝑷} +_{𝑷} A$
5	4	breq1i	$⊢ (A +_{𝑷} 1_{𝑷}) <_{𝑷} (1_{𝑷} +_{𝑷} B) \leftrightarrow (1_{𝑷} +_{𝑷} A) <_{𝑷} (1_{𝑷} +_{𝑷} B)$
6		ltsrpr	$⊢ [⟨A, 1_{𝑷}⟩] ~_{𝑹} <_{𝑹} [⟨B, 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow (A +_{𝑷} 1_{𝑷}) <_{𝑷} (1_{𝑷} +_{𝑷} B)$
7		1pr	$⊢ 1_{𝑷} \in 𝑷$
8		ltapr	$⊢ 1_{𝑷} \in 𝑷 \to (A <_{𝑷} B \leftrightarrow (1_{𝑷} +_{𝑷} A) <_{𝑷} (1_{𝑷} +_{𝑷} B))$
9	7 8	ax-mp	$⊢ A <_{𝑷} B \leftrightarrow (1_{𝑷} +_{𝑷} A) <_{𝑷} (1_{𝑷} +_{𝑷} B)$
10	5 6 9	3bitr4i	$⊢ [⟨A, 1_{𝑷}⟩] ~_{𝑹} <_{𝑹} [⟨B, 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow A <_{𝑷} B$
11	3 10	bitr3i	$⊢ (C +_{𝑹} [⟨A, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨B, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow A <_{𝑷} B$