This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )