Theorem ioombl1lem3

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	ioombl1lem3	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ G\right)\left(n\right)+\left(\left(\mathrm{abs}\circ -\right)\circ H\right)\left(n\right)=\left(\left(\mathrm{abs}\circ -\right)\circ F\right)\left(n\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		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)$$
17	9 16	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)$$
18	17	simp2d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(F\left(n\right)\right)\in ℝ$$
19	13 18	eqeltrid	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to Q\in ℝ$$
20	19	recnd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to Q\in ℂ$$
21	2	adantr	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to A\in ℝ$$
22	17	simp1d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(F\left(n\right)\right)\in ℝ$$
23	12 22	eqeltrid	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to P\in ℝ$$
24	21 23	ifcld	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to if\left(P\le A,A,P\right)\in ℝ$$
25	24 19	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 ℝ$$
26	25	recnd	$$⊢\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 ℂ$$
27	23	recnd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to P\in ℂ$$
28	20 26 27	npncand	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(Q-if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\right)+if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)-P=Q-P$$
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	ioombl1lem1	$$⊢\phi \to \left(G:\mathbb{N}⟶\le \cap {ℝ}^2\wedge H:\mathbb{N}⟶\le \cap {ℝ}^2\right)$$
30	29	simpld	$$⊢\phi \to G:\mathbb{N}⟶\le \cap {ℝ}^2$$
31		eqid	$$⊢\left(\mathrm{abs}\circ -\right)\circ G=\left(\mathrm{abs}\circ -\right)\circ G$$
32	31	ovolfsval	$$⊢\left(G:\mathbb{N}⟶\le \cap {ℝ}^2\wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ G\right)\left(n\right)=2^{nd}\left(G\left(n\right)\right)-1^{st}\left(G\left(n\right)\right)$$
33	30 32	sylan	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ G\right)\left(n\right)=2^{nd}\left(G\left(n\right)\right)-1^{st}\left(G\left(n\right)\right)$$
34		simpr	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to n\in \mathbb{N}$$
35		opex	$$⊢⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\in \mathrm{V}$$
36	14	fvmpt2	$$⊢\left(n\in \mathbb{N}\wedge ⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\in \mathrm{V}\right)\to G\left(n\right)=⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩$$
37	34 35 36	sylancl	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to G\left(n\right)=⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩$$
38	37	fveq2d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(G\left(n\right)\right)=2^{nd}\left(⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\right)$$
39		op2ndg	$$⊢\left(if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\in ℝ\wedge Q\in ℝ\right)\to 2^{nd}\left(⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\right)=Q$$
40	25 19 39	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\right)=Q$$
41	38 40	eqtrd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(G\left(n\right)\right)=Q$$
42	37	fveq2d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(G\left(n\right)\right)=1^{st}\left(⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\right)$$
43		op1stg	$$⊢\left(if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\in ℝ\wedge Q\in ℝ\right)\to 1^{st}\left(⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
44	25 19 43	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(⟨if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right),Q⟩\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
45	42 44	eqtrd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(G\left(n\right)\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
46	41 45	oveq12d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(G\left(n\right)\right)-1^{st}\left(G\left(n\right)\right)=Q-if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
47	33 46	eqtrd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ G\right)\left(n\right)=Q-if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
48	29	simprd	$$⊢\phi \to H:\mathbb{N}⟶\le \cap {ℝ}^2$$
49		eqid	$$⊢\left(\mathrm{abs}\circ -\right)\circ H=\left(\mathrm{abs}\circ -\right)\circ H$$
50	49	ovolfsval	$$⊢\left(H:\mathbb{N}⟶\le \cap {ℝ}^2\wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ H\right)\left(n\right)=2^{nd}\left(H\left(n\right)\right)-1^{st}\left(H\left(n\right)\right)$$
51	48 50	sylan	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ H\right)\left(n\right)=2^{nd}\left(H\left(n\right)\right)-1^{st}\left(H\left(n\right)\right)$$
52		opex	$$⊢⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\in \mathrm{V}$$
53	15	fvmpt2	$$⊢\left(n\in \mathbb{N}\wedge ⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\in \mathrm{V}\right)\to H\left(n\right)=⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩$$
54	34 52 53	sylancl	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to H\left(n\right)=⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩$$
55	54	fveq2d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(H\left(n\right)\right)=2^{nd}\left(⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\right)$$
56		op2ndg	$$⊢\left(P\in ℝ\wedge if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\in ℝ\right)\to 2^{nd}\left(⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
57	23 25 56	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
58	55 57	eqtrd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(H\left(n\right)\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)$$
59	54	fveq2d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(H\left(n\right)\right)=1^{st}\left(⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\right)$$
60		op1stg	$$⊢\left(P\in ℝ\wedge if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\in ℝ\right)\to 1^{st}\left(⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\right)=P$$
61	23 25 60	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(⟨P,if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)⟩\right)=P$$
62	59 61	eqtrd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 1^{st}\left(H\left(n\right)\right)=P$$
63	58 62	oveq12d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to 2^{nd}\left(H\left(n\right)\right)-1^{st}\left(H\left(n\right)\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)-P$$
64	51 63	eqtrd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ H\right)\left(n\right)=if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)-P$$
65	47 64	oveq12d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ G\right)\left(n\right)+\left(\left(\mathrm{abs}\circ -\right)\circ H\right)\left(n\right)=\left(Q-if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)\right)+if\left(if\left(P\le A,A,P\right)\le Q,if\left(P\le A,A,P\right),Q\right)-P$$
66		eqid	$$⊢\left(\mathrm{abs}\circ -\right)\circ F=\left(\mathrm{abs}\circ -\right)\circ F$$
67	66	ovolfsval	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ F\right)\left(n\right)=2^{nd}\left(F\left(n\right)\right)-1^{st}\left(F\left(n\right)\right)$$
68	9 67	sylan	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ F\right)\left(n\right)=2^{nd}\left(F\left(n\right)\right)-1^{st}\left(F\left(n\right)\right)$$
69	13 12	oveq12i	$$⊢Q-P=2^{nd}\left(F\left(n\right)\right)-1^{st}\left(F\left(n\right)\right)$$
70	68 69	eqtr4di	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ F\right)\left(n\right)=Q-P$$
71	28 65 70	3eqtr4d	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ G\right)\left(n\right)+\left(\left(\mathrm{abs}\circ -\right)\circ H\right)\left(n\right)=\left(\left(\mathrm{abs}\circ -\right)\circ F\right)\left(n\right)$$