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	$$⊢\left(C{+}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\right){<}_{𝑹}\left(C{+}_{𝑹}\left[⟨B,1_{𝑷}⟩\right]{~}_{𝑹}\right)\leftrightarrow A{<}_{𝑷}B$$

Proof

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