Metamath Proof Explorer


Theorem fourierdlem3

Description: Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis fourierdlem3.1 P = m p π π 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1
Assertion fourierdlem3 M Q P M Q π π 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1

Proof

Step Hyp Ref Expression
1 fourierdlem3.1 P = m p π π 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1
2 oveq2 m = M 0 m = 0 M
3 2 oveq2d m = M π π 0 m = π π 0 M
4 fveqeq2 m = M p m = π p M = π
5 4 anbi2d m = M p 0 = π p m = π p 0 = π p M = π
6 oveq2 m = M 0 ..^ m = 0 ..^ M
7 6 raleqdv m = M i 0 ..^ m p i < p i + 1 i 0 ..^ M p i < p i + 1
8 5 7 anbi12d m = M p 0 = π p m = π i 0 ..^ m p i < p i + 1 p 0 = π p M = π i 0 ..^ M p i < p i + 1
9 3 8 rabeqbidv m = M p π π 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1 = p π π 0 M | p 0 = π p M = π i 0 ..^ M p i < p i + 1
10 ovex π π 0 M V
11 10 rabex p π π 0 M | p 0 = π p M = π i 0 ..^ M p i < p i + 1 V
12 9 1 11 fvmpt M P M = p π π 0 M | p 0 = π p M = π i 0 ..^ M p i < p i + 1
13 12 eleq2d M Q P M Q p π π 0 M | p 0 = π p M = π i 0 ..^ M p i < p i + 1
14 fveq1 p = Q p 0 = Q 0
15 14 eqeq1d p = Q p 0 = π Q 0 = π
16 fveq1 p = Q p M = Q M
17 16 eqeq1d p = Q p M = π Q M = π
18 15 17 anbi12d p = Q p 0 = π p M = π Q 0 = π Q M = π
19 fveq1 p = Q p i = Q i
20 fveq1 p = Q p i + 1 = Q i + 1
21 19 20 breq12d p = Q p i < p i + 1 Q i < Q i + 1
22 21 ralbidv p = Q i 0 ..^ M p i < p i + 1 i 0 ..^ M Q i < Q i + 1
23 18 22 anbi12d p = Q p 0 = π p M = π i 0 ..^ M p i < p i + 1 Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
24 23 elrab Q p π π 0 M | p 0 = π p M = π i 0 ..^ M p i < p i + 1 Q π π 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
25 13 24 bitrdi M Q P M Q π π 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1