dstfrvinc

Description: A cumulative distribution function is nondecreasing. (Contributed by Thierry Arnoux, 11-Feb-2017)

	Ref	Expression
Hypotheses	dstfrv.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
	dstfrv.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
	dstfrv.3	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝑥 ) ) ) )
	dstfrvinc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	dstfrvinc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	dstfrvinc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
Assertion	dstfrvinc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		dstfrv.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		dstfrv.3	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝑥 ) ) ) )
4		dstfrvinc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5		dstfrvinc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
6		dstfrvinc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
7		domprobmeas	⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
8	1 7	syl	⊢ ( 𝜑 → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
9	1 2 4	orvclteel	⊢ ( 𝜑 → ( 𝑋 ∘_RV/𝑐 ≤ 𝐴 ) ∈ dom 𝑃 )
10	1 2 5	orvclteel	⊢ ( 𝜑 → ( 𝑋 ∘_RV/𝑐 ≤ 𝐵 ) ∈ dom 𝑃 )
11	1 2 4 5 6	orvclteinc	⊢ ( 𝜑 → ( 𝑋 ∘_RV/𝑐 ≤ 𝐴 ) ⊆ ( 𝑋 ∘_RV/𝑐 ≤ 𝐵 ) )
12	8 9 10 11	measssd	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝐴 ) ) ≤ ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝐵 ) ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
14	13	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑋 ∘_RV/𝑐 ≤ 𝑥 ) = ( 𝑋 ∘_RV/𝑐 ≤ 𝐴 ) )
15	14	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝑥 ) ) = ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝐴 ) ) )
16	1 9	probvalrnd	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝐴 ) ) ∈ ℝ )
17	3 15 4 16	fvmptd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝐴 ) ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
19	18	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝑋 ∘_RV/𝑐 ≤ 𝑥 ) = ( 𝑋 ∘_RV/𝑐 ≤ 𝐵 ) )
20	19	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝑥 ) ) = ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝐵 ) ) )
21	1 10	probvalrnd	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝐵 ) ) ∈ ℝ )
22	3 20 5 21	fvmptd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = ( 𝑃 ‘ ( 𝑋 ∘_RV/𝑐 ≤ 𝐵 ) ) )
23	12 17 22	3brtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem dstfrvinc

Proof