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

Metamath Proof Explorer

Theorem xrltled

Description: 'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	xrltled.a	$⊢ φ \to A \in ℝ^{*}$
	xrltled.b	$⊢ φ \to B \in ℝ^{*}$
	xrltled.altb	$⊢ φ \to A < B$
Assertion	xrltled	$⊢ φ \to A \leq B$

Proof

Step	Hyp	Ref	Expression
1		xrltled.a	$⊢ φ \to A \in ℝ^{*}$
2		xrltled.b	$⊢ φ \to B \in ℝ^{*}$
3		xrltled.altb	$⊢ φ \to A < B$
4		xrltle	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to A \leq B)$
5	1 2 4	syl2anc	$⊢ φ \to (A < B \to A \leq B)$
6	3 5	mpd	$⊢ φ \to A \leq B$