# Metamath Proof Explorer

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 {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{x}\in {A}$

### Proof

Step Hyp Ref Expression
1 prnmax ${⊢}\left({A}\in 𝑷\wedge {B}\in {A}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}{<}_{𝑸}{y}$
2 ltrelnq ${⊢}{<}_{𝑸}\subseteq 𝑸×𝑸$
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}↔\exists {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{x}={y}\right)$
6 5 biimpcd ${⊢}{B}{<}_{𝑸}{y}\to \left({y}\in 𝑸\to \exists {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{x}={y}\right)$
7 4 6 mpd ${⊢}{B}{<}_{𝑸}{y}\to \exists {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{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 {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{x}\in {A}\right)$
10 7 9 syl5 ${⊢}{y}\in {A}\to \left({B}{<}_{𝑸}{y}\to \exists {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{x}\in {A}\right)$
11 10 rexlimiv ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}{<}_{𝑸}{y}\to \exists {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{x}\in {A}$
12 1 11 syl ${⊢}\left({A}\in 𝑷\wedge {B}\in {A}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{B}{+}_{𝑸}{x}\in {A}$