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 0le0 ⊢ 0 ≤ 0
32 31 a1i ⊢ ( 𝜑 → 0 ≤ 0 )
33 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
34 6 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
35 6 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
36 33 34 35 ltled ⊢ ( 𝜑 → 0 ≤ 𝑀 )
37 29 30 29 32 36 elfzd ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
38 14 37 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ 0 ) ∈ ℝ )
39 38 3 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) − 𝑋 ) ∈ ℝ )
40 25 28 37 39 fvmptd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = ( ( 𝑉 ‘ 0 ) − 𝑋 ) )
41 11 simprd ⊢ ( 𝜑 → ( ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
42 41 simpld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) )
43 42 simpld ⊢ ( 𝜑 → ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) )
44 43 oveq1d ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) − 𝑋 ) = ( ( 𝐴 + 𝑋 ) − 𝑋 ) )
45 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
46 3 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
47 45 46 pncand ⊢ ( 𝜑 → ( ( 𝐴 + 𝑋 ) − 𝑋 ) = 𝐴 )
48 40 44 47 3eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
49 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑀 ) )
50 49 oveq1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 𝑀 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
52 34 leidd ⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
53 29 30 30 36 52 elfzd ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
54 14 53 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑀 ) ∈ ℝ )
55 54 3 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) ∈ ℝ )
56 25 51 53 55 fvmptd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
57 42 simprd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) )
58 57 oveq1d ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) = ( ( 𝐵 + 𝑋 ) − 𝑋 ) )
59 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
60 59 46 pncand ⊢ ( 𝜑 → ( ( 𝐵 + 𝑋 ) − 𝑋 ) = 𝐵 )
61 56 58 60 3eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
62 48 61 jca ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
63 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
64 63 15 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
65 14 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
66 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
68 65 67 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
69 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
70 41 simprd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
71 70 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
72 64 68 69 71 ltsub1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) < ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
73 63 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
74 63 17 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
75 8 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
76 73 74 75 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
77 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑗 ) )
78 77 oveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
79 78 cbvmptv ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
80 8 79 eqtri ⊢ 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
81 80 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) )
82 fveq2 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
83 82 oveq1d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
84 83 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
85 68 69 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
86 81 84 67 85 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
87 72 76 86 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
88 87 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
89 24 62 88 jca32 ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
90 5 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
91 6 90 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
92 89 91 mpbird ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) )