| Step | Hyp | Ref
| Expression |
| 1 | | nnuz 12921 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
| 2 | | 1zzd 12648 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
| 3 | | itg1climres.4 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
| 4 | | i1frn 25712 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
| 5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
| 6 | | difss 4136 |
. . . 4
⊢ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹 |
| 7 | | ssfi 9213 |
. . . 4
⊢ ((ran
𝐹 ∈ Fin ∧ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹) → (ran 𝐹 ∖ {0}) ∈
Fin) |
| 8 | 5, 6, 7 | sylancl 586 |
. . 3
⊢ (𝜑 → (ran 𝐹 ∖ {0}) ∈ Fin) |
| 9 | | 1zzd 12648 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 1 ∈
ℤ) |
| 10 | | i1fima 25713 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {𝑘}) ∈ dom vol) |
| 11 | 3, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ {𝑘}) ∈ dom vol) |
| 12 | 11 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ {𝑘}) ∈ dom vol) |
| 13 | | itg1climres.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴:ℕ⟶dom vol) |
| 14 | 13 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ dom vol) |
| 15 | 14 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ dom vol) |
| 16 | | inmbl 25577 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘𝑛) ∈ dom vol) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol) |
| 17 | 12, 15, 16 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol) |
| 18 | | mblvol 25565 |
. . . . . . . . 9
⊢ (((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ∈ dom vol → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 20 | | inss1 4237 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) |
| 21 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘})) |
| 22 | | mblss 25566 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑘}) ∈ dom vol → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
| 23 | 12, 22 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
| 24 | | mblvol 25565 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑘}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑘})) = (vol*‘(◡𝐹 “ {𝑘}))) |
| 25 | 12, 24 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(◡𝐹 “ {𝑘})) = (vol*‘(◡𝐹 “ {𝑘}))) |
| 26 | | i1fima2sn 25715 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
| 27 | 3, 26 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
| 28 | 27 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
| 29 | 25, 28 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
| 30 | | ovolsscl 25521 |
. . . . . . . . 9
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) ∧ (◡𝐹 “ {𝑘}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑘})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
| 31 | 21, 23, 29, 30 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
| 32 | 19, 31 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ∈ ℝ) |
| 33 | 32 | fmpttd 7135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))):ℕ⟶ℝ) |
| 34 | | itg1climres.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1))) |
| 35 | 34 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1))) |
| 36 | | sslin 4243 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1)) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
| 38 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴:ℕ⟶dom vol) |
| 39 | | peano2nn 12278 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
| 40 | | ffvelcdm 7101 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:ℕ⟶dom vol ∧
(𝑛 + 1) ∈ ℕ)
→ (𝐴‘(𝑛 + 1)) ∈ dom
vol) |
| 41 | 38, 39, 40 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝐴‘(𝑛 + 1)) ∈ dom vol) |
| 42 | | inmbl 25577 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹 “ {𝑘}) ∈ dom vol ∧ (𝐴‘(𝑛 + 1)) ∈ dom vol) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol) |
| 43 | 12, 41, 42 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol) |
| 44 | | mblss 25566 |
. . . . . . . . . . . 12
⊢ (((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∈ dom vol → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) |
| 46 | | ovolss 25520 |
. . . . . . . . . . 11
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ∧ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ⊆ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
| 47 | 37, 45, 46 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
| 48 | | mblvol 25565 |
. . . . . . . . . . 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 5175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
| 51 | 50 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
| 52 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (𝐴‘𝑛) = (𝐴‘𝑗)) |
| 53 | 52 | ineq2d 4220 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) |
| 54 | 53 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) |
| 55 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 56 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ∈ V |
| 57 | 54, 55, 56 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) |
| 58 | | peano2nn 12278 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
| 59 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → (𝐴‘𝑛) = (𝐴‘(𝑗 + 1))) |
| 60 | 59 | ineq2d 4220 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
| 61 | 60 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑗 + 1) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
| 62 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) ∈ V |
| 63 | 61, 55, 62 | fvmpt 7016 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
| 64 | 58, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
| 65 | 57, 64 | breq12d 5156 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))) |
| 66 | 65 | ralbiia 3091 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
| 67 | | fvoveq1 7454 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑗 + 1))) |
| 68 | 67 | ineq2d 4220 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
| 69 | 68 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
| 70 | 54, 69 | breq12d 5156 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → ((vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))))) |
| 71 | 70 | cbvralvw 3237 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
| 72 | 66, 71 | bitr4i 278 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))))) |
| 73 | 51, 72 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1))) |
| 74 | 73 | r19.21bi 3251 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘(𝑗 + 1))) |
| 75 | | ovolss 25520 |
. . . . . . . . . . 11
⊢ ((((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ (◡𝐹 “ {𝑘}) ∧ (◡𝐹 “ {𝑘}) ⊆ ℝ) →
(vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘(◡𝐹 “ {𝑘}))) |
| 76 | 20, 23, 75 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol*‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol*‘(◡𝐹 “ {𝑘}))) |
| 77 | 76, 19, 25 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
| 78 | 77 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
| 79 | 57 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘})))) |
| 80 | 79 | ralbiia 3091 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
| 81 | 54 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → ((vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘})))) |
| 82 | 81 | cbvralvw 3237 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑗 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
| 83 | 80, 82 | bitr4i 278 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘})) ↔ ∀𝑛 ∈ ℕ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
| 84 | 78, 83 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘}))) |
| 85 | | brralrspcev 5203 |
. . . . . . 7
⊢
(((vol‘(◡𝐹 “ {𝑘})) ∈ ℝ ∧ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ (vol‘(◡𝐹 “ {𝑘}))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥) |
| 86 | 27, 84, 85 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥) |
| 87 | 1, 9, 33, 74, 86 | climsup 15706 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⇝ sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
| 88 | 17 | fmpttd 7135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))):ℕ⟶dom vol) |
| 89 | 37 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
| 90 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) = (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) |
| 91 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝐴‘𝑗) ∈ V |
| 92 | 91 | inex2 5318 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ∈ V |
| 93 | 53, 90, 92 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))) |
| 94 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢ (𝐴‘(𝑗 + 1)) ∈ V |
| 95 | 94 | inex2 5318 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))) ∈ V |
| 96 | 60, 90, 95 | fvmpt 7016 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
| 97 | 58, 96 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
| 98 | 93, 97 | sseq12d 4017 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
| 99 | 98 | ralbiia 3091 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ∀𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
| 100 | 53, 68 | sseq12d 4017 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1))))) |
| 101 | 100 | cbvralvw 3237 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1))) ↔ ∀𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑗 + 1)))) |
| 102 | 99, 101 | bitr4i 278 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1)) ↔ ∀𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ⊆ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘(𝑛 + 1)))) |
| 103 | 89, 102 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) ⊆ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘(𝑗 + 1))) |
| 104 | | volsup 25591 |
. . . . . . 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 5013 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ 𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) |
| 107 | 53 | cbviunv 5040 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ∪
𝑗 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)) |
| 108 | | iunin2 5071 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) |
| 109 | 106, 107,
108 | 3eqtr2i 2771 |
. . . . . . . . 9
⊢ ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) |
| 110 | | ffn 6736 |
. . . . . . . . . . . . . 14
⊢ (𝐴:ℕ⟶dom vol →
𝐴 Fn
ℕ) |
| 111 | | fniunfv 7267 |
. . . . . . . . . . . . . 14
⊢ (𝐴 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ∪ ran 𝐴) |
| 112 | 13, 110, 111 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ∪ ran 𝐴) |
| 113 | | itg1climres.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ ran 𝐴 = ℝ) |
| 114 | 112, 113 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ℝ) |
| 115 | 114 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) = ℝ) |
| 116 | 115 | ineq2d 4220 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) = ((◡𝐹 “ {𝑘}) ∩ ℝ)) |
| 117 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) ∈ dom vol) |
| 118 | 117, 22 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) ⊆ ℝ) |
| 119 | | dfss2 3969 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑘}) ⊆ ℝ ↔ ((◡𝐹 “ {𝑘}) ∩ ℝ) = (◡𝐹 “ {𝑘})) |
| 120 | 118, 119 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ℝ) = (◡𝐹 “ {𝑘})) |
| 121 | 116, 120 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((◡𝐹 “ {𝑘}) ∩ ∪
𝑛 ∈ ℕ (𝐴‘𝑛)) = (◡𝐹 “ {𝑘})) |
| 122 | 109, 121 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = (◡𝐹 “ {𝑘})) |
| 123 | | ffn 6736 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))):ℕ⟶dom vol → (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) Fn ℕ) |
| 124 | | fniunfv 7267 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) Fn ℕ → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 125 | 88, 123, 124 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∪ 𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))‘𝑗) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 126 | 122, 125 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑘}) = ∪ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 127 | 126 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) = (vol‘∪
ran (𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 128 | 33 | frnd 6744 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⊆ ℝ) |
| 129 | 33 | fdmd 6746 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ℕ) |
| 130 | | 1nn 12277 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
| 131 | | ne0i 4341 |
. . . . . . . . . . 11
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
| 132 | 130, 131 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ℕ ≠
∅) |
| 133 | 129, 132 | eqnetrd 3008 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → dom (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
| 134 | | dm0rn0 5935 |
. . . . . . . . . 10
⊢ (dom
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ∅) |
| 135 | 134 | necon3bii 2993 |
. . . . . . . . 9
⊢ (dom
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
| 136 | 133, 135 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅) |
| 137 | | ffn 6736 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) Fn ℕ) |
| 138 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
| 139 | 138 | ralrn 7108 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
| 140 | 33, 137, 139 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
| 141 | 140 | rexbidv 3179 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ≤ 𝑥)) |
| 142 | 86, 141 | mpbird 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥) |
| 143 | | supxrre 13369 |
. . . . . . . 8
⊢ ((ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))𝑧 ≤ 𝑥) → sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup(ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
| 144 | 128, 136,
142, 143 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup(ran
(𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
| 145 | | volf 25564 |
. . . . . . . . . . . 12
⊢ vol:dom
vol⟶(0[,]+∞) |
| 146 | 145 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → vol:dom
vol⟶(0[,]+∞)) |
| 147 | 146, 17 | cofmpt 7152 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol ∘ (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 148 | 147 | rneqd 5949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (vol ∘
(𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 149 | | rnco2 6273 |
. . . . . . . . 9
⊢ ran (vol
∘ (𝑛 ∈ ℕ
↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 150 | 148, 149 | eqtr3di 2792 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (vol “ ran (𝑛 ∈ ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 151 | 150 | supeq1d 9486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, < ) = sup((vol
“ ran (𝑛 ∈
ℕ ↦ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
| 152 | 144, 151 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → sup(ran (𝑛 ∈ ℕ ↦
(vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < ) = sup((vol “ ran
(𝑛 ∈ ℕ ↦
((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ*, <
)) |
| 153 | 105, 127,
152 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) = sup(ran (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))), ℝ, < )) |
| 154 | 87, 153 | breqtrrd 5171 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ⇝ (vol‘(◡𝐹 “ {𝑘}))) |
| 155 | | i1ff 25711 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
| 156 | | frn 6743 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℝ →
ran 𝐹 ⊆
ℝ) |
| 157 | 3, 155, 156 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
| 158 | 157 | ssdifssd 4147 |
. . . . . 6
⊢ (𝜑 → (ran 𝐹 ∖ {0}) ⊆
ℝ) |
| 159 | 158 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ) |
| 160 | 159 | recnd 11289 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ) |
| 161 | | nnex 12272 |
. . . . . 6
⊢ ℕ
∈ V |
| 162 | 161 | mptex 7243 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ∈ V |
| 163 | 162 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ∈ V) |
| 164 | 33 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ∈ ℝ) |
| 165 | 164 | recnd 11289 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗) ∈ ℂ) |
| 166 | 54 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
| 167 | | eqid 2737 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) = (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 168 | | ovex 7464 |
. . . . . . 7
⊢ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) ∈ V |
| 169 | 166, 167,
168 | fvmpt 7016 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
| 170 | 57 | oveq2d 7447 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗)) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
| 171 | 169, 170 | eqtr4d 2780 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗))) |
| 172 | 171 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = (𝑘 · ((𝑛 ∈ ℕ ↦ (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))‘𝑗))) |
| 173 | 1, 9, 154, 160, 163, 165, 172 | climmulc2 15673 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) ⇝ (𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
| 174 | 161 | mptex 7243 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ∈ V |
| 175 | 174 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ∈ V) |
| 176 | 159 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → 𝑘 ∈ ℝ) |
| 177 | 176, 32 | remulcld 11291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑛 ∈ ℕ) → (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) ∈ ℝ) |
| 178 | 177 | fmpttd 7135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))):ℕ⟶ℝ) |
| 179 | 178 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℝ) |
| 180 | 179 | recnd 11289 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℂ) |
| 181 | 180 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ (ran 𝐹 ∖ {0}) ∧ 𝑗 ∈ ℕ)) → ((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) ∈ ℂ) |
| 182 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 ∈ dom
∫1) |
| 183 | | itg1climres.5 |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
| 184 | 183 | i1fres 25740 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴‘𝑛) ∈ dom vol) → 𝐺 ∈ dom
∫1) |
| 185 | 182, 14, 184 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 ∈ dom
∫1) |
| 186 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ∈
Fin) |
| 187 | | ffn 6736 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
| 188 | 3, 155, 187 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn ℝ) |
| 189 | 188 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 Fn ℝ) |
| 190 | | fnfvelrn 7100 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran 𝐹) |
| 191 | 189, 190 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran 𝐹) |
| 192 | | i1f0rn 25717 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ dom ∫1
→ 0 ∈ ran 𝐹) |
| 193 | 3, 192 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ ran 𝐹) |
| 194 | 193 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ran 𝐹) |
| 195 | 191, 194 | ifcld 4572 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ ran 𝐹) |
| 196 | 195, 183 | fmptd 7134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℝ⟶ran 𝐹) |
| 197 | | frn 6743 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ran 𝐹 → ran 𝐺 ⊆ ran 𝐹) |
| 198 | | ssdif 4144 |
. . . . . . . . 9
⊢ (ran
𝐺 ⊆ ran 𝐹 → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0})) |
| 199 | 196, 197,
198 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐺 ∖ {0}) ⊆ (ran 𝐹 ∖ {0})) |
| 200 | 157 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝐹 ⊆ ℝ) |
| 201 | 200 | ssdifd 4145 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran 𝐹 ∖ {0}) ⊆ (ℝ
∖ {0})) |
| 202 | | itg1val2 25719 |
. . . . . . . 8
⊢ ((𝐺 ∈ dom ∫1
∧ ((ran 𝐹 ∖ {0})
∈ Fin ∧ (ran 𝐺
∖ {0}) ⊆ (ran 𝐹
∖ {0}) ∧ (ran 𝐹
∖ {0}) ⊆ (ℝ ∖ {0}))) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘})))) |
| 203 | 185, 186,
199, 201, 202 | syl13anc 1374 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘})))) |
| 204 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹‘𝑥) ∈ V |
| 205 | | c0ex 11255 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
V |
| 206 | 204, 205 | ifex 4576 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ V |
| 207 | 183 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ∈ V) → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
| 208 | 206, 207 | mpan2 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
| 209 | 208 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
| 210 | 209 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘)) |
| 211 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0) |
| 212 | 211 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0) |
| 213 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0 ↔ 𝑘 ≠ 0)) |
| 214 | 212, 213 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0)) |
| 215 | | iffalse 4534 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑥 ∈ (𝐴‘𝑛) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 0) |
| 216 | 215 | necon1ai 2968 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) ≠ 0 → 𝑥 ∈ (𝐴‘𝑛)) |
| 217 | 214, 216 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 → 𝑥 ∈ (𝐴‘𝑛))) |
| 218 | 217 | pm4.71rd 562 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘))) |
| 219 | 210, 218 | bitrd 279 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘))) |
| 220 | | iftrue 4531 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴‘𝑛) → if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
| 221 | 220 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴‘𝑛) → (if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘 ↔ (𝐹‘𝑥) = 𝑘)) |
| 222 | 221 | pm5.32i 574 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘) ↔ (𝑥 ∈ (𝐴‘𝑛) ∧ (𝐹‘𝑥) = 𝑘)) |
| 223 | 222 | biancomi 462 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝐴‘𝑛) ∧ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0) = 𝑘) ↔ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛))) |
| 224 | 219, 223 | bitrdi 287 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) = 𝑘 ↔ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
| 225 | 224 | pm5.32da 579 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛))))) |
| 226 | | anass 468 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)) ↔ (𝑥 ∈ ℝ ∧ ((𝐹‘𝑥) = 𝑘 ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
| 227 | 225, 226 | bitr4di 289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
| 228 | | i1ff 25711 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
| 229 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:ℝ⟶ℝ →
𝐺 Fn
ℝ) |
| 230 | 185, 228,
229 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 Fn ℝ) |
| 231 | 230 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐺 Fn ℝ) |
| 232 | | fniniseg 7080 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Fn ℝ → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘))) |
| 233 | 231, 232 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐺‘𝑥) = 𝑘))) |
| 234 | | elin 3967 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ (𝑥 ∈ (◡𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴‘𝑛))) |
| 235 | 189 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐹 Fn ℝ) |
| 236 | | fniniseg 7080 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘))) |
| 237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐹 “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘))) |
| 238 | 237 | anbi1d 631 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ((𝑥 ∈ (◡𝐹 “ {𝑘}) ∧ 𝑥 ∈ (𝐴‘𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
| 239 | 234, 238 | bitrid 283 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ ((𝑥 ∈ ℝ ∧ (𝐹‘𝑥) = 𝑘) ∧ 𝑥 ∈ (𝐴‘𝑛)))) |
| 240 | 227, 233,
239 | 3bitr4d 311 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 241 | 240 | alrimiv 1927 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → ∀𝑥(𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 242 | | nfmpt1 5250 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0)) |
| 243 | 183, 242 | nfcxfr 2903 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝐺 |
| 244 | 243 | nfcnv 5889 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥◡𝐺 |
| 245 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥{𝑘} |
| 246 | 244, 245 | nfima 6086 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(◡𝐺 “ {𝑘}) |
| 247 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) |
| 248 | 246, 247 | cleqf 2934 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑘}) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)) ↔ ∀𝑥(𝑥 ∈ (◡𝐺 “ {𝑘}) ↔ 𝑥 ∈ ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 249 | 241, 248 | sylibr 234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (◡𝐺 “ {𝑘}) = ((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))) |
| 250 | 249 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐺 “ {𝑘})) = (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) |
| 251 | 250 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(◡𝐺 “ {𝑘}))) = (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 252 | 251 | sumeq2dv 15738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐺 “ {𝑘}))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 253 | 203, 252 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫1‘𝐺)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 254 | 253 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))) |
| 255 | 254 | fveq1d 6908 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦
(∫1‘𝐺))‘𝑗) = ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
| 256 | 166 | sumeq2sdv 15739 |
. . . . . 6
⊢ (𝑛 = 𝑗 → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
| 257 | | eqid 2737 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛))))) |
| 258 | | sumex 15724 |
. . . . . 6
⊢
Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗)))) ∈ V |
| 259 | 256, 257,
258 | fvmpt 7016 |
. . . . 5
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
| 260 | 169 | sumeq2sdv 15739 |
. . . . 5
⊢ (𝑗 ∈ ℕ →
Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑗))))) |
| 261 | 259, 260 | eqtr4d 2780 |
. . . 4
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
| 262 | 255, 261 | sylan9eq 2797 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫1‘𝐺))‘𝑗) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})((𝑛 ∈ ℕ ↦ (𝑘 · (vol‘((◡𝐹 “ {𝑘}) ∩ (𝐴‘𝑛)))))‘𝑗)) |
| 263 | 1, 2, 8, 173, 175, 181, 262 | climfsum 15856 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ⇝ Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
| 264 | | itg1val 25718 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
| 265 | 3, 264 | syl 17 |
. 2
⊢ (𝜑 →
(∫1‘𝐹)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
| 266 | 263, 265 | breqtrrd 5171 |
1
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫1‘𝐺)) ⇝ (∫1‘𝐹)) |