fourierdlem14 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem14 45432

Description: Given the partition 𝑉, 𝑄 is the partition shifted to the left by 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
fourierdlem14	⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))

Distinct variable groups: 𝐴,𝑚,𝑝 𝐵,𝑚,𝑝 𝑖,𝑀,𝑚,𝑝 𝑄,𝑖,𝑝 𝑖,𝑉,𝑝 𝑖,𝑋,𝑚,𝑝 𝜑,𝑖 Allowed substitution hints: 𝜑(𝑚,𝑝) 𝐴(𝑖) 𝐵(𝑖) 𝑃(𝑖,𝑚,𝑝) 𝑄(𝑚) 𝑂(𝑖,𝑚,𝑝) 𝑉(𝑚)

Proof of Theorem fourierdlem14 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem14.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
2		fourierdlem14.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3		fourierdlem14.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝‘𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 45420	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
6	1, 5	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
7	6	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ (ℝ ↑_m (0...𝑀)))
8		elmapi 8859	. . . . . . . 8 ⊢ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
9	7, 8	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ)
10	9	ffvelcdmda 7088	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ)
11		fourierdlem14.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℝ)
12	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
13	10, 12	resubcld 11664	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
14		fourierdlem14.q	. . . . 5 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
15	13, 14	fmptd 7118	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
16		reex 11221	. . . . . 6 ⊢ ℝ ∈ V
17	16	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ∈ V)
18		ovex 7447	. . . . . 6 ⊢ (0...𝑀) ∈ V
19	18	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ V)
20	17, 19	elmapd 8850	. . . 4 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ))
21	15, 20	mpbird 257	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
22	14	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)))
23		fveq2 6891	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑉‘𝑖) = (𝑉‘0))
24	23	oveq1d 7429	. . . . . . 7 ⊢ (𝑖 = 0 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
25	24	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
26		0zd 12592	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
27	2	nnzd 12607	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℤ)
28		0le0 12335	. . . . . . . 8 ⊢ 0 ≤ 0
29	28	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 0)
30		0red 11239	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℝ)
31	2	nnred 12249	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
32	2	nngt0d 12283	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
33	30, 31, 32	ltled 11384	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑀)
34	26, 27, 26, 29, 33	elfzd 13516	. . . . . 6 ⊢ (𝜑 → 0 ∈ (0...𝑀))
35	9, 34	ffvelcdmd 7089	. . . . . . 7 ⊢ (𝜑 → (𝑉‘0) ∈ ℝ)
36	35, 11	resubcld 11664	. . . . . 6 ⊢ (𝜑 → ((𝑉‘0) − 𝑋) ∈ ℝ)
37	22, 25, 34, 36	fvmptd 7006	. . . . 5 ⊢ (𝜑 → (𝑄‘0) = ((𝑉‘0) − 𝑋))
38	6	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))
39	38	simpld 494	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘0) = (𝐴 + 𝑋) ∧ (𝑉‘𝑀) = (𝐵 + 𝑋)))
40	39	simpld 494	. . . . . 6 ⊢ (𝜑 → (𝑉‘0) = (𝐴 + 𝑋))
41	40	oveq1d 7429	. . . . 5 ⊢ (𝜑 → ((𝑉‘0) − 𝑋) = ((𝐴 + 𝑋) − 𝑋))
42		fourierdlem14.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
43	42	recnd 11264	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℂ)
44	11	recnd 11264	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℂ)
45	43, 44	pncand 11594	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝑋) − 𝑋) = 𝐴)
46	37, 41, 45	3eqtrd 2771	. . . 4 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
47		fveq2 6891	. . . . . . . 8 ⊢ (𝑖 = 𝑀 → (𝑉‘𝑖) = (𝑉‘𝑀))
48	47	oveq1d 7429	. . . . . . 7 ⊢ (𝑖 = 𝑀 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑀) − 𝑋))
49	48	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑀) − 𝑋))
50	31	leidd 11802	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
51	26, 27, 27, 33, 50	elfzd 13516	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
52	9, 51	ffvelcdmd 7089	. . . . . . 7 ⊢ (𝜑 → (𝑉‘𝑀) ∈ ℝ)
53	52, 11	resubcld 11664	. . . . . 6 ⊢ (𝜑 → ((𝑉‘𝑀) − 𝑋) ∈ ℝ)
54	22, 49, 51, 53	fvmptd 7006	. . . . 5 ⊢ (𝜑 → (𝑄‘𝑀) = ((𝑉‘𝑀) − 𝑋))
55	39	simprd 495	. . . . . 6 ⊢ (𝜑 → (𝑉‘𝑀) = (𝐵 + 𝑋))
56	55	oveq1d 7429	. . . . 5 ⊢ (𝜑 → ((𝑉‘𝑀) − 𝑋) = ((𝐵 + 𝑋) − 𝑋))
57		fourierdlem14.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
58	57	recnd 11264	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
59	58, 44	pncand 11594	. . . . 5 ⊢ (𝜑 → ((𝐵 + 𝑋) − 𝑋) = 𝐵)
60	54, 56, 59	3eqtrd 2771	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
61	46, 60	jca 511	. . 3 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
62		elfzofz 13672	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
63	62, 10	sylan2 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
64	9	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
65		fzofzp1 13753	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
66	65	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
67	64, 66	ffvelcdmd 7089	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
68	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
69	38	simprd 495	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
70	69	r19.21bi 3243	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
71	63, 67, 68, 70	ltsub1dd 11848	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
72	62	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
73	62, 13	sylan2 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
74	14	fvmpt2 7010	. . . . . 6 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
75	72, 73, 74	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
76		fveq2 6891	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
77	76	oveq1d 7429	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
78	77	cbvmptv 5255	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
79	14, 78	eqtri 2755	. . . . . . 7 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
80	79	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
81		fveq2 6891	. . . . . . . 8 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
82	81	oveq1d 7429	. . . . . . 7 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
83	82	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
84	67, 68	resubcld 11664	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
85	80, 83, 66, 84	fvmptd 7006	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
86	71, 75, 85	3brtr4d 5174	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
87	86	ralrimiva 3141	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
88	21, 61, 87	jca32 515	. 2 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
89		fourierdlem14.o	. . . 4 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
90	89	fourierdlem2 45420	. . 3 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑂‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
91	2, 90	syl 17	. 2 ⊢ (𝜑 → (𝑄 ∈ (𝑂‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
92	88, 91	mpbird 257	1 ⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1534 ∈ wcel 2099 ∀wral 3056 {crab 3427 Vcvv 3469 class class class wbr 5142 ↦ cmpt 5225 ⟶wf 6538 ‘cfv 6542 (class class class)co 7414 ↑_m cmap 8836 ℝcr 11129 0cc0 11130 1c1 11131 + caddc 11133 < clt 11270 ≤ cle 11271 − cmin 11466 ℕcn 12234 ...cfz 13508 ..^cfzo 13651

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-er 8718 df-map 8838 df-en 8956 df-dom 8957 df-sdom 8958 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-nn 12235 df-n0 12495 df-z 12581 df-uz 12845 df-fz 13509 df-fzo 13652

This theorem is referenced by: fourierdlem74 45491 fourierdlem75 45492 fourierdlem84 45501 fourierdlem85 45502 fourierdlem88 45505 fourierdlem103 45520 fourierdlem104 45521

W3C validator