Theorem ioombl1lem1

Description: Lemma for ioombl1 . (Contributed by Mario Carneiro, 18-Aug-2014)

	Ref	Expression
Hypotheses	ioombl1.b	$$⊢B=\left(A,\mathrm{+\infty }\right)$$
	ioombl1.a	$$⊢\phi \to A\in ℝ$$
	ioombl1.e	$$⊢\phi \to E\subseteq ℝ$$
	ioombl1.v	$$⊢\phi \to {vol}^{*}\left(E\right)\in ℝ$$
	ioombl1.c	$$⊢\phi \to C\in {ℝ}^{+}$$
	ioombl1.s	$$⊢S=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ F\right)\right)$$
	ioombl1.t	$$⊢T=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ G\right)\right)$$
	ioombl1.u	$$⊢U=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ H\right)\right)$$
	ioombl1.f1	$$⊢\phi \to F:\mathbb{N}⟶\le \cap {ℝ}^2$$
	ioombl1.f2	$$⊢\phi \to E\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)$$
	ioombl1.f3	$$⊢\phi \to sup\left(\mathrm{ran}S,{ℝ}^{*},<\right)\le {vol}^{*}\left(E\right)+C$$
	ioombl1.p	$$⊢P=1^{st}\left(F\left(n\right)\right)$$
	ioombl1.q	$$⊢Q=2^{nd}\left(F\left(n\right)\right)$$
	ioombl1.g	$$⊢G=\left(n\in \mathbb{N}⟼⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\right)$$
	ioombl1.h	$$⊢H=\left(n\in \mathbb{N}⟼⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\right)$$
Assertion	ioombl1lem1	$$⊢\phi \to \left(G:\mathbb{N}⟶\le \cap {ℝ}^2\wedge H:\mathbb{N}⟶\le \cap {ℝ}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		ioombl1.b	$$⊢B=\left(A,\mathrm{+\infty }\right)$$
2		ioombl1.a	$$⊢\phi \to A\in ℝ$$
3		ioombl1.e	$$⊢\phi \to E\subseteq ℝ$$
4		ioombl1.v	$$⊢\phi \to {vol}^{*}\left(E\right)\in ℝ$$
5		ioombl1.c	$$⊢\phi \to C\in {ℝ}^{+}$$
6		ioombl1.s	$$⊢S=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ F\right)\right)$$
7		ioombl1.t	$$⊢T=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ G\right)\right)$$
8		ioombl1.u	$$⊢U=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ H\right)\right)$$
9		ioombl1.f1	$$⊢\phi \to F:\mathbb{N}⟶\le \cap {ℝ}^2$$
10		ioombl1.f2	$$⊢\phi \to E\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)$$
11		ioombl1.f3	$$⊢\phi \to sup\left(\mathrm{ran}S,{ℝ}^{*},<\right)\le {vol}^{*}\left(E\right)+C$$
12		ioombl1.p	$$⊢P=1^{st}\left(F\left(n\right)\right)$$
13		ioombl1.q	$$⊢Q=2^{nd}\left(F\left(n\right)\right)$$
14		ioombl1.g	$$⊢G=\left(n\in \mathbb{N}⟼⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\right)$$
15		ioombl1.h	$$⊢H=\left(n\in \mathbb{N}⟼⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\right)$$
16	2	adantr	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to A\in ℝ$$
17		ovolfcl	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge n\in \mathbb{N}\right)\to \left(1^{st}\left(F\left(n\right)\right)\in ℝ\wedge 2^{nd}\left(F\left(n\right)\right)\in ℝ\wedge 1^{st}\left(F\left(n\right)\right)\le 2^{nd}\left(F\left(n\right)\right)\right)$$
18	9 17	sylan	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(1^{st}\left(F\left(n\right)\right)\in ℝ\wedge 2^{nd}\left(F\left(n\right)\right)\in ℝ\wedge 1^{st}\left(F\left(n\right)\right)\le 2^{nd}\left(F\left(n\right)\right)\right)$$
19	18	simp1d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(F\left(n\right)\right)\in ℝ$$
20	12 19	eqeltrid	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to P\in ℝ$$
21	16 20	ifcld	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to if\left(P\le A,A,P\right)\in ℝ$$
22	18	simp2d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(F\left(n\right)\right)\in ℝ$$
23	13 22	eqeltrid	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to Q\in ℝ$$
24		min2	$$⊢\left(if\left(P\le A,A,P\right)\in ℝ\wedge Q\in ℝ\right)\to if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\le Q$$
25	21 23 24	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\le Q$$
26		df-br	$$⊢if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\le Q\leftrightarrow ⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\in \le$$
27	25 26	sylib	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to ⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\in \le$$
28	21 23	ifcld	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\in ℝ$$
29	28 23	opelxpd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to ⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\in {ℝ}^2$$
30	27 29	elind	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to ⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\in \left(\le \cap {ℝ}^2\right)$$
31	30 14	fmptd	$$⊢\phi \to G:\mathbb{N}⟶\le \cap {ℝ}^2$$
32		max1	$$⊢\left(P\in ℝ\wedge A\in ℝ\right)\to P\le if\left(P\le A,A,P\right)$$
33	20 16 32	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to P\le if\left(P\le A,A,P\right)$$
34	18	simp3d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(F\left(n\right)\right)\le 2^{nd}\left(F\left(n\right)\right)$$
35	34 12 13	3brtr4g	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to P\le Q$$
36		breq2	$$⊢if\left(P\le A,A,P\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\to \left(P\le if\left(P\le A,A,P\right)\leftrightarrow P\le if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\right)$$
37		breq2	$$⊢Q=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\to \left(P\le Q\leftrightarrow P\le if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\right)$$
38	36 37	ifboth	$$⊢\left(P\le if\left(P\le A,A,P\right)\wedge P\le Q\right)\to P\le if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
39	33 35 38	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to P\le if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
40		df-br	$$⊢P\le if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\leftrightarrow ⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\in \le$$
41	39 40	sylib	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to ⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\in \le$$
42	20 28	opelxpd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to ⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\in {ℝ}^2$$
43	41 42	elind	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to ⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\in \left(\le \cap {ℝ}^2\right)$$
44	43 15	fmptd	$$⊢\phi \to H:\mathbb{N}⟶\le \cap {ℝ}^2$$
45	31 44	jca	$$⊢\phi \to \left(G:\mathbb{N}⟶\le \cap {ℝ}^2\wedge H:\mathbb{N}⟶\le \cap {ℝ}^2\right)$$