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

Theorem voliunlem3 23717
Description: Lemma for voliun 23719. (Contributed by Mario Carneiro, 20-Mar-2014.)
Hypotheses
Ref Expression
voliunlem.3 (𝜑𝐹:ℕ⟶dom vol)
voliunlem.5 (𝜑Disj 𝑖 ∈ ℕ (𝐹𝑖))
voliunlem.6 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛))))
voliunlem3.1 𝑆 = seq1( + , 𝐺)
voliunlem3.2 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛)))
voliunlem3.4 (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ)
Assertion
Ref Expression
voliunlem3 (𝜑 → (vol‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
Distinct variable groups:   𝑖,𝑛,𝑥,𝐹   𝑥,𝑆   𝜑,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑖)   𝑆(𝑖,𝑛)   𝐺(𝑥,𝑖,𝑛)   𝐻(𝑥,𝑖,𝑛)

Proof of Theorem voliunlem3
Dummy variables 𝑘 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 voliunlem.3 . . . 4 (𝜑𝐹:ℕ⟶dom vol)
2 voliunlem.5 . . . 4 (𝜑Disj 𝑖 ∈ ℕ (𝐹𝑖))
3 voliunlem.6 . . . 4 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛))))
41, 2, 3voliunlem2 23716 . . 3 (𝜑 ran 𝐹 ∈ dom vol)
5 mblvol 23695 . . 3 ( ran 𝐹 ∈ dom vol → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
64, 5syl 17 . 2 (𝜑 → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
7 eqid 2824 . . . . 5 seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
8 eqid 2824 . . . . 5 (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))
91ffvelrnda 6607 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ dom vol)
10 mblss 23696 . . . . . 6 ((𝐹𝑛) ∈ dom vol → (𝐹𝑛) ⊆ ℝ)
119, 10syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ℝ)
12 mblvol 23695 . . . . . . 7 ((𝐹𝑛) ∈ dom vol → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
139, 12syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
14 voliunlem3.4 . . . . . . 7 (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ)
15 2fveq3 6437 . . . . . . . . 9 (𝑖 = 𝑛 → (vol‘(𝐹𝑖)) = (vol‘(𝐹𝑛)))
1615eleq1d 2890 . . . . . . . 8 (𝑖 = 𝑛 → ((vol‘(𝐹𝑖)) ∈ ℝ ↔ (vol‘(𝐹𝑛)) ∈ ℝ))
1716rspccva 3524 . . . . . . 7 ((∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) ∈ ℝ)
1814, 17sylan 577 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) ∈ ℝ)
1913, 18eqeltrrd 2906 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (vol*‘(𝐹𝑛)) ∈ ℝ)
207, 8, 11, 19ovoliun 23670 . . . 4 (𝜑 → (vol*‘ 𝑛 ∈ ℕ (𝐹𝑛)) ≤ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))), ℝ*, < ))
211ffnd 6278 . . . . . 6 (𝜑𝐹 Fn ℕ)
22 fniunfv 6759 . . . . . 6 (𝐹 Fn ℕ → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
2321, 22syl 17 . . . . 5 (𝜑 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
2423fveq2d 6436 . . . 4 (𝜑 → (vol*‘ 𝑛 ∈ ℕ (𝐹𝑛)) = (vol*‘ ran 𝐹))
25 voliunlem3.1 . . . . . . 7 𝑆 = seq1( + , 𝐺)
26 voliunlem3.2 . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛)))
2713mpteq2dva 4966 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
2826, 27syl5eq 2872 . . . . . . . 8 (𝜑𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
2928seqeq3d 13102 . . . . . . 7 (𝜑 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))))
3025, 29syl5req 2873 . . . . . 6 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = 𝑆)
3130rneqd 5584 . . . . 5 (𝜑 → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = ran 𝑆)
3231supeq1d 8620 . . . 4 (𝜑 → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))), ℝ*, < ) = sup(ran 𝑆, ℝ*, < ))
3320, 24, 323brtr3d 4903 . . 3 (𝜑 → (vol*‘ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ))
341frnd 6284 . . . . . . . . . . . 12 (𝜑 → ran 𝐹 ⊆ dom vol)
35 mblss 23696 . . . . . . . . . . . . . 14 (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
36 reex 10342 . . . . . . . . . . . . . . 15 ℝ ∈ V
3736elpw2 5049 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 ℝ ↔ 𝑥 ⊆ ℝ)
3835, 37sylibr 226 . . . . . . . . . . . . 13 (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫 ℝ)
3938ssriv 3830 . . . . . . . . . . . 12 dom vol ⊆ 𝒫 ℝ
4034, 39syl6ss 3838 . . . . . . . . . . 11 (𝜑 → ran 𝐹 ⊆ 𝒫 ℝ)
41 sspwuni 4831 . . . . . . . . . . 11 (ran 𝐹 ⊆ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
4240, 41sylib 210 . . . . . . . . . 10 (𝜑 ran 𝐹 ⊆ ℝ)
43 ovolcl 23643 . . . . . . . . . 10 ( ran 𝐹 ⊆ ℝ → (vol*‘ ran 𝐹) ∈ ℝ*)
4442, 43syl 17 . . . . . . . . 9 (𝜑 → (vol*‘ ran 𝐹) ∈ ℝ*)
45 ovolge0 23646 . . . . . . . . . 10 ( ran 𝐹 ⊆ ℝ → 0 ≤ (vol*‘ ran 𝐹))
4642, 45syl 17 . . . . . . . . 9 (𝜑 → 0 ≤ (vol*‘ ran 𝐹))
47 mnflt0 12244 . . . . . . . . . 10 -∞ < 0
48 mnfxr 10413 . . . . . . . . . . 11 -∞ ∈ ℝ*
49 0xr 10402 . . . . . . . . . . 11 0 ∈ ℝ*
50 xrltletr 12275 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (vol*‘ ran 𝐹) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (vol*‘ ran 𝐹)) → -∞ < (vol*‘ ran 𝐹)))
5148, 49, 50mp3an12 1581 . . . . . . . . . 10 ((vol*‘ ran 𝐹) ∈ ℝ* → ((-∞ < 0 ∧ 0 ≤ (vol*‘ ran 𝐹)) → -∞ < (vol*‘ ran 𝐹)))
5247, 51mpani 689 . . . . . . . . 9 ((vol*‘ ran 𝐹) ∈ ℝ* → (0 ≤ (vol*‘ ran 𝐹) → -∞ < (vol*‘ ran 𝐹)))
5344, 46, 52sylc 65 . . . . . . . 8 (𝜑 → -∞ < (vol*‘ ran 𝐹))
54 xrrebnd 12286 . . . . . . . . . 10 ((vol*‘ ran 𝐹) ∈ ℝ* → ((vol*‘ ran 𝐹) ∈ ℝ ↔ (-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞)))
5544, 54syl 17 . . . . . . . . 9 (𝜑 → ((vol*‘ ran 𝐹) ∈ ℝ ↔ (-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞)))
5636elpw2 5049 . . . . . . . . . . . 12 ( ran 𝐹 ∈ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
5742, 56sylibr 226 . . . . . . . . . . 11 (𝜑 ran 𝐹 ∈ 𝒫 ℝ)
58 simpl 476 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → 𝑥 = ran 𝐹)
5958sseq1d 3856 . . . . . . . . . . . . . 14 ((𝑥 = ran 𝐹𝜑) → (𝑥 ⊆ ℝ ↔ ran 𝐹 ⊆ ℝ))
6058fveq2d 6436 . . . . . . . . . . . . . . . 16 ((𝑥 = ran 𝐹𝜑) → (vol*‘𝑥) = (vol*‘ ran 𝐹))
6160eleq1d 2890 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘ ran 𝐹) ∈ ℝ))
62 simpll 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → 𝑥 = ran 𝐹)
6362ineq1d 4039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹𝑛)) = ( ran 𝐹 ∩ (𝐹𝑛)))
64 fnfvelrn 6604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
6521, 64sylan 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
66 elssuni 4688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐹𝑛) ∈ ran 𝐹 → (𝐹𝑛) ⊆ ran 𝐹)
6765, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ran 𝐹)
6867adantll 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ran 𝐹)
69 sseqin2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑛) ⊆ ran 𝐹 ↔ ( ran 𝐹 ∩ (𝐹𝑛)) = (𝐹𝑛))
7068, 69sylib 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → ( ran 𝐹 ∩ (𝐹𝑛)) = (𝐹𝑛))
7163, 70eqtrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹𝑛)) = (𝐹𝑛))
7271fveq2d 6436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹𝑛))) = (vol*‘(𝐹𝑛)))
7313adantll 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
7472, 73eqtr4d 2863 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹𝑛))) = (vol‘(𝐹𝑛)))
7574mpteq2dva 4966 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 = ran 𝐹𝜑) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))))
7675adantrr 710 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))))
7776, 3, 263eqtr4g 2885 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → 𝐻 = 𝐺)
7877seqeq3d 13102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → seq1( + , 𝐻) = seq1( + , 𝐺))
7978, 25syl6eqr 2878 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → seq1( + , 𝐻) = 𝑆)
8079fveq1d 6434 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (seq1( + , 𝐻)‘𝑘) = (𝑆𝑘))
81 difeq1 3947 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ran 𝐹 → (𝑥 ran 𝐹) = ( ran 𝐹 ran 𝐹))
82 difid 4177 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ran 𝐹 ran 𝐹) = ∅
8381, 82syl6eq 2876 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ran 𝐹 → (𝑥 ran 𝐹) = ∅)
8483fveq2d 6436 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ran 𝐹 → (vol*‘(𝑥 ran 𝐹)) = (vol*‘∅))
85 ovol0 23658 . . . . . . . . . . . . . . . . . . . . . 22 (vol*‘∅) = 0
8684, 85syl6eq 2876 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ran 𝐹 → (vol*‘(𝑥 ran 𝐹)) = 0)
8786adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (vol*‘(𝑥 ran 𝐹)) = 0)
8880, 87oveq12d 6922 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) = ((𝑆𝑘) + 0))
89 nnuz 12004 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℕ = (ℤ‘1)
90 1zzd 11735 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 1 ∈ ℤ)
91 2fveq3 6437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → (vol‘(𝐹𝑛)) = (vol‘(𝐹𝑘)))
92 fvex 6445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (vol‘(𝐹𝑘)) ∈ V
9391, 26, 92fvmpt 6528 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ℕ → (𝐺𝑘) = (vol‘(𝐹𝑘)))
9493adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) = (vol‘(𝐹𝑘)))
95 2fveq3 6437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑘 → (vol‘(𝐹𝑖)) = (vol‘(𝐹𝑘)))
9695eleq1d 2890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑘 → ((vol‘(𝐹𝑖)) ∈ ℝ ↔ (vol‘(𝐹𝑘)) ∈ ℝ))
9796rspccva 3524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹𝑘)) ∈ ℝ)
9814, 97sylan 577 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → (vol‘(𝐹𝑘)) ∈ ℝ)
9994, 98eqeltrd 2905 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
10089, 90, 99serfre 13123 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
10125feq1i 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆:ℕ⟶ℝ ↔ seq1( + , 𝐺):ℕ⟶ℝ)
102100, 101sylibr 226 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆:ℕ⟶ℝ)
103102ffvelrnda 6607 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
104103adantl 475 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑆𝑘) ∈ ℝ)
105104recnd 10384 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑆𝑘) ∈ ℂ)
106105addid1d 10554 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((𝑆𝑘) + 0) = (𝑆𝑘))
10788, 106eqtrd 2860 . . . . . . . . . . . . . . . . . 18 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) = (𝑆𝑘))
108 fveq2 6432 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ran 𝐹 → (vol*‘𝑥) = (vol*‘ ran 𝐹))
109108adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (vol*‘𝑥) = (vol*‘ ran 𝐹))
110107, 109breq12d 4885 . . . . . . . . . . . . . . . . 17 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
111110expr 450 . . . . . . . . . . . . . . . 16 ((𝑥 = ran 𝐹𝜑) → (𝑘 ∈ ℕ → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
112111pm5.74d 265 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → ((𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)) ↔ (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
11361, 112imbi12d 336 . . . . . . . . . . . . . 14 ((𝑥 = ran 𝐹𝜑) → (((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))) ↔ ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))
11459, 113imbi12d 336 . . . . . . . . . . . . 13 ((𝑥 = ran 𝐹𝜑) → ((𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)))) ↔ ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))))
115114pm5.74da 840 . . . . . . . . . . . 12 (𝑥 = ran 𝐹 → ((𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))))) ↔ (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))))
11613ad2ant1 1169 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
11723ad2ant1 1169 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → Disj 𝑖 ∈ ℕ (𝐹𝑖))
118 simp2 1173 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝑥 ⊆ ℝ)
119 simp3 1174 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘𝑥) ∈ ℝ)
120116, 117, 3, 118, 119voliunlem1 23715 . . . . . . . . . . . . 13 (((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))
1211203exp1 1467 . . . . . . . . . . . 12 (𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)))))
122115, 121vtoclg 3481 . . . . . . . . . . 11 ( ran 𝐹 ∈ 𝒫 ℝ → (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))))
12357, 122mpcom 38 . . . . . . . . . 10 (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))
12442, 123mpd 15 . . . . . . . . 9 (𝜑 → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
12555, 124sylbird 252 . . . . . . . 8 (𝜑 → ((-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞) → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
12653, 125mpand 688 . . . . . . 7 (𝜑 → ((vol*‘ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
127 nltpnft 12282 . . . . . . . . 9 ((vol*‘ ran 𝐹) ∈ ℝ* → ((vol*‘ ran 𝐹) = +∞ ↔ ¬ (vol*‘ ran 𝐹) < +∞))
12844, 127syl 17 . . . . . . . 8 (𝜑 → ((vol*‘ ran 𝐹) = +∞ ↔ ¬ (vol*‘ ran 𝐹) < +∞))
129 rexr 10401 . . . . . . . . . . 11 ((𝑆𝑘) ∈ ℝ → (𝑆𝑘) ∈ ℝ*)
130 pnfge 12249 . . . . . . . . . . 11 ((𝑆𝑘) ∈ ℝ* → (𝑆𝑘) ≤ +∞)
131103, 129, 1303syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ +∞)
132131ex 403 . . . . . . . . 9 (𝜑 → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ +∞))
133 breq2 4876 . . . . . . . . . 10 ((vol*‘ ran 𝐹) = +∞ → ((𝑆𝑘) ≤ (vol*‘ ran 𝐹) ↔ (𝑆𝑘) ≤ +∞))
134133imbi2d 332 . . . . . . . . 9 ((vol*‘ ran 𝐹) = +∞ → ((𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)) ↔ (𝑘 ∈ ℕ → (𝑆𝑘) ≤ +∞)))
135132, 134syl5ibrcom 239 . . . . . . . 8 (𝜑 → ((vol*‘ ran 𝐹) = +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
136128, 135sylbird 252 . . . . . . 7 (𝜑 → (¬ (vol*‘ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
137126, 136pm2.61d 172 . . . . . 6 (𝜑 → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
138137ralrimiv 3173 . . . . 5 (𝜑 → ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹))
139102ffnd 6278 . . . . . 6 (𝜑𝑆 Fn ℕ)
140 breq1 4875 . . . . . . 7 (𝑧 = (𝑆𝑘) → (𝑧 ≤ (vol*‘ ran 𝐹) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
141140ralrn 6610 . . . . . 6 (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
142139, 141syl 17 . . . . 5 (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
143138, 142mpbird 249 . . . 4 (𝜑 → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹))
144102frnd 6284 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
145 ressxr 10399 . . . . . 6 ℝ ⊆ ℝ*
146144, 145syl6ss 3838 . . . . 5 (𝜑 → ran 𝑆 ⊆ ℝ*)
147 supxrleub 12443 . . . . 5 ((ran 𝑆 ⊆ ℝ* ∧ (vol*‘ ran 𝐹) ∈ ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹)))
148146, 44, 147syl2anc 581 . . . 4 (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹)))
149143, 148mpbird 249 . . 3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹))
150 supxrcl 12432 . . . . 5 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
151146, 150syl 17 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
152 xrletri3 12272 . . . 4 (((vol*‘ ran 𝐹) ∈ ℝ* ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ*) → ((vol*‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ) ↔ ((vol*‘ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹))))
15344, 151, 152syl2anc 581 . . 3 (𝜑 → ((vol*‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ) ↔ ((vol*‘ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹))))
15433, 149, 153mpbir2and 706 . 2 (𝜑 → (vol*‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
1556, 154eqtrd 2860 1 (𝜑 → (vol‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1113   = wceq 1658  wcel 2166  wral 3116  cdif 3794  cin 3796  wss 3797  c0 4143  𝒫 cpw 4377   cuni 4657   ciun 4739  Disj wdisj 4840   class class class wbr 4872  cmpt 4951  dom cdm 5341  ran crn 5342   Fn wfn 6117  wf 6118  cfv 6122  (class class class)co 6904  supcsup 8614  cr 10250  0cc0 10251  1c1 10252   + caddc 10254  +∞cpnf 10387  -∞cmnf 10388  *cxr 10389   < clt 10390  cle 10391  cn 11349  seqcseq 13094  vol*covol 23627  volcvol 23628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-rep 4993  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-inf2 8814  ax-cc 9571  ax-cnex 10307  ax-resscn 10308  ax-1cn 10309  ax-icn 10310  ax-addcl 10311  ax-addrcl 10312  ax-mulcl 10313  ax-mulrcl 10314  ax-mulcom 10315  ax-addass 10316  ax-mulass 10317  ax-distr 10318  ax-i2m1 10319  ax-1ne0 10320  ax-1rid 10321  ax-rnegex 10322  ax-rrecex 10323  ax-cnre 10324  ax-pre-lttri 10325  ax-pre-lttrn 10326  ax-pre-ltadd 10327  ax-pre-mulgt0 10328  ax-pre-sup 10329
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-uni 4658  df-int 4697  df-iun 4741  df-disj 4841  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-se 5301  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-isom 6131  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-of 7156  df-om 7326  df-1st 7427  df-2nd 7428  df-wrecs 7671  df-recs 7733  df-rdg 7771  df-1o 7825  df-2o 7826  df-oadd 7829  df-er 8008  df-map 8123  df-pm 8124  df-en 8222  df-dom 8223  df-sdom 8224  df-fin 8225  df-sup 8616  df-inf 8617  df-oi 8683  df-card 9077  df-cda 9304  df-pnf 10392  df-mnf 10393  df-xr 10394  df-ltxr 10395  df-le 10396  df-sub 10586  df-neg 10587  df-div 11009  df-nn 11350  df-2 11413  df-3 11414  df-n0 11618  df-z 11704  df-uz 11968  df-q 12071  df-rp 12112  df-xadd 12232  df-ioo 12466  df-ico 12468  df-icc 12469  df-fz 12619  df-fzo 12760  df-fl 12887  df-seq 13095  df-exp 13154  df-hash 13410  df-cj 14215  df-re 14216  df-im 14217  df-sqrt 14351  df-abs 14352  df-clim 14595  df-rlim 14596  df-sum 14793  df-xmet 20098  df-met 20099  df-ovol 23629  df-vol 23630
This theorem is referenced by:  voliun  23719
  Copyright terms: Public domain W3C validator