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

Proof

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

Metamath Proof Explorer

Theorem mappsrpr

Proof