Metamath Proof Explorer

Theorem fourierdlem13

Description: Value of V in terms of value of Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 fourierdlem13.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem13.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem13.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4 fourierdlem13.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
5 fourierdlem13.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6 fourierdlem13.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
7 fourierdlem13.i ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
8 fourierdlem13.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
9 8 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
11 10 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 = 𝐼 ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝐼 ) )
12 11 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 = 𝐼 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝐼 ) − 𝑋 ) )
13 4 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
14 5 13 syl ⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
15 6 14 mpbid ⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( 𝐴 + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( 𝐵 + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
16 15 simpld ⊢ ( 𝜑 → 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
17 elmapi ⊢ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
18 16 17 syl ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
19 18 7 ffvelcdmd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐼 ) ∈ ℝ )
20 19 3 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝐼 ) − 𝑋 ) ∈ ℝ )
21 9 12 7 20 fvmptd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) = ( ( 𝑉 ‘ 𝐼 ) − 𝑋 ) )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝑋 + ( 𝑄 ‘ 𝐼 ) ) = ( 𝑋 + ( ( 𝑉 ‘ 𝐼 ) − 𝑋 ) ) )
23 3 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
24 19 recnd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐼 ) ∈ ℂ )
25 23 24 pncan3d ⊢ ( 𝜑 → ( 𝑋 + ( ( 𝑉 ‘ 𝐼 ) − 𝑋 ) ) = ( 𝑉 ‘ 𝐼 ) )
26 22 25 eqtr2d ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐼 ) = ( 𝑋 + ( 𝑄 ‘ 𝐼 ) ) )
27 21 26 jca ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) = ( ( 𝑉 ‘ 𝐼 ) − 𝑋 ) ∧ ( 𝑉 ‘ 𝐼 ) = ( 𝑋 + ( 𝑄 ‘ 𝐼 ) ) ) )