This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem plpv

Description: Value of addition on positive reals. (Contributed by NM, 28-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion plpv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A + 𝑷 B = x | ∃ y ∈ A ∃ z ∈ B x = y + 𝑸 z

Proof

Step Hyp Ref Expression
1 df-plp ⊢ + 𝑷 = u ∈ 𝑷 , v ∈ 𝑷 ⟼ f | ∃ g ∈ u ∃ h ∈ v f = g + 𝑸 h
2 addclnq ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → g + 𝑸 h ∈ 𝑸
3 1 2 genpv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A + 𝑷 B = x | ∃ y ∈ A ∃ z ∈ B x = y + 𝑸 z