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𝑷BAxB+𝑸xA

Proof

Step Hyp Ref Expression
1 prnmax A𝑷BAyAB<𝑸y
2 ltrelnq <𝑸𝑸×𝑸
3 2 brel B<𝑸yB𝑸y𝑸
4 3 simprd B<𝑸yy𝑸
5 ltexnq y𝑸B<𝑸yxB+𝑸x=y
6 5 biimpcd B<𝑸yy𝑸xB+𝑸x=y
7 4 6 mpd B<𝑸yxB+𝑸x=y
8 eleq1a yAB+𝑸x=yB+𝑸xA
9 8 eximdv yAxB+𝑸x=yxB+𝑸xA
10 7 9 syl5 yAB<𝑸yxB+𝑸xA
11 10 rexlimiv yAB<𝑸yxB+𝑸xA
12 1 11 syl A𝑷BAxB+𝑸xA