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 | ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐴 ) ∈ ℝ ) |
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 | ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐴 ) ∈ ℝ ) |