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

Theorem ovolicc2lem1 23036
Description: Lemma for ovolicc2 23041. (Contributed by Mario Carneiro, 14-Jun-2014.)
Hypotheses
Ref Expression
ovolicc.1 (𝜑𝐴 ∈ ℝ)
ovolicc.2 (𝜑𝐵 ∈ ℝ)
ovolicc.3 (𝜑𝐴𝐵)
ovolicc2.4 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolicc2.5 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ovolicc2.6 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
ovolicc2.7 (𝜑 → (𝐴[,]𝐵) ⊆ 𝑈)
ovolicc2.8 (𝜑𝐺:𝑈⟶ℕ)
ovolicc2.9 ((𝜑𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
Assertion
Ref Expression
ovolicc2lem1 ((𝜑𝑋𝑈) → (𝑃𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑋))) < 𝑃𝑃 < (2nd ‘(𝐹‘(𝐺𝑋))))))
Distinct variable groups:   𝑡,𝐴   𝑡,𝐵   𝑡,𝐹   𝑡,𝐺   𝜑,𝑡   𝑡,𝑈   𝑡,𝑋
Allowed substitution hints:   𝑃(𝑡)   𝑆(𝑡)

Proof of Theorem ovolicc2lem1
StepHypRef Expression
1 ovolicc2.8 . . . . . 6 (𝜑𝐺:𝑈⟶ℕ)
21ffvelrnda 6251 . . . . 5 ((𝜑𝑋𝑈) → (𝐺𝑋) ∈ ℕ)
3 ovolicc2.5 . . . . . . 7 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4 inss2 3795 . . . . . . 7 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
5 fss 5954 . . . . . . 7 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
63, 4, 5sylancl 692 . . . . . 6 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
7 fvco3 6169 . . . . . 6 ((𝐹:ℕ⟶(ℝ × ℝ) ∧ (𝐺𝑋) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺𝑋)) = ((,)‘(𝐹‘(𝐺𝑋))))
86, 7sylan 486 . . . . 5 ((𝜑 ∧ (𝐺𝑋) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺𝑋)) = ((,)‘(𝐹‘(𝐺𝑋))))
92, 8syldan 485 . . . 4 ((𝜑𝑋𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑋)) = ((,)‘(𝐹‘(𝐺𝑋))))
10 ovolicc2.9 . . . . . 6 ((𝜑𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
1110ralrimiva 2948 . . . . 5 (𝜑 → ∀𝑡𝑈 (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
12 fveq2 6087 . . . . . . . 8 (𝑡 = 𝑋 → (𝐺𝑡) = (𝐺𝑋))
1312fveq2d 6091 . . . . . . 7 (𝑡 = 𝑋 → (((,) ∘ 𝐹)‘(𝐺𝑡)) = (((,) ∘ 𝐹)‘(𝐺𝑋)))
14 id 22 . . . . . . 7 (𝑡 = 𝑋𝑡 = 𝑋)
1513, 14eqeq12d 2624 . . . . . 6 (𝑡 = 𝑋 → ((((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡 ↔ (((,) ∘ 𝐹)‘(𝐺𝑋)) = 𝑋))
1615rspccva 3280 . . . . 5 ((∀𝑡𝑈 (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡𝑋𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑋)) = 𝑋)
1711, 16sylan 486 . . . 4 ((𝜑𝑋𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑋)) = 𝑋)
186adantr 479 . . . . . . . 8 ((𝜑𝑋𝑈) → 𝐹:ℕ⟶(ℝ × ℝ))
1918, 2ffvelrnd 6252 . . . . . . 7 ((𝜑𝑋𝑈) → (𝐹‘(𝐺𝑋)) ∈ (ℝ × ℝ))
20 1st2nd2 7073 . . . . . . 7 ((𝐹‘(𝐺𝑋)) ∈ (ℝ × ℝ) → (𝐹‘(𝐺𝑋)) = ⟨(1st ‘(𝐹‘(𝐺𝑋))), (2nd ‘(𝐹‘(𝐺𝑋)))⟩)
2119, 20syl 17 . . . . . 6 ((𝜑𝑋𝑈) → (𝐹‘(𝐺𝑋)) = ⟨(1st ‘(𝐹‘(𝐺𝑋))), (2nd ‘(𝐹‘(𝐺𝑋)))⟩)
2221fveq2d 6091 . . . . 5 ((𝜑𝑋𝑈) → ((,)‘(𝐹‘(𝐺𝑋))) = ((,)‘⟨(1st ‘(𝐹‘(𝐺𝑋))), (2nd ‘(𝐹‘(𝐺𝑋)))⟩))
23 df-ov 6529 . . . . 5 ((1st ‘(𝐹‘(𝐺𝑋)))(,)(2nd ‘(𝐹‘(𝐺𝑋)))) = ((,)‘⟨(1st ‘(𝐹‘(𝐺𝑋))), (2nd ‘(𝐹‘(𝐺𝑋)))⟩)
2422, 23syl6eqr 2661 . . . 4 ((𝜑𝑋𝑈) → ((,)‘(𝐹‘(𝐺𝑋))) = ((1st ‘(𝐹‘(𝐺𝑋)))(,)(2nd ‘(𝐹‘(𝐺𝑋)))))
259, 17, 243eqtr3d 2651 . . 3 ((𝜑𝑋𝑈) → 𝑋 = ((1st ‘(𝐹‘(𝐺𝑋)))(,)(2nd ‘(𝐹‘(𝐺𝑋)))))
2625eleq2d 2672 . 2 ((𝜑𝑋𝑈) → (𝑃𝑋𝑃 ∈ ((1st ‘(𝐹‘(𝐺𝑋)))(,)(2nd ‘(𝐹‘(𝐺𝑋))))))
27 xp1st 7066 . . . 4 ((𝐹‘(𝐺𝑋)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺𝑋))) ∈ ℝ)
2819, 27syl 17 . . 3 ((𝜑𝑋𝑈) → (1st ‘(𝐹‘(𝐺𝑋))) ∈ ℝ)
29 xp2nd 7067 . . . 4 ((𝐹‘(𝐺𝑋)) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺𝑋))) ∈ ℝ)
3019, 29syl 17 . . 3 ((𝜑𝑋𝑈) → (2nd ‘(𝐹‘(𝐺𝑋))) ∈ ℝ)
31 rexr 9941 . . . 4 ((1st ‘(𝐹‘(𝐺𝑋))) ∈ ℝ → (1st ‘(𝐹‘(𝐺𝑋))) ∈ ℝ*)
32 rexr 9941 . . . 4 ((2nd ‘(𝐹‘(𝐺𝑋))) ∈ ℝ → (2nd ‘(𝐹‘(𝐺𝑋))) ∈ ℝ*)
33 elioo2 12045 . . . 4 (((1st ‘(𝐹‘(𝐺𝑋))) ∈ ℝ* ∧ (2nd ‘(𝐹‘(𝐺𝑋))) ∈ ℝ*) → (𝑃 ∈ ((1st ‘(𝐹‘(𝐺𝑋)))(,)(2nd ‘(𝐹‘(𝐺𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑋))) < 𝑃𝑃 < (2nd ‘(𝐹‘(𝐺𝑋))))))
3431, 32, 33syl2an 492 . . 3 (((1st ‘(𝐹‘(𝐺𝑋))) ∈ ℝ ∧ (2nd ‘(𝐹‘(𝐺𝑋))) ∈ ℝ) → (𝑃 ∈ ((1st ‘(𝐹‘(𝐺𝑋)))(,)(2nd ‘(𝐹‘(𝐺𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑋))) < 𝑃𝑃 < (2nd ‘(𝐹‘(𝐺𝑋))))))
3528, 30, 34syl2anc 690 . 2 ((𝜑𝑋𝑈) → (𝑃 ∈ ((1st ‘(𝐹‘(𝐺𝑋)))(,)(2nd ‘(𝐹‘(𝐺𝑋)))) ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑋))) < 𝑃𝑃 < (2nd ‘(𝐹‘(𝐺𝑋))))))
3626, 35bitrd 266 1 ((𝜑𝑋𝑈) → (𝑃𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑋))) < 𝑃𝑃 < (2nd ‘(𝐹‘(𝐺𝑋))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  cin 3538  wss 3539  𝒫 cpw 4107  cop 4130   cuni 4366   class class class wbr 4577   × cxp 5025  ran crn 5028  ccom 5031  wf 5785  cfv 5789  (class class class)co 6526  1st c1st 7034  2nd c2nd 7035  Fincfn 7818  cr 9791  1c1 9793   + caddc 9795  *cxr 9929   < clt 9930  cle 9931  cmin 10117  cn 10869  (,)cioo 12004  [,]cicc 12007  seqcseq 12620  abscabs 13770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-pre-lttri 9866  ax-pre-lttrn 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-po 4948  df-so 4949  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-1st 7036  df-2nd 7037  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-ioo 12008
This theorem is referenced by:  ovolicc2lem2  23037  ovolicc2lem3  23038  ovolicc2lem4  23039
  Copyright terms: Public domain W3C validator