Metamath Proof Explorer


Theorem 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 φ P Prob
dstfrv.2 φ X RndVar P
dstfrv.3 φ F = x P X RV/c x
Assertion dstfrvclim1 φ F 1

Proof

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