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

Theorem voliunlem1 23241
Description: Lemma for voliun 23245. (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 voliunlem1.7 . . . . 5 (𝜑𝐸 ⊆ ℝ)
21adantr 481 . . . 4 ((𝜑𝑘 ∈ ℕ) → 𝐸 ⊆ ℝ)
3 voliunlem1.8 . . . . 5 (𝜑 → (vol*‘𝐸) ∈ ℝ)
43adantr 481 . . . 4 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐸) ∈ ℝ)
5 difss 3720 . . . . 5 (𝐸 ran 𝐹) ⊆ 𝐸
6 ovolsscl 23177 . . . . 5 (((𝐸 ran 𝐹) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ran 𝐹)) ∈ ℝ)
75, 6mp3an1 1408 . . . 4 ((𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ran 𝐹)) ∈ ℝ)
82, 4, 7syl2anc 692 . . 3 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 ran 𝐹)) ∈ ℝ)
9 difss 3720 . . . . 5 (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ 𝐸
10 ovolsscl 23177 . . . . 5 (((𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
119, 10mp3an1 1408 . . . 4 ((𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
122, 4, 11syl2anc 692 . . 3 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
13 inss1 3816 . . . . 5 (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ 𝐸
14 ovolsscl 23177 . . . . 5 (((𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
1513, 14mp3an1 1408 . . . 4 ((𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
162, 4, 15syl2anc 692 . . 3 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℝ)
17 elfznn 12320 . . . . . . . . 9 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
18 voliunlem.3 . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶dom vol)
19 ffn 6007 . . . . . . . . . . . 12 (𝐹:ℕ⟶dom vol → 𝐹 Fn ℕ)
2018, 19syl 17 . . . . . . . . . . 11 (𝜑𝐹 Fn ℕ)
21 fnfvelrn 6317 . . . . . . . . . . 11 ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
2220, 21sylan 488 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
23 elssuni 4438 . . . . . . . . . 10 ((𝐹𝑛) ∈ ran 𝐹 → (𝐹𝑛) ⊆ ran 𝐹)
2422, 23syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ran 𝐹)
2517, 24sylan2 491 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑘)) → (𝐹𝑛) ⊆ ran 𝐹)
2625ralrimiva 2961 . . . . . . 7 (𝜑 → ∀𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹)
2726adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ∀𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹)
28 iunss 4532 . . . . . 6 ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹 ↔ ∀𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹)
2927, 28sylibr 224 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...𝑘)(𝐹𝑛) ⊆ ran 𝐹)
3029sscond 3730 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐸 ran 𝐹) ⊆ (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
319, 2syl5ss 3598 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ ℝ)
32 ovolss 23176 . . . 4 (((𝐸 ran 𝐹) ⊆ (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ∧ (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)) ⊆ ℝ) → (vol*‘(𝐸 ran 𝐹)) ≤ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
3330, 31, 32syl2anc 692 . . 3 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 ran 𝐹)) ≤ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
348, 12, 16, 33leadd2dd 10594 . 2 ((𝜑𝑘 ∈ ℕ) → ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ran 𝐹))) ≤ ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))))
35 oveq2 6618 . . . . . . . . . . 11 (𝑧 = 1 → (1...𝑧) = (1...1))
3635iuneq1d 4516 . . . . . . . . . 10 (𝑧 = 1 → 𝑛 ∈ (1...𝑧)(𝐹𝑛) = 𝑛 ∈ (1...1)(𝐹𝑛))
3736eleq1d 2683 . . . . . . . . 9 (𝑧 = 1 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ↔ 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol))
3836ineq2d 3797 . . . . . . . . . . 11 (𝑧 = 1 → (𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛)) = (𝐸 𝑛 ∈ (1...1)(𝐹𝑛)))
3938fveq2d 6157 . . . . . . . . . 10 (𝑧 = 1 → (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))))
40 fveq2 6153 . . . . . . . . . 10 (𝑧 = 1 → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘1))
4139, 40eqeq12d 2636 . . . . . . . . 9 (𝑧 = 1 → ((vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1)))
4237, 41anbi12d 746 . . . . . . . 8 (𝑧 = 1 → (( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ ( 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1))))
4342imbi2d 330 . . . . . . 7 (𝑧 = 1 → ((𝜑 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → ( 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1)))))
44 oveq2 6618 . . . . . . . . . . 11 (𝑧 = 𝑘 → (1...𝑧) = (1...𝑘))
4544iuneq1d 4516 . . . . . . . . . 10 (𝑧 = 𝑘 𝑛 ∈ (1...𝑧)(𝐹𝑛) = 𝑛 ∈ (1...𝑘)(𝐹𝑛))
4645eleq1d 2683 . . . . . . . . 9 (𝑧 = 𝑘 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ↔ 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol))
4745ineq2d 3797 . . . . . . . . . . 11 (𝑧 = 𝑘 → (𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛)) = (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
4847fveq2d 6157 . . . . . . . . . 10 (𝑧 = 𝑘 → (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
49 fveq2 6153 . . . . . . . . . 10 (𝑧 = 𝑘 → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘𝑘))
5048, 49eqeq12d 2636 . . . . . . . . 9 (𝑧 = 𝑘 → ((vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)))
5146, 50anbi12d 746 . . . . . . . 8 (𝑧 = 𝑘 → (( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘))))
5251imbi2d 330 . . . . . . 7 (𝑧 = 𝑘 → ((𝜑 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)))))
53 oveq2 6618 . . . . . . . . . . 11 (𝑧 = (𝑘 + 1) → (1...𝑧) = (1...(𝑘 + 1)))
5453iuneq1d 4516 . . . . . . . . . 10 (𝑧 = (𝑘 + 1) → 𝑛 ∈ (1...𝑧)(𝐹𝑛) = 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
5554eleq1d 2683 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ↔ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol))
5654ineq2d 3797 . . . . . . . . . . 11 (𝑧 = (𝑘 + 1) → (𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛)) = (𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)))
5756fveq2d 6157 . . . . . . . . . 10 (𝑧 = (𝑘 + 1) → (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))))
58 fveq2 6153 . . . . . . . . . 10 (𝑧 = (𝑘 + 1) → (seq1( + , 𝐻)‘𝑧) = (seq1( + , 𝐻)‘(𝑘 + 1)))
5957, 58eqeq12d 2636 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → ((vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧) ↔ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))
6055, 59anbi12d 746 . . . . . . . 8 (𝑧 = (𝑘 + 1) → (( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧)) ↔ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))))
6160imbi2d 330 . . . . . . 7 (𝑧 = (𝑘 + 1) → ((𝜑 → ( 𝑛 ∈ (1...𝑧)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑧)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑧))) ↔ (𝜑 → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))))
62 1z 11359 . . . . . . . . . . 11 1 ∈ ℤ
63 fzsn 12333 . . . . . . . . . . 11 (1 ∈ ℤ → (1...1) = {1})
64 iuneq1 4505 . . . . . . . . . . 11 ((1...1) = {1} → 𝑛 ∈ (1...1)(𝐹𝑛) = 𝑛 ∈ {1} (𝐹𝑛))
6562, 63, 64mp2b 10 . . . . . . . . . 10 𝑛 ∈ (1...1)(𝐹𝑛) = 𝑛 ∈ {1} (𝐹𝑛)
66 1ex 9987 . . . . . . . . . . 11 1 ∈ V
67 fveq2 6153 . . . . . . . . . . 11 (𝑛 = 1 → (𝐹𝑛) = (𝐹‘1))
6866, 67iunxsn 4574 . . . . . . . . . 10 𝑛 ∈ {1} (𝐹𝑛) = (𝐹‘1)
6965, 68eqtri 2643 . . . . . . . . 9 𝑛 ∈ (1...1)(𝐹𝑛) = (𝐹‘1)
70 1nn 10983 . . . . . . . . . 10 1 ∈ ℕ
71 ffvelrn 6318 . . . . . . . . . 10 ((𝐹:ℕ⟶dom vol ∧ 1 ∈ ℕ) → (𝐹‘1) ∈ dom vol)
7218, 70, 71sylancl 693 . . . . . . . . 9 (𝜑 → (𝐹‘1) ∈ dom vol)
7369, 72syl5eqel 2702 . . . . . . . 8 (𝜑 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol)
7467ineq2d 3797 . . . . . . . . . . . 12 (𝑛 = 1 → (𝐸 ∩ (𝐹𝑛)) = (𝐸 ∩ (𝐹‘1)))
7574fveq2d 6157 . . . . . . . . . . 11 (𝑛 = 1 → (vol*‘(𝐸 ∩ (𝐹𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘1))))
76 voliunlem1.6 . . . . . . . . . . 11 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹𝑛))))
77 fvex 6163 . . . . . . . . . . 11 (vol*‘(𝐸 ∩ (𝐹‘1))) ∈ V
7875, 76, 77fvmpt 6244 . . . . . . . . . 10 (1 ∈ ℕ → (𝐻‘1) = (vol*‘(𝐸 ∩ (𝐹‘1))))
7970, 78ax-mp 5 . . . . . . . . 9 (𝐻‘1) = (vol*‘(𝐸 ∩ (𝐹‘1)))
80 seq1 12762 . . . . . . . . . 10 (1 ∈ ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1))
8162, 80ax-mp 5 . . . . . . . . 9 (seq1( + , 𝐻)‘1) = (𝐻‘1)
8269ineq2i 3794 . . . . . . . . . 10 (𝐸 𝑛 ∈ (1...1)(𝐹𝑛)) = (𝐸 ∩ (𝐹‘1))
8382fveq2i 6156 . . . . . . . . 9 (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘1)))
8479, 81, 833eqtr4ri 2654 . . . . . . . 8 (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1)
8573, 84jctir 560 . . . . . . 7 (𝜑 → ( 𝑛 ∈ (1...1)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...1)(𝐹𝑛))) = (seq1( + , 𝐻)‘1)))
86 peano2nn 10984 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
87 ffvelrn 6318 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶dom vol ∧ (𝑘 + 1) ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ dom vol)
8818, 86, 87syl2an 494 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ dom vol)
89 unmbl 23228 . . . . . . . . . . . . 13 (( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (𝐹‘(𝑘 + 1)) ∈ dom vol) → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol)
9089ex 450 . . . . . . . . . . . 12 ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol → ((𝐹‘(𝑘 + 1)) ∈ dom vol → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol))
9188, 90syl5com 31 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol))
92 simpr 477 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
93 nnuz 11675 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
9492, 93syl6eleq 2708 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
95 fzsuc 12338 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
96 iuneq1 4505 . . . . . . . . . . . . . 14 ((1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}) → 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) = 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹𝑛))
9794, 95, 963syl 18 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) = 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹𝑛))
98 iunxun 4576 . . . . . . . . . . . . . 14 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹𝑛) = ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ 𝑛 ∈ {(𝑘 + 1)} (𝐹𝑛))
99 ovex 6638 . . . . . . . . . . . . . . . 16 (𝑘 + 1) ∈ V
100 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (𝐹𝑛) = (𝐹‘(𝑘 + 1)))
10199, 100iunxsn 4574 . . . . . . . . . . . . . . 15 𝑛 ∈ {(𝑘 + 1)} (𝐹𝑛) = (𝐹‘(𝑘 + 1))
102101uneq2i 3747 . . . . . . . . . . . . . 14 ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ 𝑛 ∈ {(𝑘 + 1)} (𝐹𝑛)) = ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1)))
10398, 102eqtri 2643 . . . . . . . . . . . . 13 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹𝑛) = ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1)))
10497, 103syl6eq 2671 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) = ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))))
105104eleq1d 2683 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ↔ ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) ∈ dom vol))
10691, 105sylibrd 249 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol → 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol))
107 oveq1 6617 . . . . . . . . . . 11 ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘) → ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
108 inss1 3816 . . . . . . . . . . . . . . 15 (𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ⊆ 𝐸
109108, 2syl5ss 3598 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ⊆ ℝ)
110 ovolsscl 23177 . . . . . . . . . . . . . . . 16 (((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) ∈ ℝ)
111108, 110mp3an1 1408 . . . . . . . . . . . . . . 15 ((𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) ∈ ℝ)
1122, 4, 111syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) ∈ ℝ)
113 mblsplit 23223 . . . . . . . . . . . . . 14 (((𝐹‘(𝑘 + 1)) ∈ dom vol ∧ (𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ⊆ ℝ ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) ∈ ℝ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = ((vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1))))))
11488, 109, 112, 113syl3anc 1323 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = ((vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1))))))
115 in32 3808 . . . . . . . . . . . . . . . 16 ((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1))) = ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
116 inss2 3817 . . . . . . . . . . . . . . . . . 18 (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ (𝐹‘(𝑘 + 1))
11786adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
118117, 93syl6eleq 2708 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ (ℤ‘1))
119 eluzfz2 12299 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ (ℤ‘1) → (𝑘 + 1) ∈ (1...(𝑘 + 1)))
120100ssiun2s 4535 . . . . . . . . . . . . . . . . . . 19 ((𝑘 + 1) ∈ (1...(𝑘 + 1)) → (𝐹‘(𝑘 + 1)) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
121118, 119, 1203syl 18 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
122116, 121syl5ss 3598 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
123 df-ss 3573 . . . . . . . . . . . . . . . . 17 ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ↔ ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1))))
124122, 123sylib 208 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → ((𝐸 ∩ (𝐹‘(𝑘 + 1))) ∩ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1))))
125115, 124syl5eq 2667 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1))) = (𝐸 ∩ (𝐹‘(𝑘 + 1))))
126125fveq2d 6157 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1)))) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))
127 indif2 3851 . . . . . . . . . . . . . . . 16 (𝐸 ∩ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1)))) = ((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1)))
128 uncom 3740 . . . . . . . . . . . . . . . . . . 19 ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∪ (𝐹‘(𝑘 + 1))) = ((𝐹‘(𝑘 + 1)) ∪ 𝑛 ∈ (1...𝑘)(𝐹𝑛))
129104, 128syl6req 2672 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ∪ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))
130 voliunlem.5 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑Disj 𝑖 ∈ ℕ (𝐹𝑖))
131130ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → Disj 𝑖 ∈ ℕ (𝐹𝑖))
132117adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑘 + 1) ∈ ℕ)
13317adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ)
134133nnred 10987 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℝ)
135 elfzle2 12295 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (1...𝑘) → 𝑛𝑘)
136135adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛𝑘)
13792adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑘 ∈ ℕ)
138 nnleltp1 11384 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑛𝑘𝑛 < (𝑘 + 1)))
139133, 137, 138syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑛𝑘𝑛 < (𝑘 + 1)))
140136, 139mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 < (𝑘 + 1))
141134, 140gtned 10124 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑘 + 1) ≠ 𝑛)
142 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝐹𝑖) = (𝐹‘(𝑘 + 1)))
143 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑛 → (𝐹𝑖) = (𝐹𝑛))
144142, 143disji2 4604 . . . . . . . . . . . . . . . . . . . . . 22 ((Disj 𝑖 ∈ ℕ (𝐹𝑖) ∧ ((𝑘 + 1) ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑘 + 1) ≠ 𝑛) → ((𝐹‘(𝑘 + 1)) ∩ (𝐹𝑛)) = ∅)
145131, 132, 133, 141, 144syl121anc 1328 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((𝐹‘(𝑘 + 1)) ∩ (𝐹𝑛)) = ∅)
146145iuneq2dv 4513 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...𝑘)((𝐹‘(𝑘 + 1)) ∩ (𝐹𝑛)) = 𝑛 ∈ (1...𝑘)∅)
147 iunin2 4555 . . . . . . . . . . . . . . . . . . . 20 𝑛 ∈ (1...𝑘)((𝐹‘(𝑘 + 1)) ∩ (𝐹𝑛)) = ((𝐹‘(𝑘 + 1)) ∩ 𝑛 ∈ (1...𝑘)(𝐹𝑛))
148 iun0 4547 . . . . . . . . . . . . . . . . . . . 20 𝑛 ∈ (1...𝑘)∅ = ∅
149146, 147, 1483eqtr3g 2678 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ∩ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = ∅)
150 uneqdifeq 4034 . . . . . . . . . . . . . . . . . . 19 (((𝐹‘(𝑘 + 1)) ⊆ 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∧ ((𝐹‘(𝑘 + 1)) ∩ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = ∅) → (((𝐹‘(𝑘 + 1)) ∪ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ↔ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1))) = 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
151121, 149, 150syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (((𝐹‘(𝑘 + 1)) ∪ 𝑛 ∈ (1...𝑘)(𝐹𝑛)) = 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ↔ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1))) = 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
152129, 151mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1))) = 𝑛 ∈ (1...𝑘)(𝐹𝑛))
153152ineq2d 3797 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝐸 ∩ ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∖ (𝐹‘(𝑘 + 1)))) = (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
154127, 153syl5eqr 2669 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1))) = (𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))
155154fveq2d 6157 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1)))) = (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
156126, 155oveq12d 6628 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘((𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛)) ∖ (𝐹‘(𝑘 + 1))))) = ((vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))))
157 inss1 3816 . . . . . . . . . . . . . . . . 17 (𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝐸
158 ovolsscl 23177 . . . . . . . . . . . . . . . . 17 (((𝐸 ∩ (𝐹‘(𝑘 + 1))) ⊆ 𝐸𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℝ)
159157, 158mp3an1 1408 . . . . . . . . . . . . . . . 16 ((𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℝ)
1602, 4, 159syl2anc 692 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℝ)
161160recnd 10020 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ ℂ)
16216recnd 10020 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) ∈ ℂ)
163161, 162addcomd 10190 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
164114, 156, 1633eqtrd 2659 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
165 seqp1 12764 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1))))
16694, 165syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1))))
167100ineq2d 3797 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → (𝐸 ∩ (𝐹𝑛)) = (𝐸 ∩ (𝐹‘(𝑘 + 1))))
168167fveq2d 6157 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (vol*‘(𝐸 ∩ (𝐹𝑛))) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))
169 fvex 6163 . . . . . . . . . . . . . . . 16 (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))) ∈ V
170168, 76, 169fvmpt 6244 . . . . . . . . . . . . . . 15 ((𝑘 + 1) ∈ ℕ → (𝐻‘(𝑘 + 1)) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))
171117, 170syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(𝑘 + 1)) = (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))
172171oveq2d 6626 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (𝐻‘(𝑘 + 1))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
173166, 172eqtrd 2655 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘(𝑘 + 1)) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))))
174164, 173eqeq12d 2636 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)) ↔ ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1))))) = ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∩ (𝐹‘(𝑘 + 1)))))))
175107, 174syl5ibr 236 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘) → (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))
176106, 175anim12d 585 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)) → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1)))))
177176expcom 451 . . . . . . . 8 (𝑘 ∈ ℕ → (𝜑 → (( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)) → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))))
178177a2d 29 . . . . . . 7 (𝑘 ∈ ℕ → ((𝜑 → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘))) → (𝜑 → ( 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...(𝑘 + 1))(𝐹𝑛))) = (seq1( + , 𝐻)‘(𝑘 + 1))))))
17943, 52, 61, 52, 85, 178nnind 10990 . . . . . 6 (𝑘 ∈ ℕ → (𝜑 → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘))))
180179impcom 446 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘)))
181180simprd 479 . . . 4 ((𝜑𝑘 ∈ ℕ) → (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) = (seq1( + , 𝐻)‘𝑘))
182181eqcomd 2627 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))))
183182oveq1d 6625 . 2 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ran 𝐹))) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 ran 𝐹))))
184180simpld 475 . . 3 ((𝜑𝑘 ∈ ℕ) → 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol)
185 mblsplit 23223 . . 3 (( 𝑛 ∈ (1...𝑘)(𝐹𝑛) ∈ dom vol ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘𝐸) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))))
186184, 2, 4, 185syl3anc 1323 . 2 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐸) = ((vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛))) + (vol*‘(𝐸 𝑛 ∈ (1...𝑘)(𝐹𝑛)))))
18734, 183, 1863brtr4d 4650 1 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ran 𝐹))) ≤ (vol*‘𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  {csn 4153   cuni 4407   ciun 4490  Disj wdisj 4588   class class class wbr 4618  cmpt 4678  dom cdm 5079  ran crn 5080   Fn wfn 5847  wf 5848  cfv 5852  (class class class)co 6610  cr 9887  1c1 9889   + caddc 9891   < clt 10026  cle 10027  cn 10972  cz 11329  cuz 11639  ...cfz 12276  seqcseq 12749  vol*covol 23154  volcvol 23155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-disj 4589  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-sup 8300  df-inf 8301  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-n0 11245  df-z 11330  df-uz 11640  df-q 11741  df-rp 11785  df-ioo 12129  df-ico 12131  df-icc 12132  df-fz 12277  df-fl 12541  df-seq 12750  df-exp 12809  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-ovol 23156  df-vol 23157
This theorem is referenced by:  voliunlem2  23242  voliunlem3  23243
  Copyright terms: Public domain W3C validator