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	|- ( ( A e. P. /\ B e. A ) -> E. x ( B +Q x ) e. A )

Proof

Step	Hyp	Ref	Expression
1		prnmax	|- ( ( A e. P. /\ B e. A ) -> E. y e. A B
2		ltrelnq	|-
3	2	brel	|- ( B ( B e. Q. /\ y e. Q. ) )
4	3	simprd	|- ( B y e. Q. )
5		ltexnq	|- ( y e. Q. -> ( B E. x ( B +Q x ) = y ) )
6	5	biimpcd	|- ( B ( y e. Q. -> E. x ( B +Q x ) = y ) )
7	4 6	mpd	|- ( B E. x ( B +Q x ) = y )
8		eleq1a	|- ( y e. A -> ( ( B +Q x ) = y -> ( B +Q x ) e. A ) )
9	8	eximdv	|- ( y e. A -> ( E. x ( B +Q x ) = y -> E. x ( B +Q x ) e. A ) )
10	7 9	syl5	|- ( y e. A -> ( B E. x ( B +Q x ) e. A ) )
11	10	rexlimiv	|- ( E. y e. A B E. x ( B +Q x ) e. A )
12	1 11	syl	|- ( ( A e. P. /\ B e. A ) -> E. x ( B +Q x ) e. A )