Proof of Theorem hoidmv1lelem1
Step | Hyp | Ref
| Expression |
1 | | hoidmv1lelem1.s |
. . . . . 6
⊢ 𝑆 = sup(𝑈, ℝ, < ) |
2 | | hoidmv1lelem1.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | | hoidmv1lelem1.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | | hoidmv1lelem1.u |
. . . . . . . . 9
⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} |
5 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ⊆ (𝐴[,]𝐵) |
6 | 4, 5 | eqsstri 3635 |
. . . . . . . 8
⊢ 𝑈 ⊆ (𝐴[,]𝐵) |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵)) |
8 | 2 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
9 | 3 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
10 | | hoidmv1lelem1.l |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 𝐵) |
11 | 2, 3, 10 | ltled 10185 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
12 | | lbicc2 12288 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
13 | 8, 9, 11, 12 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
14 | 2 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℂ) |
15 | 14 | subidd 10380 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 − 𝐴) = 0) |
16 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝜑 |
17 | | nnex 11026 |
. . . . . . . . . . . . . 14
⊢ ℕ
∈ V |
18 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ ∈
V) |
19 | | volf 23297 |
. . . . . . . . . . . . . . 15
⊢ vol:dom
vol⟶(0[,]+∞) |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → vol:dom
vol⟶(0[,]+∞)) |
21 | | hoidmv1lelem1.c |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶:ℕ⟶ℝ) |
22 | 21 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ) |
23 | | hoidmv1lelem1.d |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷:ℕ⟶ℝ) |
24 | 23 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ) |
25 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ ℝ) |
26 | 24, 25 | ifcld 4131 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ) |
27 | 26 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈
ℝ*) |
28 | | icombl 23332 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol) |
29 | 22, 27, 28 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol) |
30 | 20, 29 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))) ∈ (0[,]+∞)) |
31 | 16, 18, 30 | sge0ge0mpt 40655 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))) |
32 | 15, 31 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))) |
33 | 13, 32 | jca 554 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))) |
34 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐴 → (𝑧 − 𝐴) = (𝐴 − 𝐴)) |
35 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝐴 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝐴)) |
36 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝐴 → 𝑧 = 𝐴) |
37 | 35, 36 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝐴 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) |
38 | 37 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝐴 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))) |
39 | 38 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝐴 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))) |
40 | 39 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐴 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))) |
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐴 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))) |
42 | 34, 41 | breq12d 4666 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝐴 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))) |
43 | 42 | elrab 3363 |
. . . . . . . . . 10
⊢ (𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))) |
44 | 33, 43 | sylibr 224 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
45 | 44, 4 | syl6eleqr 2712 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
46 | | ne0i 3921 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑈 → 𝑈 ≠ ∅) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ≠ ∅) |
48 | 2, 3, 7, 47 | supicc 12320 |
. . . . . 6
⊢ (𝜑 → sup(𝑈, ℝ, < ) ∈ (𝐴[,]𝐵)) |
49 | 1, 48 | syl5eqel 2705 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ (𝐴[,]𝐵)) |
50 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑆 = sup(𝑈, ℝ, < )) |
51 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝜑 |
52 | 2, 3 | iccssred 39727 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
53 | 7, 52 | sstrd 3613 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ⊆ ℝ) |
54 | 53 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℝ) |
55 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ 𝑈) |
56 | 17 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ℕ ∈ V) |
57 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → vol:dom
vol⟶(0[,]+∞)) |
58 | 22 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ) |
59 | 24 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ) |
60 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → 𝑧 ∈ ℝ) |
61 | 59, 60 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ) |
62 | 61 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈
ℝ*) |
63 | | icombl 23332 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol) |
64 | 58, 62, 63 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol) |
65 | 57, 64 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ∈ (0[,]+∞)) |
66 | 55, 56, 65 | sge0xrclmpt 40645 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈
ℝ*) |
67 | | pnfxr 10092 |
. . . . . . . . . . . . . . . 16
⊢ +∞
∈ ℝ* |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → +∞ ∈
ℝ*) |
69 | | hoidmv1lelem1.r |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ) |
70 | 69 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈
ℝ*) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈
ℝ*) |
72 | 24 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈
ℝ*) |
73 | | icombl 23332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ*) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
74 | 22, 72, 73 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
75 | 20, 74 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞)) |
76 | 75 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞)) |
77 | 74 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
78 | 22 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈
ℝ*) |
79 | 78 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈
ℝ*) |
80 | 72 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈
ℝ*) |
81 | 22 | leidd 10594 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗)) |
82 | 81 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗)) |
83 | | min1 12020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑧 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗)) |
84 | 59, 60, 83 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗)) |
85 | | icossico 12243 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶‘𝑗) ∈ ℝ* ∧ (𝐷‘𝑗) ∈ ℝ*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
86 | 79, 80, 82, 84, 85 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
87 | | volss 23301 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
88 | 64, 77, 86, 87 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
89 | 55, 56, 65, 76, 88 | sge0lempt 40627 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) |
90 | 69 | ltpnfd 11955 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞) |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞) |
92 | 66, 71, 68, 89, 91 | xrlelttrd 11991 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) < +∞) |
93 | 66, 68, 92 | xrltned 39573 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≠ +∞) |
94 | 93 | neneqd 2799 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞) |
95 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ ↦
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) |
96 | 65, 95 | fmptd 6385 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))):ℕ⟶(0[,]+∞)) |
97 | 56, 96 | sge0repnf 40603 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞)) |
98 | 94, 97 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ) |
99 | 2 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝐴 ∈ ℝ) |
100 | 98, 99 | readdcld 10069 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ∈ ℝ) |
101 | 52, 49 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑆 ∈ ℝ) |
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ) |
103 | 24, 102 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ) |
104 | 103 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈
ℝ*) |
105 | | icombl 23332 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol) |
106 | 22, 104, 105 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol) |
107 | 20, 106 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞)) |
108 | 16, 18, 107 | sge0xrclmpt 40645 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈
ℝ*) |
109 | 67 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → +∞ ∈
ℝ*) |
110 | | min1 12020 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗)) |
111 | 24, 102, 110 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗)) |
112 | | icossico 12243 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐶‘𝑗) ∈ ℝ* ∧ (𝐷‘𝑗) ∈ ℝ*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
113 | 78, 72, 81, 111, 112 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
114 | | volss 23301 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
115 | 106, 74, 113, 114 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
116 | 16, 18, 107, 75, 115 | sge0lempt 40627 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) |
117 | 108, 70, 109, 116, 90 | xrlelttrd 11991 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) < +∞) |
118 | 108, 109,
117 | xrltned 39573 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≠ +∞) |
119 | 118 | neneqd 2799 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞) |
120 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ ↦
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) |
121 | 107, 120 | fmptd 6385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))):ℕ⟶(0[,]+∞)) |
122 | 18, 121 | sge0repnf 40603 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞)) |
123 | 119, 122 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ) |
124 | 123, 2 | readdcld 10069 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ) |
125 | 124 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ) |
126 | 4 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
127 | 126 | biimpi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑈 → 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
128 | 127 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
129 | | rabid 3116 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑧 ∈ (𝐴[,]𝐵) ∧ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))))) |
130 | 128, 129 | sylib 208 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑧 ∈ (𝐴[,]𝐵) ∧ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))))) |
131 | 130 | simprd 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))) |
132 | 54, 99, 98 | lesubaddd 10624 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ 𝑧 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴))) |
133 | 131, 132 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴)) |
134 | 123 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ) |
135 | 107 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞)) |
136 | 106 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol) |
137 | 104 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈
ℝ*) |
138 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ) |
139 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) = (𝐷‘𝑗)) |
140 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷‘𝑗) ≤ 𝑧 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = (𝐷‘𝑗)) |
141 | 140 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = (𝐷‘𝑗)) |
142 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ∈ ℝ) |
143 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ∈ ℝ) |
144 | 101 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑆 ∈ ℝ) |
145 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ≤ 𝑧) |
146 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑈 ⊆ ℝ) |
147 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑈 ≠ ∅) |
148 | 2, 3 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
149 | | iccsupr 12266 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑈 ⊆ (𝐴[,]𝐵) ∧ 𝐴 ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |
150 | 148, 7, 45, 149 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |
151 | 150 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) |
152 | 151 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) |
153 | 128, 126 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈) |
154 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < )) |
155 | 146, 147,
152, 153, 154 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < )) |
156 | 155, 1 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ 𝑆) |
157 | 156 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ 𝑆) |
158 | 142, 143,
144, 145, 157 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ≤ 𝑆) |
159 | 158 | iftrued 4094 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗)) |
160 | 139, 141,
159 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) |
161 | 138, 160 | eqled 10140 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) |
162 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ∈ ℝ) |
163 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ∈ ℝ) |
164 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → ¬ (𝐷‘𝑗) ≤ 𝑧) |
165 | 162, 163 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝑧 < (𝐷‘𝑗) ↔ ¬ (𝐷‘𝑗) ≤ 𝑧)) |
166 | 164, 165 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 < (𝐷‘𝑗)) |
167 | 162, 163,
166 | ltled 10185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ (𝐷‘𝑗)) |
168 | 167 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ (𝐷‘𝑗)) |
169 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
(𝐷‘𝑗) ≤ 𝑧 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧) |
170 | 169 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧) |
171 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗)) |
172 | 171 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗)) |
173 | 170, 172 | breq12d 4666 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → (if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ↔ 𝑧 ≤ (𝐷‘𝑗))) |
174 | 168, 173 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) |
175 | 156 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ 𝑆) |
176 | 169 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧) |
177 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
(𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆) |
178 | 177 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆) |
179 | 176, 178 | breq12d 4666 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → (if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ↔ 𝑧 ≤ 𝑆)) |
180 | 175, 179 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) |
181 | 174, 180 | pm2.61dan 832 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) |
182 | 161, 181 | pm2.61dan 832 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) |
183 | | icossico 12243 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶‘𝑗) ∈ ℝ* ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) |
184 | 79, 137, 82, 182, 183 | syl22anc 1327 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) |
185 | | volss 23301 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) |
186 | 64, 136, 184, 185 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) |
187 | 55, 56, 65, 135, 186 | sge0lempt 40627 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) |
188 | 98, 134, 99, 187 | leadd1dd 10641 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)) |
189 | 54, 100, 125, 133, 188 | letrd 10194 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)) |
190 | 189 | ex 450 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ 𝑈 → 𝑧 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))) |
191 | 51, 190 | ralrimi 2957 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝑈 𝑧 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)) |
192 | | suprleub 10989 |
. . . . . . . . 9
⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ) → (sup(𝑈, ℝ, < ) ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ↔ ∀𝑧 ∈ 𝑈 𝑧 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))) |
193 | 53, 47, 151, 124, 192 | syl31anc 1329 |
. . . . . . . 8
⊢ (𝜑 → (sup(𝑈, ℝ, < ) ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ↔ ∀𝑧 ∈ 𝑈 𝑧 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))) |
194 | 191, 193 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → sup(𝑈, ℝ, < ) ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)) |
195 | 50, 194 | eqbrtrd 4675 |
. . . . . 6
⊢ (𝜑 → 𝑆 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)) |
196 | 101, 2, 123 | lesubaddd 10624 |
. . . . . 6
⊢ (𝜑 → ((𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ↔ 𝑆 ≤
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))) |
197 | 195, 196 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) |
198 | 49, 197 | jca 554 |
. . . 4
⊢ (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
199 | | oveq1 6657 |
. . . . . 6
⊢ (𝑧 = 𝑆 → (𝑧 − 𝐴) = (𝑆 − 𝐴)) |
200 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑆)) |
201 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → 𝑧 = 𝑆) |
202 | 200, 201 | ifbieq2d 4111 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑆 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) |
203 | 202 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑧 = 𝑆 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) |
204 | 203 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑧 = 𝑆 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) |
205 | 204 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) |
206 | 205 | fveq2d 6195 |
. . . . . 6
⊢ (𝑧 = 𝑆 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) |
207 | 199, 206 | breq12d 4666 |
. . . . 5
⊢ (𝑧 = 𝑆 → ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
208 | 207 | elrab 3363 |
. . . 4
⊢ (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
209 | 198, 208 | sylibr 224 |
. . 3
⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
210 | 209, 4 | syl6eleqr 2712 |
. 2
⊢ (𝜑 → 𝑆 ∈ 𝑈) |
211 | 210, 45, 151 | 3jca 1242 |
1
⊢ (𝜑 → (𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |