Theorem ltaddrp2d

Description: Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	rpgecld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	rpgecld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
Assertion	ltaddrp2d	⊢ ( 𝜑 → 𝐴 < ( 𝐵 + 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rpgecld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		rpgecld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3	1 2	ltaddrpd	⊢ ( 𝜑 → 𝐴 < ( 𝐴 + 𝐵 ) )
4	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5	2	rpcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6	4 5	addcomd	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
7	3 6	breqtrd	⊢ ( 𝜑 → 𝐴 < ( 𝐵 + 𝐴 ) )