Step | Hyp | Ref
| Expression |
1 | | nnuz 12806 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 12534 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | itg1climres.4 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
4 | | i1frn 25041 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
6 | | difss 4091 |
. . . 4
⊢ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹 |
7 | | ssfi 9117 |
. . . 4
⊢ ((ran
𝐹 ∈ Fin ∧ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹) → (ran 𝐹 ∖ {0}) ∈
Fin) |
8 | 5, 6, 7 | sylancl 586 |
. . 3
⊢ (𝜑 → (ran 𝐹 ∖ {0}) ∈ Fin) |
9 | | 1zzd 12534 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 1 ∈
ℤ) |
10 | | i1fima 25042 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {𝑘}) ∈ dom vol) |
11 | 3, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ {𝑘}) ∈ dom vol) |
12 | 11 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ {𝑘}) ∈ dom vol) |
13 | | itg1climres.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴:ℕ⟶dom vol) |
14 | 13 | ffvelcdmda 7035 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ dom vol) |
15 | 14 | adantlr 713 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ dom vol) |
16 | | inmbl 24906 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘𝑛) ∈ dom vol) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol) |
17 | 12, 15, 16 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol) |
18 | | mblvol 24894 |
. . . . . . . . 9
⊢ (((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
20 | | inss1 4188 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) |
21 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘})) |
22 | | mblss 24895 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑘}) ∈ dom vol → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
23 | 12, 22 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
24 | | mblvol 24894 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑘}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑘})) = (vol*‘(◡𝐹 “ {𝑘}))) |
25 | 12, 24 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(◡𝐹 “ {𝑘})) = (vol*‘(◡𝐹 “ {𝑘}))) |
26 | | i1fima2sn 25044 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
27 | 3, 26 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
28 | 27 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
29 | 25, 28 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
30 | | ovolsscl 24850 |
. . . . . . . . 9
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) ∧ (◡𝐹 “ {𝑘}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑘})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
31 | 21, 23, 29, 30 | syl3anc 1371 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
32 | 19, 31 | eqeltrd 2838 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
33 | 32 | fmpttd 7063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))):ℕ⟶ℝ) |
34 | | itg1climres.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1))) |
35 | 34 | adantlr 713 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1))) |
36 | | sslin 4194 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1)) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
38 | 13 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴:ℕ⟶dom vol) |
39 | | peano2nn 12165 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
40 | | ffvelcdm 7032 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:ℕ⟶dom vol ∧
(𝑛 + 1) ∈ ℕ)
→ (𝐴‘(𝑛 + 1)) ∈ dom
vol) |
41 | 38, 39, 40 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol) |
42 | | inmbl 24906 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘(𝑛 + 1)) ∈ dom vol) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol) |
43 | 12, 41, 42 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol) |
44 | | mblss 24895 |
. . . . . . . . . . . 12
⊢ (((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) |
46 | | ovolss 24849 |
. . . . . . . . . . 11
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∧ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
47 | 37, 45, 46 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
48 | | mblvol 24894 |
. . . . . . . . . . 11
⊢ (((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol →
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
49 | 43, 48 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
50 | 47, 19, 49 | 3brtr4d 5137 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
51 | 50 | ralrimiva 3143 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
52 | | fveq2 6842 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (𝐴‘𝑛) = (𝐴‘𝑗)) |
53 | 52 | ineq2d 4172 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) |
54 | 53 | fveq2d 6846 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) |
55 | | eqid 2736 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
56 | | fvex 6855 |
. . . . . . . . . . . 12
⊢
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ∈ V |
57 | 54, 55, 56 | fvmpt 6948 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) |
58 | | peano2nn 12165 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
59 | | fveq2 6842 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → (𝐴‘𝑛) = (𝐴‘(𝑗 + 1))) |
60 | 59 | ineq2d 4172 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
61 | 60 | fveq2d 6846 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑗 + 1) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
62 | | fvex 6855 |
. . . . . . . . . . . . 13
⊢
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) ∈ V |
63 | 61, 55, 62 | fvmpt 6948 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
64 | 58, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
65 | 57, 64 | breq12d 5118 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))) |
66 | 65 | ralbiia 3094 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
67 | | fvoveq1 7380 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑗 + 1))) |
68 | 67 | ineq2d 4172 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
69 | 68 | fveq2d 6846 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
70 | 54, 69 | breq12d 5118 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → ((vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))) |
71 | 70 | cbvralvw 3225 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
72 | 66, 71 | bitr4i 277 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
73 | 51, 72 | sylibr 233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1))) |
74 | 73 | r19.21bi 3234 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1))) |
75 | | ovolss 24849 |
. . . . . . . . . . 11
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) ∧ (◡𝐹 “ {𝑘}) ⊆ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘(◡𝐹 “ {𝑘}))) |
76 | 20, 23, 75 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘(◡𝐹 “ {𝑘}))) |
77 | 76, 19, 25 | 3brtr4d 5137 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
78 | 77 | ralrimiva 3143 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
79 | 57 | breq1d 5115 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘})))) |
80 | 79 | ralbiia 3094 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
81 | 54 | breq1d 5115 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → ((vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘})))) |
82 | 81 | cbvralvw 3225 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
83 | 80, 82 | bitr4i 277 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑛 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
84 | 78, 83 | sylibr 233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
85 | | brralrspcev 5165 |
. . . . . . 7
⊢
(((vol‘(◡𝐹 “ {𝑘})) ∈ ℝ ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘}))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥) |
86 | 27, 84, 85 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥) |
87 | 1, 9, 33, 74, 86 | climsup 15554 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
88 | 17 | fmpttd 7063 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))):ℕ⟶dom vol) |
89 | 37 | ralrimiva 3143 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
90 | | eqid 2736 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) |
91 | | fvex 6855 |
. . . . . . . . . . . . 13
⊢ (𝐴‘𝑗) ∈ V |
92 | 91 | inex2 5275 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ∈ V |
93 | 53, 90, 92 | fvmpt 6948 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) |
94 | | fvex 6855 |
. . . . . . . . . . . . . 14
⊢ (𝐴‘(𝑗 + 1)) ∈ V |
95 | 94 | inex2 5275 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))) ∈ V |
96 | 60, 90, 95 | fvmpt 6948 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
97 | 58, 96 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
98 | 93, 97 | sseq12d 3977 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
99 | 98 | ralbiia 3094 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
100 | 53, 68 | sseq12d 3977 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
101 | 100 | cbvralvw 3225 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ∀𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
102 | 99, 101 | bitr4i 277 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
103 | 89, 102 | sylibr 233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1))) |
104 | | volsup 24920 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))):ℕ⟶dom vol ∧
∀𝑗 ∈ ℕ
((𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1))) → (vol‘∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
105 | 88, 103, 104 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = sup((vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
106 | 93 | iuneq2i 4975 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ 𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) |
107 | 53 | cbviunv 5000 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ∪
𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) |
108 | | iunin2 5031 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) |
109 | 106, 107,
108 | 3eqtr2i 2770 |
. . . . . . . . 9
⊢ ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) |
110 | | ffn 6668 |
. . . . . . . . . . . . . 14
⊢ (𝐴:ℕ⟶dom vol →
𝐴 Fn
ℕ) |
111 | | fniunfv 7194 |
. . . . . . . . . . . . . 14
⊢ (𝐴 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ∪ ran 𝐴) |
112 | 13, 110, 111 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ∪ ran 𝐴) |
113 | | itg1climres.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ ran 𝐴 = ℝ) |
114 | 112, 113 | eqtrd 2776 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ℝ) |
115 | 114 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ℝ) |
116 | 115 | ineq2d 4172 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ ℝ)) |
117 | 11 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) ∈ dom vol) |
118 | 117, 22 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
119 | | df-ss 3927 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑘}) ⊆ ℝ ↔ ((◡𝐹 “ {𝑘}) ∩ ℝ) = (◡𝐹 “ {𝑘})) |
120 | 118, 119 | sylib 217 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ℝ) = (◡𝐹 “ {𝑘})) |
121 | 116, 120 | eqtrd 2776 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) = (◡𝐹 “ {𝑘})) |
122 | 109, 121 | eqtrid 2788 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = (◡𝐹 “ {𝑘})) |
123 | | ffn 6668 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))):ℕ⟶dom vol → (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) Fn ℕ) |
124 | | fniunfv 7194 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) Fn ℕ → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
125 | 88, 123, 124 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
126 | 122, 125 | eqtr3d 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
127 | 126 | fveq2d 6846 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) = (vol‘∪
ran (𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
128 | 33 | frnd 6676 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⊆ ℝ) |
129 | 33 | fdmd 6679 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ℕ) |
130 | | 1nn 12164 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
131 | | ne0i 4294 |
. . . . . . . . . . 11
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
132 | 130, 131 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ℕ ≠
∅) |
133 | 129, 132 | eqnetrd 3011 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
134 | | dm0rn0 5880 |
. . . . . . . . . 10
⊢ (dom
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ∅) |
135 | 134 | necon3bii 2996 |
. . . . . . . . 9
⊢ (dom
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
136 | 133, 135 | sylib 217 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
137 | | ffn 6668 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) Fn ℕ) |
138 | | breq1 5108 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
139 | 138 | ralrn 7038 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
140 | 33, 137, 139 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
141 | 140 | rexbidv 3175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
142 | 86, 141 | mpbird 256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥) |
143 | | supxrre 13246 |
. . . . . . . 8
⊢ ((ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup(ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
144 | 128, 136,
142, 143 | syl3anc 1371 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup(ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
145 | | volf 24893 |
. . . . . . . . . . . 12
⊢ vol:dom
vol⟶(0[,]+∞) |
146 | 145 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → vol:dom
vol⟶(0[,]+∞)) |
147 | 146, 17 | cofmpt 7078 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol ∘ (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
148 | 147 | rneqd 5893 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (vol ∘
(𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
149 | | rnco2 6205 |
. . . . . . . . 9
⊢ ran (vol
∘ (𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
150 | 148, 149 | eqtr3di 2791 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
151 | 150 | supeq1d 9382 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup((vol
“ ran (𝑛 ∈
ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
152 | 144, 151 | eqtr3d 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < ) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
153 | 105, 127,
152 | 3eqtr4d 2786 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
154 | 87, 153 | breqtrrd 5133 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⇝ (vol‘(◡𝐹 “ {𝑘}))) |
155 | | i1ff 25040 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
156 | | frn 6675 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℝ →
ran 𝐹 ⊆
ℝ) |
157 | 3, 155, 156 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
158 | 157 | ssdifssd 4102 |
. . . . . 6
⊢ (𝜑 → (ran 𝐹 ∖ {0}) ⊆
ℝ) |
159 | 158 | sselda 3944 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ) |
160 | 159 | recnd 11183 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ) |
161 | | nnex 12159 |
. . . . . 6
⊢ ℕ
∈ V |
162 | 161 | mptex 7173 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ∈ V |
163 | 162 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ∈ V) |
164 | 33 | ffvelcdmda 7035 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ∈ ℝ) |
165 | 164 | recnd 11183 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ∈ ℂ) |
166 | 54 | oveq2d 7373 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
167 | | eqid 2736 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) = (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
168 | | ovex 7390 |
. . . . . . 7
⊢ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) ∈ V |
169 | 166, 167,
168 | fvmpt 6948 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
170 | 57 | oveq2d 7373 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗)) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
171 | 169, 170 | eqtr4d 2779 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗))) |
172 | 171 | adantl 482 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗))) |
173 | 1, 9, 154, 160, 163, 165, 172 | climmulc2 15519 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ⇝ (𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
174 | 161 | mptex 7173 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ∈ V |
175 | 174 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ∈ V) |
176 | 159 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → 𝑘 ∈ ℝ) |
177 | 176, 32 | remulcld 11185 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ∈ ℝ) |
178 | 177 | fmpttd 7063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))):ℕ⟶ℝ) |
179 | 178 | ffvelcdmda 7035 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℝ) |
180 | 179 | recnd 11183 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℂ) |
181 | 180 | anasss 467 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ (ran 𝐹 ∖ {0}) ∧ 𝑗 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℂ) |
182 | 3 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 ∈ dom
∫1) |
183 | | itg1climres.5 |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
184 | 183 | i1fres 25070 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴‘𝑛) ∈ dom vol) → 𝐺 ∈ dom
∫1) |
185 | 182, 14, 184 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 ∈ dom
∫1) |
186 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ∈
Fin) |
187 | | ffn 6668 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
188 | 3, 155, 187 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn ℝ) |
189 | 188 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 Fn ℝ) |
190 | | fnfvelrn 7031 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran 𝐹) |
191 | 189, 190 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran 𝐹) |
192 | | i1f0rn 25046 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ dom ∫1
→ 0 ∈ ran 𝐹) |
193 | 3, 192 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ ran 𝐹) |
194 | 193 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ran 𝐹) |
195 | 191, 194 | ifcld 4532 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ ran 𝐹) |
196 | 195, 183 | fmptd 7062 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℝ⟶ran 𝐹) |
197 | | frn 6675 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ran 𝐹 → ran 𝐺 ⊆ ran 𝐹) |
198 | | ssdif 4099 |
. . . . . . . . 9
⊢ (ran
𝐺 ⊆ ran 𝐹 → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0})) |
199 | 196, 197,
198 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0})) |
200 | 157 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝐹 ⊆ ℝ) |
201 | 200 | ssdifd 4100 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ⊆ (ℝ
∖ {0})) |
202 | | itg1val2 25048 |
. . . . . . . 8
⊢ ((𝐺 ∈ dom ∫1
∧ ((ran 𝐹 ∖ {0})
∈ Fin ∧ (ran 𝐺
∖ {0}) ⊆ (ran 𝐹
∖ {0}) ∧ (ran 𝐹
∖ {0}) ⊆ (ℝ ∖ {0}))) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘})))) |
203 | 185, 186,
199, 201, 202 | syl13anc 1372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘})))) |
204 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹‘𝑥) ∈ V |
205 | | c0ex 11149 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
V |
206 | 204, 205 | ifex 4536 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ V |
207 | 183 | fvmpt2 6959 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ V) → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
208 | 206, 207 | mpan2 689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
209 | 208 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
210 | 209 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘)) |
211 | | eldifsni 4750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0) |
212 | 211 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0) |
213 | | neeq1 3006 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0 ↔ 𝑘 ≠ 0)) |
214 | 212, 213 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0)) |
215 | | iffalse 4495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑥 ∈ (𝐴‘𝑛) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 0) |
216 | 215 | necon1ai 2971 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0 → 𝑥 ∈ (𝐴‘𝑛)) |
217 | 214, 216 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → 𝑥 ∈ (𝐴‘𝑛))) |
218 | 217 | pm4.71rd 563 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘))) |
219 | 210, 218 | bitrd 278 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘))) |
220 | | iftrue 4492 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴‘𝑛) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
221 | 220 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴‘𝑛) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 ↔ (𝐹‘𝑥) = 𝑘)) |
222 | 221 | pm5.32i 575 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘) ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ (𝐹‘𝑥) = 𝑘)) |
223 | 222 | biancomi 463 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘) ↔ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛))) |
224 | 219, 223 | bitrdi 286 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
225 | 224 | pm5.32da 579 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛))))) |
226 | | anass 469 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)) ↔ (𝑥 ∈ ℝ ∧ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
227 | 225, 226 | bitr4di 288 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
228 | | i1ff 25040 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
229 | | ffn 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:ℝ⟶ℝ →
𝐺 Fn
ℝ) |
230 | 185, 228,
229 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 Fn ℝ) |
231 | 230 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐺 Fn ℝ) |
232 | | fniniseg 7010 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Fn ℝ → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘))) |
233 | 231, 232 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘))) |
234 | | elin 3926 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ (𝑥 ∈ (◡𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴‘𝑛))) |
235 | 189 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐹 Fn ℝ) |
236 | | fniniseg 7010 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘))) |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘))) |
238 | 237 | anbi1d 630 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ (◡𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴‘𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
239 | 234, 238 | bitrid 282 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
240 | 227, 233,
239 | 3bitr4d 310 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
241 | 240 | alrimiv 1930 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑥(𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
242 | | nfmpt1 5213 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
243 | 183, 242 | nfcxfr 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝐺 |
244 | 243 | nfcnv 5834 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥◡𝐺 |
245 | | nfcv 2907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥{𝑘} |
246 | 244, 245 | nfima 6021 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(◡𝐺 “ {𝑘}) |
247 | | nfcv 2907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) |
248 | 246, 247 | cleqf 2938 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑘}) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ ∀𝑥(𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
249 | 241, 248 | sylibr 233 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐺 “ {𝑘}) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) |
250 | 249 | fveq2d 6846 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐺 “ {𝑘})) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
251 | 250 | oveq2d 7373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(◡𝐺 “ {𝑘}))) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
252 | 251 | sumeq2dv 15588 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘}))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
253 | 203, 252 | eqtrd 2776 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
254 | 253 | mpteq2dva 5205 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))) |
255 | 254 | fveq1d 6844 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦
(∫1‘𝐺))‘𝑗) = ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
256 | 166 | sumeq2sdv 15589 |
. . . . . 6
⊢ (𝑛 = 𝑗 → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
257 | | eqid 2736 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
258 | | sumex 15572 |
. . . . . 6
⊢
Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) ∈ V |
259 | 256, 257,
258 | fvmpt 6948 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
260 | 169 | sumeq2sdv 15589 |
. . . . 5
⊢ (𝑗 ∈ ℕ →
Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
261 | 259, 260 | eqtr4d 2779 |
. . . 4
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
262 | 255, 261 | sylan9eq 2796 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫1‘𝐺))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
263 | 1, 2, 8, 173, 175, 181, 262 | climfsum 15705 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ⇝ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
264 | | itg1val 25047 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
265 | 3, 264 | syl 17 |
. 2
⊢ (𝜑 →
(∫1‘𝐹)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
266 | 263, 265 | breqtrrd 5133 |
1
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ⇝ (∫1‘𝐹)) |