fourierdlem15 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem15 43988

Description: The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem15.1	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem15.2	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem15.3	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))

**Assertion**
Ref	Expression
fourierdlem15	⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))

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

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

Step	Hyp	Ref	Expression
1		fourierdlem15.3	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
2		fourierdlem15.2	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3		fourierdlem15.1	. . . . . . . 8 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 43975	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 231	. . . . 5 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simpld 495	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
8		reex 11055	. . . . . 6 ⊢ ℝ ∈ V
9	8	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ∈ V)
10		ovex 7362	. . . . . 6 ⊢ (0...𝑀) ∈ V
11	10	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ V)
12	9, 11	elmapd 8692	. . . 4 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ))
13	7, 12	mpbid 231	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
14		ffn 6645	. . 3 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
15	13, 14	syl 17	. 2 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
16	6	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
17	16	simpld 495	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
18	17	simpld 495	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
19		nnnn0 12333	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
20		nn0uz 12713	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
21	19, 20	eleqtrdi 2847	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘0))
22	2, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
23		eluzfz1 13356	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
24	22, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
25	13, 24	ffvelcdmd 7012	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
26	18, 25	eqeltrrd 2838	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ)
27	26	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ∈ ℝ)
28	17	simprd 496	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
29		eluzfz2 13357	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
30	22, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
31	13, 30	ffvelcdmd 7012	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
32	28, 31	eqeltrrd 2838	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
33	32	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐵 ∈ ℝ)
34	13	ffvelcdmda 7011	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
35	18	eqcomd 2742	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
36	35	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 = (𝑄‘0))
37		elfzuz 13345	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ (ℤ_≥‘0))
38	37	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (ℤ_≥‘0))
39	13	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
40		0zd 12424	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ∈ ℤ)
41		elfzel2 13347	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
42	41	adantr 481	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℤ)
43		elfzelz 13349	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℤ)
44	43	adantl 482	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℤ)
45		elfzle1 13352	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 0 ≤ 𝑗)
46	45	adantl 482	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ≤ 𝑗)
47	43	zred 12519	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℝ)
48	47	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℝ)
49		elfzelz 13349	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
50	49	zred 12519	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
51	50	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ∈ ℝ)
52	41	zred 12519	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
53	52	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℝ)
54		elfzle2 13353	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ≤ 𝑖)
55	54	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑖)
56		elfzle2 13353	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
57	56	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ≤ 𝑀)
58	48, 51, 53, 55, 57	letrd 11225	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑀)
59	40, 42, 44, 46, 58	elfzd 13340	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
60	59	adantll 711	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
61	39, 60	ffvelcdmd 7012	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → (𝑄‘𝑗) ∈ ℝ)
62		simpll 764	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝜑)
63		elfzle1 13352	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 0 ≤ 𝑗)
64	63	adantl 482	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ≤ 𝑗)
65		elfzelz 13349	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℤ)
66	65	zred 12519	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℝ)
67	66	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℝ)
68	50	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ∈ ℝ)
69	52	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℝ)
70		peano2rem 11381	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
71	68, 70	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
72		elfzle2 13353	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
73	72	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
74	68	ltm1d 12000	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
75	67, 71, 68, 73, 74	lelttrd 11226	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑖)
76	56	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ≤ 𝑀)
77	67, 68, 69, 75, 76	ltletrd 11228	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑀)
78	65	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℤ)
79		0zd 12424	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ∈ ℤ)
80	41	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℤ)
81		elfzo 13482	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
82	78, 79, 80, 81	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
83	64, 77, 82	mpbir2and 710	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
84	83	adantll 711	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
85	13	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
86		elfzofz 13496	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀))
87	86	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
88	85, 87	ffvelcdmd 7012	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ)
89		fzofzp1 13577	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
90	89	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
91	85, 90	ffvelcdmd 7012	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
92		eleq1w 2819	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
93	92	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
94		fveq2 6819	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
95		oveq1 7336	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
96	95	fveq2d 6823	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
97	94, 96	breq12d 5102	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
98	93, 97	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
99	16	simprd 496	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
100	99	r19.21bi 3230	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
101	98, 100	chvarvv 2001	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
102	88, 91, 101	ltled 11216	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
103	62, 84, 102	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
104	38, 61, 103	monoord 13846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
105	36, 104	eqbrtrd 5111	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ≤ (𝑄‘𝑖))
106		elfzuz3 13346	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ (ℤ_≥‘𝑖))
107	106	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (ℤ_≥‘𝑖))
108	13	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
109		fz0fzelfz0 13455	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
110	109	adantll 711	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
111	108, 110	ffvelcdmd 7012	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
112	13	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
113		0zd 12424	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℤ)
114	41	ad2antlr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℤ)
115		elfzelz 13349	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℤ)
116	115	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℤ)
117		0red 11071	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℝ)
118	50	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ∈ ℝ)
119	115	zred 12519	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℝ)
120	119	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
121		elfzle1 13352	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
122	121	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑖)
123		elfzle1 13352	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑖 ≤ 𝑗)
124	123	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ≤ 𝑗)
125	117, 118, 120, 122, 124	letrd 11225	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
126	125	adantll 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
127	119	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
128	2	nnred 12081	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
129	128	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℝ)
130		1red 11069	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
131	129, 130	resubcld 11496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
132		elfzle2 13353	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ≤ (𝑀 − 1))
133	132	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ (𝑀 − 1))
134	129	ltm1d 12000	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
135	127, 131, 129, 133, 134	lelttrd 11226	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
136	127, 129, 135	ltled 11216	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
137	136	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
138	113, 114, 116, 126, 137	elfzd 13340	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0...𝑀))
139	112, 138	ffvelcdmd 7012	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ∈ ℝ)
140	116	peano2zd 12522	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ ℤ)
141	119	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
142		1red 11069	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
143		0le1 11591	. . . . . . . . . . . 12 ⊢ 0 ≤ 1
144	143	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 1)
145	141, 142, 126, 144	addge0d 11644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ (𝑗 + 1))
146	127, 131, 130, 133	leadd1dd 11682	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ ((𝑀 − 1) + 1))
147	2	nncnd 12082	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℂ)
148	147	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℂ)
149		1cnd 11063	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℂ)
150	148, 149	npcand 11429	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
151	146, 150	breqtrd 5115	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
152	151	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
153	113, 114, 140, 145, 152	elfzd 13340	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ (0...𝑀))
154	112, 153	ffvelcdmd 7012	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
155		simpll 764	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝜑)
156	135	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
157	116, 113, 114, 81	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
158	126, 156, 157	mpbir2and 710	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0..^𝑀))
159	155, 158, 101	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
160	139, 154, 159	ltled 11216	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
161	107, 111, 160	monoord 13846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
162	28	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑀) = 𝐵)
163	161, 162	breqtrd 5115	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ 𝐵)
164	27, 33, 34, 105, 163	eliccd 43367	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (𝐴[,]𝐵))
165	164	ralrimiva 3139	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵))
166		fnfvrnss 7044	. . 3 ⊢ ((𝑄 Fn (0...𝑀) ∧ ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵)) → ran 𝑄 ⊆ (𝐴[,]𝐵))
167	15, 165, 166	syl2anc 584	. 2 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
168		df-f 6477	. 2 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) ↔ (𝑄 Fn (0...𝑀) ∧ ran 𝑄 ⊆ (𝐴[,]𝐵)))
169	15, 167, 168	sylanbrc 583	1 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ∀wral 3061 {crab 3403 Vcvv 3441 ⊆ wss 3897 class class class wbr 5089 ↦ cmpt 5172 ran crn 5615 Fn wfn 6468 ⟶wf 6469 ‘cfv 6473 (class class class)co 7329 ↑_m cmap 8678 ℂcc 10962 ℝcr 10963 0cc0 10964 1c1 10965 + caddc 10967 < clt 11102 ≤ cle 11103 − cmin 11298 ℕcn 12066 ℕ₀cn0 12326 ℤcz 12412 ℤ_≥cuz 12675 [,]cicc 13175 ...cfz 13332 ..^cfzo 13475

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5240 ax-nul 5247 ax-pow 5305 ax-pr 5369 ax-un 7642 ax-cnex 11020 ax-resscn 11021 ax-1cn 11022 ax-icn 11023 ax-addcl 11024 ax-addrcl 11025 ax-mulcl 11026 ax-mulrcl 11027 ax-mulcom 11028 ax-addass 11029 ax-mulass 11030 ax-distr 11031 ax-i2m1 11032 ax-1ne0 11033 ax-1rid 11034 ax-rnegex 11035 ax-rrecex 11036 ax-cnre 11037 ax-pre-lttri 11038 ax-pre-lttrn 11039 ax-pre-ltadd 11040 ax-pre-mulgt0 11041

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3727 df-csb 3843 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3916 df-nul 4269 df-if 4473 df-pw 4548 df-sn 4573 df-pr 4575 df-op 4579 df-uni 4852 df-iun 4940 df-br 5090 df-opab 5152 df-mpt 5173 df-tr 5207 df-id 5512 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5569 df-we 5571 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6232 df-ord 6299 df-on 6300 df-lim 6301 df-suc 6302 df-iota 6425 df-fun 6475 df-fn 6476 df-f 6477 df-f1 6478 df-fo 6479 df-f1o 6480 df-fv 6481 df-riota 7286 df-ov 7332 df-oprab 7333 df-mpo 7334 df-om 7773 df-1st 7891 df-2nd 7892 df-frecs 8159 df-wrecs 8190 df-recs 8264 df-rdg 8303 df-er 8561 df-map 8680 df-en 8797 df-dom 8798 df-sdom 8799 df-pnf 11104 df-mnf 11105 df-xr 11106 df-ltxr 11107 df-le 11108 df-sub 11300 df-neg 11301 df-nn 12067 df-n0 12327 df-z 12413 df-uz 12676 df-icc 13179 df-fz 13333 df-fzo 13476

This theorem is referenced by: fourierdlem38 44011 fourierdlem50 44022 fourierdlem54 44026 fourierdlem63 44035 fourierdlem65 44037 fourierdlem69 44041 fourierdlem70 44042 fourierdlem74 44046 fourierdlem75 44047 fourierdlem76 44048 fourierdlem79 44051 fourierdlem81 44053 fourierdlem84 44056 fourierdlem85 44057 fourierdlem88 44060 fourierdlem89 44061 fourierdlem90 44062 fourierdlem91 44063 fourierdlem92 44064 fourierdlem93 44065 fourierdlem100 44072 fourierdlem101 44073 fourierdlem103 44075 fourierdlem104 44076 fourierdlem107 44079 fourierdlem111 44083 fourierdlem112 44084 fourierdlem113 44085

W3C validator