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 |
|
uniioombllem2.h |
⊢ 𝐻 = ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
12 |
|
uniioombllem2.k |
⊢ 𝐾 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , 〈 0 , 0 〉 , 〈 inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) 〉 ) ) |
13 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
14 |
|
eqid |
⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) |
15 |
|
1zzd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 1 ∈ ℤ ) |
16 |
|
eqidd |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ) |
17 |
1 2 3 4 5 6 7 8 9 10
|
uniioombllem2a |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ran (,) ) |
18 |
11
|
a1i |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐻 = ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
19 |
12
|
ioorf |
⊢ 𝐾 : ran (,) ⟶ ( ≤ ∩ ( ℝ* × ℝ* ) ) |
20 |
19
|
a1i |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐾 : ran (,) ⟶ ( ≤ ∩ ( ℝ* × ℝ* ) ) ) |
21 |
20
|
feqmptd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐾 = ( 𝑦 ∈ ran (,) ↦ ( 𝐾 ‘ 𝑦 ) ) ) |
22 |
|
fveq2 |
⊢ ( 𝑦 = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) → ( 𝐾 ‘ 𝑦 ) = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
23 |
17 18 21 22
|
fmptco |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐾 ∘ 𝐻 ) = ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) ) |
24 |
|
inss2 |
⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) |
25 |
|
inss2 |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) |
26 |
7
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
27 |
25 26
|
sselid |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) ∈ ( ℝ × ℝ ) ) |
28 |
|
1st2nd2 |
⊢ ( ( 𝐺 ‘ 𝐽 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝐽 ) = 〈 ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) 〉 ) |
29 |
27 28
|
syl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) = 〈 ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) 〉 ) |
30 |
29
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) = ( (,) ‘ 〈 ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) 〉 ) ) |
31 |
|
df-ov |
⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( (,) ‘ 〈 ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) 〉 ) |
32 |
30 31
|
eqtr4di |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) = ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
33 |
|
ioossre |
⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ⊆ ℝ |
34 |
32 33
|
eqsstrdi |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ⊆ ℝ ) |
35 |
32
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
36 |
|
ovolfcl |
⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐽 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
37 |
7 36
|
sylan |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
38 |
|
ovolioo |
⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
39 |
37 38
|
syl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
40 |
35 39
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
41 |
37
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ) |
42 |
37
|
simp1d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ) |
43 |
41 42
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝐽 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ℝ ) |
44 |
40 43
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ℝ ) |
45 |
|
ovolsscl |
⊢ ( ( ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∧ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ℝ ) |
46 |
24 34 44 45
|
mp3an2i |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ℝ ) |
47 |
46
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ℝ ) |
48 |
12
|
ioorcl |
⊢ ( ( ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ran (,) ∧ ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ℝ ) → ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
49 |
17 47 48
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
50 |
23 49
|
fmpt3d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐾 ∘ 𝐻 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
51 |
|
eqid |
⊢ ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) = ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) |
52 |
51
|
ovolfsf |
⊢ ( ( 𝐾 ∘ 𝐻 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
53 |
50 52
|
syl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
54 |
53
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ) |
55 |
|
elrege0 |
⊢ ( ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ) ) |
56 |
54 55
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ) ) |
57 |
56
|
simpld |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ∈ ℝ ) |
58 |
56
|
simprd |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ‘ 𝑛 ) ) |
59 |
23
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑧 ) = ( ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) ‘ 𝑧 ) ) |
60 |
|
fvex |
⊢ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ V |
61 |
|
eqid |
⊢ ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) = ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
62 |
61
|
fvmpt2 |
⊢ ( ( 𝑧 ∈ ℕ ∧ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ V ) → ( ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) ‘ 𝑧 ) = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
63 |
60 62
|
mpan2 |
⊢ ( 𝑧 ∈ ℕ → ( ( 𝑧 ∈ ℕ ↦ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) ‘ 𝑧 ) = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
64 |
59 63
|
sylan9eq |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑧 ) = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
65 |
64
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑧 ) ) = ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) ) |
66 |
12
|
ioorinv |
⊢ ( ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ran (,) → ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
67 |
17 66
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
68 |
65 67
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑧 ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
69 |
68
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∀ 𝑧 ∈ ℕ ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑧 ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
70 |
|
2fveq3 |
⊢ ( 𝑧 = 𝑥 → ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑧 ) ) = ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) ) |
71 |
|
2fveq3 |
⊢ ( 𝑧 = 𝑥 → ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ) |
72 |
71
|
ineq1d |
⊢ ( 𝑧 = 𝑥 → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
73 |
70 72
|
eqeq12d |
⊢ ( 𝑧 = 𝑥 → ( ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑧 ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ↔ ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
74 |
73
|
rspccva |
⊢ ( ( ∀ 𝑧 ∈ ℕ ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑧 ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
75 |
69 74
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
76 |
|
inss1 |
⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ⊆ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) |
77 |
75 76
|
eqsstrdi |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑥 ∈ ℕ ) → ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) ⊆ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ) |
78 |
77
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∀ 𝑥 ∈ ℕ ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) ⊆ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ) |
79 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ) |
80 |
|
disjss2 |
⊢ ( ∀ 𝑥 ∈ ℕ ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) ⊆ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) → ( Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) → Disj 𝑥 ∈ ℕ ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) ) ) |
81 |
78 79 80
|
sylc |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → Disj 𝑥 ∈ ℕ ( (,) ‘ ( ( 𝐾 ∘ 𝐻 ) ‘ 𝑥 ) ) ) |
82 |
50 81 14
|
uniioovol |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ‘ ∪ ran ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) ) |
83 |
67
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝑧 ∈ ℕ ↦ ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) ) = ( 𝑧 ∈ ℕ ↦ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) |
84 |
|
rexpssxrxp |
⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) |
85 |
25 84
|
sstri |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) |
86 |
85 49
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ( ℝ* × ℝ* ) ) |
87 |
|
ioof |
⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ |
88 |
87
|
a1i |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ) |
89 |
88
|
feqmptd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → (,) = ( 𝑦 ∈ ( ℝ* × ℝ* ) ↦ ( (,) ‘ 𝑦 ) ) ) |
90 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) → ( (,) ‘ 𝑦 ) = ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) ) |
91 |
86 23 89 90
|
fmptco |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) = ( 𝑧 ∈ ℕ ↦ ( (,) ‘ ( 𝐾 ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ) ) ) |
92 |
83 91 18
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) = 𝐻 ) |
93 |
92
|
rneqd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ran ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) = ran 𝐻 ) |
94 |
93
|
unieqd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∪ ran ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) = ∪ ran 𝐻 ) |
95 |
|
fvex |
⊢ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ V |
96 |
95
|
inex1 |
⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ V |
97 |
11
|
fvmpt2 |
⊢ ( ( 𝑧 ∈ ℕ ∧ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ V ) → ( 𝐻 ‘ 𝑧 ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
98 |
96 97
|
mpan2 |
⊢ ( 𝑧 ∈ ℕ → ( 𝐻 ‘ 𝑧 ) = ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) |
99 |
|
incom |
⊢ ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) |
100 |
98 99
|
eqtrdi |
⊢ ( 𝑧 ∈ ℕ → ( 𝐻 ‘ 𝑧 ) = ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) |
101 |
100
|
iuneq2i |
⊢ ∪ 𝑧 ∈ ℕ ( 𝐻 ‘ 𝑧 ) = ∪ 𝑧 ∈ ℕ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) |
102 |
|
iunin2 |
⊢ ∪ 𝑧 ∈ ℕ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ ∪ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) |
103 |
101 102
|
eqtri |
⊢ ∪ 𝑧 ∈ ℕ ( 𝐻 ‘ 𝑧 ) = ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ ∪ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) |
104 |
17 11
|
fmptd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐻 : ℕ ⟶ ran (,) ) |
105 |
104
|
ffnd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐻 Fn ℕ ) |
106 |
|
fniunfv |
⊢ ( 𝐻 Fn ℕ → ∪ 𝑧 ∈ ℕ ( 𝐻 ‘ 𝑧 ) = ∪ ran 𝐻 ) |
107 |
105 106
|
syl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∪ 𝑧 ∈ ℕ ( 𝐻 ‘ 𝑧 ) = ∪ ran 𝐻 ) |
108 |
103 107
|
eqtr3id |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ ∪ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) = ∪ ran 𝐻 ) |
109 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
110 |
|
fvco3 |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) |
111 |
109 110
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) |
112 |
111
|
iuneq2dv |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∪ 𝑧 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ∪ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) |
113 |
|
ffn |
⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) ) |
114 |
87 113
|
ax-mp |
⊢ (,) Fn ( ℝ* × ℝ* ) |
115 |
|
fss |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) |
116 |
109 85 115
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) |
117 |
|
fnfco |
⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐹 ) Fn ℕ ) |
118 |
114 116 117
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ∘ 𝐹 ) Fn ℕ ) |
119 |
|
fniunfv |
⊢ ( ( (,) ∘ 𝐹 ) Fn ℕ → ∪ 𝑧 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ∪ ran ( (,) ∘ 𝐹 ) ) |
120 |
118 119
|
syl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∪ 𝑧 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = ∪ ran ( (,) ∘ 𝐹 ) ) |
121 |
120 4
|
eqtr4di |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∪ 𝑧 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑧 ) = 𝐴 ) |
122 |
112 121
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∪ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) = 𝐴 ) |
123 |
122
|
ineq2d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ ∪ 𝑧 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) |
124 |
94 108 123
|
3eqtr2d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∪ ran ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) = ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) |
125 |
124
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ‘ ∪ ran ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) ) = ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) ) |
126 |
82 125
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) = ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) ) |
127 |
|
inss1 |
⊢ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) |
128 |
|
ovolsscl |
⊢ ( ( ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∧ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ℝ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) ∈ ℝ ) |
129 |
127 34 44 128
|
mp3an2i |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) ∈ ℝ ) |
130 |
126 129
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) ∈ ℝ ) |
131 |
51 14
|
ovolsf |
⊢ ( ( 𝐾 ∘ 𝐻 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
132 |
50 131
|
syl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
133 |
132
|
frnd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ⊆ ( 0 [,) +∞ ) ) |
134 |
|
icossxr |
⊢ ( 0 [,) +∞ ) ⊆ ℝ* |
135 |
133 134
|
sstrdi |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ⊆ ℝ* ) |
136 |
132
|
ffnd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) Fn ℕ ) |
137 |
|
fnfvelrn |
⊢ ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) Fn ℕ ∧ 𝑦 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ) |
138 |
136 137
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑦 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ) |
139 |
|
supxrub |
⊢ ( ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ⊆ ℝ* ∧ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) ) |
140 |
135 138 139
|
syl2an2r |
⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑦 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) ) |
141 |
140
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) ) |
142 |
|
brralrspcev |
⊢ ( ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) |
143 |
130 141 142
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) |
144 |
13 14 15 16 57 58 143
|
isumsup2 |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ⇝ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ , < ) ) |
145 |
51
|
ovolfs2 |
⊢ ( ( 𝐾 ∘ 𝐻 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) = ( ( vol* ∘ (,) ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) |
146 |
50 145
|
syl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) = ( ( vol* ∘ (,) ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) |
147 |
|
coass |
⊢ ( ( vol* ∘ (,) ) ∘ ( 𝐾 ∘ 𝐻 ) ) = ( vol* ∘ ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) ) |
148 |
92
|
coeq2d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( vol* ∘ ( (,) ∘ ( 𝐾 ∘ 𝐻 ) ) ) = ( vol* ∘ 𝐻 ) ) |
149 |
147 148
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( vol* ∘ (,) ) ∘ ( 𝐾 ∘ 𝐻 ) ) = ( vol* ∘ 𝐻 ) ) |
150 |
146 149
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) = ( vol* ∘ 𝐻 ) ) |
151 |
150
|
seqeq3d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) = seq 1 ( + , ( vol* ∘ 𝐻 ) ) ) |
152 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
153 |
133 152
|
sstrdi |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ⊆ ℝ ) |
154 |
|
1nn |
⊢ 1 ∈ ℕ |
155 |
132
|
fdmd |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) = ℕ ) |
156 |
154 155
|
eleqtrrid |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 1 ∈ dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ) |
157 |
156
|
ne0d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ≠ ∅ ) |
158 |
|
dm0rn0 |
⊢ ( dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) = ∅ ↔ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) = ∅ ) |
159 |
158
|
necon3bii |
⊢ ( dom seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ≠ ∅ ↔ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ≠ ∅ ) |
160 |
157 159
|
sylib |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ≠ ∅ ) |
161 |
|
breq1 |
⊢ ( 𝑧 = ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) → ( 𝑧 ≤ 𝑥 ↔ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) ) |
162 |
161
|
ralrn |
⊢ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) ) |
163 |
136 162
|
syl |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) ) |
164 |
163
|
rexbidv |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ‘ 𝑦 ) ≤ 𝑥 ) ) |
165 |
143 164
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) 𝑧 ≤ 𝑥 ) |
166 |
|
supxrre |
⊢ ( ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) 𝑧 ≤ 𝑥 ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ , < ) ) |
167 |
153 160 165 166
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ , < ) ) |
168 |
167 126
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐾 ∘ 𝐻 ) ) ) , ℝ , < ) = ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) ) |
169 |
144 151 168
|
3brtr3d |
⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → seq 1 ( + , ( vol* ∘ 𝐻 ) ) ⇝ ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ∩ 𝐴 ) ) ) |