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 ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ( 𝐵 +Q 𝑥 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 prnmax ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝐵 <Q 𝑦 )
2 ltrelnq ⊢ <Q ⊆ ( Q × Q )
3 2 brel ⊢ ( 𝐵 <Q 𝑦 → ( 𝐵 ∈ Q ∧ 𝑦 ∈ Q ) )
4 3 simprd ⊢ ( 𝐵 <Q 𝑦 → 𝑦 ∈ Q )
5 ltexnq ⊢ ( 𝑦 ∈ Q → ( 𝐵 <Q 𝑦 ↔ ∃ 𝑥 ( 𝐵 +Q 𝑥 ) = 𝑦 ) )
6 5 biimpcd ⊢ ( 𝐵 <Q 𝑦 → ( 𝑦 ∈ Q → ∃ 𝑥 ( 𝐵 +Q 𝑥 ) = 𝑦 ) )
7 4 6 mpd ⊢ ( 𝐵 <Q 𝑦 → ∃ 𝑥 ( 𝐵 +Q 𝑥 ) = 𝑦 )
8 eleq1a ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐵 +Q 𝑥 ) = 𝑦 → ( 𝐵 +Q 𝑥 ) ∈ 𝐴 ) )
9 8 eximdv ⊢ ( 𝑦 ∈ 𝐴 → ( ∃ 𝑥 ( 𝐵 +Q 𝑥 ) = 𝑦 → ∃ 𝑥 ( 𝐵 +Q 𝑥 ) ∈ 𝐴 ) )
10 7 9 syl5 ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐵 <Q 𝑦 → ∃ 𝑥 ( 𝐵 +Q 𝑥 ) ∈ 𝐴 ) )
11 10 rexlimiv ⊢ ( ∃ 𝑦 ∈ 𝐴 𝐵 <Q 𝑦 → ∃ 𝑥 ( 𝐵 +Q 𝑥 ) ∈ 𝐴 )
12 1 11 syl ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ( 𝐵 +Q 𝑥 ) ∈ 𝐴 )