Step | Hyp | Ref
| Expression |
1 | | ensym 8005 |
. 2
⊢ (𝐴 ≈ ℕ → ℕ
≈ 𝐴) |
2 | | bren 7964 |
. . . 4
⊢ (ℕ
≈ 𝐴 ↔
∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
3 | | simpll 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 𝐴 ⊆ ℝ) |
4 | | f1of 6137 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ⟶𝐴) |
5 | 4 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ⟶𝐴) |
6 | 5 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ∈ 𝐴) |
7 | 3, 6 | sseldd 3604 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ∈ ℝ) |
8 | 7 | leidd 10594 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ≤ (𝑓‘𝑥)) |
9 | | df-br 4654 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑥) ≤ (𝑓‘𝑥) ↔ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ ≤ ) |
10 | 8, 9 | sylib 208 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ ≤ ) |
11 | | opelxpi 5148 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘𝑥) ∈ ℝ ∧ (𝑓‘𝑥) ∈ ℝ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ (ℝ ×
ℝ)) |
12 | 7, 7, 11 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ (ℝ ×
ℝ)) |
13 | 10, 12 | elind 3798 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
14 | | df-ov 6653 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑥) I (𝑓‘𝑥)) = ( I ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) |
15 | | opex 4932 |
. . . . . . . . . . . . . 14
⊢
〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ V |
16 | | fvi 6255 |
. . . . . . . . . . . . . 14
⊢
(〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ V → ( I
‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ( I
‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 |
18 | 14, 17 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑥) I (𝑓‘𝑥)) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 |
19 | 18 | mpteq2i 4741 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥) I (𝑓‘𝑥))) = (𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) |
20 | 13, 19 | fmptd 6385 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥) I (𝑓‘𝑥))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
21 | | nnex 11026 |
. . . . . . . . . . . . 13
⊢ ℕ
∈ V |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ℕ ∈
V) |
23 | 7 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ∈ ℂ) |
24 | 5 | feqmptd 6249 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓 = (𝑥 ∈ ℕ ↦ (𝑓‘𝑥))) |
25 | 22, 23, 23, 24, 24 | offval2 6914 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓 ∘𝑓 I 𝑓) = (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥) I (𝑓‘𝑥)))) |
26 | 25 | feq1d 6030 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((𝑓 ∘𝑓 I 𝑓):ℕ⟶( ≤ ∩
(ℝ × ℝ)) ↔ (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥) I (𝑓‘𝑥))):ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) |
27 | 20, 26 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓 ∘𝑓 I 𝑓):ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
28 | | f1ofo 6144 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ–onto→𝐴) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ–onto→𝐴) |
30 | | forn 6118 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:ℕ–onto→𝐴 → ran 𝑓 = 𝐴) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran 𝑓 = 𝐴) |
32 | 31 | eleq2d 2687 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ 𝐴)) |
33 | | f1ofn 6138 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓 Fn ℕ) |
34 | 33 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓 Fn ℕ) |
35 | | fvelrnb 6243 |
. . . . . . . . . . . . . 14
⊢ (𝑓 Fn ℕ → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ ℕ (𝑓‘𝑥) = 𝑦)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ ℕ (𝑓‘𝑥) = 𝑦)) |
37 | 32, 36 | bitr3d 270 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ ℕ (𝑓‘𝑥) = 𝑦)) |
38 | 25, 19 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓 ∘𝑓 I 𝑓) = (𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉)) |
39 | 38 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((𝑓 ∘𝑓 I 𝑓)‘𝑥) = ((𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉)‘𝑥)) |
40 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℕ ↦
〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = (𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) |
41 | 40 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧
〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ V) → ((𝑥 ∈ ℕ ↦ 〈(𝑓‘𝑥), (𝑓‘𝑥)〉)‘𝑥) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) |
42 | 15, 41 | mpan2 707 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℕ → ((𝑥 ∈ ℕ ↦
〈(𝑓‘𝑥), (𝑓‘𝑥)〉)‘𝑥) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) |
43 | 39, 42 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → ((𝑓 ∘𝑓 I 𝑓)‘𝑥) = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉) |
44 | 43 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) = (1st ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉)) |
45 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓‘𝑥) ∈ V |
46 | 45, 45 | op1st 7176 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = (𝑓‘𝑥) |
47 | 44, 46 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) = (𝑓‘𝑥)) |
48 | 47, 8 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) ≤ (𝑓‘𝑥)) |
49 | 43 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (2nd
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) = (2nd ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉)) |
50 | 45, 45 | op2nd 7177 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) = (𝑓‘𝑥) |
51 | 49, 50 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (2nd
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) = (𝑓‘𝑥)) |
52 | 8, 51 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → (𝑓‘𝑥) ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥))) |
53 | 48, 52 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → ((1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) ≤ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)))) |
54 | | breq2 4657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑥) = 𝑦 → ((1st ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)) ≤ (𝑓‘𝑥) ↔ (1st ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)) ≤ 𝑦)) |
55 | | breq1 4656 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑥) = 𝑦 → ((𝑓‘𝑥) ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)) ↔ 𝑦 ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)))) |
56 | 54, 55 | anbi12d 747 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑥) = 𝑦 → (((1st ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)) ≤ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥))) ↔ ((1st ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥))))) |
57 | 53, 56 | syl5ibcom 235 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → ((𝑓‘𝑥) = 𝑦 → ((1st ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥))))) |
58 | 57 | reximdva 3017 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (∃𝑥 ∈ ℕ (𝑓‘𝑥) = 𝑦 → ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥))))) |
59 | 37, 58 | sylbid 230 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑦 ∈ 𝐴 → ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥))))) |
60 | 59 | ralrimiv 2965 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ∀𝑦 ∈ 𝐴 ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥)))) |
61 | | ovolficc 23237 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ (𝑓 ∘𝑓 I
𝑓):ℕ⟶( ≤
∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
([,] ∘ (𝑓
∘𝑓 I 𝑓)) ↔ ∀𝑦 ∈ 𝐴 ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥))))) |
62 | 27, 61 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝐴 ⊆ ∪ ran
([,] ∘ (𝑓
∘𝑓 I 𝑓)) ↔ ∀𝑦 ∈ 𝐴 ∃𝑥 ∈ ℕ ((1st
‘((𝑓
∘𝑓 I 𝑓)‘𝑥)) ≤ 𝑦 ∧ 𝑦 ≤ (2nd ‘((𝑓 ∘𝑓 I
𝑓)‘𝑥))))) |
63 | 60, 62 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝐴 ⊆ ∪ ran
([,] ∘ (𝑓
∘𝑓 I 𝑓))) |
64 | | eqid 2622 |
. . . . . . . . . 10
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑓 ∘𝑓 I 𝑓))) = seq1( + , ((abs ∘
− ) ∘ (𝑓
∘𝑓 I 𝑓))) |
65 | 64 | ovollb2 23257 |
. . . . . . . . 9
⊢ (((𝑓 ∘𝑓 I
𝑓):ℕ⟶( ≤
∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ (𝑓
∘𝑓 I 𝑓))) → (vol*‘𝐴) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ (𝑓
∘𝑓 I 𝑓))), ℝ*, <
)) |
66 | 27, 63, 65 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (vol*‘𝐴) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘𝑓 I 𝑓))), ℝ*, <
)) |
67 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓‘𝑥) ∈ ℂ ∧ (𝑓‘𝑥) ∈ ℂ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ (ℂ ×
ℂ)) |
68 | 23, 23, 67 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 ∈ (ℂ ×
ℂ)) |
69 | | absf 14077 |
. . . . . . . . . . . . . . . . . . . 20
⊢
abs:ℂ⟶ℝ |
70 | | subf 10283 |
. . . . . . . . . . . . . . . . . . . 20
⊢ −
:(ℂ × ℂ)⟶ℂ |
71 | | fco 6058 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((abs:ℂ⟶ℝ ∧ − :(ℂ ×
ℂ)⟶ℂ) → (abs ∘ − ):(ℂ ×
ℂ)⟶ℝ) |
72 | 69, 70, 71 | mp2an 708 |
. . . . . . . . . . . . . . . . . . 19
⊢ (abs
∘ − ):(ℂ × ℂ)⟶ℝ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (abs ∘ −
):(ℂ × ℂ)⟶ℝ) |
74 | 73 | feqmptd 6249 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (abs ∘ − )
= (𝑦 ∈ (ℂ
× ℂ) ↦ ((abs ∘ − )‘𝑦))) |
75 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 → ((abs ∘ −
)‘𝑦) = ((abs ∘
− )‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉)) |
76 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥)) = ((abs ∘ −
)‘〈(𝑓‘𝑥), (𝑓‘𝑥)〉) |
77 | 75, 76 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈(𝑓‘𝑥), (𝑓‘𝑥)〉 → ((abs ∘ −
)‘𝑦) = ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥))) |
78 | 68, 38, 74, 77 | fmptco 6396 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((abs ∘ − )
∘ (𝑓
∘𝑓 I 𝑓)) = (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥)))) |
79 | | cnmet 22575 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
80 | | met0 22148 |
. . . . . . . . . . . . . . . . . 18
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ (𝑓‘𝑥) ∈ ℂ) → ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥)) = 0) |
81 | 79, 23, 80 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) ∧ 𝑥 ∈ ℕ) → ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥)) = 0) |
82 | 81 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑥 ∈ ℕ ↦ ((𝑓‘𝑥)(abs ∘ − )(𝑓‘𝑥))) = (𝑥 ∈ ℕ ↦ 0)) |
83 | 78, 82 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((abs ∘ − )
∘ (𝑓
∘𝑓 I 𝑓)) = (𝑥 ∈ ℕ ↦ 0)) |
84 | | fconstmpt 5163 |
. . . . . . . . . . . . . . 15
⊢ (ℕ
× {0}) = (𝑥 ∈
ℕ ↦ 0) |
85 | 83, 84 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((abs ∘ − )
∘ (𝑓
∘𝑓 I 𝑓)) = (ℕ × {0})) |
86 | 85 | seqeq3d 12809 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → seq1( + , ((abs ∘
− ) ∘ (𝑓
∘𝑓 I 𝑓))) = seq1( + , (ℕ ×
{0}))) |
87 | | 1z 11407 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
88 | | nnuz 11723 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
89 | 88 | ser0f 12854 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {0})) = (ℕ ×
{0})) |
90 | 87, 89 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ seq1( + ,
(ℕ × {0})) = (ℕ × {0}) |
91 | 86, 90 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → seq1( + , ((abs ∘
− ) ∘ (𝑓
∘𝑓 I 𝑓))) = (ℕ × {0})) |
92 | 91 | rneqd 5353 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘𝑓 I 𝑓))) = ran (ℕ ×
{0})) |
93 | | 1nn 11031 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
94 | | ne0i 3921 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
95 | | rnxp 5564 |
. . . . . . . . . . . 12
⊢ (ℕ
≠ ∅ → ran (ℕ × {0}) = {0}) |
96 | 93, 94, 95 | mp2b 10 |
. . . . . . . . . . 11
⊢ ran
(ℕ × {0}) = {0} |
97 | 92, 96 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘𝑓 I 𝑓))) = {0}) |
98 | 97 | supeq1d 8352 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘𝑓 I 𝑓))), ℝ*, < )
= sup({0}, ℝ*, < )) |
99 | | xrltso 11974 |
. . . . . . . . . 10
⊢ < Or
ℝ* |
100 | | 0xr 10086 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
101 | | supsn 8378 |
. . . . . . . . . 10
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
102 | 99, 100, 101 | mp2an 708 |
. . . . . . . . 9
⊢ sup({0},
ℝ*, < ) = 0 |
103 | 98, 102 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → sup(ran seq1( + , ((abs
∘ − ) ∘ (𝑓 ∘𝑓 I 𝑓))), ℝ*, < )
= 0) |
104 | 66, 103 | breqtrd 4679 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (vol*‘𝐴) ≤ 0) |
105 | | ovolge0 23249 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ → 0 ≤
(vol*‘𝐴)) |
106 | 105 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → 0 ≤
(vol*‘𝐴)) |
107 | | ovolcl 23246 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) ∈
ℝ*) |
108 | 107 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (vol*‘𝐴) ∈
ℝ*) |
109 | | xrletri3 11985 |
. . . . . . . 8
⊢
(((vol*‘𝐴)
∈ ℝ* ∧ 0 ∈ ℝ*) →
((vol*‘𝐴) = 0 ↔
((vol*‘𝐴) ≤ 0
∧ 0 ≤ (vol*‘𝐴)))) |
110 | 108, 100,
109 | sylancl 694 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → ((vol*‘𝐴) = 0 ↔ ((vol*‘𝐴) ≤ 0 ∧ 0 ≤
(vol*‘𝐴)))) |
111 | 104, 106,
110 | mpbir2and 957 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑓:ℕ–1-1-onto→𝐴) → (vol*‘𝐴) = 0) |
112 | 111 | ex 450 |
. . . . 5
⊢ (𝐴 ⊆ ℝ → (𝑓:ℕ–1-1-onto→𝐴 → (vol*‘𝐴) = 0)) |
113 | 112 | exlimdv 1861 |
. . . 4
⊢ (𝐴 ⊆ ℝ →
(∃𝑓 𝑓:ℕ–1-1-onto→𝐴 → (vol*‘𝐴) = 0)) |
114 | 2, 113 | syl5bi 232 |
. . 3
⊢ (𝐴 ⊆ ℝ → (ℕ
≈ 𝐴 →
(vol*‘𝐴) =
0)) |
115 | 114 | imp 445 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ ℕ
≈ 𝐴) →
(vol*‘𝐴) =
0) |
116 | 1, 115 | sylan2 491 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≈ ℕ) →
(vol*‘𝐴) =
0) |