Step |
Hyp |
Ref |
Expression |
1 |
|
hoidmv1lelem1.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
2 |
|
hoidmv1lelem1.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
3 |
|
hoidmv1lelem1.l |
⊢ ( 𝜑 → 𝐴 < 𝐵 ) |
4 |
|
hoidmv1lelem1.c |
⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ℝ ) |
5 |
|
hoidmv1lelem1.d |
⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ℝ ) |
6 |
|
hoidmv1lelem1.r |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ ) |
7 |
|
hoidmv1lelem1.u |
⊢ 𝑈 = { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } |
8 |
|
hoidmv1lelem1.s |
⊢ 𝑆 = sup ( 𝑈 , ℝ , < ) |
9 |
|
ssrab2 |
⊢ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ⊆ ( 𝐴 [,] 𝐵 ) |
10 |
7 9
|
eqsstri |
⊢ 𝑈 ⊆ ( 𝐴 [,] 𝐵 ) |
11 |
10
|
a1i |
⊢ ( 𝜑 → 𝑈 ⊆ ( 𝐴 [,] 𝐵 ) ) |
12 |
1
|
rexrd |
⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) |
13 |
2
|
rexrd |
⊢ ( 𝜑 → 𝐵 ∈ ℝ* ) |
14 |
1 2 3
|
ltled |
⊢ ( 𝜑 → 𝐴 ≤ 𝐵 ) |
15 |
|
lbicc2 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ) |
16 |
12 13 14 15
|
syl3anc |
⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ) |
17 |
1
|
recnd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
18 |
17
|
subidd |
⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = 0 ) |
19 |
|
nfv |
⊢ Ⅎ 𝑗 𝜑 |
20 |
|
nnex |
⊢ ℕ ∈ V |
21 |
20
|
a1i |
⊢ ( 𝜑 → ℕ ∈ V ) |
22 |
|
volf |
⊢ vol : dom vol ⟶ ( 0 [,] +∞ ) |
23 |
22
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → vol : dom vol ⟶ ( 0 [,] +∞ ) ) |
24 |
4
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ ) |
25 |
5
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ ) |
26 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐴 ∈ ℝ ) |
27 |
25 26
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ∈ ℝ ) |
28 |
27
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ∈ ℝ* ) |
29 |
|
icombl |
⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ∈ dom vol ) |
30 |
24 28 29
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ∈ dom vol ) |
31 |
23 30
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ∈ ( 0 [,] +∞ ) ) |
32 |
19 21 31
|
sge0ge0mpt |
⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ) ) ) |
33 |
18 32
|
eqbrtrd |
⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ) ) ) |
34 |
16 33
|
jca |
⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐴 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ) ) ) ) |
35 |
|
oveq1 |
⊢ ( 𝑧 = 𝐴 → ( 𝑧 − 𝐴 ) = ( 𝐴 − 𝐴 ) ) |
36 |
|
breq2 |
⊢ ( 𝑧 = 𝐴 → ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ↔ ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 ) ) |
37 |
|
id |
⊢ ( 𝑧 = 𝐴 → 𝑧 = 𝐴 ) |
38 |
36 37
|
ifbieq2d |
⊢ ( 𝑧 = 𝐴 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) |
39 |
38
|
oveq2d |
⊢ ( 𝑧 = 𝐴 → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) |
40 |
39
|
fveq2d |
⊢ ( 𝑧 = 𝐴 → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ) |
41 |
40
|
mpteq2dv |
⊢ ( 𝑧 = 𝐴 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ) ) |
42 |
41
|
fveq2d |
⊢ ( 𝑧 = 𝐴 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ) ) ) |
43 |
35 42
|
breq12d |
⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ ( 𝐴 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ) ) ) ) |
44 |
43
|
elrab |
⊢ ( 𝐴 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ↔ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐴 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐴 , ( 𝐷 ‘ 𝑗 ) , 𝐴 ) ) ) ) ) ) ) |
45 |
34 44
|
sylibr |
⊢ ( 𝜑 → 𝐴 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ) |
46 |
45 7
|
eleqtrrdi |
⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) |
47 |
46
|
ne0d |
⊢ ( 𝜑 → 𝑈 ≠ ∅ ) |
48 |
1 2 11 47
|
supicc |
⊢ ( 𝜑 → sup ( 𝑈 , ℝ , < ) ∈ ( 𝐴 [,] 𝐵 ) ) |
49 |
8 48
|
eqeltrid |
⊢ ( 𝜑 → 𝑆 ∈ ( 𝐴 [,] 𝐵 ) ) |
50 |
8
|
a1i |
⊢ ( 𝜑 → 𝑆 = sup ( 𝑈 , ℝ , < ) ) |
51 |
|
nfv |
⊢ Ⅎ 𝑧 𝜑 |
52 |
1 2
|
iccssred |
⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
53 |
11 52
|
sstrd |
⊢ ( 𝜑 → 𝑈 ⊆ ℝ ) |
54 |
53
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ℝ ) |
55 |
|
nfv |
⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) |
56 |
20
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ℕ ∈ V ) |
57 |
22
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → vol : dom vol ⟶ ( 0 [,] +∞ ) ) |
58 |
24
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ ) |
59 |
25
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ ) |
60 |
54
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑧 ∈ ℝ ) |
61 |
59 60
|
ifcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ∈ ℝ ) |
62 |
61
|
rexrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ∈ ℝ* ) |
63 |
|
icombl |
⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ∈ dom vol ) |
64 |
58 62 63
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ∈ dom vol ) |
65 |
57 64
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) ) |
66 |
55 56 65
|
sge0xrclmpt |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ∈ ℝ* ) |
67 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
68 |
67
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → +∞ ∈ ℝ* ) |
69 |
6
|
rexrd |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* ) |
70 |
69
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* ) |
71 |
25
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) |
72 |
|
icombl |
⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol ) |
73 |
24 71 72
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol ) |
74 |
23 73
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) ) |
75 |
74
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) ) |
76 |
73
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol ) |
77 |
24
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ) |
78 |
77
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ) |
79 |
71
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) |
80 |
24
|
leidd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ) |
81 |
80
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ) |
82 |
|
min1 |
⊢ ( ( ( 𝐷 ‘ 𝑗 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ ( 𝐷 ‘ 𝑗 ) ) |
83 |
59 60 82
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ ( 𝐷 ‘ 𝑗 ) ) |
84 |
|
icossico |
⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) ∧ ( ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ ( 𝐷 ‘ 𝑗 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) |
85 |
78 79 81 83 84
|
syl22anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) |
86 |
|
volss |
⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) |
87 |
64 76 85 86
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) |
88 |
55 56 65 75 87
|
sge0lempt |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) |
89 |
6
|
ltpnfd |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ ) |
90 |
89
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ ) |
91 |
66 70 68 88 90
|
xrlelttrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) < +∞ ) |
92 |
66 68 91
|
xrltned |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ≠ +∞ ) |
93 |
92
|
neneqd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = +∞ ) |
94 |
|
eqid |
⊢ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) |
95 |
65 94
|
fmptd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) ) |
96 |
56 95
|
sge0repnf |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = +∞ ) ) |
97 |
93 96
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ∈ ℝ ) |
98 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝐴 ∈ ℝ ) |
99 |
97 98
|
readdcld |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) + 𝐴 ) ∈ ℝ ) |
100 |
52 49
|
sseldd |
⊢ ( 𝜑 → 𝑆 ∈ ℝ ) |
101 |
100
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑆 ∈ ℝ ) |
102 |
25 101
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ ) |
103 |
102
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ* ) |
104 |
|
icombl |
⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol ) |
105 |
24 103 104
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol ) |
106 |
23 105
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ∈ ( 0 [,] +∞ ) ) |
107 |
19 21 106
|
sge0xrclmpt |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ* ) |
108 |
67
|
a1i |
⊢ ( 𝜑 → +∞ ∈ ℝ* ) |
109 |
|
min1 |
⊢ ( ( ( 𝐷 ‘ 𝑗 ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ ( 𝐷 ‘ 𝑗 ) ) |
110 |
25 101 109
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ ( 𝐷 ‘ 𝑗 ) ) |
111 |
|
icossico |
⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) ∧ ( ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ ( 𝐷 ‘ 𝑗 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) |
112 |
77 71 80 110 111
|
syl22anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) |
113 |
|
volss |
⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) |
114 |
105 73 112 113
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) |
115 |
19 21 106 74 114
|
sge0lempt |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) |
116 |
107 69 108 115 89
|
xrlelttrd |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) < +∞ ) |
117 |
107 108 116
|
xrltned |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ≠ +∞ ) |
118 |
117
|
neneqd |
⊢ ( 𝜑 → ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) = +∞ ) |
119 |
|
eqid |
⊢ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) |
120 |
106 119
|
fmptd |
⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) ) |
121 |
21 120
|
sge0repnf |
⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) = +∞ ) ) |
122 |
118 121
|
mpbird |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ ) |
123 |
122 1
|
readdcld |
⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ∈ ℝ ) |
124 |
123
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ∈ ℝ ) |
125 |
7
|
eleq2i |
⊢ ( 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ) |
126 |
125
|
biimpi |
⊢ ( 𝑧 ∈ 𝑈 → 𝑧 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ) |
127 |
126
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ) |
128 |
|
rabid |
⊢ ( 𝑧 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ↔ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ) ) |
129 |
127 128
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ) ) |
130 |
129
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ) |
131 |
54 98 97
|
lesubaddd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) + 𝐴 ) ) ) |
132 |
130 131
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) + 𝐴 ) ) |
133 |
122
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ ) |
134 |
106
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ∈ ( 0 [,] +∞ ) ) |
135 |
105
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol ) |
136 |
103
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ* ) |
137 |
61
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ∈ ℝ ) |
138 |
|
eqidd |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑗 ) ) |
139 |
|
iftrue |
⊢ ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = ( 𝐷 ‘ 𝑗 ) ) |
140 |
139
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = ( 𝐷 ‘ 𝑗 ) ) |
141 |
59
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ ) |
142 |
60
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 ∈ ℝ ) |
143 |
100
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑆 ∈ ℝ ) |
144 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) |
145 |
53
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑈 ⊆ ℝ ) |
146 |
47
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑈 ≠ ∅ ) |
147 |
1 2
|
jca |
⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) |
148 |
|
iccsupr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑈 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ) |
149 |
147 11 46 148
|
syl3anc |
⊢ ( 𝜑 → ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ) |
150 |
149
|
simp3d |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) |
151 |
150
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) |
152 |
127 125
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑈 ) |
153 |
|
suprub |
⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ sup ( 𝑈 , ℝ , < ) ) |
154 |
145 146 151 152 153
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ sup ( 𝑈 , ℝ , < ) ) |
155 |
154 8
|
breqtrrdi |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ 𝑆 ) |
156 |
155
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 ≤ 𝑆 ) |
157 |
141 142 143 144 156
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) |
158 |
157
|
iftrued |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = ( 𝐷 ‘ 𝑗 ) ) |
159 |
138 140 158
|
3eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) |
160 |
137 159
|
eqled |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) |
161 |
60
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 ∈ ℝ ) |
162 |
59
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ ) |
163 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) |
164 |
161 162
|
ltnled |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝑧 < ( 𝐷 ‘ 𝑗 ) ↔ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ) |
165 |
163 164
|
mpbird |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 < ( 𝐷 ‘ 𝑗 ) ) |
166 |
161 162 165
|
ltled |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 ≤ ( 𝐷 ‘ 𝑗 ) ) |
167 |
166
|
adantr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑧 ≤ ( 𝐷 ‘ 𝑗 ) ) |
168 |
|
iffalse |
⊢ ( ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = 𝑧 ) |
169 |
168
|
ad2antlr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = 𝑧 ) |
170 |
|
iftrue |
⊢ ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = ( 𝐷 ‘ 𝑗 ) ) |
171 |
170
|
adantl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = ( 𝐷 ‘ 𝑗 ) ) |
172 |
169 171
|
breq12d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ↔ 𝑧 ≤ ( 𝐷 ‘ 𝑗 ) ) ) |
173 |
167 172
|
mpbird |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) |
174 |
155
|
ad3antrrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑧 ≤ 𝑆 ) |
175 |
168
|
ad2antlr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = 𝑧 ) |
176 |
|
iffalse |
⊢ ( ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = 𝑆 ) |
177 |
176
|
adantl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = 𝑆 ) |
178 |
175 177
|
breq12d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ↔ 𝑧 ≤ 𝑆 ) ) |
179 |
174 178
|
mpbird |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) |
180 |
173 179
|
pm2.61dan |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) |
181 |
160 180
|
pm2.61dan |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) |
182 |
|
icossico |
⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ* ) ∧ ( ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) |
183 |
78 136 81 181 182
|
syl22anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) |
184 |
|
volss |
⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) |
185 |
64 135 183 184
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) |
186 |
55 56 65 134 185
|
sge0lempt |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) |
187 |
97 133 98 186
|
leadd1dd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) + 𝐴 ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) |
188 |
54 99 124 132 187
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) |
189 |
188
|
ex |
⊢ ( 𝜑 → ( 𝑧 ∈ 𝑈 → 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) ) |
190 |
51 189
|
ralrimi |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑈 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) |
191 |
|
suprleub |
⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ∧ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ∈ ℝ ) → ( sup ( 𝑈 , ℝ , < ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ↔ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) ) |
192 |
53 47 150 123 191
|
syl31anc |
⊢ ( 𝜑 → ( sup ( 𝑈 , ℝ , < ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ↔ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) ) |
193 |
190 192
|
mpbird |
⊢ ( 𝜑 → sup ( 𝑈 , ℝ , < ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) |
194 |
50 193
|
eqbrtrd |
⊢ ( 𝜑 → 𝑆 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) |
195 |
100 1 122
|
lesubaddd |
⊢ ( 𝜑 → ( ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ↔ 𝑆 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) ) |
196 |
194 195
|
mpbird |
⊢ ( 𝜑 → ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) |
197 |
49 196
|
jca |
⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ) |
198 |
|
oveq1 |
⊢ ( 𝑧 = 𝑆 → ( 𝑧 − 𝐴 ) = ( 𝑆 − 𝐴 ) ) |
199 |
|
breq2 |
⊢ ( 𝑧 = 𝑆 → ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ↔ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) ) |
200 |
|
id |
⊢ ( 𝑧 = 𝑆 → 𝑧 = 𝑆 ) |
201 |
199 200
|
ifbieq2d |
⊢ ( 𝑧 = 𝑆 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) |
202 |
201
|
oveq2d |
⊢ ( 𝑧 = 𝑆 → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) |
203 |
202
|
fveq2d |
⊢ ( 𝑧 = 𝑆 → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) |
204 |
203
|
mpteq2dv |
⊢ ( 𝑧 = 𝑆 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) |
205 |
204
|
fveq2d |
⊢ ( 𝑧 = 𝑆 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) |
206 |
198 205
|
breq12d |
⊢ ( 𝑧 = 𝑆 → ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ) |
207 |
206
|
elrab |
⊢ ( 𝑆 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ↔ ( 𝑆 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ) |
208 |
197 207
|
sylibr |
⊢ ( 𝜑 → 𝑆 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ) |
209 |
208 7
|
eleqtrrdi |
⊢ ( 𝜑 → 𝑆 ∈ 𝑈 ) |
210 |
209 46 150
|
3jca |
⊢ ( 𝜑 → ( 𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ) |