Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovolval5lem2 Structured version   Visualization version   GIF version

Theorem ovolval5lem2 42477
Description: |- ( ( ph /\ n e. NN ) -> <. ( ( 1st (𝐹 n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd (𝐹 n ) ) >. e. ( RR X. RR ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
ovolval5lem2.q 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
ovolval5lem2.y (𝜑𝑌 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
ovolval5lem2.z 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))
ovolval5lem2.f (𝜑𝐹:ℕ⟶(ℝ × ℝ))
ovolval5lem2.s (𝜑𝐴 ran ([,) ∘ 𝐹))
ovolval5lem2.w (𝜑𝑊 ∈ ℝ+)
ovolval5lem2.g 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
Assertion
Ref Expression
ovolval5lem2 (𝜑 → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
Distinct variable groups:   𝐴,𝑓,𝑧   𝑛,𝐹   𝑓,𝐺   𝑛,𝐺   𝑧,𝑄   𝑛,𝑊   𝑧,𝑊   𝑧,𝑌   𝑓,𝑍,𝑧   𝜑,𝑛
Allowed substitution hints:   𝜑(𝑧,𝑓)   𝐴(𝑛)   𝑄(𝑓,𝑛)   𝐹(𝑧,𝑓)   𝐺(𝑧)   𝑊(𝑓)   𝑌(𝑓,𝑛)   𝑍(𝑛)

Proof of Theorem ovolval5lem2
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 ovolval5lem2.z . . . . . 6 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))
21a1i 11 . . . . 5 (𝜑𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))
3 nnex 11492 . . . . . . 7 ℕ ∈ V
43a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
5 volioof 41814 . . . . . . . 8 (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞)
65a1i 11 . . . . . . 7 (𝜑 → (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞))
7 rexpssxrxp 10532 . . . . . . . 8 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
87a1i 11 . . . . . . 7 (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
9 ovolval5lem2.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
109ffvelrnda 6716 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ (ℝ × ℝ))
11 xp1st 7577 . . . . . . . . . . 11 ((𝐹𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
1210, 11syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
13 ovolval5lem2.w . . . . . . . . . . . . 13 (𝜑𝑊 ∈ ℝ+)
1413rpred 12281 . . . . . . . . . . . 12 (𝜑𝑊 ∈ ℝ)
1514adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ)
16 2nn 11558 . . . . . . . . . . . . . . 15 2 ∈ ℕ
1716a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 2 ∈ ℕ)
18 nnnn0 11752 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
1917, 18nnexpcld 13456 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
2019nnred 11501 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
2120adantl 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
2219nnne0d 11535 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
2322adantl 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
2415, 21, 23redivcld 11316 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ)
2512, 24resubcld 10916 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ ℝ)
26 xp2nd 7578 . . . . . . . . . 10 ((𝐹𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2710, 26syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2825, 27opelxpd 5481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ (ℝ × ℝ))
29 ovolval5lem2.g . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
3028, 29fmptd 6741 . . . . . . 7 (𝜑𝐺:ℕ⟶(ℝ × ℝ))
316, 8, 30fcoss 41013 . . . . . 6 (𝜑 → ((vol ∘ (,)) ∘ 𝐺):ℕ⟶(0[,]+∞))
324, 31sge0xrcl 42209 . . . . 5 (𝜑 → (Σ^‘((vol ∘ (,)) ∘ 𝐺)) ∈ ℝ*)
332, 32eqeltrd 2883 . . . 4 (𝜑𝑍 ∈ ℝ*)
34 reex 10474 . . . . . . . . 9 ℝ ∈ V
3534, 34xpex 7333 . . . . . . . 8 (ℝ × ℝ) ∈ V
3635a1i 11 . . . . . . 7 (𝜑 → (ℝ × ℝ) ∈ V)
3736, 4elmapd 8270 . . . . . 6 (𝜑 → (𝐺 ∈ ((ℝ × ℝ) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶(ℝ × ℝ)))
3830, 37mpbird 258 . . . . 5 (𝜑𝐺 ∈ ((ℝ × ℝ) ↑𝑚 ℕ))
39 ovolval5lem2.s . . . . . . 7 (𝜑𝐴 ran ([,) ∘ 𝐹))
4030ffvelrnda 6716 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ (ℝ × ℝ))
41 xp1st 7577 . . . . . . . . . . . . . 14 ((𝐺𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
4240, 41syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
4342rexrd 10537 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ*)
44 xp2nd 7578 . . . . . . . . . . . . . 14 ((𝐺𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
4540, 44syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
4645rexrd 10537 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ*)
4713adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ+)
4819nnrpd 12279 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
4948adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
5047, 49rpdivcld 12298 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ+)
5112, 50ltsubrpd 12313 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) < (1st ‘(𝐹𝑛)))
52 id 22 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ)
53 opex 5248 . . . . . . . . . . . . . . . . . . 19 ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V)
5529fvmpt2 6645 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V) → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
5652, 54, 55syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
5756fveq2d 6542 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩))
58 ovex 7048 . . . . . . . . . . . . . . . . . 18 ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ V
59 fvex 6551 . . . . . . . . . . . . . . . . . 18 (2nd ‘(𝐹𝑛)) ∈ V
60 op1stg 7557 . . . . . . . . . . . . . . . . . 18 ((((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ V ∧ (2nd ‘(𝐹𝑛)) ∈ V) → (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6158, 59, 60mp2an 688 . . . . . . . . . . . . . . . . 17 (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))
6261a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6357, 62eqtrd 2831 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6463adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6564breq1d 4972 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)) ↔ ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) < (1st ‘(𝐹𝑛))))
6651, 65mpbird 258 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)))
6756fveq2d 6542 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩))
6858, 59op2nd 7554 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = (2nd ‘(𝐹𝑛))
6968a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = (2nd ‘(𝐹𝑛)))
7067, 69eqtrd 2831 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘(𝐹𝑛)))
7170adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = (2nd ‘(𝐹𝑛)))
7271eqcomd 2801 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) = (2nd ‘(𝐺𝑛)))
7327, 72eqled 10590 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ≤ (2nd ‘(𝐺𝑛)))
74 icossioo 12678 . . . . . . . . . . . 12 ((((1st ‘(𝐺𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐺𝑛)) ∈ ℝ*) ∧ ((1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)) ∧ (2nd ‘(𝐹𝑛)) ≤ (2nd ‘(𝐺𝑛)))) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
7543, 46, 66, 73, 74syl22anc 835 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
76 1st2nd2 7584 . . . . . . . . . . . . . . 15 ((𝐹𝑛) ∈ (ℝ × ℝ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
7710, 76syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
7877fveq2d 6542 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
79 df-ov 7019 . . . . . . . . . . . . . 14 ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
8079a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
8178, 80eqtr4d 2834 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) = ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))))
82 1st2nd2 7584 . . . . . . . . . . . . . . 15 ((𝐺𝑛) ∈ (ℝ × ℝ) → (𝐺𝑛) = ⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8340, 82syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = ⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8483fveq2d 6542 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐺𝑛)) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩))
85 df-ov 7019 . . . . . . . . . . . . . 14 ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8685a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩))
8784, 86eqtr4d 2834 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐺𝑛)) = ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
8881, 87sseq12d 3921 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)) ↔ ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛)))))
8975, 88mpbird 258 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)))
9089ralrimiva 3149 . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)))
91 ss2iun 4842 . . . . . . . . 9 (∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)) → 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
9290, 91syl 17 . . . . . . . 8 (𝜑 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
93 fvex 6551 . . . . . . . . . . . . 13 ([,)‘(𝐹𝑛)) ∈ V
9493rgenw 3117 . . . . . . . . . . . 12 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V
9594a1i 11 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V)
96 dfiun3g 5716 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V → 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) = ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
9795, 96syl 17 . . . . . . . . . 10 (𝜑 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) = ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
98 icof 41022 . . . . . . . . . . . . . . 15 [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
9998a1i 11 . . . . . . . . . . . . . 14 (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
1009, 8, 99fcomptss 41006 . . . . . . . . . . . . 13 (𝜑 → ([,) ∘ 𝐹) = (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
101100eqcomd 2801 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ([,) ∘ 𝐹))
102101rneqd 5690 . . . . . . . . . . 11 (𝜑 → ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ran ([,) ∘ 𝐹))
103102unieqd 4755 . . . . . . . . . 10 (𝜑 ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ran ([,) ∘ 𝐹))
10497, 103eqtr2d 2832 . . . . . . . . 9 (𝜑 ran ([,) ∘ 𝐹) = 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)))
105 fvex 6551 . . . . . . . . . . . . 13 ((,)‘(𝐺𝑛)) ∈ V
106105rgenw 3117 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V
107106a1i 11 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V)
108 dfiun3g 5716 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V → 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) = ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
109107, 108syl 17 . . . . . . . . . 10 (𝜑 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) = ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
110 ioof 12685 . . . . . . . . . . . . . . 15 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
111110a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
11230, 8, 111fcomptss 41006 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
113112eqcomd 2801 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ((,) ∘ 𝐺))
114113rneqd 5690 . . . . . . . . . . 11 (𝜑 → ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ran ((,) ∘ 𝐺))
115114unieqd 4755 . . . . . . . . . 10 (𝜑 ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ran ((,) ∘ 𝐺))
116109, 115eqtr2d 2832 . . . . . . . . 9 (𝜑 ran ((,) ∘ 𝐺) = 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
117104, 116sseq12d 3921 . . . . . . . 8 (𝜑 → ( ran ([,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐺) ↔ 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛))))
11892, 117mpbird 258 . . . . . . 7 (𝜑 ran ([,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐺))
11939, 118sstrd 3899 . . . . . 6 (𝜑𝐴 ran ((,) ∘ 𝐺))
120119, 2jca 512 . . . . 5 (𝜑 → (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))))
121 coeq2 5615 . . . . . . . . . 10 (𝑓 = 𝐺 → ((,) ∘ 𝑓) = ((,) ∘ 𝐺))
122121rneqd 5690 . . . . . . . . 9 (𝑓 = 𝐺 → ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝐺))
123122unieqd 4755 . . . . . . . 8 (𝑓 = 𝐺 ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝐺))
124123sseq2d 3920 . . . . . . 7 (𝑓 = 𝐺 → (𝐴 ran ((,) ∘ 𝑓) ↔ 𝐴 ran ((,) ∘ 𝐺)))
125 coeq2 5615 . . . . . . . . 9 (𝑓 = 𝐺 → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘ 𝐺))
126125fveq2d 6542 . . . . . . . 8 (𝑓 = 𝐺 → (Σ^‘((vol ∘ (,)) ∘ 𝑓)) = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))
127126eqeq2d 2805 . . . . . . 7 (𝑓 = 𝐺 → (𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))))
128124, 127anbi12d 630 . . . . . 6 (𝑓 = 𝐺 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))))
129128rspcev 3559 . . . . 5 ((𝐺 ∈ ((ℝ × ℝ) ↑𝑚 ℕ) ∧ (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))) → ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
13038, 120, 129syl2anc 584 . . . 4 (𝜑 → ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
13133, 130jca 512 . . 3 (𝜑 → (𝑍 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
132 eqeq1 2799 . . . . . 6 (𝑧 = 𝑍 → (𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
133132anbi2d 628 . . . . 5 (𝑧 = 𝑍 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
134133rexbidv 3260 . . . 4 (𝑧 = 𝑍 → (∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
135 ovolval5lem2.q . . . 4 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
136134, 135elrab2 3621 . . 3 (𝑍𝑄 ↔ (𝑍 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
137131, 136sylibr 235 . 2 (𝜑𝑍𝑄)
138 2fveq3 6543 . . . . . 6 (𝑚 = 𝑛 → (1st ‘(𝐹𝑚)) = (1st ‘(𝐹𝑛)))
139 2fveq3 6543 . . . . . 6 (𝑚 = 𝑛 → (2nd ‘(𝐹𝑚)) = (2nd ‘(𝐹𝑛)))
140138, 139breq12d 4975 . . . . 5 (𝑚 = 𝑛 → ((1st ‘(𝐹𝑚)) < (2nd ‘(𝐹𝑚)) ↔ (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛))))
141140cbvrabv 3434 . . . 4 {𝑚 ∈ ℕ ∣ (1st ‘(𝐹𝑚)) < (2nd ‘(𝐹𝑚))} = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛))}
14212, 27, 13, 141ovolval5lem1 42476 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊))
143 nfcv 2949 . . . . . . . 8 𝑛𝐺
14430, 8fssd 6396 . . . . . . . 8 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
145143, 144volioofmpt 41821 . . . . . . 7 (𝜑 → ((vol ∘ (,)) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))))
14664, 71oveq12d 7034 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = (((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))
147146fveq2d 6542 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛)))) = (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))
148147mpteq2dva 5055 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))) = (𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))))
149145, 148eqtrd 2831 . . . . . 6 (𝜑 → ((vol ∘ (,)) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))))
150149fveq2d 6542 . . . . 5 (𝜑 → (Σ^‘((vol ∘ (,)) ∘ 𝐺)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))))
1512, 150eqtrd 2831 . . . 4 (𝜑𝑍 = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))))
152 ovolval5lem2.y . . . . . 6 (𝜑𝑌 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
153 nfcv 2949 . . . . . . . 8 𝑛𝐹
154 ressxr 10531 . . . . . . . . . . 11 ℝ ⊆ ℝ*
155 xpss2 5463 . . . . . . . . . . 11 (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
156154, 155ax-mp 5 . . . . . . . . . 10 (ℝ × ℝ) ⊆ (ℝ × ℝ*)
157156a1i 11 . . . . . . . . 9 (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
1589, 157fssd 6396 . . . . . . . 8 (𝜑𝐹:ℕ⟶(ℝ × ℝ*))
159153, 158volicofmpt 41824 . . . . . . 7 (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))))))
160159fveq2d 6542 . . . . . 6 (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))))
161152, 160eqtrd 2831 . . . . 5 (𝜑𝑌 = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))))
162161oveq1d 7031 . . . 4 (𝜑 → (𝑌 +𝑒 𝑊) = ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊))
163151, 162breq12d 4975 . . 3 (𝜑 → (𝑍 ≤ (𝑌 +𝑒 𝑊) ↔ (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊)))
164142, 163mpbird 258 . 2 (𝜑𝑍 ≤ (𝑌 +𝑒 𝑊))
165 breq1 4965 . . 3 (𝑧 = 𝑍 → (𝑧 ≤ (𝑌 +𝑒 𝑊) ↔ 𝑍 ≤ (𝑌 +𝑒 𝑊)))
166165rspcev 3559 . 2 ((𝑍𝑄𝑍 ≤ (𝑌 +𝑒 𝑊)) → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
167137, 164, 166syl2anc 584 1 (𝜑 → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wcel 2081  wne 2984  wral 3105  wrex 3106  {crab 3109  Vcvv 3437  wss 3859  𝒫 cpw 4453  cop 4478   cuni 4745   ciun 4825   class class class wbr 4962  cmpt 5041   × cxp 5441  ran crn 5444  ccom 5447  wf 6221  cfv 6225  (class class class)co 7016  1st c1st 7543  2nd c2nd 7544  𝑚 cmap 8256  cr 10382  0cc0 10383  +∞cpnf 10518  *cxr 10520   < clt 10521  cle 10522  cmin 10717   / cdiv 11145  cn 11486  2c2 11540  +crp 12239   +𝑒 cxad 12355  (,)cioo 12588  [,)cico 12590  [,]cicc 12591  cexp 13279  volcvol 23747  Σ^csumge0 42186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-of 7267  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-2o 7954  df-oadd 7957  df-er 8139  df-map 8258  df-pm 8259  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-fi 8721  df-sup 8752  df-inf 8753  df-oi 8820  df-dju 9176  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-n0 11746  df-z 11830  df-uz 12094  df-q 12198  df-rp 12240  df-xneg 12357  df-xadd 12358  df-xmul 12359  df-ioo 12592  df-ico 12594  df-icc 12595  df-fz 12743  df-fzo 12884  df-fl 13012  df-seq 13220  df-exp 13280  df-hash 13541  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-clim 14679  df-rlim 14680  df-sum 14877  df-rest 16525  df-topgen 16546  df-psmet 20219  df-xmet 20220  df-met 20221  df-bl 20222  df-mopn 20223  df-top 21186  df-topon 21203  df-bases 21238  df-cmp 21679  df-ovol 23748  df-vol 23749  df-sumge0 42187
This theorem is referenced by:  ovolval5lem3  42478
  Copyright terms: Public domain W3C validator