Metamath Proof Explorer

Theorem fourierdlem14

Description: Given the partition V , Q is the partition shifted to the left by X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem14.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem14.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem14.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem14.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem14.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem14.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem14.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem14.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
Assertion fourierdlem14 ( 𝜑 → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem14.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem14.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem14.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4 fourierdlem14.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
5 fourierdlem14.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
6 fourierdlem14.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 fourierdlem14.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
8 fourierdlem14.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
9 4 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
10 6 9 syl ⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
11 7 10 mpbid ⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
12 11 simpld ⊢ ( 𝜑 → 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
13 elmapi ⊢ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
14 12 13 syl ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
15 14 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ℝ )
17 15 16 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
18 17 8 fmptd ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
19 reex ⊢ ℝ ∈ V
20 19 a1i ⊢ ( 𝜑 → ℝ ∈ V )
21 ovex ⊢ ( 0 ... 𝑀 ) ∈ V
22 21 a1i ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ V )
23 20 22 elmapd ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ↔ 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ) )
24 18 23 mpbird ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
25 8 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) )
26 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 0 ) )
27 26 oveq1d ⊢ ( 𝑖 = 0 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 0 ) − 𝑋 ) )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 0 ) − 𝑋 ) )
29 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
30 6 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
31 29 30 29 3jca ⊢ ( 𝜑 → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ ) )
32 0le0 ⊢ 0 ≤ 0
33 32 a1i ⊢ ( 𝜑 → 0 ≤ 0 )
34 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
35 6 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
36 6 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
37 34 35 36 ltled ⊢ ( 𝜑 → 0 ≤ 𝑀 )
38 31 33 37 jca32 ⊢ ( 𝜑 → ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 0 ≤ 0 ∧ 0 ≤ 𝑀 ) ) )
39 elfz2 ⊢ ( 0 ∈ ( 0 ... 𝑀 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 0 ≤ 0 ∧ 0 ≤ 𝑀 ) ) )
40 38 39 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
41 14 40 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ 0 ) ∈ ℝ )
42 41 3 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) − 𝑋 ) ∈ ℝ )
43 25 28 40 42 fvmptd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = ( ( 𝑉 ‘ 0 ) − 𝑋 ) )
44 11 simprd ⊢ ( 𝜑 → ( ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
45 44 simpld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) )
46 45 simpld ⊢ ( 𝜑 → ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) )
47 46 oveq1d ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) − 𝑋 ) = ( ( 𝐴 + 𝑋 ) − 𝑋 ) )
48 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
49 3 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
50 48 49 pncand ⊢ ( 𝜑 → ( ( 𝐴 + 𝑋 ) − 𝑋 ) = 𝐴 )
51 43 47 50 3eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
52 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑀 ) )
53 52 oveq1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 𝑀 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
55 29 30 30 3jca ⊢ ( 𝜑 → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
56 35 leidd ⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
57 55 37 56 jca32 ⊢ ( 𝜑 → ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀 ) ) )
58 elfz2 ⊢ ( 𝑀 ∈ ( 0 ... 𝑀 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀 ) ) )
59 57 58 sylibr ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
60 14 59 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑀 ) ∈ ℝ )
61 60 3 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) ∈ ℝ )
62 25 54 59 61 fvmptd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
63 45 simprd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) )
64 63 oveq1d ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) = ( ( 𝐵 + 𝑋 ) − 𝑋 ) )
65 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
66 65 49 pncand ⊢ ( 𝜑 → ( ( 𝐵 + 𝑋 ) − 𝑋 ) = 𝐵 )
67 62 64 66 3eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
68 51 67 jca ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
69 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
70 69 15 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
71 14 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
72 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
73 72 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
74 71 73 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
75 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
76 44 simprd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
77 76 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
78 70 74 75 77 ltsub1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) < ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
79 69 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
80 69 17 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
81 8 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
82 79 80 81 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
83 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑗 ) )
84 83 oveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
85 84 cbvmptv ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
86 8 85 eqtri ⊢ 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
87 86 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) )
88 fveq2 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
89 88 oveq1d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
90 89 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
91 74 75 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
92 87 90 73 91 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
93 78 82 92 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
94 93 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
95 24 68 94 jca32 ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
96 5 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
97 6 96 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
98 95 97 mpbird ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) )