Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(TopOpenβ(β*π
βΎs (0[,]+β))) =
(TopOpenβ(β*π βΎs
(0[,]+β))) |
2 | | dstfrv.1 |
. . . . . 6
β’ (π β π β Prob) |
3 | | domprobmeas 33067 |
. . . . . 6
β’ (π β Prob β π β (measuresβdom
π)) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ (π β π β (measuresβdom π)) |
5 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β Prob) |
6 | | dstfrv.2 |
. . . . . . . 8
β’ (π β π β (rRndVarβπ)) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β (rRndVarβπ)) |
8 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
9 | 8 | nnred 12173 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
10 | 5, 7, 9 | orvclteel 33129 |
. . . . . 6
β’ ((π β§ π β β) β (πβRV/π β€ π) β dom π) |
11 | 10 | fmpttd 7064 |
. . . . 5
β’ (π β (π β β β¦ (πβRV/π β€ π)):ββΆdom π) |
12 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β Prob) |
13 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β (rRndVarβπ)) |
14 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
15 | 14 | nnred 12173 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
16 | 14 | peano2nnd 12175 |
. . . . . . . 8
β’ ((π β§ π β β) β (π + 1) β β) |
17 | 16 | nnred 12173 |
. . . . . . 7
β’ ((π β§ π β β) β (π + 1) β β) |
18 | 15 | lep1d 12091 |
. . . . . . 7
β’ ((π β§ π β β) β π β€ (π + 1)) |
19 | 12, 13, 15, 17, 18 | orvclteinc 33132 |
. . . . . 6
β’ ((π β§ π β β) β (πβRV/π β€ π) β (πβRV/π β€ (π + 1))) |
20 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ π β β) β (π β β β¦ (πβRV/π β€ π)) = (π β β β¦ (πβRV/π β€ π))) |
21 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π = π) β π = π) |
22 | 21 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π β β) β§ π = π) β (πβRV/π β€ π) = (πβRV/π β€ π)) |
23 | 12, 13, 15 | orvclteel 33129 |
. . . . . . 7
β’ ((π β§ π β β) β (πβRV/π β€ π) β dom π) |
24 | 20, 22, 14, 23 | fvmptd 6956 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β β¦ (πβRV/π β€ π))βπ) = (πβRV/π β€ π)) |
25 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π = (π + 1)) β π = (π + 1)) |
26 | 25 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π β β) β§ π = (π + 1)) β (πβRV/π β€ π) = (πβRV/π β€ (π + 1))) |
27 | 12, 13, 17 | orvclteel 33129 |
. . . . . . 7
β’ ((π β§ π β β) β (πβRV/π β€ (π + 1)) β dom π) |
28 | 20, 26, 16, 27 | fvmptd 6956 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β β¦ (πβRV/π β€ π))β(π + 1)) = (πβRV/π β€ (π + 1))) |
29 | 19, 24, 28 | 3sstr4d 3992 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ (πβRV/π β€ π))βπ) β ((π β β β¦ (πβRV/π β€ π))β(π + 1))) |
30 | 1, 4, 11, 29 | meascnbl 32875 |
. . . 4
β’ (π β (π β (π β β β¦ (πβRV/π β€ π)))(βπ‘β(TopOpenβ(β*π
βΎs (0[,]+β))))(πββͺ
ran (π β β β¦ (πβRV/π β€ π)))) |
31 | | measfn 32860 |
. . . . . . . 8
β’ (π β (measuresβdom
π) β π Fn dom π) |
32 | | dffn5 6902 |
. . . . . . . . 9
β’ (π Fn dom π β π = (π β dom π β¦ (πβπ))) |
33 | 32 | biimpi 215 |
. . . . . . . 8
β’ (π Fn dom π β π = (π β dom π β¦ (πβπ))) |
34 | 4, 31, 33 | 3syl 18 |
. . . . . . 7
β’ (π β π = (π β dom π β¦ (πβπ))) |
35 | | prob01 33070 |
. . . . . . . 8
β’ ((π β Prob β§ π β dom π) β (πβπ) β (0[,]1)) |
36 | 2, 35 | sylan 581 |
. . . . . . 7
β’ ((π β§ π β dom π) β (πβπ) β (0[,]1)) |
37 | 34, 36 | fmpt3d 7065 |
. . . . . 6
β’ (π β π:dom πβΆ(0[,]1)) |
38 | | fco 6693 |
. . . . . 6
β’ ((π:dom πβΆ(0[,]1) β§ (π β β β¦ (πβRV/π β€ π)):ββΆdom π) β (π β (π β β β¦ (πβRV/π β€ π))):ββΆ(0[,]1)) |
39 | 37, 11, 38 | syl2anc 585 |
. . . . 5
β’ (π β (π β (π β β β¦ (πβRV/π β€ π))):ββΆ(0[,]1)) |
40 | 2, 6 | dstfrvunirn 33131 |
. . . . . . 7
β’ (π β βͺ ran (π β β β¦ (πβRV/π β€ π)) = βͺ dom π) |
41 | 2 | unveldomd 33072 |
. . . . . . 7
β’ (π β βͺ dom π β dom π) |
42 | 40, 41 | eqeltrd 2834 |
. . . . . 6
β’ (π β βͺ ran (π β β β¦ (πβRV/π β€ π)) β dom π) |
43 | | prob01 33070 |
. . . . . 6
β’ ((π β Prob β§ βͺ ran (π β β β¦ (πβRV/π β€ π)) β dom π) β (πββͺ ran
(π β β β¦
(πβRV/π β€ π))) β
(0[,]1)) |
44 | 2, 42, 43 | syl2anc 585 |
. . . . 5
β’ (π β (πββͺ ran
(π β β β¦
(πβRV/π β€ π))) β
(0[,]1)) |
45 | | 0xr 11207 |
. . . . . 6
β’ 0 β
β* |
46 | | pnfxr 11214 |
. . . . . 6
β’ +β
β β* |
47 | | 0le0 12259 |
. . . . . 6
β’ 0 β€
0 |
48 | | 1re 11160 |
. . . . . . 7
β’ 1 β
β |
49 | | ltpnf 13046 |
. . . . . . 7
β’ (1 β
β β 1 < +β) |
50 | 48, 49 | ax-mp 5 |
. . . . . 6
β’ 1 <
+β |
51 | | iccssico 13342 |
. . . . . 6
β’ (((0
β β* β§ +β β β*) β§ (0
β€ 0 β§ 1 < +β)) β (0[,]1) β
(0[,)+β)) |
52 | 45, 46, 47, 50, 51 | mp4an 692 |
. . . . 5
β’ (0[,]1)
β (0[,)+β) |
53 | 1, 39, 44, 52 | lmlimxrge0 32586 |
. . . 4
β’ (π β ((π β (π β β β¦ (πβRV/π β€ π)))(βπ‘β(TopOpenβ(β*π
βΎs (0[,]+β))))(πββͺ
ran (π β β β¦ (πβRV/π β€ π)))
β (π β (π
β β β¦ (πβRV/π β€ π))) β (πββͺ ran (π β β β¦ (πβRV/π β€ π))))) |
54 | 30, 53 | mpbid 231 |
. . 3
β’ (π β (π β (π β β β¦ (πβRV/π β€ π))) β (πββͺ ran
(π β β β¦
(πβRV/π β€ π)))) |
55 | | eqidd 2734 |
. . . . 5
β’ (π β (π β β β¦ (πβRV/π β€ π)) = (π β β β¦ (πβRV/π β€ π))) |
56 | | fveq2 6843 |
. . . . 5
β’ (π = (πβRV/π β€ π) β (πβπ) = (πβ(πβRV/π β€ π))) |
57 | 10, 55, 34, 56 | fmptco 7076 |
. . . 4
β’ (π β (π β (π β β β¦ (πβRV/π β€ π))) = (π β β β¦ (πβ(πβRV/π β€ π)))) |
58 | | dstfrv.3 |
. . . . . . 7
β’ (π β πΉ = (π₯ β β β¦ (πβ(πβRV/π β€ π₯)))) |
59 | 58 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β πΉ = (π₯ β β β¦ (πβ(πβRV/π β€ π₯)))) |
60 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ = π) β π₯ = π) |
61 | 60 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ = π) β (πβRV/π β€ π₯) = (πβRV/π β€ π)) |
62 | 61 | fveq2d 6847 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ = π) β (πβ(πβRV/π β€ π₯)) = (πβ(πβRV/π β€ π))) |
63 | 5, 10 | probvalrnd 33081 |
. . . . . 6
β’ ((π β§ π β β) β (πβ(πβRV/π β€ π)) β
β) |
64 | 59, 62, 9, 63 | fvmptd 6956 |
. . . . 5
β’ ((π β§ π β β) β (πΉβπ) = (πβ(πβRV/π β€ π))) |
65 | 64 | mpteq2dva 5206 |
. . . 4
β’ (π β (π β β β¦ (πΉβπ)) = (π β β β¦ (πβ(πβRV/π β€ π)))) |
66 | 57, 65 | eqtr4d 2776 |
. . 3
β’ (π β (π β (π β β β¦ (πβRV/π β€ π))) = (π β β β¦ (πΉβπ))) |
67 | 40 | fveq2d 6847 |
. . . 4
β’ (π β (πββͺ ran
(π β β β¦
(πβRV/π β€ π))) = (πββͺ dom
π)) |
68 | | probtot 33069 |
. . . . 5
β’ (π β Prob β (πββͺ dom π) = 1) |
69 | 2, 68 | syl 17 |
. . . 4
β’ (π β (πββͺ dom
π) = 1) |
70 | 67, 69 | eqtrd 2773 |
. . 3
β’ (π β (πββͺ ran
(π β β β¦
(πβRV/π β€ π))) = 1) |
71 | 54, 66, 70 | 3brtr3d 5137 |
. 2
β’ (π β (π β β β¦ (πΉβπ)) β 1) |
72 | | 1z 12538 |
. . 3
β’ 1 β
β€ |
73 | | reex 11147 |
. . . . 5
β’ β
β V |
74 | 73 | mptex 7174 |
. . . 4
β’ (π₯ β β β¦ (πβ(πβRV/π β€ π₯))) β V |
75 | 58, 74 | eqeltrdi 2842 |
. . 3
β’ (π β πΉ β V) |
76 | | nnuz 12811 |
. . . 4
β’ β =
(β€β₯β1) |
77 | | eqid 2733 |
. . . 4
β’ (π β β β¦ (πΉβπ)) = (π β β β¦ (πΉβπ)) |
78 | 76, 77 | climmpt 15459 |
. . 3
β’ ((1
β β€ β§ πΉ
β V) β (πΉ β
1 β (π β β
β¦ (πΉβπ)) β 1)) |
79 | 72, 75, 78 | sylancr 588 |
. 2
β’ (π β (πΉ β 1 β (π β β β¦ (πΉβπ)) β 1)) |
80 | 71, 79 | mpbird 257 |
1
β’ (π β πΉ β 1) |