MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  voliunlem1 Structured version   Visualization version   GIF version

Theorem voliunlem1 24068
Description: Lemma for voliun 24072. (Contributed by Mario Carneiro, 20-Mar-2014.)
Hypotheses
Ref Expression
voliunlem.3 (𝜑𝐹:ℕ⟶dom vol)
voliunlem.5 (𝜑Disj 𝑖 ∈ ℕ (𝐹𝑖))
voliunlem1.6 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹𝑛))))
voliunlem1.7 (𝜑𝐸 ⊆ ℝ)
voliunlem1.8 (𝜑 → (vol*‘𝐸) ∈ ℝ)
Assertion
Ref Expression
voliunlem1 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ran 𝐹))) ≤ (vol*‘𝐸))
Distinct variable groups:   𝑘,𝑛,𝐸   𝑖,𝑘,𝑛,𝐹   𝑘,𝐻   𝜑,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑖)   𝐸(𝑖)   𝐻(𝑖,𝑛)

Proof of Theorem voliunlem1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 difss 4111 . . . 4 (𝐸 ran 𝐹) ⊆ 𝐸
2 voliunlem1.7 . . . 4 (𝜑𝐸 ⊆ ℝ)
3 voliunlem1.8 . . . . 5 (𝜑 → (vol*‘𝐸) ∈ ℝ)
43adantr 481 . . . 4 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐸) ∈ ℝ)
5 ovolsscl 24004 . . . 4 (((𝐸 ran 𝐹) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ran 𝐹)) ∈ ℝ)
61, 2, 4, 5mp3an2ani 1461 . . 3 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 ran 𝐹)) ∈ ℝ)
7 difss 4111 . . . 4 (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ 𝐸
8 ovolsscl 24004 . . . 4 (((𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
97, 2, 4, 8mp3an2ani 1461 . . 3 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
10 inss1 4208 . . . 4 (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ 𝐸
11 ovolsscl 24004 . . . 4 (((𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
1210, 2, 4, 11mp3an2ani 1461 . . 3 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
13 elfznn 12929 . . . . . . . . 9 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
14 voliunlem.3 . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶dom vol)
1514ffnd 6511 . . . . . . . . . . 11 (𝜑𝐹 Fn ℕ)
16 fnfvelrn 6843 . . . . . . . . . . 11 ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
1715, 16sylan 580 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
18 elssuni 4865 . . . . . . . . . 10 ((𝐹𝑛) ∈ ran 𝐹 → (𝐹𝑛) ⊆ ran 𝐹)
1917, 18syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ran 𝐹)
2013, 19sylan2 592 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑘)) → (𝐹𝑛) ⊆ ran 𝐹)
2120ralrimiva 3186 . . . . . . 7 (𝜑 → ∀𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹)
2221adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ∀𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹)
23 iunss 4965 . . . . . 6 ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹 ↔ ∀𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹)
2422, 23sylibr 235 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹)
2524sscond 4121 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐸 ran 𝐹) ⊆ (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
262adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝐸 ⊆ ℝ)
277, 26sstrid 3981 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ ℝ)
28 ovolss 24003 . . . 4 (((𝐸 ran 𝐹) ⊆ (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ∧ (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ ℝ) → (vol*‘(𝐸 ran 𝐹)) ≤ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
2925, 27, 28syl2anc 584 . . 3 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 ran 𝐹)) ≤ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
306, 9, 12, 29leadd2dd 11247 . 2 ((𝜑𝑘 ∈ ℕ) → ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ran 𝐹))) ≤ ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))))
31 oveq2 7159 . . . . . . . . . . 11 (𝑧 = 1 → (1...𝑧) = (1...1))
3231iuneq1d 4942 . . . . . . . . . 10 (𝑧 = 1 → 𝑛 ∈ (1...𝑧)(𝐹𝑛) = 𝑛 ∈ (1...1)(𝐹𝑛))
3332eleq1d 2901 . . . . . . . . 9 (𝑧 = 1 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ↔ 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol))
3432ineq2d 4192 . . . . . . . . . . 11 (𝑧 = 1 → (𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛)) = (𝐸 𝑛 ∈ (1...1)(𝐹𝑛)))
3534fveq2d 6670 . . . . . . . . . 10 (𝑧 = 1 → (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))))
36 fveq2 6666 . . . . . . . . . 10 (𝑧 = 1 → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘1))
3735, 36eqeq12d 2841 . . . . . . . . 9 (𝑧 = 1 → ((vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1)))
3833, 37anbi12d 630 . . . . . . . 8 (𝑧 = 1 → (( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ ( 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1))))
3938imbi2d 342 . . . . . . 7 (𝑧 = 1 → ((𝜑 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → ( 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1)))))
40 oveq2 7159 . . . . . . . . . . 11 (𝑧 = 𝑘 → (1...𝑧) = (1...𝑘))
4140iuneq1d 4942 . . . . . . . . . 10 (𝑧 = 𝑘 𝑛 ∈ (1...𝑧)(𝐹𝑛) = 𝑛 ∈ (1...𝑘)(𝐹𝑛))
4241eleq1d 2901 . . . . . . . . 9 (𝑧 = 𝑘 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ↔ 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol))
4341ineq2d 4192 . . . . . . . . . . 11 (𝑧 = 𝑘 → (𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛)) = (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
4443fveq2d 6670 . . . . . . . . . 10 (𝑧 = 𝑘 → (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
45 fveq2 6666 . . . . . . . . . 10 (𝑧 = 𝑘 → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘𝑘))
4644, 45eqeq12d 2841 . . . . . . . . 9 (𝑧 = 𝑘 → ((vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)))
4742, 46anbi12d 630 . . . . . . . 8 (𝑧 = 𝑘 → (( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘))))
4847imbi2d 342 . . . . . . 7 (𝑧 = 𝑘 → ((𝜑 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)))))
49 oveq2 7159 . . . . . . . . . . 11 (𝑧 = (𝑘 + 1) → (1...𝑧) = (1...(𝑘 + 1)))
5049iuneq1d 4942 . . . . . . . . . 10 (𝑧 = (𝑘 + 1) → 𝑛 ∈ (1...𝑧)(𝐹𝑛) = 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
5150eleq1d 2901 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ↔ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol))
5250ineq2d 4192 . . . . . . . . . . 11 (𝑧 = (𝑘 + 1) → (𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛)) = (𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)))
5352fveq2d 6670 . . . . . . . . . 10 (𝑧 = (𝑘 + 1) → (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))))
54 fveq2 6666 . . . . . . . . . 10 (𝑧 = (𝑘 + 1) → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘(𝑘 + 1)))
5553, 54eqeq12d 2841 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → ((vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))
5651, 55anbi12d 630 . . . . . . . 8 (𝑧 = (𝑘 + 1) → (( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))))
5756imbi2d 342 . . . . . . 7 (𝑧 = (𝑘 + 1) → ((𝜑 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))))
58 1z 12004 . . . . . . . . . . 11 1 ∈ ℤ
59 fzsn 12942 . . . . . . . . . . 11 (1 ∈ ℤ → (1...1) = {1})
60 iuneq1 4931 . . . . . . . . . . 11 ((1...1) = {1} → 𝑛 ∈ (1...1)(𝐹𝑛) = 𝑛 ∈ {1} (𝐹𝑛))
6158, 59, 60mp2b 10 . . . . . . . . . 10 𝑛 ∈ (1...1)(𝐹𝑛) = 𝑛 ∈ {1} (𝐹𝑛)
62 1ex 10629 . . . . . . . . . . 11 1 ∈ V
63 fveq2 6666 . . . . . . . . . . 11 (𝑛 = 1 → (𝐹𝑛) = (𝐹‘1))
6462, 63iunxsn 5009 . . . . . . . . . 10 𝑛 ∈ {1} (𝐹𝑛) = (𝐹‘1)
6561, 64eqtri 2848 . . . . . . . . 9 𝑛 ∈ (1...1)(𝐹𝑛) = (𝐹‘1)
66 1nn 11641 . . . . . . . . . 10 1 ∈ ℕ
67 ffvelrn 6844 . . . . . . . . . 10 ((𝐹:ℕ⟶dom vol ∧ 1 ∈ ℕ) → (𝐹‘1) ∈ dom vol)
6814, 66, 67sylancl 586 . . . . . . . . 9 (𝜑 → (𝐹‘1) ∈ dom vol)
6965, 68eqeltrid 2921 . . . . . . . 8 (𝜑 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol)
7063ineq2d 4192 . . . . . . . . . . . 12 (𝑛 = 1 → (𝐸 ∩ (𝐹𝑛)) = (𝐸 ∩ (𝐹‘1)))
7170fveq2d 6670 . . . . . . . . . . 11 (𝑛 = 1 → (vol*‘(𝐸 ∩ (𝐹𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘1))))
72 voliunlem1.6 . . . . . . . . . . 11 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹𝑛))))
73 fvex 6679 . . . . . . . . . . 11 (vol*‘(𝐸 ∩ (𝐹‘1))) ∈ V
7471, 72, 73fvmpt 6764 . . . . . . . . . 10 (1 ∈ ℕ → (𝐻‘1) = (vol*‘(𝐸 ∩ (𝐹‘1))))
7566, 74ax-mp 5 . . . . . . . . 9 (𝐻‘1) = (vol*‘(𝐸 ∩ (𝐹‘1)))
76 seq1 13375 . . . . . . . . . 10 (1 ∈ ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1))
7758, 76ax-mp 5 . . . . . . . . 9 (seq1( + , 𝐻)‘1) = (𝐻‘1)
7865ineq2i 4189 . . . . . . . . . 10 (𝐸 𝑛 ∈ (1...1)(𝐹𝑛)) = (𝐸 ∩ (𝐹‘1))
7978fveq2i 6669 . . . . . . . . 9 (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘1)))
8075, 77, 793eqtr4ri 2859 . . . . . . . 8 (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1)
8169, 80jctir 521 . . . . . . 7 (𝜑 → ( 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1)))
82 peano2nn 11642 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
83 ffvelrn 6844 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶dom vol ∧ (𝑘 + 1) ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ dom vol)
8414, 82, 83syl2an 595 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ dom vol)
85 unmbl 24055 . . . . . . . . . . . . 13 (( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (𝐹‘(𝑘 + 1)) ∈ dom vol) → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol)
8685ex 413 . . . . . . . . . . . 12 ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol → ((𝐹‘(𝑘 + 1)) ∈ dom vol → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol))
8784, 86syl5com 31 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol))
88 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
89 nnuz 12273 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
9088, 89syl6eleq 2927 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
91 fzsuc 12947 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
92 iuneq1 4931 . . . . . . . . . . . . . 14 ((1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}) → 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) = 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹𝑛))
9390, 91, 923syl 18 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) = 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹𝑛))
94 iunxun 5012 . . . . . . . . . . . . . 14 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹𝑛) = ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ 𝑛 ∈ {(𝑘 + 1)} (𝐹𝑛))
95 ovex 7184 . . . . . . . . . . . . . . . 16 (𝑘 + 1) ∈ V
96 fveq2 6666 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (𝐹𝑛) = (𝐹‘(𝑘 + 1)))
9795, 96iunxsn 5009 . . . . . . . . . . . . . . 15 𝑛 ∈ {(𝑘 + 1)} (𝐹𝑛) = (𝐹‘(𝑘 + 1))
9897uneq2i 4139 . . . . . . . . . . . . . 14 ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ 𝑛 ∈ {(𝑘 + 1)} (𝐹𝑛)) = ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1)))
9994, 98eqtri 2848 . . . . . . . . . . . . 13 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹𝑛) = ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1)))
10093, 99syl6eq 2876 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) = ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))))
101100eleq1d 2901 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ↔ ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol))
10287, 101sylibrd 260 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol → 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol))
103 oveq1 7158 . . . . . . . . . . 11 ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘) → ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
104 inss1 4208 . . . . . . . . . . . . . . 15 (𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ⊆ 𝐸
105104, 26sstrid 3981 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ⊆ ℝ)
106 ovolsscl 24004 . . . . . . . . . . . . . . 15 (((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) ∈ ℝ)
107104, 2, 4, 106mp3an2ani 1461 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) ∈ ℝ)
108 mblsplit 24050 . . . . . . . . . . . . . 14 (((𝐹‘(𝑘 + 1)) ∈ dom vol ∧ (𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ⊆ ℝ ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = ((vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1))))))
10984, 105, 107, 108syl3anc 1365 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = ((vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1))))))
110 in32 4201 . . . . . . . . . . . . . . . 16 ((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1))) = ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
111 inss2 4209 . . . . . . . . . . . . . . . . . 18 (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ (𝐹‘(𝑘 + 1))
11282adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
113112, 89syl6eleq 2927 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ (ℤ‘1))
114 eluzfz2 12908 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ (ℤ‘1) → (𝑘 + 1) ∈ (1...(𝑘 + 1)))
11596ssiun2s 4968 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ (1...(𝑘 + 1)) → (𝐹‘(𝑘 + 1)) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
116113, 114, 1153syl 18 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
117111, 116sstrid 3981 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
118 df-ss 3955 . . . . . . . . . . . . . . . . 17 ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ↔ ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1))))
119117, 118sylib 219 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1))))
120110, 119syl5eq 2872 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1))) = (𝐸 ∩ (𝐹‘(𝑘 + 1))))
121120fveq2d 6670 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1)))) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))
122 indif2 4250 . . . . . . . . . . . . . . . 16 (𝐸 ∩ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1)))) = ((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1)))
123 uncom 4132 . . . . . . . . . . . . . . . . . . 19 ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) = ((𝐹‘(𝑘 + 1)) ∪ 𝑛 ∈ (1...𝑘)(𝐹𝑛))
124100, 123syl6req 2877 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ∪ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
125 voliunlem.5 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑Disj 𝑖 ∈ ℕ (𝐹𝑖))
126125ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → Disj 𝑖 ∈ ℕ (𝐹𝑖))
127112adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑘 + 1) ∈ ℕ)
12813adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ)
129128nnred 11645 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℝ)
130 elfzle2 12904 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (1...𝑘) → 𝑛𝑘)
131130adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛𝑘)
13288adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑘 ∈ ℕ)
133 nnleltp1 12029 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑛𝑘𝑛 < (𝑘 + 1)))
134128, 132, 133syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑛𝑘𝑛 < (𝑘 + 1)))
135131, 134mpbid 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 < (𝑘 + 1))
136129, 135gtned 10767 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑘 + 1) ≠ 𝑛)
137 fveq2 6666 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝐹𝑖) = (𝐹‘(𝑘 + 1)))
138 fveq2 6666 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑛 → (𝐹𝑖) = (𝐹𝑛))
139137, 138disji2 5044 . . . . . . . . . . . . . . . . . . . . . 22 ((Disj 𝑖 ∈ ℕ (𝐹𝑖) ∧ ((𝑘 + 1) ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑘 + 1) ≠ 𝑛) → ((𝐹‘(𝑘 + 1)) ∩ (𝐹𝑛)) = ∅)
140126, 127, 128, 136, 139syl121anc 1369 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((𝐹‘(𝑘 + 1)) ∩ (𝐹𝑛)) = ∅)
141140iuneq2dv 4939 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...𝑘)((𝐹‘(𝑘 + 1)) ∩ (𝐹𝑛)) = 𝑛 ∈ (1...𝑘)∅)
142 iunin2 4989 . . . . . . . . . . . . . . . . . . . 20 𝑛 ∈ (1...𝑘)((𝐹‘(𝑘 + 1)) ∩ (𝐹𝑛)) = ((𝐹‘(𝑘 + 1)) ∩ 𝑛 ∈ (1...𝑘)(𝐹𝑛))
143 iun0 4981 . . . . . . . . . . . . . . . . . . . 20 𝑛 ∈ (1...𝑘)∅ = ∅
144141, 142, 1433eqtr3g 2883 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ∩ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = ∅)
145 uneqdifeq 4440 . . . . . . . . . . . . . . . . . . 19 (((𝐹‘(𝑘 + 1)) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∧ ((𝐹‘(𝑘 + 1)) ∩ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = ∅) → (((𝐹‘(𝑘 + 1)) ∪ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ↔ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1))) = 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
146116, 144, 145syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (((𝐹‘(𝑘 + 1)) ∪ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ↔ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1))) = 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
147124, 146mpbid 233 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1))) = 𝑛 ∈ (1...𝑘)(𝐹𝑛))
148147ineq2d 4192 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝐸 ∩ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1)))) = (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
149122, 148syl5eqr 2874 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1))) = (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
150149fveq2d 6670 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1)))) = (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
151121, 150oveq12d 7169 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1))))) = ((vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))))
152 inss1 4208 . . . . . . . . . . . . . . . 16 (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝐸
153 ovolsscl 24004 . . . . . . . . . . . . . . . 16 (((𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℝ)
154152, 2, 4, 153mp3an2ani 1461 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℝ)
155154recnd 10661 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℂ)
15612recnd 10661 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℂ)
157155, 156addcomd 10834 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
158109, 151, 1573eqtrd 2864 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
159 seqp1 13377 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1))))
16090, 159syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1))))
16196ineq2d 4192 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → (𝐸 ∩ (𝐹𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1))))
162161fveq2d 6670 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (vol*‘(𝐸 ∩ (𝐹𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))
163 fvex 6679 . . . . . . . . . . . . . . . 16 (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ V
164162, 72, 163fvmpt 6764 . . . . . . . . . . . . . . 15 ((𝑘 + 1) ∈ ℕ → (𝐻‘(𝑘 + 1)) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))
165112, 164syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(𝑘 + 1)) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))
166165oveq2d 7167 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
167160, 166eqtrd 2860 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
168158, 167eqeq12d 2841 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)) ↔ ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))))
169103, 168syl5ibr 247 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))
170102, 169anim12d 608 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)) → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))))
171170expcom 414 . . . . . . . 8 (𝑘 ∈ ℕ → (𝜑 → (( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)) → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))))
172171a2d 29 . . . . . . 7 (𝑘 ∈ ℕ → ((𝜑 → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘))) → (𝜑 → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))))
17339, 48, 57, 48, 81, 172nnind 11648 . . . . . 6 (𝑘 ∈ ℕ → (𝜑 → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘))))
174173impcom 408 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)))
175174simprd 496 . . . 4 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘))
176175eqcomd 2831 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
177176oveq1d 7166 . 2 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ran 𝐹))) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ran 𝐹))))
178174simpld 495 . . 3 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol)
179 mblsplit 24050 . . 3 (( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘𝐸) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))))
180178, 26, 4, 179syl3anc 1365 . 2 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐸) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))))
18130, 177, 1803brtr4d 5094 1 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ran 𝐹))) ≤ (vol*‘𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wcel 2107  wne 3020  wral 3142  cdif 3936  cun 3937  cin 3938  wss 3939  c0 4294  {csn 4563   cuni 4836   ciun 4916  Disj wdisj 5027   class class class wbr 5062  cmpt 5142  dom cdm 5553  ran crn 5554   Fn wfn 6346  wf 6347  cfv 6351  (class class class)co 7151  cr 10528  1c1 10530   + caddc 10532   < clt 10667  cle 10668  cn 11630  cz 11973  cuz 12235  ...cfz 12885  seqcseq 13362  vol*covol 23980  volcvol 23981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-disj 5028  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8282  df-map 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-sup 8898  df-inf 8899  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12383  df-ioo 12735  df-ico 12737  df-icc 12738  df-fz 12886  df-fl 13155  df-seq 13363  df-exp 13423  df-cj 14451  df-re 14452  df-im 14453  df-sqrt 14587  df-abs 14588  df-ovol 23982  df-vol 23983
This theorem is referenced by:  voliunlem2  24069  voliunlem3  24070
  Copyright terms: Public domain W3C validator