Step | Hyp | Ref
| Expression |
1 | | uniioombl.1 |
. . 3
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
2 | | ssid 3624 |
. . 3
⊢ ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
((,) ∘ 𝐹) |
3 | | uniioombl.3 |
. . . 4
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
4 | 3 | ovollb 23247 |
. . 3
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐹) ⊆ ∪ ran ((,) ∘ 𝐹)) → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, <
)) |
5 | 1, 2, 4 | sylancl 694 |
. 2
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, <
)) |
6 | 1 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
7 | | elfznn 12370 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...𝑛) → 𝑥 ∈ ℕ) |
8 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
9 | 8 | ovolfsval 23239 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑥) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥)))) |
10 | 6, 7, 9 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
𝐹)‘𝑥) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥)))) |
11 | | fvco3 6275 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
12 | 6, 7, 11 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
13 | | inss2 3834 |
. . . . . . . . . . . . . . . . . 18
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
14 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
15 | 6, 7, 14 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
16 | 13, 15 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) ∈ (ℝ ×
ℝ)) |
17 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) ∈ (ℝ × ℝ) →
(𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
19 | 18 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((,)‘(𝐹‘𝑥)) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
20 | | df-ov 6653 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
21 | 19, 20 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((,)‘(𝐹‘𝑥)) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) |
22 | 12, 21 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) |
23 | | ioombl 23333 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ∈ dom vol |
24 | 22, 23 | syl6eqel 2709 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) ∈ dom vol) |
25 | | mblvol 23298 |
. . . . . . . . . . . 12
⊢ ((((,)
∘ 𝐹)‘𝑥) ∈ dom vol →
(vol‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘(((,) ∘ 𝐹)‘𝑥))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘(((,) ∘ 𝐹)‘𝑥))) |
27 | 22 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol*‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘((1st
‘(𝐹‘𝑥))(,)(2nd
‘(𝐹‘𝑥))))) |
28 | | ovolfcl 23235 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((1st
‘(𝐹‘𝑥)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑥)) ≤ (2nd
‘(𝐹‘𝑥)))) |
29 | 6, 7, 28 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((1st ‘(𝐹‘𝑥)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑥)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥)))) |
30 | | ovolioo 23336 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑥)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑥)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))) → (vol*‘((1st
‘(𝐹‘𝑥))(,)(2nd
‘(𝐹‘𝑥)))) = ((2nd
‘(𝐹‘𝑥)) − (1st
‘(𝐹‘𝑥)))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol*‘((1st
‘(𝐹‘𝑥))(,)(2nd
‘(𝐹‘𝑥)))) = ((2nd
‘(𝐹‘𝑥)) − (1st
‘(𝐹‘𝑥)))) |
32 | 26, 27, 31 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥)))) |
33 | 10, 32 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
𝐹)‘𝑥) = (vol‘(((,) ∘ 𝐹)‘𝑥))) |
34 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
35 | | nnuz 11723 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
36 | 34, 35 | syl6eleq 2711 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
37 | 29 | simp2d 1074 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (2nd ‘(𝐹‘𝑥)) ∈ ℝ) |
38 | 29 | simp1d 1073 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (1st ‘(𝐹‘𝑥)) ∈ ℝ) |
39 | 37, 38 | resubcld 10458 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥))) ∈ ℝ) |
40 | 32, 39 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ) |
41 | 40 | recnd 10068 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℂ) |
42 | 33, 36, 41 | fsumser 14461 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑛)) |
43 | 3 | fveq1i 6192 |
. . . . . . . 8
⊢ (𝑆‘𝑛) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑛) |
44 | 42, 43 | syl6reqr 2675 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥))) |
45 | | fzfid 12772 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin) |
46 | 24, 40 | jca 554 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,)
∘ 𝐹)‘𝑥)) ∈
ℝ)) |
47 | 46 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ (1...𝑛)((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,)
∘ 𝐹)‘𝑥)) ∈
ℝ)) |
48 | 7 | ssriv 3607 |
. . . . . . . . 9
⊢
(1...𝑛) ⊆
ℕ |
49 | | uniioombl.2 |
. . . . . . . . . . 11
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
50 | 1, 11 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
51 | 50 | disjeq2dv 4625 |
. . . . . . . . . . 11
⊢ (𝜑 → (Disj 𝑥 ∈ ℕ (((,) ∘
𝐹)‘𝑥) ↔ Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))) |
52 | 49, 51 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑥 ∈ ℕ (((,) ∘
𝐹)‘𝑥)) |
53 | 52 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑥 ∈ ℕ (((,) ∘
𝐹)‘𝑥)) |
54 | | disjss1 4626 |
. . . . . . . . 9
⊢
((1...𝑛) ⊆
ℕ → (Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) → Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))) |
55 | 48, 53, 54 | mpsyl 68 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) |
56 | | volfiniun 23315 |
. . . . . . . 8
⊢
(((1...𝑛) ∈ Fin
∧ ∀𝑥 ∈
(1...𝑛)((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,)
∘ 𝐹)‘𝑥)) ∈ ℝ) ∧
Disj 𝑥 ∈
(1...𝑛)(((,) ∘ 𝐹)‘𝑥)) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥))) |
57 | 45, 47, 55, 56 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥))) |
58 | 24 | ralrimiva 2966 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) |
59 | | finiunmbl 23312 |
. . . . . . . . 9
⊢
(((1...𝑛) ∈ Fin
∧ ∀𝑥 ∈
(1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) |
60 | 45, 58, 59 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) |
61 | | mblvol 23298 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))) |
62 | 60, 61 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))) |
63 | 44, 57, 62 | 3eqtr2d 2662 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))) |
64 | | iunss1 4532 |
. . . . . . . . 9
⊢
((1...𝑛) ⊆
ℕ → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪
𝑥 ∈ ℕ (((,)
∘ 𝐹)‘𝑥)) |
65 | 48, 64 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪
𝑥 ∈ ℕ (((,)
∘ 𝐹)‘𝑥)) |
66 | | ioof 12271 |
. . . . . . . . . . 11
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
67 | | rexpssxrxp 10084 |
. . . . . . . . . . . . 13
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
68 | 13, 67 | sstri 3612 |
. . . . . . . . . . . 12
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
69 | | fss 6056 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
70 | 1, 68, 69 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
71 | | fco 6058 |
. . . . . . . . . . 11
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
72 | 66, 70, 71 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
73 | 72 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
74 | | ffn 6045 |
. . . . . . . . 9
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
((,) ∘ 𝐹) Fn
ℕ) |
75 | | fniunfv 6505 |
. . . . . . . . 9
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
76 | 73, 74, 75 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
77 | 65, 76 | sseqtrd 3641 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪ ran
((,) ∘ 𝐹)) |
78 | | frn 6053 |
. . . . . . . . . 10
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
ran ((,) ∘ 𝐹) ⊆
𝒫 ℝ) |
79 | 72, 78 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran ((,) ∘ 𝐹) ⊆ 𝒫
ℝ) |
80 | | sspwuni 4611 |
. . . . . . . . 9
⊢ (ran ((,)
∘ 𝐹) ⊆
𝒫 ℝ ↔ ∪ ran ((,) ∘ 𝐹) ⊆
ℝ) |
81 | 79, 80 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) |
82 | 81 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) |
83 | | ovolss 23253 |
. . . . . . 7
⊢
((∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪ ran
((,) ∘ 𝐹) ∧ ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) →
(vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
84 | 77, 82, 83 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
85 | 63, 84 | eqbrtrd 4675 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
86 | 85 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
87 | 8, 3 | ovolsf 23241 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
88 | 1, 87 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
89 | | ffn 6045 |
. . . . 5
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ 𝑆 Fn
ℕ) |
90 | | breq1 4656 |
. . . . . 6
⊢ (𝑦 = (𝑆‘𝑛) → (𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
91 | 90 | ralrn 6362 |
. . . . 5
⊢ (𝑆 Fn ℕ →
(∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
92 | 88, 89, 91 | 3syl 18 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
93 | 86, 92 | mpbird 247 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
94 | | frn 6053 |
. . . . . 6
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
95 | 1, 87, 94 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
96 | | icossxr 12258 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ* |
97 | 95, 96 | syl6ss 3615 |
. . . 4
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
98 | | ovolcl 23246 |
. . . . 5
⊢ (∪ ran ((,) ∘ 𝐹) ⊆ ℝ → (vol*‘∪ ran ((,) ∘ 𝐹)) ∈
ℝ*) |
99 | 81, 98 | syl 17 |
. . . 4
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) ∈
ℝ*) |
100 | | supxrleub 12156 |
. . . 4
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (vol*‘∪ ran ((,)
∘ 𝐹)) ∈
ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
101 | 97, 99, 100 | syl2anc 693 |
. . 3
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
102 | 93, 101 | mpbird 247 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran ((,) ∘ 𝐹))) |
103 | | supxrcl 12145 |
. . . 4
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
104 | 97, 103 | syl 17 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
105 | | xrletri3 11985 |
. . 3
⊢
(((vol*‘∪ ran ((,) ∘ 𝐹)) ∈ ℝ*
∧ sup(ran 𝑆,
ℝ*, < ) ∈ ℝ*) →
((vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ) ↔
((vol*‘∪ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran
𝑆, ℝ*,
< ) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))))) |
106 | 99, 104, 105 | syl2anc 693 |
. 2
⊢ (𝜑 → ((vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ) ↔
((vol*‘∪ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran
𝑆, ℝ*,
< ) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))))) |
107 | 5, 102, 106 | mpbir2and 957 |
1
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, <
)) |