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

Theorem ovolval5lem2 43704
 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 11694 . . . . . . 7 ℕ ∈ V
43a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
5 volioof 43041 . . . . . . . 8 (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞)
65a1i 11 . . . . . . 7 (𝜑 → (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞))
7 rexpssxrxp 10738 . . . . . . . 8 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
87a1i 11 . . . . . . 7 (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
9 ovolval5lem2.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
109ffvelrnda 6849 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ (ℝ × ℝ))
11 xp1st 7732 . . . . . . . . . . 11 ((𝐹𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
1210, 11syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
13 ovolval5lem2.w . . . . . . . . . . . . 13 (𝜑𝑊 ∈ ℝ+)
1413rpred 12486 . . . . . . . . . . . 12 (𝜑𝑊 ∈ ℝ)
1514adantr 484 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ)
16 2nn 11761 . . . . . . . . . . . . . . 15 2 ∈ ℕ
1716a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 2 ∈ ℕ)
18 nnnn0 11955 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
1917, 18nnexpcld 13670 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
2019nnred 11703 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
2120adantl 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
2219nnne0d 11738 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
2322adantl 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
2415, 21, 23redivcld 11520 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ)
2512, 24resubcld 11120 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ ℝ)
26 xp2nd 7733 . . . . . . . . . 10 ((𝐹𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2710, 26syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2825, 27opelxpd 5567 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ (ℝ × ℝ))
29 ovolval5lem2.g . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
3028, 29fmptd 6876 . . . . . . 7 (𝜑𝐺:ℕ⟶(ℝ × ℝ))
316, 8, 30fcoss 42255 . . . . . 6 (𝜑 → ((vol ∘ (,)) ∘ 𝐺):ℕ⟶(0[,]+∞))
324, 31sge0xrcl 43436 . . . . 5 (𝜑 → (Σ^‘((vol ∘ (,)) ∘ 𝐺)) ∈ ℝ*)
332, 32eqeltrd 2853 . . . 4 (𝜑𝑍 ∈ ℝ*)
34 reex 10680 . . . . . . . . 9 ℝ ∈ V
3534, 34xpex 7481 . . . . . . . 8 (ℝ × ℝ) ∈ V
3635a1i 11 . . . . . . 7 (𝜑 → (ℝ × ℝ) ∈ V)
3736, 4elmapd 8437 . . . . . 6 (𝜑 → (𝐺 ∈ ((ℝ × ℝ) ↑m ℕ) ↔ 𝐺:ℕ⟶(ℝ × ℝ)))
3830, 37mpbird 260 . . . . 5 (𝜑𝐺 ∈ ((ℝ × ℝ) ↑m ℕ))
39 ovolval5lem2.s . . . . . . 7 (𝜑𝐴 ran ([,) ∘ 𝐹))
4030ffvelrnda 6849 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ (ℝ × ℝ))
41 xp1st 7732 . . . . . . . . . . . . . 14 ((𝐺𝑛) ∈ (ℝ × ℝ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
4240, 41syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ)
4342rexrd 10743 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) ∈ ℝ*)
44 xp2nd 7733 . . . . . . . . . . . . . 14 ((𝐺𝑛) ∈ (ℝ × ℝ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
4540, 44syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ)
4645rexrd 10743 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) ∈ ℝ*)
4713adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ+)
4819nnrpd 12484 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
4948adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
5047, 49rpdivcld 12503 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ+)
5112, 50ltsubrpd 12518 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) < (1st ‘(𝐹𝑛)))
52 id 22 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ)
53 opex 5329 . . . . . . . . . . . . . . . . . . 19 ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V)
5529fvmpt2 6776 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩ ∈ V) → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
5652, 54, 55syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩)
5756fveq2d 6668 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩))
58 ovex 7190 . . . . . . . . . . . . . . . . . 18 ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ V
59 fvex 6677 . . . . . . . . . . . . . . . . . 18 (2nd ‘(𝐹𝑛)) ∈ V
60 op1stg 7712 . . . . . . . . . . . . . . . . . 18 ((((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) ∈ V ∧ (2nd ‘(𝐹𝑛)) ∈ V) → (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6158, 59, 60mp2an 691 . . . . . . . . . . . . . . . . 17 (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))
6261a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (1st ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6357, 62eqtrd 2794 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6463adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))))
6564breq1d 5047 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)) ↔ ((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))) < (1st ‘(𝐹𝑛))))
6651, 65mpbird 260 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)))
6756fveq2d 6668 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩))
6858, 59op2nd 7709 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = (2nd ‘(𝐹𝑛))
6968a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2nd ‘⟨((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹𝑛))⟩) = (2nd ‘(𝐹𝑛)))
7067, 69eqtrd 2794 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘(𝐹𝑛)))
7170adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = (2nd ‘(𝐹𝑛)))
7271eqcomd 2765 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) = (2nd ‘(𝐺𝑛)))
7327, 72eqled 10795 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ≤ (2nd ‘(𝐺𝑛)))
74 icossioo 12886 . . . . . . . . . . . 12 ((((1st ‘(𝐺𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐺𝑛)) ∈ ℝ*) ∧ ((1st ‘(𝐺𝑛)) < (1st ‘(𝐹𝑛)) ∧ (2nd ‘(𝐹𝑛)) ≤ (2nd ‘(𝐺𝑛)))) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
7543, 46, 66, 73, 74syl22anc 837 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
76 1st2nd2 7739 . . . . . . . . . . . . . . 15 ((𝐹𝑛) ∈ (ℝ × ℝ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
7710, 76syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
7877fveq2d 6668 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
79 df-ov 7160 . . . . . . . . . . . . . 14 ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
8079a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) = ([,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
8178, 80eqtr4d 2797 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) = ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))))
82 1st2nd2 7739 . . . . . . . . . . . . . . 15 ((𝐺𝑛) ∈ (ℝ × ℝ) → (𝐺𝑛) = ⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8340, 82syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = ⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8483fveq2d 6668 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐺𝑛)) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩))
85 df-ov 7160 . . . . . . . . . . . . . 14 ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩)
8685a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = ((,)‘⟨(1st ‘(𝐺𝑛)), (2nd ‘(𝐺𝑛))⟩))
8784, 86eqtr4d 2797 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐺𝑛)) = ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))
8881, 87sseq12d 3928 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)) ↔ ((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))) ⊆ ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛)))))
8975, 88mpbird 260 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)))
9089ralrimiva 3114 . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)))
91 ss2iun 4905 . . . . . . . . 9 (∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ ((,)‘(𝐺𝑛)) → 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
9290, 91syl 17 . . . . . . . 8 (𝜑 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
93 fvex 6677 . . . . . . . . . . . . 13 ([,)‘(𝐹𝑛)) ∈ V
9493rgenw 3083 . . . . . . . . . . . 12 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V
9594a1i 11 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V)
96 dfiun3g 5811 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ∈ V → 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) = ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
9795, 96syl 17 . . . . . . . . . 10 (𝜑 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) = ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
98 icof 42264 . . . . . . . . . . . . . . 15 [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
9998a1i 11 . . . . . . . . . . . . . 14 (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
1009, 8, 99fcomptss 42248 . . . . . . . . . . . . 13 (𝜑 → ([,) ∘ 𝐹) = (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))))
101100eqcomd 2765 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ([,) ∘ 𝐹))
102101rneqd 5785 . . . . . . . . . . 11 (𝜑 → ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ran ([,) ∘ 𝐹))
103102unieqd 4816 . . . . . . . . . 10 (𝜑 ran (𝑛 ∈ ℕ ↦ ([,)‘(𝐹𝑛))) = ran ([,) ∘ 𝐹))
10497, 103eqtr2d 2795 . . . . . . . . 9 (𝜑 ran ([,) ∘ 𝐹) = 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)))
105 fvex 6677 . . . . . . . . . . . . 13 ((,)‘(𝐺𝑛)) ∈ V
106105rgenw 3083 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V
107106a1i 11 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V)
108 dfiun3g 5811 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) ∈ V → 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) = ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
109107, 108syl 17 . . . . . . . . . 10 (𝜑 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)) = ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
110 ioof 12893 . . . . . . . . . . . . . . 15 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
111110a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
11230, 8, 111fcomptss 42248 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))))
113112eqcomd 2765 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ((,) ∘ 𝐺))
114113rneqd 5785 . . . . . . . . . . 11 (𝜑 → ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ran ((,) ∘ 𝐺))
115114unieqd 4816 . . . . . . . . . 10 (𝜑 ran (𝑛 ∈ ℕ ↦ ((,)‘(𝐺𝑛))) = ran ((,) ∘ 𝐺))
116109, 115eqtr2d 2795 . . . . . . . . 9 (𝜑 ran ((,) ∘ 𝐺) = 𝑛 ∈ ℕ ((,)‘(𝐺𝑛)))
117104, 116sseq12d 3928 . . . . . . . 8 (𝜑 → ( ran ([,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐺) ↔ 𝑛 ∈ ℕ ([,)‘(𝐹𝑛)) ⊆ 𝑛 ∈ ℕ ((,)‘(𝐺𝑛))))
11892, 117mpbird 260 . . . . . . 7 (𝜑 ran ([,) ∘ 𝐹) ⊆ ran ((,) ∘ 𝐺))
11939, 118sstrd 3905 . . . . . 6 (𝜑𝐴 ran ((,) ∘ 𝐺))
120119, 2jca 515 . . . . 5 (𝜑 → (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))))
121 coeq2 5705 . . . . . . . . . 10 (𝑓 = 𝐺 → ((,) ∘ 𝑓) = ((,) ∘ 𝐺))
122121rneqd 5785 . . . . . . . . 9 (𝑓 = 𝐺 → ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝐺))
123122unieqd 4816 . . . . . . . 8 (𝑓 = 𝐺 ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝐺))
124123sseq2d 3927 . . . . . . 7 (𝑓 = 𝐺 → (𝐴 ran ((,) ∘ 𝑓) ↔ 𝐴 ran ((,) ∘ 𝐺)))
125 coeq2 5705 . . . . . . . . 9 (𝑓 = 𝐺 → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘ 𝐺))
126125fveq2d 6668 . . . . . . . 8 (𝑓 = 𝐺 → (Σ^‘((vol ∘ (,)) ∘ 𝑓)) = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))
127126eqeq2d 2770 . . . . . . 7 (𝑓 = 𝐺 → (𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺))))
128124, 127anbi12d 633 . . . . . 6 (𝑓 = 𝐺 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))))
129128rspcev 3544 . . . . 5 ((𝐺 ∈ ((ℝ × ℝ) ↑m ℕ) ∧ (𝐴 ran ((,) ∘ 𝐺) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)))) → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
13038, 120, 129syl2anc 587 . . . 4 (𝜑 → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
13133, 130jca 515 . . 3 (𝜑 → (𝑍 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
132 eqeq1 2763 . . . . . 6 (𝑧 = 𝑍 → (𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))))
133132anbi2d 631 . . . . 5 (𝑧 = 𝑍 → ((𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
134133rexbidv 3222 . . . 4 (𝑧 = 𝑍 → (∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
135 ovolval5lem2.q . . . 4 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))}
136134, 135elrab2 3608 . . 3 (𝑍𝑄 ↔ (𝑍 ∈ ℝ* ∧ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))))
137131, 136sylibr 237 . 2 (𝜑𝑍𝑄)
138 2fveq3 6669 . . . . . 6 (𝑚 = 𝑛 → (1st ‘(𝐹𝑚)) = (1st ‘(𝐹𝑛)))
139 2fveq3 6669 . . . . . 6 (𝑚 = 𝑛 → (2nd ‘(𝐹𝑚)) = (2nd ‘(𝐹𝑛)))
140138, 139breq12d 5050 . . . . 5 (𝑚 = 𝑛 → ((1st ‘(𝐹𝑚)) < (2nd ‘(𝐹𝑚)) ↔ (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛))))
141140cbvrabv 3405 . . . 4 {𝑚 ∈ ℕ ∣ (1st ‘(𝐹𝑚)) < (2nd ‘(𝐹𝑚))} = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛))}
14212, 27, 13, 141ovolval5lem1 43703 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊))
143 nfcv 2920 . . . . . . . 8 𝑛𝐺
14430, 8fssd 6519 . . . . . . . 8 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
145143, 144volioofmpt 43048 . . . . . . 7 (𝜑 → ((vol ∘ (,)) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))))
14664, 71oveq12d 7175 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))) = (((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))
147146fveq2d 6668 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛)))) = (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))
148147mpteq2dva 5132 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐺𝑛))(,)(2nd ‘(𝐺𝑛))))) = (𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))))
149145, 148eqtrd 2794 . . . . . 6 (𝜑 → ((vol ∘ (,)) ∘ 𝐺) = (𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛))))))
150149fveq2d 6668 . . . . 5 (𝜑 → (Σ^‘((vol ∘ (,)) ∘ 𝐺)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))))
1512, 150eqtrd 2794 . . . 4 (𝜑𝑍 = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))))
152 ovolval5lem2.y . . . . . 6 (𝜑𝑌 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
153 nfcv 2920 . . . . . . . 8 𝑛𝐹
154 ressxr 10737 . . . . . . . . . . 11 ℝ ⊆ ℝ*
155 xpss2 5549 . . . . . . . . . . 11 (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
156154, 155ax-mp 5 . . . . . . . . . 10 (ℝ × ℝ) ⊆ (ℝ × ℝ*)
157156a1i 11 . . . . . . . . 9 (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
1589, 157fssd 6519 . . . . . . . 8 (𝜑𝐹:ℕ⟶(ℝ × ℝ*))
159153, 158volicofmpt 43051 . . . . . . 7 (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛))))))
160159fveq2d 6668 . . . . . 6 (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))))
161152, 160eqtrd 2794 . . . . 5 (𝜑𝑌 = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))))
162161oveq1d 7172 . . . 4 (𝜑 → (𝑌 +𝑒 𝑊) = ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊))
163151, 162breq12d 5050 . . 3 (𝜑 → (𝑍 ≤ (𝑌 +𝑒 𝑊) ↔ (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(((1st ‘(𝐹𝑛)) − (𝑊 / (2↑𝑛)))(,)(2nd ‘(𝐹𝑛)))))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑛))[,)(2nd ‘(𝐹𝑛)))))) +𝑒 𝑊)))
164142, 163mpbird 260 . 2 (𝜑𝑍 ≤ (𝑌 +𝑒 𝑊))
165 breq1 5040 . . 3 (𝑧 = 𝑍 → (𝑧 ≤ (𝑌 +𝑒 𝑊) ↔ 𝑍 ≤ (𝑌 +𝑒 𝑊)))
166165rspcev 3544 . 2 ((𝑍𝑄𝑍 ≤ (𝑌 +𝑒 𝑊)) → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
167137, 164, 166syl2anc 587 1 (𝜑 → ∃𝑧𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1539   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071  ∃wrex 3072  {crab 3075  Vcvv 3410   ⊆ wss 3861  𝒫 cpw 4498  ⟨cop 4532  ∪ cuni 4802  ∪ ciun 4887   class class class wbr 5037   ↦ cmpt 5117   × cxp 5527  ran crn 5530   ∘ ccom 5533  ⟶wf 6337  ‘cfv 6341  (class class class)co 7157  1st c1st 7698  2nd c2nd 7699   ↑m cmap 8423  ℝcr 10588  0cc0 10589  +∞cpnf 10724  ℝ*cxr 10726   < clt 10727   ≤ cle 10728   − cmin 10922   / cdiv 11349  ℕcn 11688  2c2 11743  ℝ+crp 12444   +𝑒 cxad 12560  (,)cioo 12793  [,)cico 12795  [,]cicc 12796  ↑cexp 13493  volcvol 24178  Σ^csumge0 43413 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-inf2 9151  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666  ax-pre-sup 10667 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-se 5489  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-of 7412  df-om 7587  df-1st 7700  df-2nd 7701  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-1o 8119  df-2o 8120  df-er 8306  df-map 8425  df-pm 8426  df-en 8542  df-dom 8543  df-sdom 8544  df-fin 8545  df-fi 8922  df-sup 8953  df-inf 8954  df-oi 9021  df-dju 9377  df-card 9415  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-div 11350  df-nn 11689  df-2 11751  df-3 11752  df-n0 11949  df-z 12035  df-uz 12297  df-q 12403  df-rp 12445  df-xneg 12562  df-xadd 12563  df-xmul 12564  df-ioo 12797  df-ico 12799  df-icc 12800  df-fz 12954  df-fzo 13097  df-fl 13225  df-seq 13433  df-exp 13494  df-hash 13755  df-cj 14520  df-re 14521  df-im 14522  df-sqrt 14656  df-abs 14657  df-clim 14907  df-rlim 14908  df-sum 15105  df-rest 16769  df-topgen 16790  df-psmet 20173  df-xmet 20174  df-met 20175  df-bl 20176  df-mopn 20177  df-top 21609  df-topon 21626  df-bases 21661  df-cmp 22102  df-ovol 24179  df-vol 24180  df-sumge0 43414 This theorem is referenced by:  ovolval5lem3  43705
 Copyright terms: Public domain W3C validator