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 |
|
ffvelrn |
⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
34 |
7 32 33
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
35 |
31 34
|
sseldi |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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
|
syl5eq |
⊢ ( 𝜑 → ℕ = ( ( 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
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑇 ‘ 𝑀 ) ∈ ( 0 [,) +∞ ) ) |
125 |
120 124
|
sseldi |
⊢ ( 𝜑 → ( 𝑇 ‘ 𝑀 ) ∈ ℝ ) |
126 |
90 125
|
resubcld |
⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ℝ ) |
127 |
97
|
rexrd |
⊢ ( 𝜑 → ( vol* ‘ ∪ ( ( (,) ∘ 𝐺 ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ∈ ℝ* ) |
128 |
|
id |
⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℕ ) |
129 |
|
nnaddcl |
⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑧 + 𝑀 ) ∈ ℕ ) |
130 |
128 11 129
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) → ( 𝑧 + 𝑀 ) ∈ ℕ ) |
131 |
7
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ ( 𝑧 + 𝑀 ) ∈ ℕ ) → ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
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
|
syl5eqr |
⊢ ( 𝜑 → ( 𝐺 “ 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
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑇 ‘ ( 𝑀 + 𝑛 ) ) = ( ( 𝑇 ‘ 𝑀 ) + ( 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
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑧 ∈ ℕ ↦ ( 𝐺 ‘ ( 𝑧 + 𝑀 ) ) ) ) ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ) |
294 |
120 293
|
sseldi |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 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* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) ) |