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 ∈ 𝑷 ∧ B ∈ A → ∃ x B + 𝑸 x ∈ A

Proof

Step Hyp Ref Expression
1 prnmax ⊢ A ∈ 𝑷 ∧ B ∈ A → ∃ y ∈ A B < 𝑸 y
2 ltrelnq ⊢ < 𝑸 ⊆ 𝑸 × 𝑸
3 2 brel ⊢ B < 𝑸 y → B ∈ 𝑸 ∧ y ∈ 𝑸
4 3 simprd ⊢ B < 𝑸 y → y ∈ 𝑸
5 ltexnq ⊢ y ∈ 𝑸 → B < 𝑸 y ↔ ∃ x B + 𝑸 x = y
6 5 biimpcd ⊢ B < 𝑸 y → y ∈ 𝑸 → ∃ x B + 𝑸 x = y
7 4 6 mpd ⊢ B < 𝑸 y → ∃ x B + 𝑸 x = y
8 eleq1a ⊢ y ∈ A → B + 𝑸 x = y → B + 𝑸 x ∈ A
9 8 eximdv ⊢ y ∈ A → ∃ x B + 𝑸 x = y → ∃ x B + 𝑸 x ∈ A
10 7 9 syl5 ⊢ y ∈ A → B < 𝑸 y → ∃ x B + 𝑸 x ∈ A
11 10 rexlimiv ⊢ ∃ y ∈ A B < 𝑸 y → ∃ x B + 𝑸 x ∈ A
12 1 11 syl ⊢ A ∈ 𝑷 ∧ B ∈ A → ∃ x B + 𝑸 x ∈ A