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

Metamath Proof Explorer

Theorem sn-addgt0d

Description: The sum of positive numbers is positive. Proof of addgt0d without ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Hypotheses sn-addgt0d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
sn-addgt0d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
sn-addgt0d.1 ⊢ ( 𝜑 → 0 < 𝐴 )
sn-addgt0d.2 ⊢ ( 𝜑 → 0 < 𝐵 )
Assertion sn-addgt0d ( 𝜑 → 0 < ( 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sn-addgt0d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 sn-addgt0d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 sn-addgt0d.1 ⊢ ( 𝜑 → 0 < 𝐴 )
4 sn-addgt0d.2 ⊢ ( 𝜑 → 0 < 𝐵 )
5 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
6 1 2 readdcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
7 sn-ltaddpos ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐵 ↔ 𝐴 < ( 𝐴 + 𝐵 ) ) )
8 2 1 7 syl2anc ⊢ ( 𝜑 → ( 0 < 𝐵 ↔ 𝐴 < ( 𝐴 + 𝐵 ) ) )
9 4 8 mpbid ⊢ ( 𝜑 → 𝐴 < ( 𝐴 + 𝐵 ) )
10 5 1 6 3 9 lttrd ⊢ ( 𝜑 → 0 < ( 𝐴 + 𝐵 ) )