Step | Hyp | Ref
| Expression |
1 | | 1re 10039 |
. . . . . . 7
|
2 | 1 | rexri 10097 |
. . . . . 6
|
3 | | 0le1 10551 |
. . . . . 6
|
4 | | pnfge 11964 |
. . . . . . 7
|
5 | 2, 4 | ax-mp 5 |
. . . . . 6
|
6 | | 0xr 10086 |
. . . . . . 7
|
7 | | pnfxr 10092 |
. . . . . . 7
|
8 | | elicc1 12219 |
. . . . . . 7
|
9 | 6, 7, 8 | mp2an 708 |
. . . . . 6
|
10 | 2, 3, 5, 9 | mpbir3an 1244 |
. . . . 5
|
11 | | 0e0iccpnf 12283 |
. . . . 5
|
12 | 10, 11 | keepel 4155 |
. . . 4
|
13 | 12 | rgenw 2924 |
. . 3
|
14 | | df-dde 30296 |
. . . 4
δ |
15 | 14 | fmpt 6381 |
. . 3
δ |
16 | 13, 15 | mpbi 220 |
. 2
δ |
17 | | 0ss 3972 |
. . 3
|
18 | | noel 3919 |
. . 3
|
19 | | ddeval0 30298 |
. . 3
δ |
20 | 17, 18, 19 | mp2an 708 |
. 2
δ |
21 | | rabxm 3961 |
. . . . . . . . 9
|
22 | | esumeq1 30096 |
. . . . . . . . 9
Σ* δ Σ* δ |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
Σ* δ Σ* δ |
24 | | nfv 1843 |
. . . . . . . . 9
|
25 | | nfcv 2764 |
. . . . . . . . 9
|
26 | | nfcv 2764 |
. . . . . . . . 9
|
27 | | rabexg 4812 |
. . . . . . . . 9
|
28 | | rabexg 4812 |
. . . . . . . . 9
|
29 | | rabnc 3962 |
. . . . . . . . . 10
|
30 | 29 | a1i 11 |
. . . . . . . . 9
|
31 | | elrabi 3359 |
. . . . . . . . . . . 12
|
32 | 31 | adantl 482 |
. . . . . . . . . . 11
|
33 | | simpl 473 |
. . . . . . . . . . 11
|
34 | | elelpwi 4171 |
. . . . . . . . . . 11
|
35 | 32, 33, 34 | syl2anc 693 |
. . . . . . . . . 10
|
36 | 16 | ffvelrni 6358 |
. . . . . . . . . 10
δ |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
δ |
38 | | elrabi 3359 |
. . . . . . . . . . . 12
|
39 | 38 | adantl 482 |
. . . . . . . . . . 11
|
40 | | simpl 473 |
. . . . . . . . . . 11
|
41 | 39, 40, 34 | syl2anc 693 |
. . . . . . . . . 10
|
42 | 41, 36 | syl 17 |
. . . . . . . . 9
δ |
43 | 24, 25, 26, 27, 28, 30, 37, 42 | esumsplit 30115 |
. . . . . . . 8
Σ* δ Σ* δΣ* δ |
44 | 23, 43 | syl5eq 2668 |
. . . . . . 7
Σ* δ Σ* δΣ* δ |
45 | 44 | adantr 481 |
. . . . . 6
Disj
Σ* δ Σ* δΣ* δ |
46 | | esumeq1 30096 |
. . . . . . . . . . . 12
Σ* δ Σ* δ |
47 | 46 | adantl 482 |
. . . . . . . . . . 11
Disj
Σ* δ Σ*
δ |
48 | | simp-4l 806 |
. . . . . . . . . . . 12
Disj
|
49 | | vex 3203 |
. . . . . . . . . . . . . 14
|
50 | 49 | rabsnel 29341 |
. . . . . . . . . . . . 13
|
51 | 50 | adantl 482 |
. . . . . . . . . . . 12
Disj
|
52 | | eleq2 2690 |
. . . . . . . . . . . . . 14
|
53 | 49, 52 | rabsnt 4266 |
. . . . . . . . . . . . 13
|
54 | 53 | adantl 482 |
. . . . . . . . . . . 12
Disj
|
55 | | elelpwi 4171 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | ancoms 469 |
. . . . . . . . . . . . . . 15
|
57 | 56 | adantrr 753 |
. . . . . . . . . . . . . 14
|
58 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
δ δ |
60 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
|
61 | 16 | ffvelrni 6358 |
. . . . . . . . . . . . . . 15
δ |
62 | 59, 60, 61 | esumsn 30127 |
. . . . . . . . . . . . . 14
Σ* δ δ |
63 | 57, 62 | syl 17 |
. . . . . . . . . . . . 13
Σ* δ δ |
64 | 57 | elpwid 4170 |
. . . . . . . . . . . . . 14
|
65 | | simprr 796 |
. . . . . . . . . . . . . 14
|
66 | | ddeval1 30297 |
. . . . . . . . . . . . . 14
δ |
67 | 64, 65, 66 | syl2anc 693 |
. . . . . . . . . . . . 13
δ |
68 | 63, 67 | eqtrd 2656 |
. . . . . . . . . . . 12
Σ* δ |
69 | 48, 51, 54, 68 | syl12anc 1324 |
. . . . . . . . . . 11
Disj
Σ* δ |
70 | 47, 69 | eqtrd 2656 |
. . . . . . . . . 10
Disj
Σ* δ |
71 | | df-disj 4621 |
. . . . . . . . . . . . . . 15
Disj
|
72 | | c0ex 10034 |
. . . . . . . . . . . . . . . 16
|
73 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
74 | 73 | rmobidv 3131 |
. . . . . . . . . . . . . . . 16
|
75 | 72, 74 | spcv 3299 |
. . . . . . . . . . . . . . 15
|
76 | 71, 75 | sylbi 207 |
. . . . . . . . . . . . . 14
Disj
|
77 | | rmo5 3162 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | biimpi 206 |
. . . . . . . . . . . . . . 15
|
79 | 78 | imp 445 |
. . . . . . . . . . . . . 14
|
80 | 76, 79 | sylan 488 |
. . . . . . . . . . . . 13
Disj
|
81 | | reusn 4262 |
. . . . . . . . . . . . 13
|
82 | 80, 81 | sylib 208 |
. . . . . . . . . . . 12
Disj
|
83 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
84 | 83 | cbvrabv 3199 |
. . . . . . . . . . . . . . . 16
|
85 | 84 | eqeq1i 2627 |
. . . . . . . . . . . . . . 15
|
86 | 50 | ancri 575 |
. . . . . . . . . . . . . . 15
|
87 | 85, 86 | sylbir 225 |
. . . . . . . . . . . . . 14
|
88 | 87 | eximi 1762 |
. . . . . . . . . . . . 13
|
89 | | df-rex 2918 |
. . . . . . . . . . . . 13
|
90 | 88, 89 | sylibr 224 |
. . . . . . . . . . . 12
|
91 | 82, 90 | syl 17 |
. . . . . . . . . . 11
Disj
|
92 | 91 | adantll 750 |
. . . . . . . . . 10
Disj
|
93 | 70, 92 | r19.29a 3078 |
. . . . . . . . 9
Disj
Σ* δ |
94 | | elpwi 4168 |
. . . . . . . . . . . 12
|
95 | | sspwuni 4611 |
. . . . . . . . . . . 12
|
96 | 94, 95 | sylib 208 |
. . . . . . . . . . 11
|
97 | | eluni2 4440 |
. . . . . . . . . . . 12
|
98 | 97 | biimpri 218 |
. . . . . . . . . . 11
|
99 | | ddeval1 30297 |
. . . . . . . . . . 11
δ |
100 | 96, 98, 99 | syl2an 494 |
. . . . . . . . . 10
δ |
101 | 100 | adantlr 751 |
. . . . . . . . 9
Disj
δ |
102 | 93, 101 | eqtr4d 2659 |
. . . . . . . 8
Disj
Σ* δ δ |
103 | | nfre1 3005 |
. . . . . . . . . . . . 13
|
104 | 103 | nfn 1784 |
. . . . . . . . . . . 12
|
105 | 83 | elrab 3363 |
. . . . . . . . . . . . . . . 16
|
106 | 105 | exbii 1774 |
. . . . . . . . . . . . . . 15
|
107 | | neq0 3930 |
. . . . . . . . . . . . . . 15
|
108 | | df-rex 2918 |
. . . . . . . . . . . . . . 15
|
109 | 106, 107,
108 | 3bitr4i 292 |
. . . . . . . . . . . . . 14
|
110 | 109 | biimpi 206 |
. . . . . . . . . . . . 13
|
111 | 110 | con1i 144 |
. . . . . . . . . . . 12
|
112 | 104, 111 | esumeq1d 30097 |
. . . . . . . . . . 11
Σ* δ
Σ* δ |
113 | | esumnul 30110 |
. . . . . . . . . . 11
Σ* δ |
114 | 112, 113 | syl6eq 2672 |
. . . . . . . . . 10
Σ* δ |
115 | 114 | adantl 482 |
. . . . . . . . 9
Disj Σ* δ |
116 | 97 | biimpi 206 |
. . . . . . . . . . . 12
|
117 | 116 | con3i 150 |
. . . . . . . . . . 11
|
118 | | ddeval0 30298 |
. . . . . . . . . . 11
δ |
119 | 96, 117, 118 | syl2an 494 |
. . . . . . . . . 10
δ |
120 | 119 | adantlr 751 |
. . . . . . . . 9
Disj δ |
121 | 115, 120 | eqtr4d 2659 |
. . . . . . . 8
Disj Σ* δ δ |
122 | 102, 121 | pm2.61dan 832 |
. . . . . . 7
Disj
Σ* δ δ |
123 | 41 | elpwid 4170 |
. . . . . . . . . . 11
|
124 | 83 | notbid 308 |
. . . . . . . . . . . . . 14
|
125 | 124 | elrab 3363 |
. . . . . . . . . . . . 13
|
126 | 125 | simprbi 480 |
. . . . . . . . . . . 12
|
127 | 126 | adantl 482 |
. . . . . . . . . . 11
|
128 | | ddeval0 30298 |
. . . . . . . . . . 11
δ |
129 | 123, 127,
128 | syl2anc 693 |
. . . . . . . . . 10
δ |
130 | 129 | esumeq2dv 30100 |
. . . . . . . . 9
Σ* δ
Σ* |
131 | | vex 3203 |
. . . . . . . . . . 11
|
132 | 131 | rabex 4813 |
. . . . . . . . . 10
|
133 | 26 | esum0 30111 |
. . . . . . . . . 10
Σ* |
134 | 132, 133 | ax-mp 5 |
. . . . . . . . 9
Σ* |
135 | 130, 134 | syl6eq 2672 |
. . . . . . . 8
Σ* δ |
136 | 135 | adantr 481 |
. . . . . . 7
Disj
Σ* δ |
137 | 122, 136 | oveq12d 6668 |
. . . . . 6
Disj
Σ* δΣ* δ δ |
138 | | vuniex 6954 |
. . . . . . . . . 10
|
139 | 138 | elpw 4164 |
. . . . . . . . 9
|
140 | 139 | biimpri 218 |
. . . . . . . 8
|
141 | | iccssxr 12256 |
. . . . . . . . 9
|
142 | 16 | ffvelrni 6358 |
. . . . . . . . 9
δ |
143 | 141, 142 | sseldi 3601 |
. . . . . . . 8
δ |
144 | | xaddid1 12072 |
. . . . . . . 8
δ δ δ |
145 | 96, 140, 143, 144 | 4syl 19 |
. . . . . . 7
δ δ |
146 | 145 | adantr 481 |
. . . . . 6
Disj
δ δ |
147 | 45, 137, 146 | 3eqtrrd 2661 |
. . . . 5
Disj
δ Σ* δ |
148 | 147 | adantrl 752 |
. . . 4
Disj δ Σ* δ |
149 | 148 | ex 450 |
. . 3
Disj
δ Σ* δ |
150 | 149 | rgen 2922 |
. 2
Disj δ Σ* δ |
151 | | reex 10027 |
. . . 4
|
152 | | pwsiga 30193 |
. . . 4
sigAlgebra |
153 | 151, 152 | ax-mp 5 |
. . 3
sigAlgebra |
154 | | elrnsiga 30189 |
. . 3
sigAlgebra sigAlgebra |
155 | | ismeas 30262 |
. . 3
sigAlgebra δ measures δ δ
Disj δ Σ* δ |
156 | 153, 154,
155 | mp2b 10 |
. 2
δ measures δ δ
Disj δ Σ* δ |
157 | 16, 20, 150, 156 | mpbir3an 1244 |
1
δ measures |