Metamath Proof Explorer


Theorem axcontlem6

Description: Lemma for axcont . State the defining properties of the value of F . (Contributed by Scott Fenton, 19-Jun-2013)

Ref Expression
Hypotheses axcontlem5.1 D=p𝔼N|UBtwnZppBtwnZU
axcontlem5.2 F=xt|xDt0+∞i1Nxi=1tZi+tUi
Assertion axcontlem6 NZ𝔼NU𝔼NZUPDFP0+∞i1NPi=1FPZi+FPUi

Proof

Step Hyp Ref Expression
1 axcontlem5.1 D=p𝔼N|UBtwnZppBtwnZU
2 axcontlem5.2 F=xt|xDt0+∞i1Nxi=1tZi+tUi
3 eqid FP=FP
4 2 axcontlem1 F=ys|yDs0+∞j1Nyj=1sZj+sUj
5 1 4 axcontlem5 NZ𝔼NU𝔼NZUPDFP=FPFP0+∞j1NPj=1FPZj+FPUj
6 3 5 mpbii NZ𝔼NU𝔼NZUPDFP0+∞j1NPj=1FPZj+FPUj
7 fveq2 j=iPj=Pi
8 fveq2 j=iZj=Zi
9 8 oveq2d j=i1FPZj=1FPZi
10 fveq2 j=iUj=Ui
11 10 oveq2d j=iFPUj=FPUi
12 9 11 oveq12d j=i1FPZj+FPUj=1FPZi+FPUi
13 7 12 eqeq12d j=iPj=1FPZj+FPUjPi=1FPZi+FPUi
14 13 cbvralvw j1NPj=1FPZj+FPUji1NPi=1FPZi+FPUi
15 14 anbi2i FP0+∞j1NPj=1FPZj+FPUjFP0+∞i1NPi=1FPZi+FPUi
16 6 15 sylib NZ𝔼NU𝔼NZUPDFP0+∞i1NPi=1FPZi+FPUi