Theorem mappsrpr

Description: Mapping 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	mappsrpr.2	$$⊢C\in 𝑹$$
Assertion	mappsrpr	$$⊢\left(C{+}_{𝑹}{-1}_{𝑹}\right){<}_{𝑹}\left(C{+}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\right)\leftrightarrow A\in 𝑷$$

Proof

Step	Hyp	Ref	Expression
1		mappsrpr.2	$$⊢C\in 𝑹$$
2		df-m1r	$$⊢{-1}_{𝑹}=\left[⟨1_{𝑷},1_{𝑷}{+}_{𝑷}{1}_{𝑷}⟩\right]{~}_{𝑹}$$
3	2	breq1i	$$⊢{-1}_{𝑹}{<}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\leftrightarrow \left[⟨1_{𝑷},1_{𝑷}{+}_{𝑷}{1}_{𝑷}⟩\right]{~}_{𝑹}{<}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}$$
4		ltsrpr	$$⊢\left[⟨1_{𝑷},1_{𝑷}{+}_{𝑷}{1}_{𝑷}⟩\right]{~}_{𝑹}{<}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\leftrightarrow \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\right)$$
5	3 4	bitri	$$⊢{-1}_{𝑹}{<}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\leftrightarrow \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\right)$$
6		ltasr	$$⊢C\in 𝑹\to \left({-1}_{𝑹}{<}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\leftrightarrow \left(C{+}_{𝑹}{-1}_{𝑹}\right){<}_{𝑹}\left(C{+}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\right)\right)$$
7	1 6	ax-mp	$$⊢{-1}_{𝑹}{<}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\leftrightarrow \left(C{+}_{𝑹}{-1}_{𝑹}\right){<}_{𝑹}\left(C{+}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\right)$$
8		ltrelpr	$$⊢{<}_{𝑷}\subseteq 𝑷\times 𝑷$$
9	8	brel	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\right)\to \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\in 𝑷\wedge \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\in 𝑷\right)$$
10		dmplp	$$⊢\mathrm{dom}{+}_{𝑷}=𝑷\times 𝑷$$
11		0npr	$$⊢\neg \varnothing \in 𝑷$$
12	10 11	ndmovrcl	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\in 𝑷\to \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\in 𝑷\wedge A\in 𝑷\right)$$
13	12	simprd	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\in 𝑷\to A\in 𝑷$$
14	9 13	simpl2im	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\right)\to A\in 𝑷$$
15		1pr	$$⊢1_{𝑷}\in 𝑷$$
16		addclpr	$$⊢\left(1_{𝑷}\in 𝑷\wedge 1_{𝑷}\in 𝑷\right)\to 1_{𝑷}{+}_{𝑷}{1}_{𝑷}\in 𝑷$$
17	15 15 16	mp2an	$$⊢1_{𝑷}{+}_{𝑷}{1}_{𝑷}\in 𝑷$$
18		ltaddpr	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\in 𝑷\wedge A\in 𝑷\right)\to \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\right)$$
19	17 18	mpan	$$⊢A\in 𝑷\to \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\right)$$
20	14 19	impbii	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}A\right)\leftrightarrow A\in 𝑷$$
21	5 7 20	3bitr3i	$$⊢\left(C{+}_{𝑹}{-1}_{𝑹}\right){<}_{𝑹}\left(C{+}_{𝑹}\left[⟨A,1_{𝑷}⟩\right]{~}_{𝑹}\right)\leftrightarrow A\in 𝑷$$