Theorem meale0eq0

Description: A measure that is less than or equal to 0 is 0 . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	meale0eq0.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meale0eq0.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑀 )
	meale0eq0.l	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ 0 )
Assertion	meale0eq0	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		meale0eq0.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meale0eq0.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑀 )
3		meale0eq0.l	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ 0 )
4		eqid	⊢ dom 𝑀 = dom 𝑀
5	1 4 2	meaxrcl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
6		0xr	⊢ 0 ∈ ℝ*
7	6	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
8	1 2	meage0	⊢ ( 𝜑 → 0 ≤ ( 𝑀 ‘ 𝐴 ) )
9	5 7 3 8	xrletrid	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = 0 )