Theorem sn-ltaddpos

Description: ltaddpos without ax-mulcom . (Contributed by SN, 13-Feb-2024)

	Ref	Expression
Assertion	sn-ltaddpos	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 ↔ 𝐵 < ( 𝐵 + 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		ltadd2	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 ↔ ( 𝐵 + 0 ) < ( 𝐵 + 𝐴 ) ) )
3	1 2	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 ↔ ( 𝐵 + 0 ) < ( 𝐵 + 𝐴 ) ) )
4		readdid1	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 0 ) = 𝐵 )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 + 0 ) = 𝐵 )
6	5	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 + 0 ) < ( 𝐵 + 𝐴 ) ↔ 𝐵 < ( 𝐵 + 𝐴 ) ) )
7	3 6	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 ↔ 𝐵 < ( 𝐵 + 𝐴 ) ) )