Theorem prnmadd

Description: A positive real has no largest member. Addition version. (Contributed by NM, 7-Apr-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	prnmadd	$$⊢\left(A\in 𝑷\wedge B\in A\right)\to \exists xB{+}_{𝑸}x\in A$$

Proof

Step	Hyp	Ref	Expression
1		prnmax	$$⊢\left(A\in 𝑷\wedge B\in A\right)\to \exists y\in AB{<}_{𝑸}y$$
2		ltrelnq	$$⊢{<}_{𝑸}\subseteq 𝑸\times 𝑸$$
3	2	brel	$$⊢B{<}_{𝑸}y\to \left(B\in 𝑸\wedge y\in 𝑸\right)$$
4	3	simprd	$$⊢B{<}_{𝑸}y\to y\in 𝑸$$
5		ltexnq	$$⊢y\in 𝑸\to \left(B{<}_{𝑸}y\leftrightarrow \exists xB{+}_{𝑸}x=y\right)$$
6	5	biimpcd	$$⊢B{<}_{𝑸}y\to \left(y\in 𝑸\to \exists xB{+}_{𝑸}x=y\right)$$
7	4 6	mpd	$$⊢B{<}_{𝑸}y\to \exists xB{+}_{𝑸}x=y$$
8		eleq1a	$$⊢y\in A\to \left(B{+}_{𝑸}x=y\to B{+}_{𝑸}x\in A\right)$$
9	8	eximdv	$$⊢y\in A\to \left(\exists xB{+}_{𝑸}x=y\to \exists xB{+}_{𝑸}x\in A\right)$$
10	7 9	syl5	$$⊢y\in A\to \left(B{<}_{𝑸}y\to \exists xB{+}_{𝑸}x\in A\right)$$
11	10	rexlimiv	$$⊢\exists y\in AB{<}_{𝑸}y\to \exists xB{+}_{𝑸}x\in A$$
12	1 11	syl	$$⊢\left(A\in 𝑷\wedge B\in A\right)\to \exists xB{+}_{𝑸}x\in A$$