Step |
Hyp |
Ref |
Expression |
1 |
|
meaiininc2.f |
|- F/ n ph |
2 |
|
meaiininc2.p |
|- F/ k ph |
3 |
|
meaiininc2.m |
|- ( ph -> M e. Meas ) |
4 |
|
meaiininc2.n |
|- ( ph -> N e. ZZ ) |
5 |
|
meaiininc2.z |
|- Z = ( ZZ>= ` N ) |
6 |
|
meaiininc2.e |
|- ( ph -> E : Z --> dom M ) |
7 |
|
meaiininc2.i |
|- ( ( ph /\ n e. Z ) -> ( E ` ( n + 1 ) ) C_ ( E ` n ) ) |
8 |
|
meaiininc2.k |
|- ( ph -> E. k e. Z ( M ` ( E ` k ) ) e. RR ) |
9 |
|
meaiininc2.s |
|- S = ( n e. Z |-> ( M ` ( E ` n ) ) ) |
10 |
|
nfv |
|- F/ k S ~~> ( M ` |^|_ n e. Z ( E ` n ) ) |
11 |
|
nfv |
|- F/ n k e. Z |
12 |
|
nfv |
|- F/ n ( M ` ( E ` k ) ) e. RR |
13 |
1 11 12
|
nf3an |
|- F/ n ( ph /\ k e. Z /\ ( M ` ( E ` k ) ) e. RR ) |
14 |
3
|
3ad2ant1 |
|- ( ( ph /\ k e. Z /\ ( M ` ( E ` k ) ) e. RR ) -> M e. Meas ) |
15 |
4
|
3ad2ant1 |
|- ( ( ph /\ k e. Z /\ ( M ` ( E ` k ) ) e. RR ) -> N e. ZZ ) |
16 |
6
|
3ad2ant1 |
|- ( ( ph /\ k e. Z /\ ( M ` ( E ` k ) ) e. RR ) -> E : Z --> dom M ) |
17 |
7
|
3ad2antl1 |
|- ( ( ( ph /\ k e. Z /\ ( M ` ( E ` k ) ) e. RR ) /\ n e. Z ) -> ( E ` ( n + 1 ) ) C_ ( E ` n ) ) |
18 |
|
id |
|- ( k e. Z -> k e. Z ) |
19 |
18 5
|
eleqtrdi |
|- ( k e. Z -> k e. ( ZZ>= ` N ) ) |
20 |
19
|
3ad2ant2 |
|- ( ( ph /\ k e. Z /\ ( M ` ( E ` k ) ) e. RR ) -> k e. ( ZZ>= ` N ) ) |
21 |
|
simp3 |
|- ( ( ph /\ k e. Z /\ ( M ` ( E ` k ) ) e. RR ) -> ( M ` ( E ` k ) ) e. RR ) |
22 |
13 14 15 5 16 17 20 21 9
|
meaiininc |
|- ( ( ph /\ k e. Z /\ ( M ` ( E ` k ) ) e. RR ) -> S ~~> ( M ` |^|_ n e. Z ( E ` n ) ) ) |
23 |
22
|
3exp |
|- ( ph -> ( k e. Z -> ( ( M ` ( E ` k ) ) e. RR -> S ~~> ( M ` |^|_ n e. Z ( E ` n ) ) ) ) ) |
24 |
2 10 23
|
rexlimd |
|- ( ph -> ( E. k e. Z ( M ` ( E ` k ) ) e. RR -> S ~~> ( M ` |^|_ n e. Z ( E ` n ) ) ) ) |
25 |
8 24
|
mpd |
|- ( ph -> S ~~> ( M ` |^|_ n e. Z ( E ` n ) ) ) |