# Metamath Proof Explorer

## Theorem ovolval2lem

Description: The value of the Lebesgue outer measure for subsets of the reals, expressed using sum^ . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis ovolval2lem.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
Assertion ovolval2lem ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)=\mathrm{ran}\left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ovolval2lem.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
2 reex ${⊢}ℝ\in \mathrm{V}$
3 2 2 xpex ${⊢}{ℝ}^{2}\in \mathrm{V}$
4 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
5 mapss ${⊢}\left({ℝ}^{2}\in \mathrm{V}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{2}\right)\to {\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\subseteq {{ℝ}^{2}}^{ℕ}$
6 3 4 5 mp2an ${⊢}{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\subseteq {{ℝ}^{2}}^{ℕ}$
7 3 inex2 ${⊢}\le \cap {ℝ}^{2}\in \mathrm{V}$
8 7 a1i ${⊢}{\phi }\to \le \cap {ℝ}^{2}\in \mathrm{V}$
9 nnex ${⊢}ℕ\in \mathrm{V}$
10 9 a1i ${⊢}{\phi }\to ℕ\in \mathrm{V}$
11 8 10 elmapd ${⊢}{\phi }\to \left({F}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{F}:ℕ⟶\le \cap {ℝ}^{2}\right)$
12 1 11 mpbird ${⊢}{\phi }\to {F}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
13 6 12 sseldi ${⊢}{\phi }\to {F}\in \left({{ℝ}^{2}}^{ℕ}\right)$
14 1zzd ${⊢}{F}\in \left({{ℝ}^{2}}^{ℕ}\right)\to 1\in ℤ$
15 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
16 elmapi ${⊢}{F}\in \left({{ℝ}^{2}}^{ℕ}\right)\to {F}:ℕ⟶{ℝ}^{2}$
17 16 adantr ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {F}:ℕ⟶{ℝ}^{2}$
18 simpr ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {k}\in ℕ$
19 17 18 fvovco ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to \left(\left[.\right)\circ {F}\right)\left({k}\right)=\left[{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)\right)$
20 19 fveq2d ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)=vol\left(\left[{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)\right)\right)$
21 16 ffvelrnda ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {F}\left({k}\right)\in {ℝ}^{2}$
22 xp1st ${⊢}{F}\left({k}\right)\in {ℝ}^{2}\to {1}^{st}\left({F}\left({k}\right)\right)\in ℝ$
23 21 22 syl ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {1}^{st}\left({F}\left({k}\right)\right)\in ℝ$
24 xp2nd ${⊢}{F}\left({k}\right)\in {ℝ}^{2}\to {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ$
25 21 24 syl ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ$
26 volicore ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\right)\to vol\left(\left[{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)\right)\right)\in ℝ$
27 23 25 26 syl2anc ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to vol\left(\left[{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)\right)\right)\in ℝ$
28 20 27 eqeltrd ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\in ℝ$
29 28 recnd ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\in ℂ$
30 eqid ${⊢}\left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)=\left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)$
31 eqid ${⊢}seq1\left(+,\left({k}\in ℕ⟼vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)\right)=seq1\left(+,\left({k}\in ℕ⟼vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)\right)$
32 14 15 29 30 31 fsumsermpt ${⊢}{F}\in \left({{ℝ}^{2}}^{ℕ}\right)\to \left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)=seq1\left(+,\left({k}\in ℕ⟼vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)\right)$
33 13 32 syl ${⊢}{\phi }\to \left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)=seq1\left(+,\left({k}\in ℕ⟼vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)\right)$
34 simpr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to {1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)$
35 34 iftrued ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to if\left({1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right),0\right)={2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right)$
36 13 23 sylan ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {1}^{st}\left({F}\left({k}\right)\right)\in ℝ$
37 36 adantr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to {1}^{st}\left({F}\left({k}\right)\right)\in ℝ$
38 13 25 sylan ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ$
39 38 adantr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ$
40 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
41 40 37 sseldi ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to {1}^{st}\left({F}\left({k}\right)\right)\in {ℝ}^{*}$
42 40 39 sseldi ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to {2}^{nd}\left({F}\left({k}\right)\right)\in {ℝ}^{*}$
43 xpss ${⊢}{ℝ}^{2}\subseteq \mathrm{V}×\mathrm{V}$
44 43 21 sseldi ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {F}\left({k}\right)\in \left(\mathrm{V}×\mathrm{V}\right)$
45 1st2ndb ${⊢}{F}\left({k}\right)\in \left(\mathrm{V}×\mathrm{V}\right)↔{F}\left({k}\right)=⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩$
46 44 45 sylib ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {F}\left({k}\right)=⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩$
47 13 46 sylan ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right)=⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩$
48 47 eqcomd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to ⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩={F}\left({k}\right)$
49 inss1 ${⊢}\le \cap {ℝ}^{2}\subseteq \le$
50 49 a1i ${⊢}{\phi }\to \le \cap {ℝ}^{2}\subseteq \le$
51 1 50 fssd ${⊢}{\phi }\to {F}:ℕ⟶\le$
52 51 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right)\in \le$
53 48 52 eqeltrd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to ⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩\in \le$
54 df-br ${⊢}{1}^{st}\left({F}\left({k}\right)\right)\le {2}^{nd}\left({F}\left({k}\right)\right)↔⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩\in \le$
55 53 54 sylibr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {1}^{st}\left({F}\left({k}\right)\right)\le {2}^{nd}\left({F}\left({k}\right)\right)$
56 55 adantr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to {1}^{st}\left({F}\left({k}\right)\right)\le {2}^{nd}\left({F}\left({k}\right)\right)$
57 simpr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)$
58 39 37 lenltd ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to \left({2}^{nd}\left({F}\left({k}\right)\right)\le {1}^{st}\left({F}\left({k}\right)\right)↔¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)$
59 57 58 mpbird ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to {2}^{nd}\left({F}\left({k}\right)\right)\le {1}^{st}\left({F}\left({k}\right)\right)$
60 41 42 56 59 xrletrid ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)$
61 simp3 ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)$
62 simp1 ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to {1}^{st}\left({F}\left({k}\right)\right)\in ℝ$
63 simp2 ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ$
64 62 63 eqleltd ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to \left({1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)↔\left({1}^{st}\left({F}\left({k}\right)\right)\le {2}^{nd}\left({F}\left({k}\right)\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\right)$
65 61 64 mpbid ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to \left({1}^{st}\left({F}\left({k}\right)\right)\le {2}^{nd}\left({F}\left({k}\right)\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)$
66 65 simprd ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)$
67 66 iffalsed ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to if\left({1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right),0\right)=0$
68 63 recnd ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to {2}^{nd}\left({F}\left({k}\right)\right)\in ℂ$
69 61 eqcomd ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to {2}^{nd}\left({F}\left({k}\right)\right)={1}^{st}\left({F}\left({k}\right)\right)$
70 68 69 subeq0bd ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to {2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right)=0$
71 67 70 eqtr4d ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({k}\right)\right)={2}^{nd}\left({F}\left({k}\right)\right)\right)\to if\left({1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right),0\right)={2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right)$
72 37 39 60 71 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge ¬{1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right)\right)\to if\left({1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right),0\right)={2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right)$
73 35 72 pm2.61dan ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to if\left({1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right),0\right)={2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right)$
74 volico ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℝ\right)\to vol\left(\left[{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)\right)\right)=if\left({1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right),0\right)$
75 36 38 74 syl2anc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to vol\left(\left[{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)\right)\right)=if\left({1}^{st}\left({F}\left({k}\right)\right)<{2}^{nd}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right),0\right)$
76 36 38 55 abssuble0d ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left|{1}^{st}\left({F}\left({k}\right)\right)-{2}^{nd}\left({F}\left({k}\right)\right)\right|={2}^{nd}\left({F}\left({k}\right)\right)-{1}^{st}\left({F}\left({k}\right)\right)$
77 73 75 76 3eqtr4d ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to vol\left(\left[{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)\right)\right)=\left|{1}^{st}\left({F}\left({k}\right)\right)-{2}^{nd}\left({F}\left({k}\right)\right)\right|$
78 13 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\in \left({{ℝ}^{2}}^{ℕ}\right)$
79 simpr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {k}\in ℕ$
80 78 79 20 syl2anc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)=vol\left(\left[{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)\right)\right)$
81 46 fveq2d ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to \left(\mathrm{abs}\circ -\right)\left({F}\left({k}\right)\right)=\left(\mathrm{abs}\circ -\right)\left(⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩\right)$
82 df-ov ${⊢}{1}^{st}\left({F}\left({k}\right)\right)\left(\mathrm{abs}\circ -\right){2}^{nd}\left({F}\left({k}\right)\right)=\left(\mathrm{abs}\circ -\right)\left(⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩\right)$
83 82 eqcomi ${⊢}\left(\mathrm{abs}\circ -\right)\left(⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩\right)={1}^{st}\left({F}\left({k}\right)\right)\left(\mathrm{abs}\circ -\right){2}^{nd}\left({F}\left({k}\right)\right)$
84 83 a1i ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to \left(\mathrm{abs}\circ -\right)\left(⟨{1}^{st}\left({F}\left({k}\right)\right),{2}^{nd}\left({F}\left({k}\right)\right)⟩\right)={1}^{st}\left({F}\left({k}\right)\right)\left(\mathrm{abs}\circ -\right){2}^{nd}\left({F}\left({k}\right)\right)$
85 23 recnd ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {1}^{st}\left({F}\left({k}\right)\right)\in ℂ$
86 25 recnd ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {2}^{nd}\left({F}\left({k}\right)\right)\in ℂ$
87 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
88 87 cnmetdval ${⊢}\left({1}^{st}\left({F}\left({k}\right)\right)\in ℂ\wedge {2}^{nd}\left({F}\left({k}\right)\right)\in ℂ\right)\to {1}^{st}\left({F}\left({k}\right)\right)\left(\mathrm{abs}\circ -\right){2}^{nd}\left({F}\left({k}\right)\right)=\left|{1}^{st}\left({F}\left({k}\right)\right)-{2}^{nd}\left({F}\left({k}\right)\right)\right|$
89 85 86 88 syl2anc ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to {1}^{st}\left({F}\left({k}\right)\right)\left(\mathrm{abs}\circ -\right){2}^{nd}\left({F}\left({k}\right)\right)=\left|{1}^{st}\left({F}\left({k}\right)\right)-{2}^{nd}\left({F}\left({k}\right)\right)\right|$
90 81 84 89 3eqtrd ${⊢}\left({F}\in \left({{ℝ}^{2}}^{ℕ}\right)\wedge {k}\in ℕ\right)\to \left(\mathrm{abs}\circ -\right)\left({F}\left({k}\right)\right)=\left|{1}^{st}\left({F}\left({k}\right)\right)-{2}^{nd}\left({F}\left({k}\right)\right)\right|$
91 78 79 90 syl2anc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left(\mathrm{abs}\circ -\right)\left({F}\left({k}\right)\right)=\left|{1}^{st}\left({F}\left({k}\right)\right)-{2}^{nd}\left({F}\left({k}\right)\right)\right|$
92 77 80 91 3eqtr4d ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)=\left(\mathrm{abs}\circ -\right)\left({F}\left({k}\right)\right)$
93 92 mpteq2dva ${⊢}{\phi }\to \left({k}\in ℕ⟼vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)=\left({k}\in ℕ⟼\left(\mathrm{abs}\circ -\right)\left({F}\left({k}\right)\right)\right)$
94 13 16 syl ${⊢}{\phi }\to {F}:ℕ⟶{ℝ}^{2}$
95 rr2sscn2 ${⊢}{ℝ}^{2}\subseteq ℂ×ℂ$
96 95 a1i ${⊢}{\phi }\to {ℝ}^{2}\subseteq ℂ×ℂ$
97 absf ${⊢}\mathrm{abs}:ℂ⟶ℝ$
98 subf ${⊢}-:ℂ×ℂ⟶ℂ$
99 fco ${⊢}\left(\mathrm{abs}:ℂ⟶ℝ\wedge -:ℂ×ℂ⟶ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
100 97 98 99 mp2an ${⊢}\left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
101 100 a1i ${⊢}{\phi }\to \left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
102 94 96 101 fcomptss ${⊢}{\phi }\to \left(\mathrm{abs}\circ -\right)\circ {F}=\left({k}\in ℕ⟼\left(\mathrm{abs}\circ -\right)\left({F}\left({k}\right)\right)\right)$
103 93 102 eqtr4d ${⊢}{\phi }\to \left({k}\in ℕ⟼vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)=\left(\mathrm{abs}\circ -\right)\circ {F}$
104 103 seqeq3d ${⊢}{\phi }\to seq1\left(+,\left({k}\in ℕ⟼vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
105 33 104 eqtr2d ${⊢}{\phi }\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)=\left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)$
106 105 rneqd ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)=\mathrm{ran}\left({n}\in ℕ⟼\sum _{{k}=1}^{{n}}vol\left(\left(\left[.\right)\circ {F}\right)\left({k}\right)\right)\right)$