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 44884
Description: ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ (ℝ × ℝ)). (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
ovolval5lem2.q 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 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 12159 . . . . . . 7 ℕ ∈ V
43a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
5 volioof 44218 . . . . . . . 8 (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞)
65a1i 11 . . . . . . 7 (𝜑 → (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞))
7 rexpssxrxp 11200 . . . . . . . 8 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
87a1i 11 . . . . . . 7 (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
9 ovolval5lem2.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
109ffvelcdmda 7035 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ (ℝ × ℝ))
11 xp1st 7953 . . . . . . . . . . 11 ((𝐹𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
1210, 11syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
13 ovolval5lem2.w . . . . . . . . . . . . 13 (𝜑𝑊 ∈ ℝ+)
1413rpred 12957 . . . . . . . . . . . 12 (𝜑𝑊 ∈ ℝ)
1514adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ)
16 2nn 12226 . . . . . . . . . . . . . . 15 2 ∈ ℕ
1716a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 2 ∈ ℕ)
18 nnnn0 12420 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
1917, 18nnexpcld 14148 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
2019nnred 12168 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
2120adantl 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
2219nnne0d 12203 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
2322adantl 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
2415, 21, 23redivcld 11983 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ)
2512, 24resubcld 11583 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ ℝ)
26 xp2nd 7954 . . . . . . . . . 10 ((𝐹𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2710, 26syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2825, 27opelxpd 5671 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ (ℝ × ℝ))
29 ovolval5lem2.g . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
3028, 29fmptd 7062 . . . . . . 7 (𝜑𝐺:ℕ⟶(ℝ × ℝ))
316, 8, 30fcoss 43421 . . . . . 6 (𝜑 → ((vol ∘ (,)) ∘ 𝐺):ℕ⟶(0[,]+∞))
324, 31sge0xrcl 44616 . . . . 5 (𝜑 → (Σ^‘((vol ∘ (,)) ∘ 𝐺)) ∈ ℝ*)
332, 32eqeltrd 2838 . . . 4 (𝜑𝑍 ∈ ℝ*)
34 reex 11142 . . . . . . . . 9 ℝ ∈ V
3534, 34xpex 7687 . . . . . . . 8 (ℝ × ℝ) ∈ V
3635a1i 11 . . . . . . 7 (𝜑 → (ℝ × ℝ) ∈ V)
3736, 4elmapd 8779 . . . . . 6 (𝜑 → (𝐺 ∈ ((ℝ × ℝ) ↑m ℕ) ↔ 𝐺:ℕ⟶(ℝ × ℝ)))
3830, 37mpbird 256 . . . . 5 (𝜑𝐺 ∈ ((ℝ × ℝ) ↑m ℕ))
39 ovolval5lem2.s . . . . . . 7 (𝜑𝐴 ran ([,) ∘ 𝐹))
4030ffvelcdmda 7035 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ (ℝ × ℝ))
41 xp1st 7953 . . . . . . . . . . . . . 14 ((𝐺𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
4240, 41syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
4342rexrd 11205 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ*)
44 xp2nd 7954 . . . . . . . . . . . . . 14 ((𝐺𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
4540, 44syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
4645rexrd 11205 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ*)
4713adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ+)
4819nnrpd 12955 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
4948adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
5047, 49rpdivcld 12974 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ+)
5112, 50ltsubrpd 12989 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) < (1st ‘(𝐹𝑛)))
52 id 22 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ)
53 opex 5421 . . . . . . . . . . . . . . . . . . 19 ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V)
5529fvmpt2 6959 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V) → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
5652, 54, 55syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
5756fveq2d 6846 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩))
58 ovex 7390 . . . . . . . . . . . . . . . . . 18 ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ V
59 fvex 6855 . . . . . . . . . . . . . . . . . 18 (2nd ‘(𝐹𝑛)) ∈ V
60 op1stg 7933 . . . . . . . . . . . . . . . . . 18 ((((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ V ∧ (2nd ‘(𝐹𝑛)) ∈ V) → (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6158, 59, 60mp2an 690 . . . . . . . . . . . . . . . . 17 (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))
6261a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6357, 62eqtrd 2776 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6463adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6564breq1d 5115 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)) ↔ ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) < (1st ‘(𝐹𝑛))))
6651, 65mpbird 256 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)))
6756fveq2d 6846 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩))
6858, 59op2nd 7930 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = (2nd ‘(𝐹𝑛))
6968a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = (2nd ‘(𝐹𝑛)))
7067, 69eqtrd 2776 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘(𝐹𝑛)))
7170adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = (2nd ‘(𝐹𝑛)))
7271eqcomd 2742 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) = (2nd ‘(𝐺𝑛)))
7327, 72eqled 11258 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ≤ (2nd ‘(𝐺𝑛)))
74 icossioo 13357 . . . . . . . . . . . 12 ((((1st ‘(𝐺𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐺𝑛)) ∈ ℝ*) ∧ ((1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)) ∧ (2nd ‘(𝐹𝑛)) ≤ (2nd ‘(𝐺𝑛)))) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
7543, 46, 66, 73, 74syl22anc 837 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
76 1st2nd2 7960 . . . . . . . . . . . . . . 15 ((𝐹𝑛) ∈ (ℝ × ℝ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
7710, 76syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
7877fveq2d 6846 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
79 df-ov 7360 . . . . . . . . . . . . . 14 ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
8079a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
8178, 80eqtr4d 2779 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) = ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))))
82 1st2nd2 7960 . . . . . . . . . . . . . . 15 ((𝐺𝑛) ∈ (ℝ × ℝ) → (𝐺𝑛) = ⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8340, 82syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = ⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8483fveq2d 6846 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐺𝑛)) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩))
85 df-ov 7360 . . . . . . . . . . . . . 14 ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8685a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩))
8784, 86eqtr4d 2779 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐺𝑛)) = ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
8881, 87sseq12d 3977 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)) ↔ ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛)))))
8975, 88mpbird 256 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)))
9089ralrimiva 3143 . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)))
91 ss2iun 4972 . . . . . . . . 9 (∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)) → 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
9290, 91syl 17 . . . . . . . 8 (𝜑 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
93 fvex 6855 . . . . . . . . . . . . 13 ([,)‘(𝐹𝑛)) ∈ V
9493rgenw 3068 . . . . . . . . . . . 12 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V
9594a1i 11 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V)
96 dfiun3g 5919 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V → 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) = ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
9795, 96syl 17 . . . . . . . . . 10 (𝜑 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) = ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
98 icof 43430 . . . . . . . . . . . . . . 15 [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
9998a1i 11 . . . . . . . . . . . . . 14 (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
1009, 8, 99fcomptss 43414 . . . . . . . . . . . . 13 (𝜑 → ([,) ∘ 𝐹) = (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
101100eqcomd 2742 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ([,) ∘ 𝐹))
102101rneqd 5893 . . . . . . . . . . 11 (𝜑 → ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ran ([,) ∘ 𝐹))
103102unieqd 4879 . . . . . . . . . 10 (𝜑 ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ran ([,) ∘ 𝐹))
10497, 103eqtr2d 2777 . . . . . . . . 9 (𝜑 ran ([,) ∘ 𝐹) = 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)))
105 fvex 6855 . . . . . . . . . . . . 13 ((,)‘(𝐺𝑛)) ∈ V
106105rgenw 3068 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V
107106a1i 11 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V)
108 dfiun3g 5919 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V → 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) = ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
109107, 108syl 17 . . . . . . . . . 10 (𝜑 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) = ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
110 ioof 13364 . . . . . . . . . . . . . . 15 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
111110a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
11230, 8, 111fcomptss 43414 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
113112eqcomd 2742 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ((,) ∘ 𝐺))
114113rneqd 5893 . . . . . . . . . . 11 (𝜑 → ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ran ((,) ∘ 𝐺))
115114unieqd 4879 . . . . . . . . . 10 (𝜑 ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ran ((,) ∘ 𝐺))
116109, 115eqtr2d 2777 . . . . . . . . 9 (𝜑 ran ((,) ∘ 𝐺) = 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
117104, 116sseq12d 3977 . . . . . . . 8 (𝜑 → ( ran ([,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐺) ↔ 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛))))
11892, 117mpbird 256 . . . . . . 7 (𝜑 ran ([,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐺))
11939, 118sstrd 3954 . . . . . 6 (𝜑𝐴 ran ((,) ∘ 𝐺))
120119, 2jca 512 . . . . 5 (𝜑 → (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))))
121 coeq2 5814 . . . . . . . . . 10 (𝑓 = 𝐺 → ((,) ∘ 𝑓) = ((,) ∘ 𝐺))
122121rneqd 5893 . . . . . . . . 9 (𝑓 = 𝐺 → ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝐺))
123122unieqd 4879 . . . . . . . 8 (𝑓 = 𝐺 ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝐺))
124123sseq2d 3976 . . . . . . 7 (𝑓 = 𝐺 → (𝐴 ran ((,) ∘ 𝑓) ↔ 𝐴 ran ((,) ∘ 𝐺)))
125 coeq2 5814 . . . . . . . . 9 (𝑓 = 𝐺 → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘ 𝐺))
126125fveq2d 6846 . . . . . . . 8 (𝑓 = 𝐺 → (Σ^‘((vol ∘ (,)) ∘ 𝑓)) = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))
127126eqeq2d 2747 . . . . . . 7 (𝑓 = 𝐺 → (𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))))
128124, 127anbi12d 631 . . . . . 6 (𝑓 = 𝐺 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))))
129128rspcev 3581 . . . . 5 ((𝐺 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))) → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
13038, 120, 129syl2anc 584 . . . 4 (𝜑 → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
13133, 130jca 512 . . 3 (𝜑 → (𝑍 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
132 eqeq1 2740 . . . . . 6 (𝑧 = 𝑍 → (𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
133132anbi2d 629 . . . . 5 (𝑧 = 𝑍 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
134133rexbidv 3175 . . . 4 (𝑧 = 𝑍 → (∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
135 ovolval5lem2.q . . . 4 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
136134, 135elrab2 3648 . . 3 (𝑍𝑄 ↔ (𝑍 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
137131, 136sylibr 233 . 2 (𝜑𝑍𝑄)
138 2fveq3 6847 . . . . . 6 (𝑚 = 𝑛 → (1st ‘(𝐹𝑚)) = (1st ‘(𝐹𝑛)))
139 2fveq3 6847 . . . . . 6 (𝑚 = 𝑛 → (2nd ‘(𝐹𝑚)) = (2nd ‘(𝐹𝑛)))
140138, 139breq12d 5118 . . . . 5 (𝑚 = 𝑛 → ((1st ‘(𝐹𝑚)) < (2nd ‘(𝐹𝑚)) ↔ (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛))))
141140cbvrabv 3417 . . . 4 {𝑚 ∈ ℕ ∣ (1st ‘(𝐹𝑚)) < (2nd ‘(𝐹𝑚))} = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛))}
14212, 27, 13, 141ovolval5lem1 44883 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊))
143 nfcv 2907 . . . . . . . 8 𝑛𝐺
14430, 8fssd 6686 . . . . . . . 8 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
145143, 144volioofmpt 44225 . . . . . . 7 (𝜑 → ((vol ∘ (,)) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))))
14664, 71oveq12d 7375 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = (((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))
147146fveq2d 6846 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛)))) = (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))
148147mpteq2dva 5205 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))) = (𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))))
149145, 148eqtrd 2776 . . . . . 6 (𝜑 → ((vol ∘ (,)) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))))
150149fveq2d 6846 . . . . 5 (𝜑 → (Σ^‘((vol ∘ (,)) ∘ 𝐺)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))))
1512, 150eqtrd 2776 . . . 4 (𝜑𝑍 = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))))
152 ovolval5lem2.y . . . . . 6 (𝜑𝑌 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
153 nfcv 2907 . . . . . . . 8 𝑛𝐹
154 ressxr 11199 . . . . . . . . . . 11 ℝ ⊆ ℝ*
155 xpss2 5653 . . . . . . . . . . 11 (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
156154, 155ax-mp 5 . . . . . . . . . 10 (ℝ × ℝ) ⊆ (ℝ × ℝ*)
157156a1i 11 . . . . . . . . 9 (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
1589, 157fssd 6686 . . . . . . . 8 (𝜑𝐹:ℕ⟶(ℝ × ℝ*))
159153, 158volicofmpt 44228 . . . . . . 7 (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))))))
160159fveq2d 6846 . . . . . 6 (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))))
161152, 160eqtrd 2776 . . . . 5 (𝜑𝑌 = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))))
162161oveq1d 7372 . . . 4 (𝜑 → (𝑌 +𝑒 𝑊) = ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊))
163151, 162breq12d 5118 . . 3 (𝜑 → (𝑍 ≤ (𝑌 +𝑒 𝑊) ↔ (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊)))
164142, 163mpbird 256 . 2 (𝜑𝑍 ≤ (𝑌 +𝑒 𝑊))
165 breq1 5108 . . 3 (𝑧 = 𝑍 → (𝑧 ≤ (𝑌 +𝑒 𝑊) ↔ 𝑍 ≤ (𝑌 +𝑒 𝑊)))
166165rspcev 3581 . 2 ((𝑍𝑄𝑍 ≤ (𝑌 +𝑒 𝑊)) → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
167137, 164, 166syl2anc 584 1 (𝜑 → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  wss 3910  𝒫 cpw 4560  cop 4592   cuni 4865   ciun 4954   class class class wbr 5105  cmpt 5188   × cxp 5631  ran crn 5634  ccom 5637  wf 6492  cfv 6496  (class class class)co 7357  1st c1st 7919  2nd c2nd 7920  m cmap 8765  cr 11050  0cc0 11051  +∞cpnf 11186  *cxr 11188   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  +crp 12915   +𝑒 cxad 13031  (,)cioo 13264  [,)cico 13266  [,]cicc 13267  cexp 13967  volcvol 24827  Σ^csumge0 44593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-rlim 15371  df-sum 15571  df-rest 17304  df-topgen 17325  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-top 22243  df-topon 22260  df-bases 22296  df-cmp 22738  df-ovol 24828  df-vol 24829  df-sumge0 44594
This theorem is referenced by:  ovolval5lem3  44885
  Copyright terms: Public domain W3C validator