Metamath Proof Explorer


Theorem readdrcl2d

Description: Reverse closure for addition: the second addend is real if the first addend is real and the sum is real. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses readdrcl2d.a ( 𝜑𝐴 ∈ ℝ )
readdrcl2d.b ( 𝜑𝐵 ∈ ℂ )
readdrcl2d.c ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
Assertion readdrcl2d ( 𝜑𝐵 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 readdrcl2d.a ( 𝜑𝐴 ∈ ℝ )
2 readdrcl2d.b ( 𝜑𝐵 ∈ ℂ )
3 readdrcl2d.c ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
4 1 recnd ( 𝜑𝐴 ∈ ℂ )
5 4 2 pncan2d ( 𝜑 → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = 𝐵 )
6 3 1 resubcld ( 𝜑 → ( ( 𝐴 + 𝐵 ) − 𝐴 ) ∈ ℝ )
7 5 6 eqeltrrd ( 𝜑𝐵 ∈ ℝ )