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

Theorem voliunlem3 25501
Description: Lemma for voliun 25503. (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 25500 . . 3 (𝜑 ran 𝐹 ∈ dom vol)
5 mblvol 25479 . . 3 ( ran 𝐹 ∈ dom vol → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
64, 5syl 17 . 2 (𝜑 → (vol‘ ran 𝐹) = (vol*‘ ran 𝐹))
71frnd 6735 . . . . . 6 (𝜑 → ran 𝐹 ⊆ dom vol)
8 mblss 25480 . . . . . . . 8 (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
9 reex 11237 . . . . . . . . 9 ℝ ∈ V
109elpw2 5351 . . . . . . . 8 (𝑥 ∈ 𝒫 ℝ ↔ 𝑥 ⊆ ℝ)
118, 10sylibr 233 . . . . . . 7 (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫 ℝ)
1211ssriv 3986 . . . . . 6 dom vol ⊆ 𝒫 ℝ
137, 12sstrdi 3994 . . . . 5 (𝜑 → ran 𝐹 ⊆ 𝒫 ℝ)
14 sspwuni 5107 . . . . 5 (ran 𝐹 ⊆ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
1513, 14sylib 217 . . . 4 (𝜑 ran 𝐹 ⊆ ℝ)
16 ovolcl 25427 . . . 4 ( ran 𝐹 ⊆ ℝ → (vol*‘ ran 𝐹) ∈ ℝ*)
1715, 16syl 17 . . 3 (𝜑 → (vol*‘ ran 𝐹) ∈ ℝ*)
18 nnuz 12903 . . . . . . . 8 ℕ = (ℤ‘1)
19 1zzd 12631 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
20 2fveq3 6907 . . . . . . . . . . 11 (𝑛 = 𝑘 → (vol‘(𝐹𝑛)) = (vol‘(𝐹𝑘)))
21 voliunlem3.2 . . . . . . . . . . 11 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛)))
22 fvex 6915 . . . . . . . . . . 11 (vol‘(𝐹𝑘)) ∈ V
2320, 21, 22fvmpt 7010 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝐺𝑘) = (vol‘(𝐹𝑘)))
2423adantl 480 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) = (vol‘(𝐹𝑘)))
25 voliunlem3.4 . . . . . . . . . 10 (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ)
26 2fveq3 6907 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (vol‘(𝐹𝑖)) = (vol‘(𝐹𝑘)))
2726eleq1d 2814 . . . . . . . . . . 11 (𝑖 = 𝑘 → ((vol‘(𝐹𝑖)) ∈ ℝ ↔ (vol‘(𝐹𝑘)) ∈ ℝ))
2827rspccva 3610 . . . . . . . . . 10 ((∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ ∧ 𝑘 ∈ ℕ) → (vol‘(𝐹𝑘)) ∈ ℝ)
2925, 28sylan 578 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (vol‘(𝐹𝑘)) ∈ ℝ)
3024, 29eqeltrd 2829 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
3118, 19, 30serfre 14036 . . . . . . 7 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
32 voliunlem3.1 . . . . . . . 8 𝑆 = seq1( + , 𝐺)
3332feq1i 6718 . . . . . . 7 (𝑆:ℕ⟶ℝ ↔ seq1( + , 𝐺):ℕ⟶ℝ)
3431, 33sylibr 233 . . . . . 6 (𝜑𝑆:ℕ⟶ℝ)
3534frnd 6735 . . . . 5 (𝜑 → ran 𝑆 ⊆ ℝ)
36 ressxr 11296 . . . . 5 ℝ ⊆ ℝ*
3735, 36sstrdi 3994 . . . 4 (𝜑 → ran 𝑆 ⊆ ℝ*)
38 supxrcl 13334 . . . 4 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
3937, 38syl 17 . . 3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
40 eqid 2728 . . . . 5 seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
41 eqid 2728 . . . . 5 (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))
421ffvelcdmda 7099 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ dom vol)
43 mblss 25480 . . . . . 6 ((𝐹𝑛) ∈ dom vol → (𝐹𝑛) ⊆ ℝ)
4442, 43syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ℝ)
45 mblvol 25479 . . . . . . 7 ((𝐹𝑛) ∈ dom vol → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
4642, 45syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
47 2fveq3 6907 . . . . . . . . 9 (𝑖 = 𝑛 → (vol‘(𝐹𝑖)) = (vol‘(𝐹𝑛)))
4847eleq1d 2814 . . . . . . . 8 (𝑖 = 𝑛 → ((vol‘(𝐹𝑖)) ∈ ℝ ↔ (vol‘(𝐹𝑛)) ∈ ℝ))
4948rspccva 3610 . . . . . . 7 ((∀𝑖 ∈ ℕ (vol‘(𝐹𝑖)) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) ∈ ℝ)
5025, 49sylan 578 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) ∈ ℝ)
5146, 50eqeltrrd 2830 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (vol*‘(𝐹𝑛)) ∈ ℝ)
5240, 41, 44, 51ovoliun 25454 . . . 4 (𝜑 → (vol*‘ 𝑛 ∈ ℕ (𝐹𝑛)) ≤ sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))), ℝ*, < ))
531ffnd 6728 . . . . . 6 (𝜑𝐹 Fn ℕ)
54 fniunfv 7263 . . . . . 6 (𝐹 Fn ℕ → 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
5553, 54syl 17 . . . . 5 (𝜑 𝑛 ∈ ℕ (𝐹𝑛) = ran 𝐹)
5655fveq2d 6906 . . . 4 (𝜑 → (vol*‘ 𝑛 ∈ ℕ (𝐹𝑛)) = (vol*‘ ran 𝐹))
5746mpteq2dva 5252 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))) = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
5821, 57eqtrid 2780 . . . . . . . 8 (𝜑𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛))))
5958seqeq3d 14014 . . . . . . 7 (𝜑 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))))
6032, 59eqtr2id 2781 . . . . . 6 (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = 𝑆)
6160rneqd 5944 . . . . 5 (𝜑 → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))) = ran 𝑆)
6261supeq1d 9477 . . . 4 (𝜑 → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol*‘(𝐹𝑛)))), ℝ*, < ) = sup(ran 𝑆, ℝ*, < ))
6352, 56, 623brtr3d 5183 . . 3 (𝜑 → (vol*‘ ran 𝐹) ≤ sup(ran 𝑆, ℝ*, < ))
64 ovolge0 25430 . . . . . . . . . 10 ( ran 𝐹 ⊆ ℝ → 0 ≤ (vol*‘ ran 𝐹))
6515, 64syl 17 . . . . . . . . 9 (𝜑 → 0 ≤ (vol*‘ ran 𝐹))
66 mnflt0 13145 . . . . . . . . . 10 -∞ < 0
67 mnfxr 11309 . . . . . . . . . . 11 -∞ ∈ ℝ*
68 0xr 11299 . . . . . . . . . . 11 0 ∈ ℝ*
69 xrltletr 13176 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (vol*‘ ran 𝐹) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (vol*‘ ran 𝐹)) → -∞ < (vol*‘ ran 𝐹)))
7067, 68, 69mp3an12 1447 . . . . . . . . . 10 ((vol*‘ ran 𝐹) ∈ ℝ* → ((-∞ < 0 ∧ 0 ≤ (vol*‘ ran 𝐹)) → -∞ < (vol*‘ ran 𝐹)))
7166, 70mpani 694 . . . . . . . . 9 ((vol*‘ ran 𝐹) ∈ ℝ* → (0 ≤ (vol*‘ ran 𝐹) → -∞ < (vol*‘ ran 𝐹)))
7217, 65, 71sylc 65 . . . . . . . 8 (𝜑 → -∞ < (vol*‘ ran 𝐹))
73 xrrebnd 13187 . . . . . . . . . 10 ((vol*‘ ran 𝐹) ∈ ℝ* → ((vol*‘ ran 𝐹) ∈ ℝ ↔ (-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞)))
7417, 73syl 17 . . . . . . . . 9 (𝜑 → ((vol*‘ ran 𝐹) ∈ ℝ ↔ (-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞)))
759elpw2 5351 . . . . . . . . . . . 12 ( ran 𝐹 ∈ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
7615, 75sylibr 233 . . . . . . . . . . 11 (𝜑 ran 𝐹 ∈ 𝒫 ℝ)
77 simpl 481 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → 𝑥 = ran 𝐹)
7877sseq1d 4013 . . . . . . . . . . . . . 14 ((𝑥 = ran 𝐹𝜑) → (𝑥 ⊆ ℝ ↔ ran 𝐹 ⊆ ℝ))
7977fveq2d 6906 . . . . . . . . . . . . . . . 16 ((𝑥 = ran 𝐹𝜑) → (vol*‘𝑥) = (vol*‘ ran 𝐹))
8079eleq1d 2814 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘ ran 𝐹) ∈ ℝ))
81 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → 𝑥 = ran 𝐹)
8281ineq1d 4213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹𝑛)) = ( ran 𝐹 ∩ (𝐹𝑛)))
83 fnfvelrn 7095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹 Fn ℕ ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
8453, 83sylan 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ran 𝐹)
85 elssuni 4944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐹𝑛) ∈ ran 𝐹 → (𝐹𝑛) ⊆ ran 𝐹)
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ran 𝐹)
8786adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ⊆ ran 𝐹)
88 sseqin2 4217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑛) ⊆ ran 𝐹 ↔ ( ran 𝐹 ∩ (𝐹𝑛)) = (𝐹𝑛))
8987, 88sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → ( ran 𝐹 ∩ (𝐹𝑛)) = (𝐹𝑛))
9082, 89eqtrd 2768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (𝑥 ∩ (𝐹𝑛)) = (𝐹𝑛))
9190fveq2d 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹𝑛))) = (vol*‘(𝐹𝑛)))
9246adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐹𝑛)) = (vol*‘(𝐹𝑛)))
9391, 92eqtr4d 2771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 = ran 𝐹𝜑) ∧ 𝑛 ∈ ℕ) → (vol*‘(𝑥 ∩ (𝐹𝑛))) = (vol‘(𝐹𝑛)))
9493mpteq2dva 5252 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 = ran 𝐹𝜑) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))))
9594adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹𝑛)))) = (𝑛 ∈ ℕ ↦ (vol‘(𝐹𝑛))))
9695, 3, 213eqtr4g 2793 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → 𝐻 = 𝐺)
9796seqeq3d 14014 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → seq1( + , 𝐻) = seq1( + , 𝐺))
9897, 32eqtr4di 2786 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → seq1( + , 𝐻) = 𝑆)
9998fveq1d 6904 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (seq1( + , 𝐻)‘𝑘) = (𝑆𝑘))
100 difeq1 4115 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ran 𝐹 → (𝑥 ran 𝐹) = ( ran 𝐹 ran 𝐹))
101 difid 4374 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ran 𝐹 ran 𝐹) = ∅
102100, 101eqtrdi 2784 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ran 𝐹 → (𝑥 ran 𝐹) = ∅)
103102fveq2d 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ran 𝐹 → (vol*‘(𝑥 ran 𝐹)) = (vol*‘∅))
104 ovol0 25442 . . . . . . . . . . . . . . . . . . . . . 22 (vol*‘∅) = 0
105103, 104eqtrdi 2784 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ran 𝐹 → (vol*‘(𝑥 ran 𝐹)) = 0)
106105adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (vol*‘(𝑥 ran 𝐹)) = 0)
10799, 106oveq12d 7444 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) = ((𝑆𝑘) + 0))
10834ffvelcdmda 7099 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
109108adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑆𝑘) ∈ ℝ)
110109recnd 11280 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (𝑆𝑘) ∈ ℂ)
111110addridd 11452 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((𝑆𝑘) + 0) = (𝑆𝑘))
112107, 111eqtrd 2768 . . . . . . . . . . . . . . . . . 18 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) = (𝑆𝑘))
113 fveq2 6902 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ran 𝐹 → (vol*‘𝑥) = (vol*‘ ran 𝐹))
114113adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (vol*‘𝑥) = (vol*‘ ran 𝐹))
115112, 114breq12d 5165 . . . . . . . . . . . . . . . . 17 ((𝑥 = ran 𝐹 ∧ (𝜑𝑘 ∈ ℕ)) → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
116115expr 455 . . . . . . . . . . . . . . . 16 ((𝑥 = ran 𝐹𝜑) → (𝑘 ∈ ℕ → (((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
117116pm5.74d 272 . . . . . . . . . . . . . . 15 ((𝑥 = ran 𝐹𝜑) → ((𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)) ↔ (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
11880, 117imbi12d 343 . . . . . . . . . . . . . 14 ((𝑥 = ran 𝐹𝜑) → (((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))) ↔ ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))
11978, 118imbi12d 343 . . . . . . . . . . . . 13 ((𝑥 = ran 𝐹𝜑) → ((𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)))) ↔ ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))))
120119pm5.74da 802 . . . . . . . . . . . 12 (𝑥 = ran 𝐹 → ((𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))))) ↔ (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))))
12113ad2ant1 1130 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝐹:ℕ⟶dom vol)
12223ad2ant1 1130 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → Disj 𝑖 ∈ ℕ (𝐹𝑖))
123 simp2 1134 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → 𝑥 ⊆ ℝ)
124 simp3 1135 . . . . . . . . . . . . . 14 ((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘𝑥) ∈ ℝ)
125121, 122, 3, 123, 124voliunlem1 25499 . . . . . . . . . . . . 13 (((𝜑𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥))
1261253exp1 1349 . . . . . . . . . . . 12 (𝜑 → (𝑥 ⊆ ℝ → ((vol*‘𝑥) ∈ ℝ → (𝑘 ∈ ℕ → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝑥 ran 𝐹))) ≤ (vol*‘𝑥)))))
127120, 126vtoclg 3542 . . . . . . . . . . 11 ( ran 𝐹 ∈ 𝒫 ℝ → (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))))
12876, 127mpcom 38 . . . . . . . . . 10 (𝜑 → ( ran 𝐹 ⊆ ℝ → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))))
12915, 128mpd 15 . . . . . . . . 9 (𝜑 → ((vol*‘ ran 𝐹) ∈ ℝ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
13074, 129sylbird 259 . . . . . . . 8 (𝜑 → ((-∞ < (vol*‘ ran 𝐹) ∧ (vol*‘ ran 𝐹) < +∞) → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
13172, 130mpand 693 . . . . . . 7 (𝜑 → ((vol*‘ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
132 nltpnft 13183 . . . . . . . . 9 ((vol*‘ ran 𝐹) ∈ ℝ* → ((vol*‘ ran 𝐹) = +∞ ↔ ¬ (vol*‘ ran 𝐹) < +∞))
13317, 132syl 17 . . . . . . . 8 (𝜑 → ((vol*‘ ran 𝐹) = +∞ ↔ ¬ (vol*‘ ran 𝐹) < +∞))
134 rexr 11298 . . . . . . . . . . 11 ((𝑆𝑘) ∈ ℝ → (𝑆𝑘) ∈ ℝ*)
135 pnfge 13150 . . . . . . . . . . 11 ((𝑆𝑘) ∈ ℝ* → (𝑆𝑘) ≤ +∞)
136108, 134, 1353syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ +∞)
137136ex 411 . . . . . . . . 9 (𝜑 → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ +∞))
138 breq2 5156 . . . . . . . . . 10 ((vol*‘ ran 𝐹) = +∞ → ((𝑆𝑘) ≤ (vol*‘ ran 𝐹) ↔ (𝑆𝑘) ≤ +∞))
139138imbi2d 339 . . . . . . . . 9 ((vol*‘ ran 𝐹) = +∞ → ((𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)) ↔ (𝑘 ∈ ℕ → (𝑆𝑘) ≤ +∞)))
140137, 139syl5ibrcom 246 . . . . . . . 8 (𝜑 → ((vol*‘ ran 𝐹) = +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
141133, 140sylbird 259 . . . . . . 7 (𝜑 → (¬ (vol*‘ ran 𝐹) < +∞ → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹))))
142131, 141pm2.61d 179 . . . . . 6 (𝜑 → (𝑘 ∈ ℕ → (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
143142ralrimiv 3142 . . . . 5 (𝜑 → ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹))
14434ffnd 6728 . . . . . 6 (𝜑𝑆 Fn ℕ)
145 breq1 5155 . . . . . . 7 (𝑧 = (𝑆𝑘) → (𝑧 ≤ (vol*‘ ran 𝐹) ↔ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
146145ralrn 7103 . . . . . 6 (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
147144, 146syl 17 . . . . 5 (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ (vol*‘ ran 𝐹)))
148143, 147mpbird 256 . . . 4 (𝜑 → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹))
149 supxrleub 13345 . . . . 5 ((ran 𝑆 ⊆ ℝ* ∧ (vol*‘ ran 𝐹) ∈ ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹)))
15037, 17, 149syl2anc 582 . . . 4 (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹) ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ (vol*‘ ran 𝐹)))
151148, 150mpbird 256 . . 3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ (vol*‘ ran 𝐹))
15217, 39, 63, 151xrletrid 13174 . 2 (𝜑 → (vol*‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
1536, 152eqtrd 2768 1 (𝜑 → (vol‘ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3058  cdif 3946  cin 3948  wss 3949  c0 4326  𝒫 cpw 4606   cuni 4912   ciun 5000  Disj wdisj 5117   class class class wbr 5152  cmpt 5235  dom cdm 5682  ran crn 5683   Fn wfn 6548  wf 6549  cfv 6553  (class class class)co 7426  supcsup 9471  cr 11145  0cc0 11146  1c1 11147   + caddc 11149  +∞cpnf 11283  -∞cmnf 11284  *cxr 11285   < clt 11286  cle 11287  cn 12250  seqcseq 14006  vol*covol 25411  volcvol 25412
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672  ax-cc 10466  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-disj 5118  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-2o 8494  df-er 8731  df-map 8853  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-sup 9473  df-inf 9474  df-oi 9541  df-dju 9932  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-n0 12511  df-z 12597  df-uz 12861  df-q 12971  df-rp 13015  df-xadd 13133  df-ioo 13368  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-fl 13797  df-seq 14007  df-exp 14067  df-hash 14330  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-clim 15472  df-rlim 15473  df-sum 15673  df-xmet 21279  df-met 21280  df-ovol 25413  df-vol 25414
This theorem is referenced by:  voliun  25503
  Copyright terms: Public domain W3C validator