Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | itg1climres.4 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
4 | | i1frn 23444 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
6 | | difss 3737 |
. . . 4
⊢ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹 |
7 | | ssfi 8180 |
. . . 4
⊢ ((ran
𝐹 ∈ Fin ∧ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹) → (ran 𝐹 ∖ {0}) ∈
Fin) |
8 | 5, 6, 7 | sylancl 694 |
. . 3
⊢ (𝜑 → (ran 𝐹 ∖ {0}) ∈ Fin) |
9 | | 1zzd 11408 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 1 ∈
ℤ) |
10 | | i1fima 23445 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {𝑘}) ∈ dom vol) |
11 | 3, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ {𝑘}) ∈ dom vol) |
12 | 11 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ {𝑘}) ∈ dom vol) |
13 | | itg1climres.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴:ℕ⟶dom vol) |
14 | 13 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ dom vol) |
15 | 14 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ dom vol) |
16 | | inmbl 23310 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘𝑛) ∈ dom vol) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol) |
17 | 12, 15, 16 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol) |
18 | | mblvol 23298 |
. . . . . . . . 9
⊢ (((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
20 | | inss1 3833 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) |
21 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘})) |
22 | | mblss 23299 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑘}) ∈ dom vol → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
23 | 12, 22 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
24 | | mblvol 23298 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑘}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑘})) = (vol*‘(◡𝐹 “ {𝑘}))) |
25 | 12, 24 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(◡𝐹 “ {𝑘})) = (vol*‘(◡𝐹 “ {𝑘}))) |
26 | | i1fima2sn 23447 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
27 | 3, 26 | sylan 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
28 | 27 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
29 | 25, 28 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
30 | | ovolsscl 23254 |
. . . . . . . . 9
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) ∧ (◡𝐹 “ {𝑘}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑘})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
31 | 21, 23, 29, 30 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
32 | 19, 31 | eqeltrd 2701 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
33 | | eqid 2622 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
34 | 32, 33 | fmptd 6385 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))):ℕ⟶ℝ) |
35 | | itg1climres.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1))) |
36 | 35 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1))) |
37 | | sslin 3839 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1)) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
39 | 13 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴:ℕ⟶dom vol) |
40 | | peano2nn 11032 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
41 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:ℕ⟶dom vol ∧
(𝑛 + 1) ∈ ℕ)
→ (𝐴‘(𝑛 + 1)) ∈ dom
vol) |
42 | 39, 40, 41 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol) |
43 | | inmbl 23310 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘(𝑛 + 1)) ∈ dom vol) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol) |
44 | 12, 42, 43 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol) |
45 | | mblss 23299 |
. . . . . . . . . . . 12
⊢ (((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) |
47 | | ovolss 23253 |
. . . . . . . . . . 11
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∧ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
48 | 38, 46, 47 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
49 | | mblvol 23298 |
. . . . . . . . . . 11
⊢ (((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol →
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
50 | 44, 49 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
51 | 48, 19, 50 | 3brtr4d 4685 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
52 | 51 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
53 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (𝐴‘𝑛) = (𝐴‘𝑗)) |
54 | 53 | ineq2d 3814 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) |
55 | 54 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) |
56 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ∈ V |
57 | 55, 33, 56 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) |
58 | | peano2nn 11032 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
59 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → (𝐴‘𝑛) = (𝐴‘(𝑗 + 1))) |
60 | 59 | ineq2d 3814 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
61 | 60 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑗 + 1) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
62 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) ∈ V |
63 | 61, 33, 62 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
64 | 58, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
65 | 57, 64 | breq12d 4666 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))) |
66 | 65 | ralbiia 2979 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
67 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1)) |
68 | 67 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑗 + 1))) |
69 | 68 | ineq2d 3814 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
70 | 69 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
71 | 55, 70 | breq12d 4666 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → ((vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))) |
72 | 71 | cbvralv 3171 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
73 | 66, 72 | bitr4i 267 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
74 | 52, 73 | sylibr 224 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1))) |
75 | 74 | r19.21bi 2932 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1))) |
76 | | ovolss 23253 |
. . . . . . . . . . 11
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) ∧ (◡𝐹 “ {𝑘}) ⊆ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘(◡𝐹 “ {𝑘}))) |
77 | 20, 23, 76 | sylancr 695 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘(◡𝐹 “ {𝑘}))) |
78 | 77, 19, 25 | 3brtr4d 4685 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
79 | 78 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
80 | 57 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘})))) |
81 | 80 | ralbiia 2979 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
82 | 55 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → ((vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘})))) |
83 | 82 | cbvralv 3171 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
84 | 81, 83 | bitr4i 267 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑛 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
85 | 79, 84 | sylibr 224 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
86 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑥 = (vol‘(◡𝐹 “ {𝑘})) → (((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})))) |
87 | 86 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑥 = (vol‘(◡𝐹 “ {𝑘})) → (∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})))) |
88 | 87 | rspcev 3309 |
. . . . . . 7
⊢
(((vol‘(◡𝐹 “ {𝑘})) ∈ ℝ ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘}))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥) |
89 | 27, 85, 88 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥) |
90 | 1, 9, 34, 75, 89 | climsup 14400 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
91 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) |
92 | 17, 91 | fmptd 6385 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))):ℕ⟶dom vol) |
93 | 38 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
94 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢ (𝐴‘𝑗) ∈ V |
95 | 94 | inex2 4800 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ∈ V |
96 | 54, 91, 95 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) |
97 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢ (𝐴‘(𝑗 + 1)) ∈ V |
98 | 97 | inex2 4800 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))) ∈ V |
99 | 60, 91, 98 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
100 | 58, 99 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
101 | 96, 100 | sseq12d 3634 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
102 | 101 | ralbiia 2979 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
103 | 54, 69 | sseq12d 3634 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
104 | 103 | cbvralv 3171 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ∀𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
105 | 102, 104 | bitr4i 267 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
106 | 93, 105 | sylibr 224 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1))) |
107 | | volsup 23324 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))):ℕ⟶dom vol ∧
∀𝑗 ∈ ℕ
((𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1))) → (vol‘∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
108 | 92, 106, 107 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
109 | 96 | iuneq2i 4539 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ 𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) |
110 | 54 | cbviunv 4559 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ∪
𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) |
111 | | iunin2 4584 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) |
112 | 109, 110,
111 | 3eqtr2i 2650 |
. . . . . . . . 9
⊢ ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) |
113 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ (𝐴:ℕ⟶dom vol →
𝐴 Fn
ℕ) |
114 | | fniunfv 6505 |
. . . . . . . . . . . . . 14
⊢ (𝐴 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ∪ ran 𝐴) |
115 | 13, 113, 114 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ∪ ran 𝐴) |
116 | | itg1climres.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ ran 𝐴 = ℝ) |
117 | 115, 116 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ℝ) |
118 | 117 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ℝ) |
119 | 118 | ineq2d 3814 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ ℝ)) |
120 | 11 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) ∈ dom vol) |
121 | 120, 22 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
122 | | df-ss 3588 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑘}) ⊆ ℝ ↔ ((◡𝐹 “ {𝑘}) ∩ ℝ) = (◡𝐹 “ {𝑘})) |
123 | 121, 122 | sylib 208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ℝ) = (◡𝐹 “ {𝑘})) |
124 | 119, 123 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) = (◡𝐹 “ {𝑘})) |
125 | 112, 124 | syl5eq 2668 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = (◡𝐹 “ {𝑘})) |
126 | | ffn 6045 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))):ℕ⟶dom vol → (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) Fn ℕ) |
127 | | fniunfv 6505 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) Fn ℕ → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
128 | 92, 126, 127 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
129 | 125, 128 | eqtr3d 2658 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
130 | 129 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) = (vol‘∪
ran (𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
131 | | frn 6053 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))):ℕ⟶ℝ → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⊆ ℝ) |
132 | 34, 131 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⊆ ℝ) |
133 | | fdm 6051 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))):ℕ⟶ℝ → dom (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ℕ) |
134 | 34, 133 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ℕ) |
135 | | 1nn 11031 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
136 | | ne0i 3921 |
. . . . . . . . . . 11
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
137 | 135, 136 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ℕ ≠
∅) |
138 | 134, 137 | eqnetrd 2861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
139 | | dm0rn0 5342 |
. . . . . . . . . 10
⊢ (dom
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ∅) |
140 | 139 | necon3bii 2846 |
. . . . . . . . 9
⊢ (dom
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
141 | 138, 140 | sylib 208 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
142 | | ffn 6045 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) Fn ℕ) |
143 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
144 | 143 | ralrn 6362 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
145 | 34, 142, 144 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
146 | 145 | rexbidv 3052 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
147 | 89, 146 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥) |
148 | | supxrre 12157 |
. . . . . . . 8
⊢ ((ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup(ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
149 | 132, 141,
147, 148 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup(ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
150 | | rnco2 5642 |
. . . . . . . . 9
⊢ ran (vol
∘ (𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
151 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
152 | | volf 23297 |
. . . . . . . . . . . . 13
⊢ vol:dom
vol⟶(0[,]+∞) |
153 | 152 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → vol:dom
vol⟶(0[,]+∞)) |
154 | 153 | feqmptd 6249 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → vol = (𝑦 ∈ dom vol ↦
(vol‘𝑦))) |
155 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) → (vol‘𝑦) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
156 | 17, 151, 154, 155 | fmptco 6396 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol ∘ (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
157 | 156 | rneqd 5353 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (vol ∘
(𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
158 | 150, 157 | syl5reqr 2671 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
159 | 158 | supeq1d 8352 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup((vol
“ ran (𝑛 ∈
ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
160 | 149, 159 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < ) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
161 | 108, 130,
160 | 3eqtr4d 2666 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
162 | 90, 161 | breqtrrd 4681 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⇝ (vol‘(◡𝐹 “ {𝑘}))) |
163 | | i1ff 23443 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
164 | | frn 6053 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℝ →
ran 𝐹 ⊆
ℝ) |
165 | 3, 163, 164 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
166 | 165 | ssdifssd 3748 |
. . . . . 6
⊢ (𝜑 → (ran 𝐹 ∖ {0}) ⊆
ℝ) |
167 | 166 | sselda 3603 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ) |
168 | 167 | recnd 10068 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ) |
169 | | nnex 11026 |
. . . . . 6
⊢ ℕ
∈ V |
170 | 169 | mptex 6486 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ∈ V |
171 | 170 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ∈ V) |
172 | 34 | ffvelrnda 6359 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ∈ ℝ) |
173 | 172 | recnd 10068 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ∈ ℂ) |
174 | 55 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
175 | | eqid 2622 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) = (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
176 | | ovex 6678 |
. . . . . . 7
⊢ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) ∈ V |
177 | 174, 175,
176 | fvmpt 6282 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
178 | 57 | oveq2d 6666 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗)) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
179 | 177, 178 | eqtr4d 2659 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗))) |
180 | 179 | adantl 482 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗))) |
181 | 1, 9, 162, 168, 171, 173, 180 | climmulc2 14367 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ⇝ (𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
182 | 169 | mptex 6486 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ∈ V |
183 | 182 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ∈ V) |
184 | 167 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → 𝑘 ∈ ℝ) |
185 | 184, 32 | remulcld 10070 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ∈ ℝ) |
186 | 185, 175 | fmptd 6385 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))):ℕ⟶ℝ) |
187 | 186 | ffvelrnda 6359 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℝ) |
188 | 187 | recnd 10068 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℂ) |
189 | 188 | anasss 679 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ (ran 𝐹 ∖ {0}) ∧ 𝑗 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℂ) |
190 | 3 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 ∈ dom
∫1) |
191 | | itg1climres.5 |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
192 | 191 | i1fres 23472 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴‘𝑛) ∈ dom vol) → 𝐺 ∈ dom
∫1) |
193 | 190, 14, 192 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 ∈ dom
∫1) |
194 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ∈
Fin) |
195 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
196 | 3, 163, 195 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn ℝ) |
197 | 196 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 Fn ℝ) |
198 | | fnfvelrn 6356 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran 𝐹) |
199 | 197, 198 | sylan 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran 𝐹) |
200 | | i1f0rn 23449 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ dom ∫1
→ 0 ∈ ran 𝐹) |
201 | 3, 200 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ ran 𝐹) |
202 | 201 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ran 𝐹) |
203 | 199, 202 | ifcld 4131 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ ran 𝐹) |
204 | 203, 191 | fmptd 6385 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℝ⟶ran 𝐹) |
205 | | frn 6053 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ran 𝐹 → ran 𝐺 ⊆ ran 𝐹) |
206 | | ssdif 3745 |
. . . . . . . . 9
⊢ (ran
𝐺 ⊆ ran 𝐹 → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0})) |
207 | 204, 205,
206 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0})) |
208 | 165 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝐹 ⊆ ℝ) |
209 | 208 | ssdifd 3746 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ⊆ (ℝ
∖ {0})) |
210 | | itg1val2 23451 |
. . . . . . . 8
⊢ ((𝐺 ∈ dom ∫1
∧ ((ran 𝐹 ∖ {0})
∈ Fin ∧ (ran 𝐺
∖ {0}) ⊆ (ran 𝐹
∖ {0}) ∧ (ran 𝐹
∖ {0}) ⊆ (ℝ ∖ {0}))) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘})))) |
211 | 193, 194,
207, 209, 210 | syl13anc 1328 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘})))) |
212 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹‘𝑥) ∈ V |
213 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
V |
214 | 212, 213 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ V |
215 | 191 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ V) → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
216 | 214, 215 | mpan2 707 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
217 | 216 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
218 | 217 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘)) |
219 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0) |
220 | 219 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0) |
221 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0 ↔ 𝑘 ≠ 0)) |
222 | 220, 221 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0)) |
223 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑥 ∈ (𝐴‘𝑛) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 0) |
224 | 223 | necon1ai 2821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0 → 𝑥 ∈ (𝐴‘𝑛)) |
225 | 222, 224 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → 𝑥 ∈ (𝐴‘𝑛))) |
226 | 225 | pm4.71rd 667 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘))) |
227 | 218, 226 | bitrd 268 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘))) |
228 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴‘𝑛) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
229 | 228 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴‘𝑛) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 ↔ (𝐹‘𝑥) = 𝑘)) |
230 | 229 | pm5.32i 669 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘) ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ (𝐹‘𝑥) = 𝑘)) |
231 | | ancom 466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝐴‘𝑛) ∧ (𝐹‘𝑥) = 𝑘) ↔ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛))) |
232 | 230, 231 | bitri 264 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘) ↔ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛))) |
233 | 227, 232 | syl6bb 276 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
234 | 233 | pm5.32da 673 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛))))) |
235 | | anass 681 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)) ↔ (𝑥 ∈ ℝ ∧ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
236 | 234, 235 | syl6bbr 278 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
237 | | i1ff 23443 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
238 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:ℝ⟶ℝ →
𝐺 Fn
ℝ) |
239 | 193, 237,
238 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 Fn ℝ) |
240 | 239 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐺 Fn ℝ) |
241 | | fniniseg 6338 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Fn ℝ → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘))) |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘))) |
243 | | elin 3796 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ (𝑥 ∈ (◡𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴‘𝑛))) |
244 | 197 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐹 Fn ℝ) |
245 | | fniniseg 6338 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘))) |
246 | 244, 245 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘))) |
247 | 246 | anbi1d 741 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ (◡𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴‘𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
248 | 243, 247 | syl5bb 272 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
249 | 236, 242,
248 | 3bitr4d 300 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
250 | 249 | alrimiv 1855 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑥(𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
251 | | nfmpt1 4747 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
252 | 191, 251 | nfcxfr 2762 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝐺 |
253 | 252 | nfcnv 5301 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥◡𝐺 |
254 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥{𝑘} |
255 | 253, 254 | nfima 5474 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(◡𝐺 “ {𝑘}) |
256 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) |
257 | 255, 256 | cleqf 2790 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑘}) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ ∀𝑥(𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
258 | 250, 257 | sylibr 224 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐺 “ {𝑘}) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) |
259 | 258 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐺 “ {𝑘})) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
260 | 259 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(◡𝐺 “ {𝑘}))) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
261 | 260 | sumeq2dv 14433 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘}))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
262 | 211, 261 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
263 | 262 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))) |
264 | 263 | fveq1d 6193 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦
(∫1‘𝐺))‘𝑗) = ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
265 | 174 | sumeq2sdv 14435 |
. . . . . 6
⊢ (𝑛 = 𝑗 → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
266 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
267 | | sumex 14418 |
. . . . . 6
⊢
Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) ∈ V |
268 | 265, 266,
267 | fvmpt 6282 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
269 | 177 | sumeq2sdv 14435 |
. . . . 5
⊢ (𝑗 ∈ ℕ →
Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
270 | 268, 269 | eqtr4d 2659 |
. . . 4
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
271 | 264, 270 | sylan9eq 2676 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫1‘𝐺))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
272 | 1, 2, 8, 181, 183, 189, 271 | climfsum 14552 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ⇝ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
273 | | itg1val 23450 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
274 | 3, 273 | syl 17 |
. 2
⊢ (𝜑 →
(∫1‘𝐹)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
275 | 272, 274 | breqtrrd 4681 |
1
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ⇝ (∫1‘𝐹)) |