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 46721

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 46708	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 235	. . . . 5 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simpld 499	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
8		reex 11187	. . . . . 6 ⊢ ℝ ∈ V
9	8	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ∈ V)
10		ovex 7441	. . . . . 6 ⊢ (0...𝑀) ∈ V
11	10	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ V)
12	9, 11	elmapd 8833	. . . 4 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ))
13	7, 12	mpbid 235	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
14		ffn 6703	. . 3 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
15	13, 14	syl 18	. 2 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
16	6	simprd 500	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
17	16	simpld 499	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
18	17	simpld 499	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
19		nnnn0 12507	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
20		nn0uz 12896	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
21	19, 20	eleqtrdi 2879	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘0))
22	2, 21	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
23		eluzfz1 13555	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
24	22, 23	syl 18	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
25	13, 24	ffvelcdmd 7078	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
26	18, 25	eqeltrrd 2870	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ)
27	26	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ∈ ℝ)
28	17	simprd 500	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
29		eluzfz2 13556	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
30	22, 29	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
31	13, 30	ffvelcdmd 7078	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
32	28, 31	eqeltrrd 2870	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
33	32	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐵 ∈ ℝ)
34	13	ffvelcdmda 7077	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
35	18	eqcomd 2775	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
36	35	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 = (𝑄‘0))
37		elfzuz 13544	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ (ℤ_≥‘0))
38	37	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (ℤ_≥‘0))
39	13	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
40		0zd 12599	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ∈ ℤ)
41		elfzel2 13546	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
42	41	adantr 485	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℤ)
43		elfzelz 13548	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℤ)
44	43	adantl 486	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℤ)
45		elfzle1 13551	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 0 ≤ 𝑗)
46	45	adantl 486	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ≤ 𝑗)
47	43	zred 12696	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℝ)
48	47	adantl 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℝ)
49		elfzelz 13548	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
50	49	zred 12696	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
51	50	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ∈ ℝ)
52	41	zred 12696	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
53	52	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℝ)
54		elfzle2 13552	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ≤ 𝑖)
55	54	adantl 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑖)
56		elfzle2 13552	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
57	56	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ≤ 𝑀)
58	48, 51, 53, 55, 57	letrd 11363	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑀)
59	40, 42, 44, 46, 58	elfzd 13539	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
60	59	adantll 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
61	39, 60	ffvelcdmd 7078	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → (𝑄‘𝑗) ∈ ℝ)
62		simpll 778	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝜑)
63		elfzle1 13551	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 0 ≤ 𝑗)
64	63	adantl 486	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ≤ 𝑗)
65		elfzelz 13548	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℤ)
66	65	zred 12696	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℝ)
67	66	adantl 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℝ)
68	50	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ∈ ℝ)
69	52	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℝ)
70		peano2rem 11521	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
71	68, 70	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
72		elfzle2 13552	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
73	72	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
74	68	ltm1d 12143	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
75	67, 71, 68, 73, 74	lelttrd 11364	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑖)
76	56	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ≤ 𝑀)
77	67, 68, 69, 75, 76	ltletrd 11366	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑀)
78	65	adantl 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℤ)
79		0zd 12599	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ∈ ℤ)
80	41	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℤ)
81		elfzo 13685	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
82	78, 79, 80, 81	syl3anc 1396	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
83	64, 77, 82	mpbir2and 725	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
84	83	adantll 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
85	13	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
86		elfzofz 13700	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀))
87	86	adantl 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
88	85, 87	ffvelcdmd 7078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ)
89		fzofzp1 13789	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
90	89	adantl 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
91	85, 90	ffvelcdmd 7078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
92		eleq1w 2852	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
93	92	anbi2d 641	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
94		fveq2 6879	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
95		oveq1 7415	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
96	95	fveq2d 6883	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
97	94, 96	breq12d 5123	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
98	93, 97	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
99	16	simprd 500	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
100	99	r19.21bi 3263	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
101	98, 100	chvarvv 2016	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
102	88, 91, 101	ltled 11354	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
103	62, 84, 102	syl2anc 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
104	38, 61, 103	monoord 14064	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
105	36, 104	eqbrtrd 5134	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ≤ (𝑄‘𝑖))
106		elfzuz3 13545	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ (ℤ_≥‘𝑖))
107	106	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (ℤ_≥‘𝑖))
108	13	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
109		fz0fzelfz0 13658	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
110	109	adantll 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
111	108, 110	ffvelcdmd 7078	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
112	13	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
113		0zd 12599	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℤ)
114	41	ad2antlr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℤ)
115		elfzelz 13548	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℤ)
116	115	adantl 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℤ)
117		0red 11207	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℝ)
118	50	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ∈ ℝ)
119	115	zred 12696	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℝ)
120	119	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
121		elfzle1 13551	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
122	121	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑖)
123		elfzle1 13551	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑖 ≤ 𝑗)
124	123	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ≤ 𝑗)
125	117, 118, 120, 122, 124	letrd 11363	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
126	125	adantll 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
127	119	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
128	2	nnred 12244	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
129	128	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℝ)
130		1red 11205	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
131	129, 130	resubcld 11638	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
132		elfzle2 13552	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ≤ (𝑀 − 1))
133	132	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ (𝑀 − 1))
134	129	ltm1d 12143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
135	127, 131, 129, 133, 134	lelttrd 11364	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
136	127, 129, 135	ltled 11354	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
137	136	adantlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
138	113, 114, 116, 126, 137	elfzd 13539	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0...𝑀))
139	112, 138	ffvelcdmd 7078	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ∈ ℝ)
140	116	peano2zd 12699	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ ℤ)
141	119	adantl 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
142		1red 11205	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
143		0le1 11733	. . . . . . . . . . . 12 ⊢ 0 ≤ 1
144	143	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 1)
145	141, 142, 126, 144	addge0d 11786	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ (𝑗 + 1))
146	127, 131, 130, 133	leadd1dd 11824	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ ((𝑀 − 1) + 1))
147	2	nncnd 12245	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℂ)
148	147	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℂ)
149		1cnd 11198	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℂ)
150	148, 149	npcand 11569	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
151	146, 150	breqtrd 5138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
152	151	adantlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
153	113, 114, 140, 145, 152	elfzd 13539	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ (0...𝑀))
154	112, 153	ffvelcdmd 7078	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
155		simpll 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝜑)
156	135	adantlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
157	116, 113, 114, 81	syl3anc 1396	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
158	126, 156, 157	mpbir2and 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0..^𝑀))
159	155, 158, 101	syl2anc 595	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
160	139, 154, 159	ltled 11354	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
161	107, 111, 160	monoord 14064	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
162	28	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑀) = 𝐵)
163	161, 162	breqtrd 5138	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ 𝐵)
164	27, 33, 34, 105, 163	eliccd 46105	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (𝐴[,]𝐵))
165	164	ralrimiva 3163	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵))
166		fnfvrnss 7114	. . 3 ⊢ ((𝑄 Fn (0...𝑀) ∧ ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵)) → ran 𝑄 ⊆ (𝐴[,]𝐵))
167	15, 165, 166	syl2anc 595	. 2 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
168		df-f 6537	. 2 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) ↔ (𝑄 Fn (0...𝑀) ∧ ran 𝑄 ⊆ (𝐴[,]𝐵)))
169	15, 167, 168	sylanbrc 594	1 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ∀wral 3085 {crab 3423 Vcvv 3463 ⊆ wss 3913 class class class wbr 5110 ↦ cmpt 5193 ran crn 5660 Fn wfn 6528 ⟶wf 6529 ‘cfv 6533 (class class class)co 7408 ↑_m cmap 8820 ℂcc 11094 ℝcr 11095 0cc0 11096 1c1 11097 + caddc 11099 < clt 11239 ≤ cle 11240 − cmin 11437 ℕcn 12229 ℕ₀cn0 12500 ℤcz 12587 ℤ_≥cuz 12858 [,]cicc 13371 ...cfz 13531 ..^cfzo 13678

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-cnex 11152 ax-resscn 11153 ax-1cn 11154 ax-icn 11155 ax-addcl 11156 ax-addrcl 11157 ax-mulcl 11158 ax-mulrcl 11159 ax-mulcom 11160 ax-addass 11161 ax-mulass 11162 ax-distr 11163 ax-i2m1 11164 ax-1ne0 11165 ax-1rid 11166 ax-rnegex 11167 ax-rrecex 11168 ax-cnre 11169 ax-pre-lttri 11170 ax-pre-lttrn 11171 ax-pre-ltadd 11172 ax-pre-mulgt0 11173

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244 df-le 11245 df-sub 11439 df-neg 11440 df-nn 12230 df-n0 12501 df-z 12588 df-uz 12859 df-icc 13375 df-fz 13532 df-fzo 13679

This theorem is referenced by: fourierdlem38 46744 fourierdlem50 46755 fourierdlem54 46759 fourierdlem63 46768 fourierdlem65 46770 fourierdlem69 46774 fourierdlem70 46775 fourierdlem74 46779 fourierdlem75 46780 fourierdlem76 46781 fourierdlem79 46784 fourierdlem81 46786 fourierdlem84 46789 fourierdlem85 46790 fourierdlem88 46793 fourierdlem89 46794 fourierdlem90 46795 fourierdlem91 46796 fourierdlem92 46797 fourierdlem93 46798 fourierdlem100 46805 fourierdlem101 46806 fourierdlem103 46808 fourierdlem104 46809 fourierdlem107 46812 fourierdlem111 46816 fourierdlem112 46817 fourierdlem113 46818

W3C validator