Metamath Proof Explorer


Theorem axcontlem11

Description: Lemma for axcont . Eliminate the hypotheses from axcontlem10 . (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Assertion axcontlem11 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUb𝔼NxAyBbBtwnxy

Proof

Step Hyp Ref Expression
1 opeq2 q=pZq=Zp
2 1 breq2d q=pUBtwnZqUBtwnZp
3 breq1 q=pqBtwnZUpBtwnZU
4 2 3 orbi12d q=pUBtwnZqqBtwnZUUBtwnZppBtwnZU
5 4 cbvrabv q𝔼N|UBtwnZqqBtwnZU=p𝔼N|UBtwnZppBtwnZU
6 eqid zr|zq𝔼N|UBtwnZqqBtwnZUr0+∞j1Nzj=1rZj+rUj=zr|zq𝔼N|UBtwnZqqBtwnZUr0+∞j1Nzj=1rZj+rUj
7 6 axcontlem1 zr|zq𝔼N|UBtwnZqqBtwnZUr0+∞j1Nzj=1rZj+rUj=xt|xq𝔼N|UBtwnZqqBtwnZUt0+∞i1Nxi=1tZi+tUi
8 5 7 axcontlem10 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUb𝔼NxAyBbBtwnxy