Metamath Proof Explorer


Theorem probvalrnd

Description: The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017)

Ref Expression
Hypotheses probmeasd.1 ( 𝜑𝑃 ∈ Prob )
probvalrnd.1 ( 𝜑𝐴 ∈ dom 𝑃 )
Assertion probvalrnd ( 𝜑 → ( 𝑃𝐴 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 probmeasd.1 ( 𝜑𝑃 ∈ Prob )
2 probvalrnd.1 ( 𝜑𝐴 ∈ dom 𝑃 )
3 unitssre ( 0 [,] 1 ) ⊆ ℝ
4 prob01 ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃𝐴 ) ∈ ( 0 [,] 1 ) )
5 1 2 4 syl2anc ( 𝜑 → ( 𝑃𝐴 ) ∈ ( 0 [,] 1 ) )
6 3 5 sselid ( 𝜑 → ( 𝑃𝐴 ) ∈ ℝ )