Metamath Proof Explorer

Theorem xaddge0

Description: The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	xaddge0	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 +_𝑒 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		0xr	⊢ 0 ∈ ℝ^*
2	1	a1i	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ∈ ℝ^* )
3		simplr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ^* )
4		xaddcl	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℝ^* )
5	4	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℝ^* )
6		simprr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ 𝐵 )
7		xaddlid	⊢ ( 𝐵 ∈ ℝ^* → ( 0 +_𝑒 𝐵 ) = 𝐵 )
8	3 7	syl	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → ( 0 +_𝑒 𝐵 ) = 𝐵 )
9		simpll	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ^* )
10		simprl	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ 𝐴 )
11		xleadd1a	⊢ ( ( ( 0 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 0 ≤ 𝐴 ) → ( 0 +_𝑒 𝐵 ) ≤ ( 𝐴 +_𝑒 𝐵 ) )
12	2 9 3 10 11	syl31anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → ( 0 +_𝑒 𝐵 ) ≤ ( 𝐴 +_𝑒 𝐵 ) )
13	8 12	eqbrtrrd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐵 ≤ ( 𝐴 +_𝑒 𝐵 ) )
14	2 3 5 6 13	xrletrd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 +_𝑒 𝐵 ) )