Step |
Hyp |
Ref |
Expression |
1 |
|
ioombl1.b |
⊢ 𝐵 = ( 𝐴 (,) +∞ ) |
2 |
|
ioombl1.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
3 |
|
ioombl1.e |
⊢ ( 𝜑 → 𝐸 ⊆ ℝ ) |
4 |
|
ioombl1.v |
⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ ) |
5 |
|
ioombl1.c |
⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) |
6 |
|
ioombl1.s |
⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) |
7 |
|
ioombl1.t |
⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) |
8 |
|
ioombl1.u |
⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) |
9 |
|
ioombl1.f1 |
⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
10 |
|
ioombl1.f2 |
⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) |
11 |
|
ioombl1.f3 |
⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) ) |
12 |
|
ioombl1.p |
⊢ 𝑃 = ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) |
13 |
|
ioombl1.q |
⊢ 𝑄 = ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) |
14 |
|
ioombl1.g |
⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) |
15 |
|
ioombl1.h |
⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) |
16 |
|
inss1 |
⊢ ( 𝐸 ∩ 𝐵 ) ⊆ 𝐸 |
17 |
|
ovolsscl |
⊢ ( ( ( 𝐸 ∩ 𝐵 ) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ∈ ℝ ) |
18 |
16 3 4 17
|
mp3an2i |
⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ∈ ℝ ) |
19 |
|
difss |
⊢ ( 𝐸 ∖ 𝐵 ) ⊆ 𝐸 |
20 |
|
ovolsscl |
⊢ ( ( ( 𝐸 ∖ 𝐵 ) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ∈ ℝ ) |
21 |
19 3 4 20
|
mp3an2i |
⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ∈ ℝ ) |
22 |
18 21
|
readdcld |
⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ∈ ℝ ) |
23 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
ioombl1lem2 |
⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) |
24 |
5
|
rpred |
⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
25 |
4 24
|
readdcld |
⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ ) |
26 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
ioombl1lem1 |
⊢ ( 𝜑 → ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ) |
27 |
26
|
simpld |
⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
28 |
|
eqid |
⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 ) |
29 |
28 7
|
ovolsf |
⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) ) |
30 |
27 29
|
syl |
⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) ) |
31 |
30
|
frnd |
⊢ ( 𝜑 → ran 𝑇 ⊆ ( 0 [,) +∞ ) ) |
32 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
33 |
31 32
|
sstrdi |
⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ ) |
34 |
|
1nn |
⊢ 1 ∈ ℕ |
35 |
30
|
fdmd |
⊢ ( 𝜑 → dom 𝑇 = ℕ ) |
36 |
34 35
|
eleqtrrid |
⊢ ( 𝜑 → 1 ∈ dom 𝑇 ) |
37 |
36
|
ne0d |
⊢ ( 𝜑 → dom 𝑇 ≠ ∅ ) |
38 |
|
dm0rn0 |
⊢ ( dom 𝑇 = ∅ ↔ ran 𝑇 = ∅ ) |
39 |
38
|
necon3bii |
⊢ ( dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅ ) |
40 |
37 39
|
sylib |
⊢ ( 𝜑 → ran 𝑇 ≠ ∅ ) |
41 |
30
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) ) |
42 |
32 41
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ∈ ℝ ) |
43 |
|
eqid |
⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 ) |
44 |
43 6
|
ovolsf |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) ) |
45 |
9 44
|
syl |
⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) ) |
46 |
45
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑆 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) ) |
47 |
32 46
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) |
48 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) |
49 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ ) |
50 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
51 |
49 50
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) ) |
52 |
|
simpl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝜑 ) |
53 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℕ ) |
54 |
28
|
ovolfsf |
⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
55 |
27 54
|
syl |
⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
56 |
55
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ) |
57 |
32 56
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℝ ) |
58 |
52 53 57
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℝ ) |
59 |
43
|
ovolfsf |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
60 |
9 59
|
syl |
⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
61 |
60
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ) |
62 |
|
elrege0 |
⊢ ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) ) |
63 |
61 62
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) ) |
64 |
63
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ ) |
65 |
52 53 64
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ ) |
66 |
26
|
simprd |
⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
67 |
|
eqid |
⊢ ( ( abs ∘ − ) ∘ 𝐻 ) = ( ( abs ∘ − ) ∘ 𝐻 ) |
68 |
67
|
ovolfsf |
⊢ ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐻 ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
69 |
66 68
|
syl |
⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐻 ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
70 |
69
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ) |
71 |
|
elrege0 |
⊢ ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) |
72 |
70 71
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) |
73 |
72
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) |
74 |
72
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℝ ) |
75 |
57 74
|
addge01d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ↔ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ≤ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) ) |
76 |
73 75
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ≤ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) |
77 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
ioombl1lem3 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) |
78 |
76 77
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) |
79 |
52 53 78
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) |
80 |
51 58 65 79
|
serle |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑗 ) ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) ) |
81 |
7
|
fveq1i |
⊢ ( 𝑇 ‘ 𝑗 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑗 ) |
82 |
6
|
fveq1i |
⊢ ( 𝑆 ‘ 𝑗 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) |
83 |
80 81 82
|
3brtr4g |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑗 ) ) |
84 |
|
1zzd |
⊢ ( 𝜑 → 1 ∈ ℤ ) |
85 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) |
86 |
63
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) |
87 |
45
|
frnd |
⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) ) |
88 |
|
icossxr |
⊢ ( 0 [,) +∞ ) ⊆ ℝ* |
89 |
87 88
|
sstrdi |
⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ* ) |
90 |
89
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran 𝑆 ⊆ ℝ* ) |
91 |
45
|
ffnd |
⊢ ( 𝜑 → 𝑆 Fn ℕ ) |
92 |
|
fnfvelrn |
⊢ ( ( 𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ran 𝑆 ) |
93 |
91 92
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ran 𝑆 ) |
94 |
|
supxrub |
⊢ ( ( ran 𝑆 ⊆ ℝ* ∧ ( 𝑆 ‘ 𝑘 ) ∈ ran 𝑆 ) → ( 𝑆 ‘ 𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
95 |
90 93 94
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
96 |
95
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
97 |
|
brralrspcev |
⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) |
98 |
23 96 97
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) |
99 |
50 6 84 85 64 86 98
|
isumsup2 |
⊢ ( 𝜑 → 𝑆 ⇝ sup ( ran 𝑆 , ℝ , < ) ) |
100 |
87 32
|
sstrdi |
⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ ) |
101 |
45
|
fdmd |
⊢ ( 𝜑 → dom 𝑆 = ℕ ) |
102 |
34 101
|
eleqtrrid |
⊢ ( 𝜑 → 1 ∈ dom 𝑆 ) |
103 |
102
|
ne0d |
⊢ ( 𝜑 → dom 𝑆 ≠ ∅ ) |
104 |
|
dm0rn0 |
⊢ ( dom 𝑆 = ∅ ↔ ran 𝑆 = ∅ ) |
105 |
104
|
necon3bii |
⊢ ( dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅ ) |
106 |
103 105
|
sylib |
⊢ ( 𝜑 → ran 𝑆 ≠ ∅ ) |
107 |
|
breq1 |
⊢ ( 𝑧 = ( 𝑆 ‘ 𝑘 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) ) |
108 |
107
|
ralrn |
⊢ ( 𝑆 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) ) |
109 |
91 108
|
syl |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) ) |
110 |
109
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) ) |
111 |
98 110
|
mpbird |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ) |
112 |
|
supxrre |
⊢ ( ( ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ) → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran 𝑆 , ℝ , < ) ) |
113 |
100 106 111 112
|
syl3anc |
⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran 𝑆 , ℝ , < ) ) |
114 |
99 113
|
breqtrrd |
⊢ ( 𝜑 → 𝑆 ⇝ sup ( ran 𝑆 , ℝ* , < ) ) |
115 |
114
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑆 ⇝ sup ( ran 𝑆 , ℝ* , < ) ) |
116 |
6 115
|
eqbrtrrid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ⇝ sup ( ran 𝑆 , ℝ* , < ) ) |
117 |
64
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ ) |
118 |
86
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) |
119 |
50 49 116 117 118
|
climserle |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
120 |
82 119
|
eqbrtrid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑆 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
121 |
42 47 48 83 120
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
122 |
121
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
123 |
|
brralrspcev |
⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) |
124 |
23 122 123
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) |
125 |
30
|
ffnd |
⊢ ( 𝜑 → 𝑇 Fn ℕ ) |
126 |
|
breq1 |
⊢ ( 𝑧 = ( 𝑇 ‘ 𝑗 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) ) |
127 |
126
|
ralrn |
⊢ ( 𝑇 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) ) |
128 |
125 127
|
syl |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) ) |
129 |
128
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) ) |
130 |
124 129
|
mpbird |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ) |
131 |
33 40 130
|
suprcld |
⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ , < ) ∈ ℝ ) |
132 |
67 8
|
ovolsf |
⊢ ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) ) |
133 |
66 132
|
syl |
⊢ ( 𝜑 → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) ) |
134 |
133
|
frnd |
⊢ ( 𝜑 → ran 𝑈 ⊆ ( 0 [,) +∞ ) ) |
135 |
134 32
|
sstrdi |
⊢ ( 𝜑 → ran 𝑈 ⊆ ℝ ) |
136 |
133
|
fdmd |
⊢ ( 𝜑 → dom 𝑈 = ℕ ) |
137 |
34 136
|
eleqtrrid |
⊢ ( 𝜑 → 1 ∈ dom 𝑈 ) |
138 |
137
|
ne0d |
⊢ ( 𝜑 → dom 𝑈 ≠ ∅ ) |
139 |
|
dm0rn0 |
⊢ ( dom 𝑈 = ∅ ↔ ran 𝑈 = ∅ ) |
140 |
139
|
necon3bii |
⊢ ( dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅ ) |
141 |
138 140
|
sylib |
⊢ ( 𝜑 → ran 𝑈 ≠ ∅ ) |
142 |
133
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) ) |
143 |
32 142
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ∈ ℝ ) |
144 |
52 53 74
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℝ ) |
145 |
|
elrege0 |
⊢ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ) ) |
146 |
56 145
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ) ) |
147 |
146
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ) |
148 |
74 57
|
addge02d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ↔ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ≤ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) ) |
149 |
147 148
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ≤ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) |
150 |
149 77
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) |
151 |
52 53 150
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) |
152 |
51 144 65 151
|
serle |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑗 ) ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) ) |
153 |
8
|
fveq1i |
⊢ ( 𝑈 ‘ 𝑗 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑗 ) |
154 |
152 153 82
|
3brtr4g |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑗 ) ) |
155 |
143 47 48 154 120
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
156 |
155
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
157 |
|
brralrspcev |
⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) |
158 |
23 156 157
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) |
159 |
133
|
ffnd |
⊢ ( 𝜑 → 𝑈 Fn ℕ ) |
160 |
|
breq1 |
⊢ ( 𝑧 = ( 𝑈 ‘ 𝑗 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) ) |
161 |
160
|
ralrn |
⊢ ( 𝑈 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) ) |
162 |
159 161
|
syl |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) ) |
163 |
162
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) ) |
164 |
158 163
|
mpbird |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ) |
165 |
135 141 164
|
suprcld |
⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ , < ) ∈ ℝ ) |
166 |
|
ssralv |
⊢ ( ( 𝐸 ∩ 𝐵 ) ⊆ 𝐸 → ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
167 |
16 166
|
ax-mp |
⊢ ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
168 |
12
|
breq1i |
⊢ ( 𝑃 < 𝑥 ↔ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ) |
169 |
|
ovolfcl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
170 |
9 169
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
171 |
170
|
simp1d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ) |
172 |
12 171
|
eqeltrid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℝ ) |
173 |
172
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℝ ) |
174 |
16 3
|
sstrid |
⊢ ( 𝜑 → ( 𝐸 ∩ 𝐵 ) ⊆ ℝ ) |
175 |
174
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) → 𝑥 ∈ ℝ ) |
176 |
175
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ ) |
177 |
|
ltle |
⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑃 < 𝑥 → 𝑃 ≤ 𝑥 ) ) |
178 |
173 176 177
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 < 𝑥 → 𝑃 ≤ 𝑥 ) ) |
179 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ ) |
180 |
|
opex |
⊢ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ∈ V |
181 |
14
|
fvmpt2 |
⊢ ( ( 𝑛 ∈ ℕ ∧ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ∈ V ) → ( 𝐺 ‘ 𝑛 ) = 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) |
182 |
179 180 181
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) |
183 |
182
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 1st ‘ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) ) |
184 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ ) |
185 |
184 172
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ ) |
186 |
170
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ) |
187 |
13 186
|
eqeltrid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℝ ) |
188 |
185 187
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ) |
189 |
|
op1stg |
⊢ ( ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( 1st ‘ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
190 |
188 187 189
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
191 |
183 190
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
192 |
191
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
193 |
188
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ) |
194 |
185
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ ) |
195 |
174
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → ( 𝐸 ∩ 𝐵 ) ⊆ ℝ ) |
196 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) |
197 |
195 196
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ ) |
198 |
187
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑄 ∈ ℝ ) |
199 |
|
min1 |
⊢ ( ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ) |
200 |
194 198 199
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ) |
201 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝐴 ∈ ℝ ) |
202 |
|
elinel2 |
⊢ ( 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) → 𝑥 ∈ 𝐵 ) |
203 |
202
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑥 ∈ 𝐵 ) |
204 |
2
|
rexrd |
⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) |
205 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
206 |
|
elioo2 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ) ) |
207 |
204 205 206
|
sylancl |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ) ) |
208 |
1
|
eleq2i |
⊢ ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) |
209 |
|
ltpnf |
⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ ) |
210 |
209
|
adantr |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) → 𝑥 < +∞ ) |
211 |
210
|
pm4.71i |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ∧ 𝑥 < +∞ ) ) |
212 |
|
df-3an |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ∧ 𝑥 < +∞ ) ) |
213 |
211 212
|
bitr4i |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ) |
214 |
207 208 213
|
3bitr4g |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ) ) |
215 |
|
simpr |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) → 𝐴 < 𝑥 ) |
216 |
214 215
|
syl6bi |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝐴 < 𝑥 ) ) |
217 |
216
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → ( 𝑥 ∈ 𝐵 → 𝐴 < 𝑥 ) ) |
218 |
203 217
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝐴 < 𝑥 ) |
219 |
201 197 218
|
ltled |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝐴 ≤ 𝑥 ) |
220 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑃 ≤ 𝑥 ) |
221 |
|
breq1 |
⊢ ( 𝐴 = if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) → ( 𝐴 ≤ 𝑥 ↔ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑥 ) ) |
222 |
|
breq1 |
⊢ ( 𝑃 = if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) → ( 𝑃 ≤ 𝑥 ↔ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑥 ) ) |
223 |
221 222
|
ifboth |
⊢ ( ( 𝐴 ≤ 𝑥 ∧ 𝑃 ≤ 𝑥 ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑥 ) |
224 |
219 220 223
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑥 ) |
225 |
193 194 197 200 224
|
letrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ 𝑥 ) |
226 |
192 225
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ) |
227 |
226
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ≤ 𝑥 → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ) ) |
228 |
178 227
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 < 𝑥 → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ) ) |
229 |
168 228
|
syl5bir |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ) ) |
230 |
13
|
breq2i |
⊢ ( 𝑥 < 𝑄 ↔ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) |
231 |
187
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℝ ) |
232 |
|
ltle |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( 𝑥 < 𝑄 → 𝑥 ≤ 𝑄 ) ) |
233 |
176 231 232
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < 𝑄 → 𝑥 ≤ 𝑄 ) ) |
234 |
230 233
|
syl5bir |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ≤ 𝑄 ) ) |
235 |
182
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2nd ‘ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) ) |
236 |
|
op2ndg |
⊢ ( ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( 2nd ‘ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) = 𝑄 ) |
237 |
188 187 236
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ 〈 if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 〉 ) = 𝑄 ) |
238 |
235 237
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = 𝑄 ) |
239 |
238
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = 𝑄 ) |
240 |
239
|
breq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ 𝑥 ≤ 𝑄 ) ) |
241 |
234 240
|
sylibrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) |
242 |
229 241
|
anim12d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) |
243 |
242
|
reximdva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) |
244 |
243
|
ralimdva |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) |
245 |
167 244
|
syl5 |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) |
246 |
|
ovolfioo |
⊢ ( ( 𝐸 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
247 |
3 9 246
|
syl2anc |
⊢ ( 𝜑 → ( 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
248 |
|
ovolficc |
⊢ ( ( ( 𝐸 ∩ 𝐵 ) ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) |
249 |
174 27 248
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) |
250 |
245 247 249
|
3imtr4d |
⊢ ( 𝜑 → ( 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) → ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ) ) |
251 |
10 250
|
mpd |
⊢ ( 𝜑 → ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ) |
252 |
7
|
ovollb2 |
⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ) → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) |
253 |
27 251 252
|
syl2anc |
⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) |
254 |
|
supxrre |
⊢ ( ( ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ) → sup ( ran 𝑇 , ℝ* , < ) = sup ( ran 𝑇 , ℝ , < ) ) |
255 |
33 40 130 254
|
syl3anc |
⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) = sup ( ran 𝑇 , ℝ , < ) ) |
256 |
253 255
|
breqtrd |
⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ≤ sup ( ran 𝑇 , ℝ , < ) ) |
257 |
|
ssralv |
⊢ ( ( 𝐸 ∖ 𝐵 ) ⊆ 𝐸 → ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
258 |
19 257
|
ax-mp |
⊢ ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
259 |
172
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℝ ) |
260 |
19 3
|
sstrid |
⊢ ( 𝜑 → ( 𝐸 ∖ 𝐵 ) ⊆ ℝ ) |
261 |
260
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) → 𝑥 ∈ ℝ ) |
262 |
261
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ ) |
263 |
259 262 177
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 < 𝑥 → 𝑃 ≤ 𝑥 ) ) |
264 |
168 263
|
syl5bir |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 → 𝑃 ≤ 𝑥 ) ) |
265 |
|
opex |
⊢ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ∈ V |
266 |
15
|
fvmpt2 |
⊢ ( ( 𝑛 ∈ ℕ ∧ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ∈ V ) → ( 𝐻 ‘ 𝑛 ) = 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) |
267 |
179 265 266
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐻 ‘ 𝑛 ) = 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) |
268 |
267
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) = ( 1st ‘ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) ) |
269 |
|
op1stg |
⊢ ( ( 𝑃 ∈ ℝ ∧ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ) → ( 1st ‘ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) = 𝑃 ) |
270 |
172 188 269
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) = 𝑃 ) |
271 |
268 270
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) = 𝑃 ) |
272 |
271
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) = 𝑃 ) |
273 |
272
|
breq1d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ↔ 𝑃 ≤ 𝑥 ) ) |
274 |
264 273
|
sylibrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ) ) |
275 |
187
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℝ ) |
276 |
262 275 232
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < 𝑄 → 𝑥 ≤ 𝑄 ) ) |
277 |
260
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 𝐸 ∖ 𝐵 ) ⊆ ℝ ) |
278 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) |
279 |
277 278
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ∈ ℝ ) |
280 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝐴 ∈ ℝ ) |
281 |
172
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑃 ∈ ℝ ) |
282 |
280 281
|
ifcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ ) |
283 |
|
eldifn |
⊢ ( 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) → ¬ 𝑥 ∈ 𝐵 ) |
284 |
283
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ¬ 𝑥 ∈ 𝐵 ) |
285 |
279
|
biantrurd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 𝐴 < 𝑥 ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ) ) |
286 |
214
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ) ) |
287 |
285 286
|
bitr4d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 𝐴 < 𝑥 ↔ 𝑥 ∈ 𝐵 ) ) |
288 |
284 287
|
mtbird |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ¬ 𝐴 < 𝑥 ) |
289 |
279 280 288
|
nltled |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ 𝐴 ) |
290 |
|
max2 |
⊢ ( ( 𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝐴 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ) |
291 |
281 280 290
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝐴 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ) |
292 |
279 280 282 289 291
|
letrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ) |
293 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ 𝑄 ) |
294 |
|
breq2 |
⊢ ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) → ( 𝑥 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ↔ 𝑥 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) ) |
295 |
|
breq2 |
⊢ ( 𝑄 = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) → ( 𝑥 ≤ 𝑄 ↔ 𝑥 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) ) |
296 |
294 295
|
ifboth |
⊢ ( ( 𝑥 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∧ 𝑥 ≤ 𝑄 ) → 𝑥 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
297 |
292 293 296
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
298 |
267
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) = ( 2nd ‘ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) ) |
299 |
|
op2ndg |
⊢ ( ( 𝑃 ∈ ℝ ∧ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ) → ( 2nd ‘ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
300 |
172 188 299
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ 〈 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) 〉 ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
301 |
298 300
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
302 |
301
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) |
303 |
297 302
|
breqtrrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) |
304 |
303
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ≤ 𝑄 → 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) |
305 |
276 304
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < 𝑄 → 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) |
306 |
230 305
|
syl5bir |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) |
307 |
274 306
|
anim12d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) ) |
308 |
307
|
reximdva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) ) |
309 |
308
|
ralimdva |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) ) |
310 |
258 309
|
syl5 |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) ) |
311 |
|
ovolficc |
⊢ ( ( ( 𝐸 ∖ 𝐵 ) ⊆ ℝ ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ↔ ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) ) |
312 |
260 66 311
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ↔ ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) ) |
313 |
310 247 312
|
3imtr4d |
⊢ ( 𝜑 → ( 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) → ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ) ) |
314 |
10 313
|
mpd |
⊢ ( 𝜑 → ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ) |
315 |
8
|
ovollb2 |
⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ) → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ* , < ) ) |
316 |
66 314 315
|
syl2anc |
⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ* , < ) ) |
317 |
|
supxrre |
⊢ ( ( ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ) → sup ( ran 𝑈 , ℝ* , < ) = sup ( ran 𝑈 , ℝ , < ) ) |
318 |
135 141 164 317
|
syl3anc |
⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ* , < ) = sup ( ran 𝑈 , ℝ , < ) ) |
319 |
316 318
|
breqtrd |
⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ , < ) ) |
320 |
18 21 131 165 256 319
|
le2addd |
⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ≤ ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) ) |
321 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ) |
322 |
50 7 84 321 57 147 124
|
isumsup2 |
⊢ ( 𝜑 → 𝑇 ⇝ sup ( ran 𝑇 , ℝ , < ) ) |
323 |
|
seqex |
⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ∈ V |
324 |
6 323
|
eqeltri |
⊢ 𝑆 ∈ V |
325 |
324
|
a1i |
⊢ ( 𝜑 → 𝑆 ∈ V ) |
326 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) |
327 |
50 8 84 326 74 73 158
|
isumsup2 |
⊢ ( 𝜑 → 𝑈 ⇝ sup ( ran 𝑈 , ℝ , < ) ) |
328 |
42
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ∈ ℂ ) |
329 |
143
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ∈ ℂ ) |
330 |
57
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℂ ) |
331 |
52 53 330
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℂ ) |
332 |
74
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℂ ) |
333 |
52 53 332
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℂ ) |
334 |
77
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) |
335 |
52 53 334
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) |
336 |
51 331 333 335
|
seradd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑗 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑗 ) ) ) |
337 |
81 153
|
oveq12i |
⊢ ( ( 𝑇 ‘ 𝑗 ) + ( 𝑈 ‘ 𝑗 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑗 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑗 ) ) |
338 |
336 82 337
|
3eqtr4g |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑆 ‘ 𝑗 ) = ( ( 𝑇 ‘ 𝑗 ) + ( 𝑈 ‘ 𝑗 ) ) ) |
339 |
50 84 322 325 327 328 329 338
|
climadd |
⊢ ( 𝜑 → 𝑆 ⇝ ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) ) |
340 |
|
climuni |
⊢ ( ( 𝑆 ⇝ ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) ∧ 𝑆 ⇝ sup ( ran 𝑆 , ℝ* , < ) ) → ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) = sup ( ran 𝑆 , ℝ* , < ) ) |
341 |
339 114 340
|
syl2anc |
⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) = sup ( ran 𝑆 , ℝ* , < ) ) |
342 |
320 341
|
breqtrd |
⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) |
343 |
22 23 25 342 11
|
letrd |
⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) ) |