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

Theorem fourierdlem2 42271
Description: Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
fourierdlem2.1 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
Assertion
Ref Expression
fourierdlem2 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
Distinct variable groups:   𝐴,𝑚,𝑝   𝐵,𝑚,𝑝   𝑖,𝑀,𝑚,𝑝   𝑄,𝑖,𝑝
Allowed substitution hints:   𝐴(𝑖)   𝐵(𝑖)   𝑃(𝑖,𝑚,𝑝)   𝑄(𝑚)

Proof of Theorem fourierdlem2
StepHypRef Expression
1 oveq2 7153 . . . . . 6 (𝑚 = 𝑀 → (0...𝑚) = (0...𝑀))
21oveq2d 7161 . . . . 5 (𝑚 = 𝑀 → (ℝ ↑m (0...𝑚)) = (ℝ ↑m (0...𝑀)))
3 fveqeq2 6672 . . . . . . 7 (𝑚 = 𝑀 → ((𝑝𝑚) = 𝐵 ↔ (𝑝𝑀) = 𝐵))
43anbi2d 628 . . . . . 6 (𝑚 = 𝑀 → (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵)))
5 oveq2 7153 . . . . . . 7 (𝑚 = 𝑀 → (0..^𝑚) = (0..^𝑀))
65raleqdv 3413 . . . . . 6 (𝑚 = 𝑀 → (∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1))))
74, 6anbi12d 630 . . . . 5 (𝑚 = 𝑀 → ((((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))))
82, 7rabeqbidv 3483 . . . 4 (𝑚 = 𝑀 → {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
9 fourierdlem2.1 . . . 4 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
10 ovex 7178 . . . . 5 (ℝ ↑m (0...𝑀)) ∈ V
1110rabex 5226 . . . 4 {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} ∈ V
128, 9, 11fvmpt 6761 . . 3 (𝑀 ∈ ℕ → (𝑃𝑀) = {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
1312eleq2d 2895 . 2 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ 𝑄 ∈ {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}))
14 fveq1 6662 . . . . . 6 (𝑝 = 𝑄 → (𝑝‘0) = (𝑄‘0))
1514eqeq1d 2820 . . . . 5 (𝑝 = 𝑄 → ((𝑝‘0) = 𝐴 ↔ (𝑄‘0) = 𝐴))
16 fveq1 6662 . . . . . 6 (𝑝 = 𝑄 → (𝑝𝑀) = (𝑄𝑀))
1716eqeq1d 2820 . . . . 5 (𝑝 = 𝑄 → ((𝑝𝑀) = 𝐵 ↔ (𝑄𝑀) = 𝐵))
1815, 17anbi12d 630 . . . 4 (𝑝 = 𝑄 → (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ↔ ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵)))
19 fveq1 6662 . . . . . 6 (𝑝 = 𝑄 → (𝑝𝑖) = (𝑄𝑖))
20 fveq1 6662 . . . . . 6 (𝑝 = 𝑄 → (𝑝‘(𝑖 + 1)) = (𝑄‘(𝑖 + 1)))
2119, 20breq12d 5070 . . . . 5 (𝑝 = 𝑄 → ((𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑄𝑖) < (𝑄‘(𝑖 + 1))))
2221ralbidv 3194 . . . 4 (𝑝 = 𝑄 → (∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
2318, 22anbi12d 630 . . 3 (𝑝 = 𝑄 → ((((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
2423elrab 3677 . 2 (𝑄 ∈ {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
2513, 24syl6bb 288 1 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wral 3135  {crab 3139   class class class wbr 5057  cmpt 5137  cfv 6348  (class class class)co 7145  m cmap 8395  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   < clt 10663  cn 11626  ...cfz 12880  ..^cfzo 13021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7148
This theorem is referenced by:  fourierdlem11  42280  fourierdlem12  42281  fourierdlem13  42282  fourierdlem14  42283  fourierdlem15  42284  fourierdlem34  42303  fourierdlem37  42306  fourierdlem41  42310  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem54  42322  fourierdlem63  42331  fourierdlem64  42332  fourierdlem65  42333  fourierdlem69  42337  fourierdlem70  42338  fourierdlem72  42340  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem79  42347  fourierdlem81  42349  fourierdlem85  42353  fourierdlem88  42356  fourierdlem89  42357  fourierdlem90  42358  fourierdlem91  42359  fourierdlem92  42360  fourierdlem93  42361  fourierdlem94  42362  fourierdlem97  42365  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem111  42379  fourierdlem113  42381  fourierdlem114  42382
  Copyright terms: Public domain W3C validator