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 𝑥 ) ∈ 𝐴 )