Proof of Theorem uniiccvol
Step | Hyp | Ref
| Expression |
1 | | uniioombl.1 |
. . . 4
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
2 | | ovolficcss 24633 |
. . . 4
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) |
4 | | ovolcl 24642 |
. . 3
⊢ (∪ ran ([,] ∘ 𝐹) ⊆ ℝ → (vol*‘∪ ran ([,] ∘ 𝐹)) ∈
ℝ*) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) ∈
ℝ*) |
6 | | eqid 2738 |
. . . . . . 7
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
7 | | uniioombl.3 |
. . . . . . 7
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
8 | 6, 7 | ovolsf 24636 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
9 | 1, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
10 | 9 | frnd 6608 |
. . . 4
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
11 | | icossxr 13164 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ* |
12 | 10, 11 | sstrdi 3933 |
. . 3
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
13 | | supxrcl 13049 |
. . 3
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
14 | 12, 13 | syl 17 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
15 | | ssid 3943 |
. . 3
⊢ ∪ ran ([,] ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) |
16 | 7 | ovollb2 24653 |
. . 3
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ([,] ∘
𝐹) ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘∪ ran ([,] ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, <
)) |
17 | 1, 15, 16 | sylancl 586 |
. 2
⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) ≤ sup(ran 𝑆, ℝ*, <
)) |
18 | | uniioombl.2 |
. . . 4
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
19 | 1, 18, 7 | uniioovol 24743 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, <
)) |
20 | | ioossicc 13165 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) ⊆ ((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥))) |
21 | | df-ov 7278 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
22 | | df-ov 7278 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑥))[,](2nd ‘(𝐹‘𝑥))) = ([,]‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉) |
23 | 20, 21, 22 | 3sstr3i 3963 |
. . . . . . . . . . 11
⊢
((,)‘〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) ⊆
([,]‘〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) →
((,)‘〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) ⊆
([,]‘〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉)) |
25 | | ffvelrn 6959 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
26 | 25 | elin2d 4133 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ (ℝ ×
ℝ)) |
27 | | 1st2nd2 7870 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑥) ∈ (ℝ × ℝ) →
(𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 〈(1st ‘(𝐹‘𝑥)), (2nd ‘(𝐹‘𝑥))〉) |
29 | 28 | fveq2d 6778 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((,)‘(𝐹‘𝑥)) = ((,)‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
30 | 28 | fveq2d 6778 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ([,]‘(𝐹‘𝑥)) = ([,]‘〈(1st
‘(𝐹‘𝑥)), (2nd
‘(𝐹‘𝑥))〉)) |
31 | 24, 29, 30 | 3sstr4d 3968 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → ((,)‘(𝐹‘𝑥)) ⊆ ([,]‘(𝐹‘𝑥))) |
32 | | fvco3 6867 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) = ((,)‘(𝐹‘𝑥))) |
33 | | fvco3 6867 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑥) = ([,]‘(𝐹‘𝑥))) |
34 | 31, 32, 33 | 3sstr4d 3968 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) ⊆ (([,] ∘ 𝐹)‘𝑥)) |
35 | 1, 34 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑥) ⊆ (([,] ∘ 𝐹)‘𝑥)) |
36 | 35 | ralrimiva 3103 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) ⊆ (([,] ∘ 𝐹)‘𝑥)) |
37 | | ss2iun 4942 |
. . . . . 6
⊢
(∀𝑥 ∈
ℕ (((,) ∘ 𝐹)‘𝑥) ⊆ (([,] ∘ 𝐹)‘𝑥) → ∪
𝑥 ∈ ℕ (((,)
∘ 𝐹)‘𝑥) ⊆ ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥)) |
38 | 36, 37 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) ⊆ ∪
𝑥 ∈ ℕ (([,]
∘ 𝐹)‘𝑥)) |
39 | | ioof 13179 |
. . . . . . . 8
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
40 | | ffn 6600 |
. . . . . . . 8
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
41 | 39, 40 | ax-mp 5 |
. . . . . . 7
⊢ (,) Fn
(ℝ* × ℝ*) |
42 | | inss2 4163 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
43 | | rexpssxrxp 11020 |
. . . . . . . . 9
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
44 | 42, 43 | sstri 3930 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
45 | | fss 6617 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
46 | 1, 44, 45 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
47 | | fnfco 6639 |
. . . . . . 7
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹) Fn ℕ) |
48 | 41, 46, 47 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ) |
49 | | fniunfv 7120 |
. . . . . 6
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (((,) ∘ 𝐹)‘𝑥) = ∪ ran ((,)
∘ 𝐹)) |
51 | | iccf 13180 |
. . . . . . . 8
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
52 | | ffn 6600 |
. . . . . . . 8
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → [,] Fn (ℝ* ×
ℝ*)) |
53 | 51, 52 | ax-mp 5 |
. . . . . . 7
⊢ [,] Fn
(ℝ* × ℝ*) |
54 | | fnfco 6639 |
. . . . . . 7
⊢ (([,] Fn
(ℝ* × ℝ*) ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ([,] ∘ 𝐹) Fn ℕ) |
55 | 53, 46, 54 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → ([,] ∘ 𝐹) Fn ℕ) |
56 | | fniunfv 7120 |
. . . . . 6
⊢ (([,]
∘ 𝐹) Fn ℕ
→ ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ ran ([,]
∘ 𝐹)) |
57 | 55, 56 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ ℕ (([,] ∘ 𝐹)‘𝑥) = ∪ ran ([,]
∘ 𝐹)) |
58 | 38, 50, 57 | 3sstr3d 3967 |
. . . 4
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹)) |
59 | | ovolss 24649 |
. . . 4
⊢ ((∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran
([,] ∘ 𝐹) ∧ ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ (vol*‘∪ ran ([,] ∘ 𝐹))) |
60 | 58, 3, 59 | syl2anc 584 |
. . 3
⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) ≤ (vol*‘∪ ran ([,] ∘ 𝐹))) |
61 | 19, 60 | eqbrtrrd 5098 |
. 2
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
(vol*‘∪ ran ([,] ∘ 𝐹))) |
62 | 5, 14, 17, 61 | xrletrid 12889 |
1
⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) = sup(ran 𝑆, ℝ*, <
)) |