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 41507
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 11281 . . . . . . 7 ℕ ∈ V
43a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
5 volioof 40841 . . . . . . . 8 (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞)
65a1i 11 . . . . . . 7 (𝜑 → (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞))
7 rexpssxrxp 10338 . . . . . . . 8 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
87a1i 11 . . . . . . 7 (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
9 ovolval5lem2.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
109ffvelrnda 6549 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ (ℝ × ℝ))
11 xp1st 7398 . . . . . . . . . . 11 ((𝐹𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
1210, 11syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
13 ovolval5lem2.w . . . . . . . . . . . . 13 (𝜑𝑊 ∈ ℝ+)
1413rpred 12070 . . . . . . . . . . . 12 (𝜑𝑊 ∈ ℝ)
1514adantr 472 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ)
16 2nn 11345 . . . . . . . . . . . . . . 15 2 ∈ ℕ
1716a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 2 ∈ ℕ)
18 nnnn0 11546 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
1917, 18nnexpcld 13237 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
2019nnred 11291 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
2120adantl 473 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
2219nnne0d 11322 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
2322adantl 473 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
2415, 21, 23redivcld 11107 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ)
2512, 24resubcld 10712 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ ℝ)
26 xp2nd 7399 . . . . . . . . . 10 ((𝐹𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2710, 26syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2825, 27opelxpd 5315 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ (ℝ × ℝ))
29 ovolval5lem2.g . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
3028, 29fmptd 6574 . . . . . . 7 (𝜑𝐺:ℕ⟶(ℝ × ℝ))
316, 8, 30fcoss 40047 . . . . . 6 (𝜑 → ((vol ∘ (,)) ∘ 𝐺):ℕ⟶(0[,]+∞))
324, 31sge0xrcl 41239 . . . . 5 (𝜑 → (Σ^‘((vol ∘ (,)) ∘ 𝐺)) ∈ ℝ*)
332, 32eqeltrd 2844 . . . 4 (𝜑𝑍 ∈ ℝ*)
34 reex 10280 . . . . . . . . 9 ℝ ∈ V
3534, 34xpex 7160 . . . . . . . 8 (ℝ × ℝ) ∈ V
3635a1i 11 . . . . . . 7 (𝜑 → (ℝ × ℝ) ∈ V)
3736, 4elmapd 8074 . . . . . 6 (𝜑 → (𝐺 ∈ ((ℝ × ℝ) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶(ℝ × ℝ)))
3830, 37mpbird 248 . . . . 5 (𝜑𝐺 ∈ ((ℝ × ℝ) ↑𝑚 ℕ))
39 ovolval5lem2.s . . . . . . 7 (𝜑𝐴 ran ([,) ∘ 𝐹))
4030ffvelrnda 6549 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ (ℝ × ℝ))
41 xp1st 7398 . . . . . . . . . . . . . 14 ((𝐺𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
4240, 41syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
4342rexrd 10343 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ*)
44 xp2nd 7399 . . . . . . . . . . . . . 14 ((𝐺𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
4540, 44syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
4645rexrd 10343 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ*)
4713adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ+)
4819nnrpd 12068 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
4948adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
5047, 49rpdivcld 12087 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ+)
5112, 50ltsubrpd 12102 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) < (1st ‘(𝐹𝑛)))
52 id 22 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ)
53 opex 5088 . . . . . . . . . . . . . . . . . . 19 ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V)
5529fvmpt2 6480 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V) → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
5652, 54, 55syl2anc 579 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
5756fveq2d 6379 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩))
58 ovex 6874 . . . . . . . . . . . . . . . . . 18 ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ V
59 fvex 6388 . . . . . . . . . . . . . . . . . 18 (2nd ‘(𝐹𝑛)) ∈ V
60 op1stg 7378 . . . . . . . . . . . . . . . . . 18 ((((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ V ∧ (2nd ‘(𝐹𝑛)) ∈ V) → (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6158, 59, 60mp2an 683 . . . . . . . . . . . . . . . . 17 (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))
6261a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6357, 62eqtrd 2799 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6463adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6564breq1d 4819 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)) ↔ ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) < (1st ‘(𝐹𝑛))))
6651, 65mpbird 248 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)))
6756fveq2d 6379 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩))
6858, 59op2nd 7375 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = (2nd ‘(𝐹𝑛))
6968a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = (2nd ‘(𝐹𝑛)))
7067, 69eqtrd 2799 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘(𝐹𝑛)))
7170adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = (2nd ‘(𝐹𝑛)))
7271eqcomd 2771 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) = (2nd ‘(𝐺𝑛)))
7327, 72eqled 10394 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ≤ (2nd ‘(𝐺𝑛)))
74 icossioo 12467 . . . . . . . . . . . 12 ((((1st ‘(𝐺𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐺𝑛)) ∈ ℝ*) ∧ ((1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)) ∧ (2nd ‘(𝐹𝑛)) ≤ (2nd ‘(𝐺𝑛)))) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
7543, 46, 66, 73, 74syl22anc 867 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
76 1st2nd2 7405 . . . . . . . . . . . . . . 15 ((𝐹𝑛) ∈ (ℝ × ℝ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
7710, 76syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
7877fveq2d 6379 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
79 df-ov 6845 . . . . . . . . . . . . . 14 ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
8079a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
8178, 80eqtr4d 2802 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) = ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))))
82 1st2nd2 7405 . . . . . . . . . . . . . . 15 ((𝐺𝑛) ∈ (ℝ × ℝ) → (𝐺𝑛) = ⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8340, 82syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = ⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8483fveq2d 6379 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐺𝑛)) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩))
85 df-ov 6845 . . . . . . . . . . . . . 14 ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8685a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩))
8784, 86eqtr4d 2802 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐺𝑛)) = ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
8881, 87sseq12d 3794 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)) ↔ ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛)))))
8975, 88mpbird 248 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)))
9089ralrimiva 3113 . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)))
91 ss2iun 4692 . . . . . . . . 9 (∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)) → 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
9290, 91syl 17 . . . . . . . 8 (𝜑 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
93 fvex 6388 . . . . . . . . . . . . 13 ([,)‘(𝐹𝑛)) ∈ V
9493rgenw 3071 . . . . . . . . . . . 12 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V
9594a1i 11 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V)
96 dfiun3g 5547 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V → 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) = ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
9795, 96syl 17 . . . . . . . . . 10 (𝜑 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) = ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
98 icof 40056 . . . . . . . . . . . . . . 15 [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
9998a1i 11 . . . . . . . . . . . . . 14 (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
1009, 8, 99fcomptss 40040 . . . . . . . . . . . . 13 (𝜑 → ([,) ∘ 𝐹) = (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
101100eqcomd 2771 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ([,) ∘ 𝐹))
102101rneqd 5521 . . . . . . . . . . 11 (𝜑 → ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ran ([,) ∘ 𝐹))
103102unieqd 4604 . . . . . . . . . 10 (𝜑 ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ran ([,) ∘ 𝐹))
10497, 103eqtr2d 2800 . . . . . . . . 9 (𝜑 ran ([,) ∘ 𝐹) = 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)))
105 fvex 6388 . . . . . . . . . . . . 13 ((,)‘(𝐺𝑛)) ∈ V
106105rgenw 3071 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V
107106a1i 11 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V)
108 dfiun3g 5547 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V → 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) = ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
109107, 108syl 17 . . . . . . . . . 10 (𝜑 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) = ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
110 ioof 12474 . . . . . . . . . . . . . . 15 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
111110a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
11230, 8, 111fcomptss 40040 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
113112eqcomd 2771 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ((,) ∘ 𝐺))
114113rneqd 5521 . . . . . . . . . . 11 (𝜑 → ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ran ((,) ∘ 𝐺))
115114unieqd 4604 . . . . . . . . . 10 (𝜑 ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ran ((,) ∘ 𝐺))
116109, 115eqtr2d 2800 . . . . . . . . 9 (𝜑 ran ((,) ∘ 𝐺) = 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
117104, 116sseq12d 3794 . . . . . . . 8 (𝜑 → ( ran ([,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐺) ↔ 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛))))
11892, 117mpbird 248 . . . . . . 7 (𝜑 ran ([,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐺))
11939, 118sstrd 3771 . . . . . 6 (𝜑𝐴 ran ((,) ∘ 𝐺))
120119, 2jca 507 . . . . 5 (𝜑 → (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))))
121 coeq2 5449 . . . . . . . . . 10 (𝑓 = 𝐺 → ((,) ∘ 𝑓) = ((,) ∘ 𝐺))
122121rneqd 5521 . . . . . . . . 9 (𝑓 = 𝐺 → ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝐺))
123122unieqd 4604 . . . . . . . 8 (𝑓 = 𝐺 ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝐺))
124123sseq2d 3793 . . . . . . 7 (𝑓 = 𝐺 → (𝐴 ran ((,) ∘ 𝑓) ↔ 𝐴 ran ((,) ∘ 𝐺)))
125 coeq2 5449 . . . . . . . . 9 (𝑓 = 𝐺 → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘ 𝐺))
126125fveq2d 6379 . . . . . . . 8 (𝑓 = 𝐺 → (Σ^‘((vol ∘ (,)) ∘ 𝑓)) = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))
127126eqeq2d 2775 . . . . . . 7 (𝑓 = 𝐺 → (𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))))
128124, 127anbi12d 624 . . . . . 6 (𝑓 = 𝐺 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))))
129128rspcev 3461 . . . . 5 ((𝐺 ∈ ((ℝ × ℝ) ↑𝑚 ℕ) ∧ (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))) → ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
13038, 120, 129syl2anc 579 . . . 4 (𝜑 → ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
13133, 130jca 507 . . 3 (𝜑 → (𝑍 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
132 eqeq1 2769 . . . . . 6 (𝑧 = 𝑍 → (𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
133132anbi2d 622 . . . . 5 (𝑧 = 𝑍 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
134133rexbidv 3199 . . . 4 (𝑧 = 𝑍 → (∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
135 ovolval5lem2.q . . . 4 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
136134, 135elrab2 3523 . . 3 (𝑍𝑄 ↔ (𝑍 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
137131, 136sylibr 225 . 2 (𝜑𝑍𝑄)
138 2fveq3 6380 . . . . . 6 (𝑚 = 𝑛 → (1st ‘(𝐹𝑚)) = (1st ‘(𝐹𝑛)))
139 2fveq3 6380 . . . . . 6 (𝑚 = 𝑛 → (2nd ‘(𝐹𝑚)) = (2nd ‘(𝐹𝑛)))
140138, 139breq12d 4822 . . . . 5 (𝑚 = 𝑛 → ((1st ‘(𝐹𝑚)) < (2nd ‘(𝐹𝑚)) ↔ (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛))))
141140cbvrabv 3348 . . . 4 {𝑚 ∈ ℕ ∣ (1st ‘(𝐹𝑚)) < (2nd ‘(𝐹𝑚))} = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛))}
14212, 27, 13, 141ovolval5lem1 41506 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊))
143 nfcv 2907 . . . . . . . 8 𝑛𝐺
14430, 8fssd 6237 . . . . . . . 8 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
145143, 144volioofmpt 40848 . . . . . . 7 (𝜑 → ((vol ∘ (,)) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))))
14664, 71oveq12d 6860 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = (((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))
147146fveq2d 6379 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛)))) = (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))
148147mpteq2dva 4903 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))) = (𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))))
149145, 148eqtrd 2799 . . . . . 6 (𝜑 → ((vol ∘ (,)) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))))
150149fveq2d 6379 . . . . 5 (𝜑 → (Σ^‘((vol ∘ (,)) ∘ 𝐺)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))))
1512, 150eqtrd 2799 . . . 4 (𝜑𝑍 = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))))
152 ovolval5lem2.y . . . . . 6 (𝜑𝑌 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
153 nfcv 2907 . . . . . . . 8 𝑛𝐹
154 ressxr 10337 . . . . . . . . . . 11 ℝ ⊆ ℝ*
155 xpss2 5297 . . . . . . . . . . 11 (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
156154, 155ax-mp 5 . . . . . . . . . 10 (ℝ × ℝ) ⊆ (ℝ × ℝ*)
157156a1i 11 . . . . . . . . 9 (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
1589, 157fssd 6237 . . . . . . . 8 (𝜑𝐹:ℕ⟶(ℝ × ℝ*))
159153, 158volicofmpt 40851 . . . . . . 7 (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))))))
160159fveq2d 6379 . . . . . 6 (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))))
161152, 160eqtrd 2799 . . . . 5 (𝜑𝑌 = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))))
162161oveq1d 6857 . . . 4 (𝜑 → (𝑌 +𝑒 𝑊) = ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊))
163151, 162breq12d 4822 . . 3 (𝜑 → (𝑍 ≤ (𝑌 +𝑒 𝑊) ↔ (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊)))
164142, 163mpbird 248 . 2 (𝜑𝑍 ≤ (𝑌 +𝑒 𝑊))
165 breq1 4812 . . 3 (𝑧 = 𝑍 → (𝑧 ≤ (𝑌 +𝑒 𝑊) ↔ 𝑍 ≤ (𝑌 +𝑒 𝑊)))
166165rspcev 3461 . 2 ((𝑍𝑄𝑍 ≤ (𝑌 +𝑒 𝑊)) → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
167137, 164, 166syl2anc 579 1 (𝜑 → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  wss 3732  𝒫 cpw 4315  cop 4340   cuni 4594   ciun 4676   class class class wbr 4809  cmpt 4888   × cxp 5275  ran crn 5278  ccom 5281  wf 6064  cfv 6068  (class class class)co 6842  1st c1st 7364  2nd c2nd 7365  𝑚 cmap 8060  cr 10188  0cc0 10189  +∞cpnf 10325  *cxr 10327   < clt 10328  cle 10329  cmin 10520   / cdiv 10938  cn 11274  2c2 11327  +crp 12028   +𝑒 cxad 12144  (,)cioo 12377  [,)cico 12379  [,]cicc 12380  cexp 13067  volcvol 23521  Σ^csumge0 41216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-rlim 14505  df-sum 14702  df-rest 16349  df-topgen 16370  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-top 20978  df-topon 20995  df-bases 21030  df-cmp 21470  df-ovol 23522  df-vol 23523  df-sumge0 41217
This theorem is referenced by:  ovolval5lem3  41508
  Copyright terms: Public domain W3C validator