dstfrvclim1

Description: The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017) (Revised by Thierry Arnoux, 11-Jul-2017)

	Ref	Expression
Hypotheses	dstfrv.1	$⊢ φ \to P \in Prob$
	dstfrv.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
	dstfrv.3	$⊢ φ \to F = (x \in ℝ ⟼ P (X \leq_{RV/c} x))$
Assertion	dstfrvclim1	$⊢ φ \to F ⇝ 1$

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	$⊢ φ \to P \in Prob$
2		dstfrv.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
3		dstfrv.3	$⊢ φ \to F = (x \in ℝ ⟼ P (X \leq_{RV/c} x))$
4		eqid	$⊢ TopOpen (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) = TopOpen (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])$
5		domprobmeas	$⊢ P \in Prob \to P \in measures (dom P)$
6	1 5	syl	$⊢ φ \to P \in measures (dom P)$
7	1	adantr	$⊢ (φ \land i \in ℕ) \to P \in Prob$
8	2	adantr	$⊢ (φ \land i \in ℕ) \to X \in {RndVar}_{ℝ} (P)$
9		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
10	9	nnred	$⊢ (φ \land i \in ℕ) \to i \in ℝ$
11	7 8 10	orvclteel	$⊢ (φ \land i \in ℕ) \to X \leq_{RV/c} i \in dom P$
12	11	fmpttd	$⊢ φ \to (i \in ℕ ⟼ X \leq_{RV/c} i) : ℕ ⟶ dom P$
13	1	adantr	$⊢ (φ \land n \in ℕ) \to P \in Prob$
14	2	adantr	$⊢ (φ \land n \in ℕ) \to X \in {RndVar}_{ℝ} (P)$
15		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
16	15	nnred	$⊢ (φ \land n \in ℕ) \to n \in ℝ$
17	15	peano2nnd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℕ$
18	17	nnred	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℝ$
19	16	lep1d	$⊢ (φ \land n \in ℕ) \to n \leq n + 1$
20	13 14 16 18 19	orvclteinc	$⊢ (φ \land n \in ℕ) \to X \leq_{RV/c} n \subseteq X \leq_{RV/c} (n + 1)$
21		eqidd	$⊢ (φ \land n \in ℕ) \to (i \in ℕ ⟼ X \leq_{RV/c} i) = (i \in ℕ ⟼ X \leq_{RV/c} i)$
22		simpr	$⊢ ((φ \land n \in ℕ) \land i = n) \to i = n$
23	22	oveq2d	$⊢ ((φ \land n \in ℕ) \land i = n) \to X \leq_{RV/c} i = X \leq_{RV/c} n$
24	13 14 16	orvclteel	$⊢ (φ \land n \in ℕ) \to X \leq_{RV/c} n \in dom P$
25	21 23 15 24	fvmptd	$⊢ (φ \land n \in ℕ) \to (i \in ℕ ⟼ X \leq_{RV/c} i) (n) = X \leq_{RV/c} n$
26		simpr	$⊢ ((φ \land n \in ℕ) \land i = n + 1) \to i = n + 1$
27	26	oveq2d	$⊢ ((φ \land n \in ℕ) \land i = n + 1) \to X \leq_{RV/c} i = X \leq_{RV/c} (n + 1)$
28	13 14 18	orvclteel	$⊢ (φ \land n \in ℕ) \to X \leq_{RV/c} (n + 1) \in dom P$
29	21 27 17 28	fvmptd	$⊢ (φ \land n \in ℕ) \to (i \in ℕ ⟼ X \leq_{RV/c} i) (n + 1) = X \leq_{RV/c} (n + 1)$
30	20 25 29	3sstr4d	$⊢ (φ \land n \in ℕ) \to (i \in ℕ ⟼ X \leq_{RV/c} i) (n) \subseteq (i \in ℕ ⟼ X \leq_{RV/c} i) (n + 1)$
31	4 6 12 30	meascnbl	$⊢ φ \to (P \circ (i \in ℕ ⟼ X \leq_{RV/c} i)) \underset{t}{⇝} (TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])) P (⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i))$
32		measfn	$⊢ P \in measures (dom P) \to P Fn dom P$
33		dffn5	$⊢ P Fn dom P \leftrightarrow P = (a \in dom P ⟼ P (a))$
34	33	biimpi	$⊢ P Fn dom P \to P = (a \in dom P ⟼ P (a))$
35	6 32 34	3syl	$⊢ φ \to P = (a \in dom P ⟼ P (a))$
36		prob01	$⊢ (P \in Prob \land a \in dom P) \to P (a) \in [0, 1]$
37	1 36	sylan	$⊢ (φ \land a \in dom P) \to P (a) \in [0, 1]$
38	35 37	fmpt3d	$⊢ φ \to P : dom P ⟶ [0, 1]$
39		fco	$⊢ (P : dom P ⟶ [0, 1] \land (i \in ℕ ⟼ X \leq_{RV/c} i) : ℕ ⟶ dom P) \to (P \circ (i \in ℕ ⟼ X \leq_{RV/c} i)) : ℕ ⟶ [0, 1]$
40	38 12 39	syl2anc	$⊢ φ \to (P \circ (i \in ℕ ⟼ X \leq_{RV/c} i)) : ℕ ⟶ [0, 1]$
41	1 2	dstfrvunirn	$⊢ φ \to ⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i) = ⋃ dom P$
42	1	unveldomd	$⊢ φ \to ⋃ dom P \in dom P$
43	41 42	eqeltrd	$⊢ φ \to ⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i) \in dom P$
44		prob01	$⊢ (P \in Prob \land ⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i) \in dom P) \to P (⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i)) \in [0, 1]$
45	1 43 44	syl2anc	$⊢ φ \to P (⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i)) \in [0, 1]$
46		0xr	$⊢ 0 \in ℝ^{*}$
47		pnfxr	$⊢ +∞ \in ℝ^{*}$
48		0le0	$⊢ 0 \leq 0$
49		1re	$⊢ 1 \in ℝ$
50		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
51	49 50	ax-mp	$⊢ 1 < +∞$
52		iccssico	$⊢ ((0 \in ℝ^{} \land +∞ \in ℝ^{}) \land (0 \leq 0 \land 1 < +∞)) \to [0, 1] \subseteq [0, +∞)$
53	46 47 48 51 52	mp4an	$⊢ [0, 1] \subseteq [0, +∞)$
54	4 40 45 53	lmlimxrge0	$⊢ φ \to ((P \circ (i \in ℕ ⟼ X \leq_{RV/c} i)) \underset{t}{⇝} (TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])) P (⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i)) \leftrightarrow (P \circ (i \in ℕ ⟼ X \leq_{RV/c} i)) ⇝ P (⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i)))$
55	31 54	mpbid	$⊢ φ \to (P \circ (i \in ℕ ⟼ X \leq_{RV/c} i)) ⇝ P (⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i))$
56		eqidd	$⊢ φ \to (i \in ℕ ⟼ X \leq_{RV/c} i) = (i \in ℕ ⟼ X \leq_{RV/c} i)$
57		fveq2	$⊢ a = X \leq_{RV/c} i \to P (a) = P (X \leq_{RV/c} i)$
58	11 56 35 57	fmptco	$⊢ φ \to P \circ (i \in ℕ ⟼ X \leq_{RV/c} i) = (i \in ℕ ⟼ P (X \leq_{RV/c} i))$
59	3	adantr	$⊢ (φ \land i \in ℕ) \to F = (x \in ℝ ⟼ P (X \leq_{RV/c} x))$
60		simpr	$⊢ ((φ \land i \in ℕ) \land x = i) \to x = i$
61	60	oveq2d	$⊢ ((φ \land i \in ℕ) \land x = i) \to X \leq_{RV/c} x = X \leq_{RV/c} i$
62	61	fveq2d	$⊢ ((φ \land i \in ℕ) \land x = i) \to P (X \leq_{RV/c} x) = P (X \leq_{RV/c} i)$
63	7 11	probvalrnd	$⊢ (φ \land i \in ℕ) \to P (X \leq_{RV/c} i) \in ℝ$
64	59 62 10 63	fvmptd	$⊢ (φ \land i \in ℕ) \to F (i) = P (X \leq_{RV/c} i)$
65	64	mpteq2dva	$⊢ φ \to (i \in ℕ ⟼ F (i)) = (i \in ℕ ⟼ P (X \leq_{RV/c} i))$
66	58 65	eqtr4d	$⊢ φ \to P \circ (i \in ℕ ⟼ X \leq_{RV/c} i) = (i \in ℕ ⟼ F (i))$
67	41	fveq2d	$⊢ φ \to P (⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i)) = P (⋃ dom P)$
68		probtot	$⊢ P \in Prob \to P (⋃ dom P) = 1$
69	1 68	syl	$⊢ φ \to P (⋃ dom P) = 1$
70	67 69	eqtrd	$⊢ φ \to P (⋃ ran (i \in ℕ ⟼ X \leq_{RV/c} i)) = 1$
71	55 66 70	3brtr3d	$⊢ φ \to (i \in ℕ ⟼ F (i)) ⇝ 1$
72		1z	$⊢ 1 \in ℤ$
73		reex	$⊢ ℝ \in V$
74	73	mptex	$⊢ (x \in ℝ ⟼ P (X \leq_{RV/c} x)) \in V$
75	3 74	eqeltrdi	$⊢ φ \to F \in V$
76		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
77		eqid	$⊢ (i \in ℕ ⟼ F (i)) = (i \in ℕ ⟼ F (i))$
78	76 77	climmpt	$⊢ (1 \in ℤ \land F \in V) \to (F ⇝ 1 \leftrightarrow (i \in ℕ ⟼ F (i)) ⇝ 1)$
79	72 75 78	sylancr	$⊢ φ \to (F ⇝ 1 \leftrightarrow (i \in ℕ ⟼ F (i)) ⇝ 1)$
80	71 79	mpbird	$⊢ φ \to F ⇝ 1$

Metamath Proof Explorer

Theorem dstfrvclim1

Proof