This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniioombllem3

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
uniioombl.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
uniioombl.m2 ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
uniioombl.k ⊢ 𝐾 = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
Assertion uniioombllem3 ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) < ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3 uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
5 uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6 uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
7 uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8 uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
9 uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10 uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11 uniioombl.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
12 uniioombl.m2 ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
13 uniioombl.k ⊢ 𝐾 = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
14 inss1 ⊢ ( 𝐸 ∩ 𝐴 ) ⊆ 𝐸
15 14 a1i ⊢ ( 𝜑 → ( 𝐸 ∩ 𝐴 ) ⊆ 𝐸 )
16 7 uniiccdif ⊢ ( 𝜑 → ( ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ∧ ( vol* ‘ ( ∪ ran ( [,] ∘ 𝐺 ) ∖ ∪ ran ( (,) ∘ 𝐺 ) ) ) = 0 ) )
17 16 simpld ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) )
18 ovolficcss ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐺 ) ⊆ ℝ )
19 7 18 syl ⊢ ( 𝜑 → ∪ ran ( [,] ∘ 𝐺 ) ⊆ ℝ )
20 17 19 sstrd ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ )
21 8 20 sstrd ⊢ ( 𝜑 → 𝐸 ⊆ ℝ )
22 ovolsscl ⊢ ( ( ( 𝐸 ∩ 𝐴 ) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ℝ )
23 15 21 5 22 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ℝ )
24 difssd ⊢ ( 𝜑 → ( 𝐸 ∖ 𝐴 ) ⊆ 𝐸 )
25 ovolsscl ⊢ ( ( ( 𝐸 ∖ 𝐴 ) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ∈ ℝ )
26 24 21 5 25 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ∈ ℝ )
27 inss1 ⊢ ( 𝐾 ∩ 𝐴 ) ⊆ 𝐾
28 27 a1i ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐴 ) ⊆ 𝐾 )
29 1 2 3 4 5 6 7 8 9 10 11 12 13 uniioombllem3a ⊢ ( 𝜑 → ( 𝐾 = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) )
30 29 simpld ⊢ ( 𝜑 → 𝐾 = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) )
31 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
32 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℕ )
33 ffvelcdm ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
34 7 32 33 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
35 31 34 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) )
36 1st2nd2 ⊢ ( ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) = ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
38 37 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ ) )
39 df-ov ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ⟩ )
40 38 39 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
41 ioossre ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ
42 40 41 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
43 42 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
44 iunss ⊢ ( ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ↔ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
45 43 44 sylibr ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ )
46 30 45 eqsstrd ⊢ ( 𝜑 → 𝐾 ⊆ ℝ )
47 29 simprd ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ∈ ℝ )
48 ovolsscl ⊢ ( ( ( 𝐾 ∩ 𝐴 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ∈ ℝ )
49 28 46 47 48 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ∈ ℝ )
50 6 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
51 49 50 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + 𝐶 ) ∈ ℝ )
52 difssd ⊢ ( 𝜑 → ( 𝐾 ∖ 𝐴 ) ⊆ 𝐾 )
53 ovolsscl ⊢ ( ( ( 𝐾 ∖ 𝐴 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ∈ ℝ )
54 52 46 47 53 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ∈ ℝ )
55 54 50 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + 𝐶 ) ∈ ℝ )
56 ssun2 ⊢ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
57 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
58 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
59 31 58 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
60 fss ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
61 7 59 60 sylancl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
62 fco ⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
63 57 61 62 sylancr ⊢ ( 𝜑 → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
64 63 ffnd ⊢ ( 𝜑 → ( (,) ∘ 𝐺 ) Fn ℕ )
65 fnima ⊢ ( ( (,) ∘ 𝐺 ) Fn ℕ → ( ( (,) ∘ 𝐺 ) “ ℕ ) = ran ( (,) ∘ 𝐺 ) )
66 64 65 syl ⊢ ( 𝜑 → ( ( (,) ∘ 𝐺 ) “ ℕ ) = ran ( (,) ∘ 𝐺 ) )
67 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
68 11 peano2nnd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ )
69 68 67 eleqtrdi ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
70 uzsplit ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 1 ) = ( ( 1 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
71 69 70 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 1 ) = ( ( 1 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
72 67 71 eqtrid ⊢ ( 𝜑 → ℕ = ( ( 1 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
73 11 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
74 ax-1cn ⊢ 1 ∈ ℂ
75 pncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
76 73 74 75 sylancl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
77 76 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 𝑀 + 1 ) − 1 ) ) = ( 1 ... 𝑀 ) )
78 77 uneq1d ⊢ ( 𝜑 → ( ( 1 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = ( ( 1 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
79 72 78 eqtrd ⊢ ( 𝜑 → ℕ = ( ( 1 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
80 79 imaeq2d ⊢ ( 𝜑 → ( ( (,) ∘ 𝐺 ) “ ℕ ) = ( ( (,) ∘ 𝐺 ) “ ( ( 1 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
81 66 80 eqtr3d ⊢ ( 𝜑 → ran ( (,) ∘ 𝐺 ) = ( ( (,) ∘ 𝐺 ) “ ( ( 1 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
82 imaundi ⊢ ( ( (,) ∘ 𝐺 ) “ ( ( 1 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) = ( ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
83 81 82 eqtrdi ⊢ ( 𝜑 → ran ( (,) ∘ 𝐺 ) = ( ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
84 83 unieqd ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) = ∪ ( ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
85 uniun ⊢ ∪ ( ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) = ( ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
86 84 85 eqtrdi ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) = ( ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
87 13 uneq1i ⊢ ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) = ( ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
88 86 87 eqtr4di ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) = ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
89 56 88 sseqtrrid ⊢ ( 𝜑 → ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
90 1 2 3 4 5 6 7 8 9 10 uniioombllem1 ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
91 ssid ⊢ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( (,) ∘ 𝐺 )
92 9 ovollb ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
93 7 91 92 sylancl ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
94 ovollecl ⊢ ( ( ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ )
95 20 90 93 94 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ )
96 ovolsscl ⊢ ( ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ ) → ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∈ ℝ )
97 89 20 95 96 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∈ ℝ )
98 49 97 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ∈ ℝ )
99 unss1 ⊢ ( ( 𝐾 ∩ 𝐴 ) ⊆ 𝐾 → ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
100 27 99 ax-mp ⊢ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
101 100 88 sseqtrrid ⊢ ( 𝜑 → ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
102 ovolsscl ⊢ ( ( ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ∈ ℝ )
103 101 20 95 102 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ∈ ℝ )
104 8 88 sseqtrd ⊢ ( 𝜑 → 𝐸 ⊆ ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
105 104 ssrind ⊢ ( 𝜑 → ( 𝐸 ∩ 𝐴 ) ⊆ ( ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∩ 𝐴 ) )
106 indir ⊢ ( ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∩ 𝐴 ) = ( ( 𝐾 ∩ 𝐴 ) ∪ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∩ 𝐴 ) )
107 inss1 ⊢ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∩ 𝐴 ) ⊆ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
108 unss2 ⊢ ( ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∩ 𝐴 ) ⊆ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐾 ∩ 𝐴 ) ∪ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∩ 𝐴 ) ) ⊆ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
109 107 108 ax-mp ⊢ ( ( 𝐾 ∩ 𝐴 ) ∪ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∩ 𝐴 ) ) ⊆ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
110 106 109 eqsstri ⊢ ( ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∩ 𝐴 ) ⊆ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
111 105 110 sstrdi ⊢ ( 𝜑 → ( 𝐸 ∩ 𝐴 ) ⊆ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
112 101 20 sstrd ⊢ ( 𝜑 → ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ℝ )
113 ovolss ⊢ ( ( ( 𝐸 ∩ 𝐴 ) ⊆ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ℝ ) → ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) ≤ ( vol* ‘ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
114 111 112 113 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) ≤ ( vol* ‘ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
115 28 46 sstrd ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐴 ) ⊆ ℝ )
116 89 20 sstrd ⊢ ( 𝜑 → ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ℝ )
117 ovolun ⊢ ( ( ( ( 𝐾 ∩ 𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ∈ ℝ ) ∧ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ℝ ∧ ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
118 115 49 116 97 117 syl22anc ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐾 ∩ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
119 23 103 98 114 118 letrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
120 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
121 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
122 121 9 ovolsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
123 7 122 syl ⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
124 123 11 ffvelcdmd ⊢ ( 𝜑 → ( 𝑇 ‘ 𝑀 ) ∈ ( 0 [,) +∞ ) )
125 120 124 sselid ⊢ ( 𝜑 → ( 𝑇 ‘ 𝑀 ) ∈ ℝ )
126 90 125 resubcld ⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ℝ )
127 97 rexrd ⊢ ( 𝜑 → ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∈ ℝ* )
128 id ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℕ )
129 nnaddcl ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑧 + 𝑀 ) ∈ ℕ )
130 128 11 129 syl2anr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) → ( 𝑧 + 𝑀 ) ∈ ℕ )
131 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ ( 𝑧 + 𝑀 ) ∈ ℕ ) → ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
132 130 131 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
133 132 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
134 eqid ⊢ ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) = ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) )
135 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) )
136 134 135 ovolsf ⊢ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
137 133 136 syl ⊢ ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
138 137 frnd ⊢ ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ⊆ ( 0 [,) +∞ ) )
139 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
140 138 139 sstrdi ⊢ ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ⊆ ℝ* )
141 supxrcl ⊢ ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ⊆ ℝ* → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) , ℝ* , < ) ∈ ℝ* )
142 140 141 syl ⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) , ℝ* , < ) ∈ ℝ* )
143 126 rexrd ⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ℝ* )
144 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 1 ∈ ℤ )
145 11 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
146 145 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 ∈ ℤ )
147 addcom ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑀 + 1 ) = ( 1 + 𝑀 ) )
148 73 74 147 sylancl ⊢ ( 𝜑 → ( 𝑀 + 1 ) = ( 1 + 𝑀 ) )
149 148 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) = ( ℤ≥ ‘ ( 1 + 𝑀 ) ) )
150 149 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ 𝑥 ∈ ( ℤ≥ ‘ ( 1 + 𝑀 ) ) ) )
151 150 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑥 ∈ ( ℤ≥ ‘ ( 1 + 𝑀 ) ) )
152 eluzsub ⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 1 + 𝑀 ) ) ) → ( 𝑥 − 𝑀 ) ∈ ( ℤ≥ ‘ 1 ) )
153 144 146 151 152 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑥 − 𝑀 ) ∈ ( ℤ≥ ‘ 1 ) )
154 153 67 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑥 − 𝑀 ) ∈ ℕ )
155 eluzelz ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑥 ∈ ℤ )
156 155 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑥 ∈ ℤ )
157 156 zcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑥 ∈ ℂ )
158 73 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 ∈ ℂ )
159 157 158 npcand ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑥 − 𝑀 ) + 𝑀 ) = 𝑥 )
160 159 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑥 = ( ( 𝑥 − 𝑀 ) + 𝑀 ) )
161 oveq1 ⊢ ( 𝑧 = ( 𝑥 − 𝑀 ) → ( 𝑧 + 𝑀 ) = ( ( 𝑥 − 𝑀 ) + 𝑀 ) )
162 161 rspceeqv ⊢ ( ( ( 𝑥 − 𝑀 ) ∈ ℕ ∧ 𝑥 = ( ( 𝑥 − 𝑀 ) + 𝑀 ) ) → ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑧 + 𝑀 ) )
163 154 160 162 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑧 + 𝑀 ) )
164 eqid ⊢ ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) = ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) )
165 164 elrnmpt ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ↔ ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑧 + 𝑀 ) ) )
166 165 elv ⊢ ( 𝑥 ∈ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ↔ ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑧 + 𝑀 ) )
167 163 166 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑥 ∈ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) )
168 167 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑥 ∈ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ) )
169 168 ssrdv ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) )
170 imass2 ⊢ ( ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) → ( 𝐺 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ( 𝐺 “ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ) )
171 169 170 syl ⊢ ( 𝜑 → ( 𝐺 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ( 𝐺 “ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ) )
172 rnco2 ⊢ ran ( 𝐺 ∘ ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ) = ( 𝐺 “ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) )
173 7 130 cofmpt ⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ) = ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) )
174 173 rneqd ⊢ ( 𝜑 → ran ( 𝐺 ∘ ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ) = ran ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) )
175 172 174 eqtr3id ⊢ ( 𝜑 → ( 𝐺 “ ran ( 𝑧 ∈ ℕ ↦ ( 𝑧 + 𝑀 ) ) ) = ran ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) )
176 171 175 sseqtrd ⊢ ( 𝜑 → ( 𝐺 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ran ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) )
177 imass2 ⊢ ( ( 𝐺 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ran ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) → ( (,) “ ( 𝐺 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ( (,) “ ran ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) )
178 176 177 syl ⊢ ( 𝜑 → ( (,) “ ( 𝐺 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ( (,) “ ran ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) )
179 imaco ⊢ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = ( (,) “ ( 𝐺 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
180 rnco2 ⊢ ran ( (,) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) = ( (,) “ ran ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) )
181 178 179 180 3sstr4g ⊢ ( 𝜑 → ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ran ( (,) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) )
182 181 unissd ⊢ ( 𝜑 → ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ∪ ran ( (,) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) )
183 135 ovollb ⊢ ( ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ∪ ran ( (,) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) → ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) , ℝ* , < ) )
184 133 182 183 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) , ℝ* , < ) )
185 123 frnd ⊢ ( 𝜑 → ran 𝑇 ⊆ ( 0 [,) +∞ ) )
186 185 139 sstrdi ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ* )
187 9 fveq1i ⊢ ( 𝑇 ‘ ( 𝑀 + 𝑛 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ ( 𝑀 + 𝑛 ) )
188 11 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
189 188 ltp1d ⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
190 fzdisj ⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) = ∅ )
191 189 190 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) = ∅ )
192 191 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) = ∅ )
193 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
194 nn0addge1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ≤ ( 𝑀 + 𝑛 ) )
195 188 193 194 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ≤ ( 𝑀 + 𝑛 ) )
196 11 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ℕ )
197 196 67 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
198 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑀 + 𝑛 ) ∈ ℕ )
199 11 198 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 + 𝑛 ) ∈ ℕ )
200 199 nnzd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 + 𝑛 ) ∈ ℤ )
201 elfz5 ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑀 + 𝑛 ) ∈ ℤ ) → ( 𝑀 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ↔ 𝑀 ≤ ( 𝑀 + 𝑛 ) ) )
202 197 200 201 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ↔ 𝑀 ≤ ( 𝑀 + 𝑛 ) ) )
203 195 202 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) )
204 fzsplit ⊢ ( 𝑀 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) → ( 1 ... ( 𝑀 + 𝑛 ) ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) )
205 203 204 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... ( 𝑀 + 𝑛 ) ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) )
206 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... ( 𝑀 + 𝑛 ) ) ∈ Fin )
207 7 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
208 elfznn ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) → 𝑗 ∈ ℕ )
209 ovolfcl ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
210 207 208 209 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
211 210 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
212 210 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
213 211 212 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
214 213 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℂ )
215 192 205 206 214 fsumsplit ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) + Σ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) )
216 121 ovolfsval ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑗 ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
217 207 208 216 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑗 ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
218 199 67 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 + 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) )
219 217 218 214 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑛 ) ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ ( 𝑀 + 𝑛 ) ) )
220 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
221 32 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ℕ )
222 220 221 216 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑗 ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
223 7 32 209 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
224 223 simp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
225 223 simp1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
226 224 225 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
227 226 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
228 227 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℂ )
229 222 197 228 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑀 ) )
230 9 fveq1i ⊢ ( 𝑇 ‘ 𝑀 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑀 )
231 229 230 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( 𝑇 ‘ 𝑀 ) )
232 196 nnzd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ℤ )
233 232 peano2zd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 + 1 ) ∈ ℤ )
234 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
235 196 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 + 1 ) ∈ ℕ )
236 elfzuz ⊢ ( 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
237 eluznn ⊢ ( ( ( 𝑀 + 1 ) ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑗 ∈ ℕ )
238 235 236 237 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) → 𝑗 ∈ ℕ )
239 234 238 209 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) )
240 239 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
241 239 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
242 240 241 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
243 242 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℂ )
244 2fveq3 ⊢ ( 𝑗 = ( 𝑘 + 𝑀 ) → ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) = ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) )
245 2fveq3 ⊢ ( 𝑗 = ( 𝑘 + 𝑀 ) → ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) = ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) )
246 244 245 oveq12d ⊢ ( 𝑗 = ( 𝑘 + 𝑀 ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) )
247 232 233 200 243 246 fsumshftm ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) = Σ 𝑘 ∈ ( ( ( 𝑀 + 1 ) − 𝑀 ) ... ( ( 𝑀 + 𝑛 ) − 𝑀 ) ) ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) )
248 196 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ℂ )
249 pncan2 ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 𝑀 ) = 1 )
250 248 74 249 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 + 1 ) − 𝑀 ) = 1 )
251 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
252 251 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
253 248 252 pncan2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 + 𝑛 ) − 𝑀 ) = 𝑛 )
254 250 253 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑀 + 1 ) − 𝑀 ) ... ( ( 𝑀 + 𝑛 ) − 𝑀 ) ) = ( 1 ... 𝑛 ) )
255 254 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( ( ( 𝑀 + 1 ) − 𝑀 ) ... ( ( 𝑀 + 𝑛 ) − 𝑀 ) ) ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) )
256 133 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
257 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → 𝑘 ∈ ℕ )
258 134 ovolfsval ⊢ ( ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) ) − ( 1st ‘ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) ) ) )
259 256 257 258 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) ) − ( 1st ‘ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) ) ) )
260 257 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
261 fvoveq1 ⊢ ( 𝑧 = 𝑘 → ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) = ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) )
262 eqid ⊢ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) = ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) )
263 fvex ⊢ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ∈ V
264 261 262 263 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) )
265 260 264 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) )
266 265 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 2nd ‘ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) ) = ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) )
267 265 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 1st ‘ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) ) = ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) )
268 266 267 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 2nd ‘ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) ) − ( 1st ‘ ( ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ‘ 𝑘 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) )
269 259 268 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) )
270 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
271 270 67 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
272 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
273 nnaddcl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑘 + 𝑀 ) ∈ ℕ )
274 257 196 273 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑘 + 𝑀 ) ∈ ℕ )
275 ovolfcl ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝑘 + 𝑀 ) ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) )
276 272 274 275 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) )
277 276 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ∈ ℝ )
278 276 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ∈ ℝ )
279 277 278 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) ∈ ℝ )
280 279 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) ∈ ℂ )
281 269 271 280 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 𝑀 ) ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) )
282 247 255 281 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) )
283 231 282 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) + Σ 𝑗 ∈ ( ( 𝑀 + 1 ) ... ( 𝑀 + 𝑛 ) ) ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ) )
284 215 219 283 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ ( 𝑀 + 𝑛 ) ) = ( ( 𝑇 ‘ 𝑀 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ) )
285 187 284 eqtrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑇 ‘ ( 𝑀 + 𝑛 ) ) = ( ( 𝑇 ‘ 𝑀 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ) )
286 123 ffnd ⊢ ( 𝜑 → 𝑇 Fn ℕ )
287 fnfvelrn ⊢ ( ( 𝑇 Fn ℕ ∧ ( 𝑀 + 𝑛 ) ∈ ℕ ) → ( 𝑇 ‘ ( 𝑀 + 𝑛 ) ) ∈ ran 𝑇 )
288 286 199 287 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑇 ‘ ( 𝑀 + 𝑛 ) ) ∈ ran 𝑇 )
289 285 288 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑇 ‘ 𝑀 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ) ∈ ran 𝑇 )
290 supxrub ⊢ ( ( ran 𝑇 ⊆ ℝ* ∧ ( ( 𝑇 ‘ 𝑀 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ) ∈ ran 𝑇 ) → ( ( 𝑇 ‘ 𝑀 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
291 186 289 290 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑇 ‘ 𝑀 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
292 125 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑇 ‘ 𝑀 ) ∈ ℝ )
293 137 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) )
294 120 293 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ∈ ℝ )
295 90 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
296 292 294 295 leaddsub2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑇 ‘ 𝑀 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) ↔ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ) )
297 291 296 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) )
298 297 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) )
299 137 ffnd ⊢ ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) Fn ℕ )
300 breq1 ⊢ ( 𝑥 = ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) → ( 𝑥 ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ↔ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ) )
301 300 ralrn ⊢ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) Fn ℕ → ( ∀ 𝑥 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) 𝑥 ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ↔ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ) )
302 299 301 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) 𝑥 ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ↔ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ) )
303 298 302 mpbird ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) 𝑥 ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) )
304 supxrleub ⊢ ( ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ⊆ ℝ* ∧ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ℝ* ) → ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) , ℝ* , < ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ↔ ∀ 𝑥 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) 𝑥 ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ) )
305 140 143 304 syl2anc ⊢ ( 𝜑 → ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) , ℝ* , < ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ↔ ∀ 𝑥 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) 𝑥 ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ) )
306 303 305 mpbird ⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) , ℝ* , < ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) )
307 127 142 143 184 306 xrletrd ⊢ ( 𝜑 → ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) )
308 125 90 50 absdifltd ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ↔ ( ( sup ( ran 𝑇 , ℝ* , < ) − 𝐶 ) < ( 𝑇 ‘ 𝑀 ) ∧ ( 𝑇 ‘ 𝑀 ) < ( sup ( ran 𝑇 , ℝ* , < ) + 𝐶 ) ) ) )
309 12 308 mpbid ⊢ ( 𝜑 → ( ( sup ( ran 𝑇 , ℝ* , < ) − 𝐶 ) < ( 𝑇 ‘ 𝑀 ) ∧ ( 𝑇 ‘ 𝑀 ) < ( sup ( ran 𝑇 , ℝ* , < ) + 𝐶 ) ) )
310 309 simpld ⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) − 𝐶 ) < ( 𝑇 ‘ 𝑀 ) )
311 90 50 125 310 ltsub23d ⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) < 𝐶 )
312 97 126 50 307 311 lelttrd ⊢ ( 𝜑 → ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) < 𝐶 )
313 97 50 49 312 ltadd2dd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) < ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + 𝐶 ) )
314 23 98 51 119 313 lelttrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) < ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + 𝐶 ) )
315 54 97 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ∈ ℝ )
316 difss ⊢ ( 𝐾 ∖ 𝐴 ) ⊆ 𝐾
317 unss1 ⊢ ( ( 𝐾 ∖ 𝐴 ) ⊆ 𝐾 → ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
318 316 317 ax-mp ⊢ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
319 318 88 sseqtrrid ⊢ ( 𝜑 → ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
320 ovolsscl ⊢ ( ( ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ∈ ℝ )
321 319 20 95 320 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ∈ ℝ )
322 104 ssdifd ⊢ ( 𝜑 → ( 𝐸 ∖ 𝐴 ) ⊆ ( ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∖ 𝐴 ) )
323 difundir ⊢ ( ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∖ 𝐴 ) = ( ( 𝐾 ∖ 𝐴 ) ∪ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∖ 𝐴 ) )
324 difss ⊢ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∖ 𝐴 ) ⊆ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
325 unss2 ⊢ ( ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∖ 𝐴 ) ⊆ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐾 ∖ 𝐴 ) ∪ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∖ 𝐴 ) ) ⊆ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
326 324 325 ax-mp ⊢ ( ( 𝐾 ∖ 𝐴 ) ∪ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∖ 𝐴 ) ) ⊆ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
327 323 326 eqsstri ⊢ ( ( 𝐾 ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∖ 𝐴 ) ⊆ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
328 322 327 sstrdi ⊢ ( 𝜑 → ( 𝐸 ∖ 𝐴 ) ⊆ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
329 319 20 sstrd ⊢ ( 𝜑 → ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ℝ )
330 ovolss ⊢ ( ( ( 𝐸 ∖ 𝐴 ) ⊆ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ⊆ ℝ ) → ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ≤ ( vol* ‘ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
331 328 329 330 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ≤ ( vol* ‘ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
332 52 46 sstrd ⊢ ( 𝜑 → ( 𝐾 ∖ 𝐴 ) ⊆ ℝ )
333 ovolun ⊢ ( ( ( ( 𝐾 ∖ 𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ∈ ℝ ) ∧ ( ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ⊆ ℝ ∧ ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ≤ ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
334 332 54 116 97 333 syl22anc ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐾 ∖ 𝐴 ) ∪ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) ≤ ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
335 26 321 315 331 334 letrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ≤ ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) )
336 97 50 54 312 ltadd2dd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) < ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + 𝐶 ) )
337 26 315 55 335 336 lelttrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) < ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + 𝐶 ) )
338 23 26 51 55 314 337 lt2addd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) < ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + 𝐶 ) + ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + 𝐶 ) ) )
339 49 recnd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ∈ ℂ )
340 50 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
341 54 recnd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ∈ ℂ )
342 339 340 341 340 add4d ⊢ ( 𝜑 → ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + 𝐶 ) + ( ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) + 𝐶 ) ) = ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) )
343 338 342 breqtrd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) < ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) )