Step | Hyp | Ref
| Expression |
1 | | ioof 12689 |
. . . . . 6
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
2 | | uniioombl.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
3 | | inss2 4132 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
4 | | rexpssxrxp 10539 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
5 | 3, 4 | sstri 3904 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
6 | | fss 6402 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
7 | 2, 5, 6 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
8 | | fco 6406 |
. . . . . 6
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
9 | 1, 7, 8 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
10 | 9 | frnd 6396 |
. . . 4
⊢ (𝜑 → ran ((,) ∘ 𝐹) ⊆ 𝒫
ℝ) |
11 | | sspwuni 4927 |
. . . 4
⊢ (ran ((,)
∘ 𝐹) ⊆
𝒫 ℝ ↔ ∪ ran ((,) ∘ 𝐹) ⊆
ℝ) |
12 | 10, 11 | sylib 219 |
. . 3
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) |
13 | | ovolcl 23766 |
. . 3
⊢ (∪ ran ((,) ∘ 𝐹) ⊆ ℝ → (vol*‘∪ ran ((,) ∘ 𝐹)) ∈
ℝ*) |
14 | 12, 13 | syl 17 |
. 2
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) ∈
ℝ*) |
15 | | eqid 2797 |
. . . . . 6
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
16 | | uniioombl.3 |
. . . . . 6
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
17 | 15, 16 | ovolsf 23760 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
18 | | frn 6395 |
. . . . 5
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
19 | 2, 17, 18 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
20 | | icossxr 12675 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ* |
21 | 19, 20 | syl6ss 3907 |
. . 3
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
22 | | supxrcl 12562 |
. . 3
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
23 | 21, 22 | syl 17 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
24 | | ssid 3916 |
. . 3
⊢ ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
((,) ∘ 𝐹) |
25 | 16 | ovollb 23767 |
. . 3
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝐹) ⊆ ∪ ran ((,) ∘ 𝐹)) → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, <
)) |
26 | 2, 24, 25 | sylancl 586 |
. 2
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, <
)) |
27 | 2 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
28 | | elfznn 12790 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...𝑛) → 𝑥 ∈ ℕ) |
29 | 15 | ovolfsval 23758 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑥) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥)))) |
30 | 27, 28, 29 | syl2an 595 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
𝐹)‘𝑥) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥)))) |
31 | | fvco3 6634 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
32 | 27, 28, 31 | syl2an 595 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
33 | | ffvelrn 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
34 | 27, 28, 33 | syl2an 595 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
35 | 34 | elin2d 4103 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) ∈ (ℝ ×
ℝ)) |
36 | | 1st2nd2 7591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) ∈ (ℝ × ℝ) →
(𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
38 | 37 | fveq2d 6549 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((,)‘(𝐹‘𝑥)) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
39 | | df-ov 7026 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
40 | 38, 39 | syl6eqr 2851 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((,)‘(𝐹‘𝑥)) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) |
41 | 32, 40 | eqtrd 2833 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) = ((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))) |
42 | | ioombl 23853 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ∈ dom vol |
43 | 41, 42 | syl6eqel 2893 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((,) ∘ 𝐹)‘𝑥) ∈ dom vol) |
44 | | mblvol 23818 |
. . . . . . . . . . . 12
⊢ ((((,)
∘ 𝐹)‘𝑥) ∈ dom vol →
(vol‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘(((,) ∘ 𝐹)‘𝑥))) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘(((,) ∘ 𝐹)‘𝑥))) |
46 | 41 | fveq2d 6549 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol*‘(((,) ∘ 𝐹)‘𝑥)) = (vol*‘((1st
‘(𝐹‘𝑥))(,)(2nd
‘(𝐹‘𝑥))))) |
47 | | ovolfcl 23754 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((1st
‘(𝐹‘𝑥)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑥)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑥)) ≤ (2nd
‘(𝐹‘𝑥)))) |
48 | 27, 28, 47 | syl2an 595 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((1st ‘(𝐹‘𝑥)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑥)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥)))) |
49 | | ovolioo 23856 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑥)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑥)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑥)) ≤ (2nd ‘(𝐹‘𝑥))) → (vol*‘((1st
‘(𝐹‘𝑥))(,)(2nd
‘(𝐹‘𝑥)))) = ((2nd
‘(𝐹‘𝑥)) − (1st
‘(𝐹‘𝑥)))) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol*‘((1st
‘(𝐹‘𝑥))(,)(2nd
‘(𝐹‘𝑥)))) = ((2nd
‘(𝐹‘𝑥)) − (1st
‘(𝐹‘𝑥)))) |
51 | 45, 46, 50 | 3eqtrd 2837 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) = ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥)))) |
52 | 30, 51 | eqtr4d 2836 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (((abs ∘ − ) ∘
𝐹)‘𝑥) = (vol‘(((,) ∘ 𝐹)‘𝑥))) |
53 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
54 | | nnuz 12134 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
55 | 53, 54 | syl6eleq 2895 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
56 | 48 | simp2d 1136 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (2nd ‘(𝐹‘𝑥)) ∈ ℝ) |
57 | 48 | simp1d 1135 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (1st ‘(𝐹‘𝑥)) ∈ ℝ) |
58 | 56, 57 | resubcld 10922 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((2nd ‘(𝐹‘𝑥)) − (1st ‘(𝐹‘𝑥))) ∈ ℝ) |
59 | 51, 58 | eqeltrd 2885 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℝ) |
60 | 59 | recnd 10522 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → (vol‘(((,) ∘ 𝐹)‘𝑥)) ∈ ℂ) |
61 | 52, 55, 60 | fsumser 14924 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥)) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑛)) |
62 | 16 | fveq1i 6546 |
. . . . . . . 8
⊢ (𝑆‘𝑛) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑛) |
63 | 61, 62 | syl6reqr 2852 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥))) |
64 | | fzfid 13195 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin) |
65 | 43, 59 | jca 512 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑛)) → ((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,)
∘ 𝐹)‘𝑥)) ∈
ℝ)) |
66 | 65 | ralrimiva 3151 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ (1...𝑛)((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,)
∘ 𝐹)‘𝑥)) ∈
ℝ)) |
67 | | fz1ssnn 12792 |
. . . . . . . . 9
⊢
(1...𝑛) ⊆
ℕ |
68 | | uniioombl.2 |
. . . . . . . . . . 11
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
69 | 2, 31 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
70 | 69 | disjeq2dv 4941 |
. . . . . . . . . . 11
⊢ (𝜑 → (Disj 𝑥 ∈ ℕ (((,) ∘
𝐹)‘𝑥) ↔ Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))) |
71 | 68, 70 | mpbird 258 |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑥 ∈ ℕ (((,) ∘
𝐹)‘𝑥)) |
72 | 71 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑥 ∈ ℕ (((,) ∘
𝐹)‘𝑥)) |
73 | | disjss1 4942 |
. . . . . . . . 9
⊢
((1...𝑛) ⊆
ℕ → (Disj 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) → Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))) |
74 | 67, 72, 73 | mpsyl 68 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) |
75 | | volfiniun 23835 |
. . . . . . . 8
⊢
(((1...𝑛) ∈ Fin
∧ ∀𝑥 ∈
(1...𝑛)((((,) ∘ 𝐹)‘𝑥) ∈ dom vol ∧ (vol‘(((,)
∘ 𝐹)‘𝑥)) ∈ ℝ) ∧
Disj 𝑥 ∈
(1...𝑛)(((,) ∘ 𝐹)‘𝑥)) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥))) |
76 | 64, 66, 74, 75 | syl3anc 1364 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = Σ𝑥 ∈ (1...𝑛)(vol‘(((,) ∘ 𝐹)‘𝑥))) |
77 | 43 | ralrimiva 3151 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) |
78 | | finiunmbl 23832 |
. . . . . . . . 9
⊢
(((1...𝑛) ∈ Fin
∧ ∀𝑥 ∈
(1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) |
79 | 64, 77, 78 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol) |
80 | | mblvol 23818 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ∈ dom vol → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))) |
81 | 79, 80 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))) |
82 | 63, 76, 81 | 3eqtr2d 2839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) = (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥))) |
83 | | iunss1 4844 |
. . . . . . . . 9
⊢
((1...𝑛) ⊆
ℕ → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪
𝑥 ∈ ℕ (((,)
∘ 𝐹)‘𝑥)) |
84 | 67, 83 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪
𝑥 ∈ ℕ (((,)
∘ 𝐹)‘𝑥)) |
85 | 9 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
86 | | ffn 6389 |
. . . . . . . . 9
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
((,) ∘ 𝐹) Fn
ℕ) |
87 | | fniunfv 6878 |
. . . . . . . . 9
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
88 | 85, 86, 87 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
89 | 84, 88 | sseqtrd 3934 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪ ran
((,) ∘ 𝐹)) |
90 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) |
91 | | ovolss 23773 |
. . . . . . 7
⊢
((∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥) ⊆ ∪ ran
((,) ∘ 𝐹) ∧ ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) →
(vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
92 | 89, 90, 91 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘∪ 𝑥 ∈ (1...𝑛)(((,) ∘ 𝐹)‘𝑥)) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
93 | 82, 92 | eqbrtrd 4990 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
94 | 93 | ralrimiva 3151 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
95 | 2, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
96 | | ffn 6389 |
. . . . 5
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ 𝑆 Fn
ℕ) |
97 | | breq1 4971 |
. . . . . 6
⊢ (𝑦 = (𝑆‘𝑛) → (𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
98 | 97 | ralrn 6726 |
. . . . 5
⊢ (𝑆 Fn ℕ →
(∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
99 | 95, 96, 98 | 3syl 18 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑛 ∈ ℕ (𝑆‘𝑛) ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
100 | 94, 99 | mpbird 258 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹))) |
101 | | supxrleub 12573 |
. . . 4
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (vol*‘∪ ran ((,)
∘ 𝐹)) ∈
ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
102 | 21, 14, 101 | syl2anc 584 |
. . 3
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran ((,) ∘ 𝐹)) ↔ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝐹)))) |
103 | 100, 102 | mpbird 258 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran ((,) ∘ 𝐹))) |
104 | 14, 23, 26, 103 | xrletrid 12402 |
1
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, <
)) |