Step | Hyp | Ref
| Expression |
1 | | itg2gt0.2 |
. 2
⊢ (𝜑 → 0 < (vol‘𝐴)) |
2 | | itg2gt0.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ dom vol) |
3 | | iccssxr 12256 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
4 | | volf 23297 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
5 | 4 | ffvelrni 6358 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
6 | 3, 5 | sseldi 3601 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
ℝ*) |
7 | 2, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (vol‘𝐴) ∈
ℝ*) |
8 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol‘𝐴) ∈
ℝ*) |
9 | | itg2gt0.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
10 | | reex 10027 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V |
11 | | fex 6490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ ℝ ∈ V) → 𝐹 ∈ V) |
12 | 9, 10, 11 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ V) |
13 | | cnvexg 7112 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ◡𝐹 ∈ V) |
15 | | imaexg 7103 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹 ∈ V → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ V) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ V) |
17 | 16 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ V) |
18 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) = (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) |
19 | 17, 18 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶V) |
20 | | ffn 6045 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶V →
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ) |
22 | | fniunfv 6505 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ → ∪ 𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) |
24 | | itg2gt0.4 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ MblFn) |
25 | | rge0ssre 12280 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℝ |
26 | | fss 6056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ) |
27 | 9, 25, 26 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
28 | | mbfima 23399 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) →
(◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ dom
vol) |
29 | 24, 27, 28 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ dom
vol) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) ∈ dom
vol) |
31 | 30, 18 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶dom
vol) |
32 | 31 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol) |
33 | 32 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol) |
34 | | iunmbl 23321 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
ℕ ((𝑛 ∈ ℕ
↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol → ∪ 𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ∈ dom vol) |
36 | 23, 35 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (𝜑 → ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ∈ dom
vol) |
37 | | mblss 23299 |
. . . . . . . 8
⊢ (∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ∈ dom vol → ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆
ℝ) |
38 | 36, 37 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆
ℝ) |
39 | | ovolcl 23246 |
. . . . . . 7
⊢ (∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ ℝ →
(vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ∈
ℝ*) |
40 | 38, 39 | syl 17 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ∈
ℝ*) |
41 | 40 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ∈
ℝ*) |
42 | | 0xr 10086 |
. . . . . 6
⊢ 0 ∈
ℝ* |
43 | 42 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → 0 ∈
ℝ*) |
44 | | mblvol 23298 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) |
45 | 2, 44 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (vol‘𝐴) = (vol*‘𝐴)) |
46 | | mblss 23299 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
47 | 2, 46 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
48 | 47 | sselda 3603 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
49 | 9 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
50 | | elrege0 12278 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
51 | 49, 50 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
52 | 51 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
53 | 48, 52 | syldan 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
54 | | itg2gt0.5 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 < (𝐹‘𝑥)) |
55 | | nnrecl 11290 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 0 < (𝐹‘𝑥)) → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝐹‘𝑥)) |
56 | 53, 54, 55 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝐹‘𝑥)) |
57 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:ℝ⟶(0[,)+∞)
→ 𝐹 Fn
ℝ) |
58 | 9, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 Fn ℝ) |
59 | 58 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝐹 Fn ℝ) |
60 | | elpreima 6337 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)))) |
62 | 48 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ ℝ) |
63 | 62 | biantrurd 529 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)))) |
64 | | nnrecre 11057 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
65 | 64 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ) |
66 | 65 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ*) |
67 | 66 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ*) |
68 | | elioopnf 12267 |
. . . . . . . . . . . . . . . 16
⊢ ((1 /
𝑘) ∈
ℝ* → ((𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)))) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)))) |
70 | 61, 63, 69 | 3bitr2d 296 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)))) |
71 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ) |
72 | | imaexg 7103 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹 ∈ V → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) |
73 | 14, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) |
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) |
75 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
76 | 75 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((1 / 𝑛)(,)+∞) = ((1 / 𝑘)(,)+∞)) |
77 | 76 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
78 | 77, 18 | fvmptg 6280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
79 | 71, 74, 78 | syl2anr 495 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
80 | 79 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ↔ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)))) |
81 | 53 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑥) ∈ ℝ) |
82 | 81 | biantrurd 529 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘) < (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)))) |
83 | 70, 80, 82 | 3bitr4rd 301 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘) < (𝐹‘𝑥) ↔ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
84 | 83 | rexbidva 3049 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑘 ∈ ℕ (1 / 𝑘) < (𝐹‘𝑥) ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
85 | 56, 84 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) |
86 | 85 | ex 450 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
87 | | eluni2 4440 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ↔ ∃𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))𝑥 ∈ 𝑧) |
88 | | eleq2 2690 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
89 | 88 | rexrn 6361 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ →
(∃𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))𝑥 ∈ 𝑧 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
90 | 21, 89 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))𝑥 ∈ 𝑧 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
91 | 87, 90 | syl5bb 272 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ∪ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞))) ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
92 | 86, 91 | sylibrd 249 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
93 | 92 | ssrdv 3609 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))) |
94 | | ovolss 23253 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ∧ ∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ ℝ) →
(vol*‘𝐴) ≤
(vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
95 | 93, 38, 94 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (vol*‘𝐴) ≤ (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
96 | 45, 95 | eqbrtrd 4675 |
. . . . . 6
⊢ (𝜑 → (vol‘𝐴) ≤ (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
97 | 96 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol‘𝐴) ≤ (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
98 | | mblvol 23298 |
. . . . . . . . 9
⊢ (∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ∈ dom vol →
(vol‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
99 | 36, 98 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (vol‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))) |
100 | | peano2nn 11032 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
101 | 100 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
102 | | nnrecre 11057 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 + 1) ∈ ℕ → (1 /
(𝑘 + 1)) ∈
ℝ) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / (𝑘 + 1)) ∈
ℝ) |
104 | 103 | rexrd 10089 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / (𝑘 + 1)) ∈
ℝ*) |
105 | | nnre 11027 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
106 | 105 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ) |
107 | 106 | lep1d 10955 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (𝑘 + 1)) |
108 | | nngt0 11049 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
109 | 108 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < 𝑘) |
110 | 101 | nnred 11035 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ) |
111 | 101 | nngt0d 11064 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < (𝑘 + 1)) |
112 | | lerec 10906 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℝ ∧ 0 <
𝑘) ∧ ((𝑘 + 1) ∈ ℝ ∧ 0
< (𝑘 + 1))) →
(𝑘 ≤ (𝑘 + 1) ↔ (1 / (𝑘 + 1)) ≤ (1 / 𝑘))) |
113 | 106, 109,
110, 111, 112 | syl22anc 1327 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 ≤ (𝑘 + 1) ↔ (1 / (𝑘 + 1)) ≤ (1 / 𝑘))) |
114 | 107, 113 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / (𝑘 + 1)) ≤ (1 / 𝑘)) |
115 | | iooss1 12210 |
. . . . . . . . . . . . 13
⊢ (((1 /
(𝑘 + 1)) ∈
ℝ* ∧ (1 / (𝑘 + 1)) ≤ (1 / 𝑘)) → ((1 / 𝑘)(,)+∞) ⊆ ((1 / (𝑘 +
1))(,)+∞)) |
116 | 104, 114,
115 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘)(,)+∞) ⊆ ((1 /
(𝑘 +
1))(,)+∞)) |
117 | | imass2 5501 |
. . . . . . . . . . . 12
⊢ (((1 /
𝑘)(,)+∞) ⊆ ((1
/ (𝑘 + 1))(,)+∞)
→ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ⊆ (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ⊆ (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
119 | 71, 73, 78 | syl2anr 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
120 | | imaexg 7103 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 ∈ V → (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞)) ∈
V) |
121 | 14, 120 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞)) ∈
V) |
122 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1))) |
123 | 122 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑘 + 1) → ((1 / 𝑛)(,)+∞) = ((1 / (𝑘 + 1))(,)+∞)) |
124 | 123 | imaeq2d 5466 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑘 + 1) → (◡𝐹 “ ((1 / 𝑛)(,)+∞)) = (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
125 | 124, 18 | fvmptg 6280 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) ∈ ℕ ∧
(◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞)) ∈ V) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1)) = (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
126 | 100, 121,
125 | syl2anr 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1)) = (◡𝐹 “ ((1 / (𝑘 + 1))(,)+∞))) |
127 | 118, 119,
126 | 3sstr4d 3648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ⊆ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1))) |
128 | 127 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ⊆ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1))) |
129 | | volsup 23324 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶dom vol ∧
∀𝑘 ∈ ℕ
((𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) ⊆ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘(𝑘 + 1))) → (vol‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, <
)) |
130 | 31, 128, 129 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (vol‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, <
)) |
131 | 99, 130 | eqtr3d 2658 |
. . . . . . 7
⊢ (𝜑 → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, <
)) |
132 | 131 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, <
)) |
133 | 73 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ V) |
134 | 71, 133, 78 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) = (◡𝐹 “ ((1 / 𝑘)(,)+∞))) |
135 | 134 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) ∧ 𝑘 ∈ ℕ) → (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) = (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞)))) |
136 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 0 ∈
ℝ*) |
137 | | nnrecgt0 11058 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ℕ → 0 < (1
/ 𝑘)) |
138 | 137 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < (1 / 𝑘)) |
139 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
ℝ |
140 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((0
∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) → (0 < (1 / 𝑘) → 0 ≤ (1 / 𝑘))) |
141 | 139, 65, 140 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0 < (1 / 𝑘) → 0 ≤ (1 / 𝑘))) |
142 | 138, 141 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 / 𝑘)) |
143 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1 /
𝑘) ∈ (0[,]+∞)
↔ ((1 / 𝑘) ∈
ℝ* ∧ 0 ≤ (1 / 𝑘))) |
144 | 66, 142, 143 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
(0[,]+∞)) |
145 | | 0e0iccpnf 12283 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
(0[,]+∞) |
146 | | ifcl 4130 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((1 /
𝑘) ∈ (0[,]+∞)
∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ (0[,]+∞)) |
147 | 144, 145,
146 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ (0[,]+∞)) |
148 | 147 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ (0[,]+∞)) |
149 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) |
150 | 148, 149 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘),
0)):ℝ⟶(0[,]+∞)) |
151 | 150 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘),
0)):ℝ⟶(0[,]+∞)) |
152 | | itg2cl 23499 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈
ℝ*) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈
ℝ*) |
154 | | icossicc 12260 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
155 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞)) |
156 | 9, 154, 155 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
157 | | itg2cl 23499 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (∫2‘𝐹) ∈
ℝ*) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ*) |
159 | 158 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) →
(∫2‘𝐹)
∈ ℝ*) |
160 | | 0nrp 11865 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬ 0
∈ ℝ+ |
161 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
162 | 119, 32 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom
vol) |
163 | 162 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom
vol) |
164 | 163 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom
vol) |
165 | 161, 139 | syl6eqelr 2710 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈ ℝ) |
166 | 65, 138 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ+) |
167 | 166 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (1 / 𝑘) ∈
ℝ+) |
168 | 167 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (1 / 𝑘) ∈
ℝ+) |
169 | | itg2const2 23508 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom vol ∧ (1 /
𝑘) ∈
ℝ+) → ((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈ ℝ)) |
170 | 164, 168,
169 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → ((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∈ ℝ)) |
171 | 165, 170 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
ℝ) |
172 | | elrege0 12278 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1 /
𝑘) ∈ (0[,)+∞)
↔ ((1 / 𝑘) ∈
ℝ ∧ 0 ≤ (1 / 𝑘))) |
173 | 65, 142, 172 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
(0[,)+∞)) |
174 | 173 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (1 / 𝑘) ∈
(0[,)+∞)) |
175 | 174 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (1 / 𝑘) ∈ (0[,)+∞)) |
176 | | itg2const 23507 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom vol ∧
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈ ℝ ∧ (1 /
𝑘) ∈ (0[,)+∞))
→ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) = ((1 / 𝑘) · (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
177 | 164, 171,
175, 176 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) = ((1 / 𝑘) · (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
178 | 161, 177 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → 0 = ((1 / 𝑘) · (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
179 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → 0 < (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞)))) |
180 | 171, 179 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
ℝ+) |
181 | 168, 180 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → ((1 / 𝑘) · (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞)))) ∈
ℝ+) |
182 | 178, 181 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) ∧ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) → 0 ∈
ℝ+) |
183 | 182 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) → 0 ∈
ℝ+)) |
184 | 160, 183 | mtoi 190 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → ¬ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
185 | | itg2ge0 23502 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)):ℝ⟶(0[,]+∞) → 0
≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
186 | 151, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 0 ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
187 | | xrleloe 11977 |
. . . . . . . . . . . . . . . . . . . . 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)))))) |
188 | 42, 153, 187 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (0 ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ↔ (0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∨ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))))) |
189 | 186, 188 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ∨ 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))))) |
190 | 189 | ord 392 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (¬ 0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) → 0 =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))))) |
191 | 184, 190 | mt3d 140 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 0 <
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)))) |
192 | 156 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 𝐹:ℝ⟶(0[,]+∞)) |
193 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (1 / 𝑘) ∈
ℝ) |
194 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹 Fn ℝ) |
195 | 194, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)))) |
196 | 195 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞))) |
197 | 196 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → 𝑥 ∈ ℝ) |
198 | 52 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
199 | 197, 198 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (𝐹‘𝑥) ∈ ℝ) |
200 | 66 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (1 / 𝑘) ∈
ℝ*) |
201 | 196 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞)) |
202 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (1 / 𝑘) < (𝐹‘𝑥)) → (1 / 𝑘) < (𝐹‘𝑥)) |
203 | 68, 202 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1 /
𝑘) ∈
ℝ* → ((𝐹‘𝑥) ∈ ((1 / 𝑘)(,)+∞) → (1 / 𝑘) < (𝐹‘𝑥))) |
204 | 200, 201,
203 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (1 / 𝑘) < (𝐹‘𝑥)) |
205 | 193, 199,
204 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → (1 / 𝑘) ≤ (𝐹‘𝑥)) |
206 | 51 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
207 | 206 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
208 | 197, 207 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → 0 ≤ (𝐹‘𝑥)) |
209 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1 /
𝑘) = if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) → ((1 / 𝑘) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥))) |
210 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 =
if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥))) |
211 | 209, 210 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((1 /
𝑘) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
212 | 205, 208,
211 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
213 | 212 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
214 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) = 0) |
215 | 214 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) = 0) |
216 | 207 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → 0 ≤ (𝐹‘𝑥)) |
217 | 215, 216 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞))) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
218 | 213, 217 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
219 | 218 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
220 | 219 | adantrr 753 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) |
221 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ℝ ∈
V) |
222 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 /
𝑘) ∈
V |
223 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
V |
224 | 222, 223 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ V |
225 | 224 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ∈ V) |
226 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ V) |
227 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) |
228 | 9 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
229 | 221, 225,
226, 227, 228 | ofrfval2 6915 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥))) |
230 | 229 | biimpar 502 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0) ≤ (𝐹‘𝑥)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) ∘𝑟 ≤ 𝐹) |
231 | 220, 230 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) ∘𝑟 ≤ 𝐹) |
232 | | itg2le 23506 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)):ℝ⟶(0[,]+∞) ∧
𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0)) ∘𝑟 ≤ 𝐹) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ≤ (∫2‘𝐹)) |
233 | 151, 192,
231, 232 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (◡𝐹 “ ((1 / 𝑘)(,)+∞)), (1 / 𝑘), 0))) ≤ (∫2‘𝐹)) |
234 | 136, 153,
159, 191, 233 | xrltletrd 11992 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) → 0 <
(∫2‘𝐹)) |
235 | 234 | expr 643 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) → 0 <
(∫2‘𝐹))) |
236 | 235 | con3d 148 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (¬ 0 <
(∫2‘𝐹)
→ ¬ 0 < (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
237 | 4 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom vol →
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
(0[,]+∞)) |
238 | 3, 237 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐹 “ ((1 / 𝑘)(,)+∞)) ∈ dom vol →
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
ℝ*) |
239 | 162, 238 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈
ℝ*) |
240 | | xrlenlt 10103 |
. . . . . . . . . . . . . . 15
⊢
(((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ∈ ℝ*
∧ 0 ∈ ℝ*) → ((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0 ↔ ¬ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
241 | 239, 42, 240 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0 ↔ ¬ 0 <
(vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))))) |
242 | 236, 241 | sylibrd 249 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (¬ 0 <
(∫2‘𝐹)
→ (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0)) |
243 | 242 | imp 445 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ 0 <
(∫2‘𝐹)) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0) |
244 | 243 | an32s 846 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) ∧ 𝑘 ∈ ℕ) → (vol‘(◡𝐹 “ ((1 / 𝑘)(,)+∞))) ≤ 0) |
245 | 135, 244 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) ∧ 𝑘 ∈ ℕ) → (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0) |
246 | 245 | ralrimiva 2966 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → ∀𝑘 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0) |
247 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) → (vol‘𝑧) = (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘))) |
248 | 247 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘) → ((vol‘𝑧) ≤ 0 ↔ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0)) |
249 | 248 | ralrn 6362 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) Fn ℕ →
(∀𝑧 ∈ ran
(𝑛 ∈ ℕ ↦
(◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0 ↔ ∀𝑘 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0)) |
250 | 19, 20, 249 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0 ↔ ∀𝑘 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0)) |
251 | 250 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0 ↔ ∀𝑘 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))‘𝑘)) ≤ 0)) |
252 | 246, 251 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0) |
253 | | ffn 6045 |
. . . . . . . . . 10
⊢ (vol:dom
vol⟶(0[,]+∞) → vol Fn dom vol) |
254 | 4, 253 | ax-mp 5 |
. . . . . . . . 9
⊢ vol Fn
dom vol |
255 | | frn 6053 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))):ℕ⟶dom vol →
ran (𝑛 ∈ ℕ
↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ dom
vol) |
256 | 31, 255 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ dom
vol) |
257 | 256 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ dom
vol) |
258 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑥 = (vol‘𝑧) → (𝑥 ≤ 0 ↔ (vol‘𝑧) ≤ 0)) |
259 | 258 | ralima 6498 |
. . . . . . . . 9
⊢ ((vol Fn
dom vol ∧ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))) ⊆ dom vol) →
(∀𝑥 ∈ (vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0)) |
260 | 254, 257,
259 | sylancr 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (∀𝑥 ∈ (vol “ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))(vol‘𝑧) ≤ 0)) |
261 | 252, 260 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → ∀𝑥 ∈ (vol “ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0) |
262 | | imassrn 5477 |
. . . . . . . . 9
⊢ (vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ⊆ ran
vol |
263 | | frn 6053 |
. . . . . . . . . . 11
⊢ (vol:dom
vol⟶(0[,]+∞) → ran vol ⊆
(0[,]+∞)) |
264 | 4, 263 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran vol
⊆ (0[,]+∞) |
265 | 264, 3 | sstri 3612 |
. . . . . . . . 9
⊢ ran vol
⊆ ℝ* |
266 | 262, 265 | sstri 3612 |
. . . . . . . 8
⊢ (vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ⊆
ℝ* |
267 | | supxrleub 12156 |
. . . . . . . 8
⊢ (((vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ⊆ ℝ*
∧ 0 ∈ ℝ*) → (sup((vol “ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, < )
≤ 0 ↔ ∀𝑥
∈ (vol “ ran (𝑛
∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0)) |
268 | 266, 42, 267 | mp2an 708 |
. . . . . . 7
⊢ (sup((vol
“ ran (𝑛 ∈
ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, < )
≤ 0 ↔ ∀𝑥
∈ (vol “ ran (𝑛
∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞))))𝑥 ≤ 0) |
269 | 261, 268 | sylibr 224 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → sup((vol “ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))), ℝ*, < )
≤ 0) |
270 | 132, 269 | eqbrtrd 4675 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol*‘∪ ran (𝑛 ∈ ℕ ↦ (◡𝐹 “ ((1 / 𝑛)(,)+∞)))) ≤ 0) |
271 | 8, 41, 43, 97, 270 | xrletrd 11993 |
. . . 4
⊢ ((𝜑 ∧ ¬ 0 <
(∫2‘𝐹)) → (vol‘𝐴) ≤ 0) |
272 | 271 | ex 450 |
. . 3
⊢ (𝜑 → (¬ 0 <
(∫2‘𝐹)
→ (vol‘𝐴) ≤
0)) |
273 | | xrlenlt 10103 |
. . . 4
⊢
(((vol‘𝐴)
∈ ℝ* ∧ 0 ∈ ℝ*) →
((vol‘𝐴) ≤ 0
↔ ¬ 0 < (vol‘𝐴))) |
274 | 7, 42, 273 | sylancl 694 |
. . 3
⊢ (𝜑 → ((vol‘𝐴) ≤ 0 ↔ ¬ 0 <
(vol‘𝐴))) |
275 | 272, 274 | sylibd 229 |
. 2
⊢ (𝜑 → (¬ 0 <
(∫2‘𝐹)
→ ¬ 0 < (vol‘𝐴))) |
276 | 1, 275 | mt4d 152 |
1
⊢ (𝜑 → 0 <
(∫2‘𝐹)) |