| Step | Hyp | Ref
| Expression |
| 1 | | itg2gt0.2 |
. 2
⊢ (𝜑 → 0 < (vol‘𝐴)) |
| 2 | | itg2gt0.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ dom vol) |
| 3 | | iccssxr 13470 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
| 4 | | volf 25564 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
| 5 | 4 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
| 6 | 3, 5 | sselid 3981 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
ℝ*) |
| 7 | 2, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (vol‘𝐴) ∈
ℝ*) |
| 8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol‘𝐴) ∈
ℝ*) |
| 9 | | itg2gt0.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 ∈ MblFn) |
| 10 | 9 | elexd 3504 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ V) |
| 11 | | cnvexg 7946 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ◡𝐹 ∈ V) |
| 13 | | imaexg 7935 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹 ∈ V → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ V) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ V) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ V) |
| 16 | 15 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶V) |
| 17 | 16 | ffnd 6737 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ) |
| 18 | | fniunfv 7267 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ → ∪ 𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) |
| 20 | | itg2gt0.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
| 21 | | rge0ssre 13496 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℝ |
| 22 | | fss 6752 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ) |
| 23 | 20, 21, 22 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
| 24 | | mbfima 25665 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) →
(◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ dom
vol) |
| 25 | 9, 23, 24 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ dom
vol) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ dom
vol) |
| 27 | 26 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶dom
vol) |
| 28 | 27 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol) |
| 29 | 28 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol) |
| 30 | | iunmbl 25588 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
ℕ ((𝑛 ∈ ℕ
↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol → ∪ 𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol) |
| 32 | 19, 31 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ∈ dom
vol) |
| 33 | | mblss 25566 |
. . . . . . . 8
⊢ (∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ∈ dom vol → ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆
ℝ) |
| 34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆
ℝ) |
| 35 | | ovolcl 25513 |
. . . . . . 7
⊢ (∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ ℝ →
(vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ∈
ℝ*) |
| 36 | 34, 35 | syl 17 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ∈
ℝ*) |
| 37 | 36 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ∈
ℝ*) |
| 38 | | 0xr 11308 |
. . . . . 6
⊢ 0 ∈
ℝ* |
| 39 | 38 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → 0 ∈
ℝ*) |
| 40 | | mblvol 25565 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) |
| 41 | 2, 40 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (vol‘𝐴) = (vol*‘𝐴)) |
| 42 | | mblss 25566 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
| 43 | 2, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 44 | 43 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
| 45 | 20 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
| 46 | | elrege0 13494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 47 | 45, 46 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 48 | 47 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
| 49 | 44, 48 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
| 50 | | itg2gt0.5 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 < (𝐹‘𝑥)) |
| 51 | | nnrecl 12524 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 0 < (𝐹‘𝑥)) → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝐹‘𝑥)) |
| 52 | 49, 50, 51 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝐹‘𝑥)) |
| 53 | 20 | ffnd 6737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 Fn ℝ) |
| 54 | 53 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝐹 Fn ℝ) |
| 55 | | elpreima 7078 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)))) |
| 56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)))) |
| 57 | 44 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ ℝ) |
| 58 | 57 | biantrurd 532 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)))) |
| 59 | | nnrecre 12308 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
| 60 | 59 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ) |
| 61 | 60 | rexrd 11311 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ*) |
| 62 | 61 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ*) |
| 63 | | elioopnf 13483 |
. . . . . . . . . . . . . . . 16
⊢ ((1 /
𝑘) ∈
ℝ* → ((𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)))) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)))) |
| 65 | 56, 58, 64 | 3bitr2d 307 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)))) |
| 66 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ) |
| 67 | | imaexg 7935 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹 ∈ V → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) |
| 68 | 12, 67 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) |
| 70 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
| 71 | 70 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((1 / 𝑛)(,)+∞) = ((1 / 𝑘)(,)+∞)) |
| 72 | 71 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
| 73 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) = (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) |
| 74 | 72, 73 | fvmptg 7014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
| 75 | 66, 69, 74 | syl2anr 597 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
| 76 | 75 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ↔ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)))) |
| 77 | 49 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑥) ∈ ℝ) |
| 78 | 77 | biantrurd 532 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘) < (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)))) |
| 79 | 65, 76, 78 | 3bitr4rd 312 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘) < (𝐹‘𝑥) ↔ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
| 80 | 79 | rexbidva 3177 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑘 ∈ ℕ (1 / 𝑘) < (𝐹‘𝑥) ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
| 81 | 52, 80 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) |
| 82 | 81 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
| 83 | | eluni2 4911 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ↔ ∃𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))𝑥 ∈ 𝑧) |
| 84 | | eleq2 2830 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
| 85 | 84 | rexrn 7107 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ →
(∃𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))𝑥 ∈ 𝑧 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
| 86 | 17, 85 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))𝑥 ∈ 𝑧 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
| 87 | 83, 86 | bitrid 283 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ∪ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞))) ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
| 88 | 82, 87 | sylibrd 259 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
| 89 | 88 | ssrdv 3989 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))) |
| 90 | | ovolss 25520 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ∧ ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ ℝ) →
(vol*‘𝐴) ≤
(vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
| 91 | 89, 34, 90 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (vol*‘𝐴) ≤ (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
| 92 | 41, 91 | eqbrtrd 5165 |
. . . . . 6
⊢ (𝜑 → (vol‘𝐴) ≤ (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
| 93 | 92 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol‘𝐴) ≤ (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
| 94 | | mblvol 25565 |
. . . . . . . . 9
⊢ (∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ∈ dom vol →
(vol‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
| 95 | 32, 94 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (vol‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
| 96 | | peano2nn 12278 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
| 97 | 96 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
| 98 | | nnrecre 12308 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 + 1) ∈ ℕ → (1 /
(𝑘 + 1)) ∈
ℝ) |
| 99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / (𝑘 + 1)) ∈
ℝ) |
| 100 | 99 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / (𝑘 + 1)) ∈
ℝ*) |
| 101 | | nnre 12273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 102 | 101 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ) |
| 103 | 102 | lep1d 12199 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (𝑘 + 1)) |
| 104 | | nngt0 12297 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
| 105 | 104 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < 𝑘) |
| 106 | 97 | nnred 12281 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ) |
| 107 | 97 | nngt0d 12315 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < (𝑘 + 1)) |
| 108 | | lerec 12151 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℝ ∧ 0 <
𝑘) ∧ ((𝑘 + 1) ∈ ℝ ∧ 0
< (𝑘 + 1))) →
(𝑘 ≤ (𝑘 + 1) ↔ (1 / (𝑘 + 1)) ≤ (1 / 𝑘))) |
| 109 | 102, 105,
106, 107, 108 | syl22anc 839 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 ≤ (𝑘 + 1) ↔ (1 / (𝑘 + 1)) ≤ (1 / 𝑘))) |
| 110 | 103, 109 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / (𝑘 + 1)) ≤ (1 / 𝑘)) |
| 111 | | iooss1 13422 |
. . . . . . . . . . . . 13
⊢ (((1 /
(𝑘 + 1)) ∈
ℝ* ∧ (1 / (𝑘 + 1)) ≤ (1 / 𝑘)) → ((1 / 𝑘)(,)+∞) ⊆ ((1 / (𝑘 +
1))(,)+∞)) |
| 112 | 100, 110,
111 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘)(,)+∞) ⊆ ((1 /
(𝑘 +
1))(,)+∞)) |
| 113 | | imass2 6120 |
. . . . . . . . . . . 12
⊢ (((1 /
𝑘)(,)+∞) ⊆ ((1
/ (𝑘 + 1))(,)+∞)
→ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ⊆ (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
| 114 | 112, 113 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ⊆ (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
| 115 | 66, 68, 74 | syl2anr 597 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
| 116 | | imaexg 7935 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 ∈ V → (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞)) ∈
V) |
| 117 | 12, 116 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞)) ∈
V) |
| 118 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1))) |
| 119 | 118 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑘 + 1) → ((1 / 𝑛)(,)+∞) = ((1 / (𝑘 + 1))(,)+∞)) |
| 120 | 119 | imaeq2d 6078 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑘 + 1) → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) = (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
| 121 | 120, 73 | fvmptg 7014 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) ∈ ℕ ∧
(◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞)) ∈ V) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1)) = (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
| 122 | 96, 117, 121 | syl2anr 597 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1)) = (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
| 123 | 114, 115,
122 | 3sstr4d 4039 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ⊆ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1))) |
| 124 | 123 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ⊆ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1))) |
| 125 | | volsup 25591 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶dom vol ∧
∀𝑘 ∈ ℕ
((𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ⊆ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1))) → (vol‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, <
)) |
| 126 | 27, 124, 125 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (vol‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, <
)) |
| 127 | 95, 126 | eqtr3d 2779 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, <
)) |
| 128 | 127 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, <
)) |
| 129 | 68 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) |
| 130 | 66, 129, 74 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
| 131 | 130 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) ∧ 𝑘 ∈ ℕ) → (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) = (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞)))) |
| 132 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 0 ∈
ℝ*) |
| 133 | | nnrecgt0 12309 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ℕ → 0 < (1
/ 𝑘)) |
| 134 | 133 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < (1 / 𝑘)) |
| 135 | | 0re 11263 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
ℝ |
| 136 | | ltle 11349 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((0
∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) → (0 < (1 / 𝑘) → 0 ≤ (1 / 𝑘))) |
| 137 | 135, 60, 136 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0 < (1 / 𝑘) → 0 ≤ (1 / 𝑘))) |
| 138 | 134, 137 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 / 𝑘)) |
| 139 | | elxrge0 13497 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1 /
𝑘) ∈ (0[,]+∞)
↔ ((1 / 𝑘) ∈
ℝ* ∧ 0 ≤ (1 / 𝑘))) |
| 140 | 61, 138, 139 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
(0[,]+∞)) |
| 141 | | 0e0iccpnf 13499 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
(0[,]+∞) |
| 142 | | ifcl 4571 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((1 /
𝑘) ∈ (0[,]+∞)
∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ (0[,]+∞)) |
| 143 | 140, 141,
142 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ (0[,]+∞)) |
| 144 | 143 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ (0[,]+∞)) |
| 145 | 144 | fmpttd 7135 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘),
0)):ℝ⟶(0[,]+∞)) |
| 146 | 145 | adantrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘),
0)):ℝ⟶(0[,]+∞)) |
| 147 | | itg2cl 25767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈
ℝ*) |
| 148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈
ℝ*) |
| 149 | | icossicc 13476 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 150 | | fss 6752 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞)) |
| 151 | 20, 149, 150 | sylancl 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
| 152 | | itg2cl 25767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (∫2‘𝐹) ∈
ℝ*) |
| 153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ*) |
| 154 | 153 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) →
(∫2‘𝐹)
∈ ℝ*) |
| 155 | | 0nrp 13070 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬ 0
∈ ℝ+ |
| 156 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
| 157 | 115, 28 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom
vol) |
| 158 | 157 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom
vol) |
| 159 | 158 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom
vol) |
| 160 | 156, 135 | eqeltrrdi 2850 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈ ℝ) |
| 161 | 60, 134 | elrpd 13074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ+) |
| 162 | 161 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (1 / 𝑘) ∈
ℝ+) |
| 163 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (1 / 𝑘) ∈
ℝ+) |
| 164 | | itg2const2 25776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom vol ∧ (1 /
𝑘) ∈
ℝ+) → ((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈ ℝ)) |
| 165 | 159, 163,
164 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → ((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈ ℝ)) |
| 166 | 160, 165 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
ℝ) |
| 167 | | elrege0 13494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1 /
𝑘) ∈ (0[,)+∞)
↔ ((1 / 𝑘) ∈
ℝ ∧ 0 ≤ (1 / 𝑘))) |
| 168 | 60, 138, 167 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
(0[,)+∞)) |
| 169 | 168 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (1 / 𝑘) ∈
(0[,)+∞)) |
| 170 | 169 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (1 / 𝑘) ∈ (0[,)+∞)) |
| 171 | | itg2const 25775 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom vol ∧
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈ ℝ ∧ (1 /
𝑘) ∈ (0[,)+∞))
→ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) = ((1 / 𝑘) · (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
| 172 | 159, 166,
170, 171 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) = ((1 / 𝑘) · (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
| 173 | 156, 172 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → 0 = ((1 / 𝑘) · (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
| 174 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → 0 < (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞)))) |
| 175 | 166, 174 | elrpd 13074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
ℝ+) |
| 176 | 163, 175 | rpmulcld 13093 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → ((1 / 𝑘) · (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞)))) ∈
ℝ+) |
| 177 | 173, 176 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → 0 ∈
ℝ+) |
| 178 | 177 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) → 0 ∈
ℝ+)) |
| 179 | 155, 178 | mtoi 199 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → ¬ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
| 180 | | itg2ge0 25770 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)):ℝ⟶(0[,]+∞) → 0
≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
| 181 | 146, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 0 ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
| 182 | | xrleloe 13186 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ* ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈ ℝ*) → (0
≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ↔ (0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∨ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))))) |
| 183 | 38, 148, 182 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (0 ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ↔ (0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∨ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))))) |
| 184 | 181, 183 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∨ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))))) |
| 185 | 184 | ord 865 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (¬ 0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) → 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))))) |
| 186 | 179, 185 | mt3d 148 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
| 187 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 𝐹:ℝ⟶(0[,]+∞)) |
| 188 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (1 / 𝑘) ∈
ℝ) |
| 189 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹 Fn ℝ) |
| 190 | 189, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)))) |
| 191 | 190 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞))) |
| 192 | 191 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → 𝑥 ∈ ℝ) |
| 193 | 48 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
| 194 | 192, 193 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (𝐹‘𝑥) ∈ ℝ) |
| 195 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (1 / 𝑘) ∈
ℝ*) |
| 196 | 191 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)) |
| 197 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)) → (1 / 𝑘) < (𝐹‘𝑥)) |
| 198 | 63, 197 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1 /
𝑘) ∈
ℝ* → ((𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞) → (1 / 𝑘) < (𝐹‘𝑥))) |
| 199 | 195, 196,
198 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (1 / 𝑘) < (𝐹‘𝑥)) |
| 200 | 188, 194,
199 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (1 / 𝑘) ≤ (𝐹‘𝑥)) |
| 201 | 47 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
| 202 | 201 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
| 203 | 192, 202 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → 0 ≤ (𝐹‘𝑥)) |
| 204 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1 /
𝑘) = if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) → ((1 / 𝑘) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥))) |
| 205 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 =
if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥))) |
| 206 | 204, 205 | ifboth 4565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((1 /
𝑘) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
| 207 | 200, 203,
206 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
| 208 | 207 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
| 209 | | iffalse 4534 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) = 0) |
| 210 | 209 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) = 0) |
| 211 | 202 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → 0 ≤ (𝐹‘𝑥)) |
| 212 | 210, 211 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
| 213 | 208, 212 | pm2.61dan 813 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
| 214 | 213 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
| 215 | 214 | adantrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
| 216 | | reex 11246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℝ
∈ V |
| 217 | 216 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ℝ ∈
V) |
| 218 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 /
𝑘) ∈
V |
| 219 | | c0ex 11255 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
V |
| 220 | 218, 219 | ifex 4576 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ V |
| 221 | 220 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ V) |
| 222 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ V) |
| 223 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) |
| 224 | 20 | feqmptd 6977 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
| 225 | 217, 221,
222, 223, 224 | ofrfval2 7718 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥))) |
| 226 | 225 | biimpar 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) ∘r ≤ 𝐹) |
| 227 | 215, 226 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) ∘r ≤ 𝐹) |
| 228 | | itg2le 25774 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)):ℝ⟶(0[,]+∞) ∧
𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) ∘r ≤ 𝐹) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ≤ (∫2‘𝐹)) |
| 229 | 146, 187,
227, 228 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ≤ (∫2‘𝐹)) |
| 230 | 132, 148,
154, 186, 229 | xrltletrd 13203 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 0 <
(∫2‘𝐹)) |
| 231 | 230 | expr 456 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) → 0 <
(∫2‘𝐹))) |
| 232 | 231 | con3d 152 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (¬ 0 <
(∫2‘𝐹)
→ ¬ 0 < (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
| 233 | 4 | ffvelcdmi 7103 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom vol →
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
(0[,]+∞)) |
| 234 | 3, 233 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom vol →
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
ℝ*) |
| 235 | 157, 234 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
ℝ*) |
| 236 | | xrlenlt 11326 |
. . . . . . . . . . . . . . 15
⊢
(((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈ ℝ*
∧ 0 ∈ ℝ*) → ((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0 ↔ ¬ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
| 237 | 235, 38, 236 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0 ↔ ¬ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
| 238 | 232, 237 | sylibrd 259 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (¬ 0 <
(∫2‘𝐹)
→ (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0)) |
| 239 | 238 | imp 406 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ 0 <
(∫2‘𝐹)) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0) |
| 240 | 239 | an32s 652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) ∧ 𝑘 ∈ ℕ) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0) |
| 241 | 131, 240 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) ∧ 𝑘 ∈ ℕ) → (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0) |
| 242 | 241 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → ∀𝑘 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0) |
| 243 | | ffn 6736 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶V →
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ) |
| 244 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) → (vol‘𝑧) = (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
| 245 | 244 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) → ((vol‘𝑧) ≤ 0 ↔ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0)) |
| 246 | 245 | ralrn 7108 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ →
(∀𝑧 ∈ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0 ↔ ∀𝑘 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0)) |
| 247 | 16, 243, 246 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0 ↔ ∀𝑘 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0)) |
| 248 | 247 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0 ↔ ∀𝑘 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0)) |
| 249 | 242, 248 | mpbird 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0) |
| 250 | | ffn 6736 |
. . . . . . . . . 10
⊢ (vol:dom
vol⟶(0[,]+∞) → vol Fn dom vol) |
| 251 | 4, 250 | ax-mp 5 |
. . . . . . . . 9
⊢ vol Fn
dom vol |
| 252 | 27 | frnd 6744 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ dom
vol) |
| 253 | 252 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ dom
vol) |
| 254 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑥 = (vol‘𝑧) → (𝑥 ≤ 0 ↔ (vol‘𝑧) ≤ 0)) |
| 255 | 254 | ralima 7257 |
. . . . . . . . 9
⊢ ((vol Fn
dom vol ∧ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ dom vol) →
(∀𝑥 ∈ (vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0)) |
| 256 | 251, 253,
255 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (∀𝑥 ∈ (vol “ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0)) |
| 257 | 249, 256 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → ∀𝑥 ∈ (vol “ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0) |
| 258 | | imassrn 6089 |
. . . . . . . . 9
⊢ (vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ⊆ ran
vol |
| 259 | | frn 6743 |
. . . . . . . . . . 11
⊢ (vol:dom
vol⟶(0[,]+∞) → ran vol ⊆
(0[,]+∞)) |
| 260 | 4, 259 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran vol
⊆ (0[,]+∞) |
| 261 | 260, 3 | sstri 3993 |
. . . . . . . . 9
⊢ ran vol
⊆ ℝ* |
| 262 | 258, 261 | sstri 3993 |
. . . . . . . 8
⊢ (vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ⊆
ℝ* |
| 263 | | supxrleub 13368 |
. . . . . . . 8
⊢ (((vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ⊆ ℝ*
∧ 0 ∈ ℝ*) → (sup((vol “ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, < )
≤ 0 ↔ ∀𝑥
∈ (vol “ ran (𝑛
∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0)) |
| 264 | 262, 38, 263 | mp2an 692 |
. . . . . . 7
⊢ (sup((vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, < )
≤ 0 ↔ ∀𝑥
∈ (vol “ ran (𝑛
∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0) |
| 265 | 257, 264 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → sup((vol “ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, < )
≤ 0) |
| 266 | 128, 265 | eqbrtrd 5165 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ≤ 0) |
| 267 | 8, 37, 39, 93, 266 | xrletrd 13204 |
. . . 4
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol‘𝐴) ≤ 0) |
| 268 | 267 | ex 412 |
. . 3
⊢ (𝜑 → (¬ 0 <
(∫2‘𝐹)
→ (vol‘𝐴) ≤
0)) |
| 269 | | xrlenlt 11326 |
. . . 4
⊢
(((vol‘𝐴)
∈ ℝ* ∧ 0 ∈ ℝ*) →
((vol‘𝐴) ≤ 0
↔ ¬ 0 < (vol‘𝐴))) |
| 270 | 7, 38, 269 | sylancl 586 |
. . 3
⊢ (𝜑 → ((vol‘𝐴) ≤ 0 ↔ ¬ 0 <
(vol‘𝐴))) |
| 271 | 268, 270 | sylibd 239 |
. 2
⊢ (𝜑 → (¬ 0 <
(∫2‘𝐹)
→ ¬ 0 < (vol‘𝐴))) |
| 272 | 1, 271 | mt4d 117 |
1
⊢ (𝜑 → 0 <
(∫2‘𝐹)) |