Proof of Theorem uniiccvol
Step | Hyp | Ref
| Expression |
1 | | uniioombl.1 |
. . . 4
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
2 | | ovolficcss 24224 |
. . . 4
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) |
4 | | ovolcl 24233 |
. . 3
⊢ (∪ ran ([,] ∘ 𝐹) ⊆ ℝ → (vol*‘∪ ran ([,] ∘ 𝐹)) ∈
ℝ*) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) ∈
ℝ*) |
6 | | eqid 2739 |
. . . . . . 7
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
7 | | uniioombl.3 |
. . . . . . 7
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
8 | 6, 7 | ovolsf 24227 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
9 | 1, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
10 | 9 | frnd 6513 |
. . . 4
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
11 | | icossxr 12909 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ* |
12 | 10, 11 | sstrdi 3890 |
. . 3
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
13 | | supxrcl 12794 |
. . 3
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
14 | 12, 13 | syl 17 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
15 | | ssid 3900 |
. . 3
⊢ ∪ ran ([,] ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) |
16 | 7 | ovollb2 24244 |
. . 3
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ([,] ∘
𝐹) ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘∪ ran ([,] ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, <
)) |
17 | 1, 15, 16 | sylancl 589 |
. 2
⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, <
)) |
18 | | uniioombl.2 |
. . . 4
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
19 | 1, 18, 7 | uniioovol 24334 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, <
)) |
20 | | ioossicc 12910 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ⊆ ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥))) |
21 | | df-ov 7176 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
22 | | df-ov 7176 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥))) = ([,]‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
23 | 20, 21, 22 | 3sstr3i 3920 |
. . . . . . . . . . 11
⊢
((,)‘〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) ⊆
([,]‘〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) →
((,)‘〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) ⊆
([,]‘〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉)) |
25 | | ffvelrn 6862 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
26 | 25 | elin2d 4090 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ (ℝ ×
ℝ)) |
27 | | 1st2nd2 7756 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑥) ∈ (ℝ × ℝ) →
(𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
29 | 28 | fveq2d 6681 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((,)‘(𝐹‘𝑥)) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
30 | 28 | fveq2d 6681 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ([,]‘(𝐹‘𝑥)) = ([,]‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
31 | 24, 29, 30 | 3sstr4d 3925 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((,)‘(𝐹‘𝑥)) ⊆ ([,]‘(𝐹‘𝑥))) |
32 | | fvco3 6770 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
33 | | fvco3 6770 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ([,]‘(𝐹‘𝑥))) |
34 | 31, 32, 33 | 3sstr4d 3925 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) ⊆ (([,] ∘ 𝐹)‘𝑥)) |
35 | 1, 34 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) ⊆ (([,] ∘ 𝐹)‘𝑥)) |
36 | 35 | ralrimiva 3097 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) ⊆ (([,] ∘ 𝐹)‘𝑥)) |
37 | | ss2iun 4900 |
. . . . . 6
⊢
(∀𝑥 ∈
ℕ (((,) ∘ 𝐹)‘𝑥) ⊆ (([,] ∘ 𝐹)‘𝑥) → ∪
𝑥 ∈ ℕ (((,)
∘ 𝐹)‘𝑥) ⊆ ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥)) |
38 | 36, 37 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) ⊆ ∪
𝑥 ∈ ℕ (([,]
∘ 𝐹)‘𝑥)) |
39 | | ioof 12924 |
. . . . . . . 8
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
40 | | ffn 6505 |
. . . . . . . 8
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
41 | 39, 40 | ax-mp 5 |
. . . . . . 7
⊢ (,) Fn
(ℝ* × ℝ*) |
42 | | inss2 4121 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
43 | | rexpssxrxp 10767 |
. . . . . . . . 9
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
44 | 42, 43 | sstri 3887 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
45 | | fss 6522 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
46 | 1, 44, 45 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
47 | | fnfco 6544 |
. . . . . . 7
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹) Fn ℕ) |
48 | 41, 46, 47 | sylancr 590 |
. . . . . 6
⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ) |
49 | | fniunfv 7020 |
. . . . . 6
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
51 | | iccf 12925 |
. . . . . . . 8
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
52 | | ffn 6505 |
. . . . . . . 8
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → [,] Fn (ℝ* ×
ℝ*)) |
53 | 51, 52 | ax-mp 5 |
. . . . . . 7
⊢ [,] Fn
(ℝ* × ℝ*) |
54 | | fnfco 6544 |
. . . . . . 7
⊢ (([,] Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ([,] ∘ 𝐹) Fn ℕ) |
55 | 53, 46, 54 | sylancr 590 |
. . . . . 6
⊢ (𝜑 → ([,] ∘ 𝐹) Fn ℕ) |
56 | | fniunfv 7020 |
. . . . . 6
⊢ (([,]
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ ran ([,]
∘ 𝐹)) |
57 | 55, 56 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ ran ([,]
∘ 𝐹)) |
58 | 38, 50, 57 | 3sstr3d 3924 |
. . . 4
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹)) |
59 | | ovolss 24240 |
. . . 4
⊢ ((∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) ∧ ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ (vol*‘∪ ran ([,] ∘ 𝐹))) |
60 | 58, 3, 59 | syl2anc 587 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ (vol*‘∪ ran ([,] ∘ 𝐹))) |
61 | 19, 60 | eqbrtrrd 5055 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran ([,] ∘ 𝐹))) |
62 | 5, 14, 17, 61 | xrletrid 12634 |
1
⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) = sup(ran 𝑆, ℝ*, <
)) |