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 46477

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 46464	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simpld 494	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
8		reex 11129	. . . . . 6 ⊢ ℝ ∈ V
9	8	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ∈ V)
10		ovex 7401	. . . . . 6 ⊢ (0...𝑀) ∈ V
11	10	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ V)
12	9, 11	elmapd 8789	. . . 4 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ))
13	7, 12	mpbid 232	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
14		ffn 6670	. . 3 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
15	13, 14	syl 17	. 2 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
16	6	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
17	16	simpld 494	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
18	17	simpld 494	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
19		nnnn0 12420	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
20		nn0uz 12801	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
21	19, 20	eleqtrdi 2847	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘0))
22	2, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
23		eluzfz1 13459	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
24	22, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
25	13, 24	ffvelcdmd 7039	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
26	18, 25	eqeltrrd 2838	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ)
27	26	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ∈ ℝ)
28	17	simprd 495	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
29		eluzfz2 13460	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
30	22, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
31	13, 30	ffvelcdmd 7039	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
32	28, 31	eqeltrrd 2838	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
33	32	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐵 ∈ ℝ)
34	13	ffvelcdmda 7038	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
35	18	eqcomd 2743	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
36	35	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 = (𝑄‘0))
37		elfzuz 13448	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ (ℤ_≥‘0))
38	37	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (ℤ_≥‘0))
39	13	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
40		0zd 12512	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ∈ ℤ)
41		elfzel2 13450	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
42	41	adantr 480	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℤ)
43		elfzelz 13452	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℤ)
44	43	adantl 481	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℤ)
45		elfzle1 13455	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 0 ≤ 𝑗)
46	45	adantl 481	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ≤ 𝑗)
47	43	zred 12608	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℝ)
48	47	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℝ)
49		elfzelz 13452	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
50	49	zred 12608	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
51	50	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ∈ ℝ)
52	41	zred 12608	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
53	52	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℝ)
54		elfzle2 13456	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ≤ 𝑖)
55	54	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑖)
56		elfzle2 13456	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
57	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ≤ 𝑀)
58	48, 51, 53, 55, 57	letrd 11302	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑀)
59	40, 42, 44, 46, 58	elfzd 13443	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
60	59	adantll 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
61	39, 60	ffvelcdmd 7039	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → (𝑄‘𝑗) ∈ ℝ)
62		simpll 767	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝜑)
63		elfzle1 13455	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 0 ≤ 𝑗)
64	63	adantl 481	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ≤ 𝑗)
65		elfzelz 13452	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℤ)
66	65	zred 12608	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℝ)
67	66	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℝ)
68	50	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ∈ ℝ)
69	52	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℝ)
70		peano2rem 11460	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
71	68, 70	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
72		elfzle2 13456	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
73	72	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
74	68	ltm1d 12086	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
75	67, 71, 68, 73, 74	lelttrd 11303	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑖)
76	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ≤ 𝑀)
77	67, 68, 69, 75, 76	ltletrd 11305	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑀)
78	65	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℤ)
79		0zd 12512	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ∈ ℤ)
80	41	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℤ)
81		elfzo 13589	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
82	78, 79, 80, 81	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
83	64, 77, 82	mpbir2and 714	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
84	83	adantll 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
85	13	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
86		elfzofz 13603	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀))
87	86	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
88	85, 87	ffvelcdmd 7039	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ)
89		fzofzp1 13692	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
90	89	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
91	85, 90	ffvelcdmd 7039	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
92		eleq1w 2820	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
93	92	anbi2d 631	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
94		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
95		oveq1 7375	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
96	95	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
97	94, 96	breq12d 5113	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
98	93, 97	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
99	16	simprd 495	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
100	99	r19.21bi 3230	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
101	98, 100	chvarvv 1991	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
102	88, 91, 101	ltled 11293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
103	62, 84, 102	syl2anc 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
104	38, 61, 103	monoord 13967	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
105	36, 104	eqbrtrd 5122	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ≤ (𝑄‘𝑖))
106		elfzuz3 13449	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ (ℤ_≥‘𝑖))
107	106	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (ℤ_≥‘𝑖))
108	13	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
109		fz0fzelfz0 13562	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
110	109	adantll 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
111	108, 110	ffvelcdmd 7039	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
112	13	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
113		0zd 12512	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℤ)
114	41	ad2antlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℤ)
115		elfzelz 13452	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℤ)
116	115	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℤ)
117		0red 11147	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℝ)
118	50	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ∈ ℝ)
119	115	zred 12608	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℝ)
120	119	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
121		elfzle1 13455	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
122	121	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑖)
123		elfzle1 13455	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑖 ≤ 𝑗)
124	123	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ≤ 𝑗)
125	117, 118, 120, 122, 124	letrd 11302	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
126	125	adantll 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
127	119	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
128	2	nnred 12172	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
129	128	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℝ)
130		1red 11145	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
131	129, 130	resubcld 11577	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
132		elfzle2 13456	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ≤ (𝑀 − 1))
133	132	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ (𝑀 − 1))
134	129	ltm1d 12086	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
135	127, 131, 129, 133, 134	lelttrd 11303	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
136	127, 129, 135	ltled 11293	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
137	136	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
138	113, 114, 116, 126, 137	elfzd 13443	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0...𝑀))
139	112, 138	ffvelcdmd 7039	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ∈ ℝ)
140	116	peano2zd 12611	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ ℤ)
141	119	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
142		1red 11145	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
143		0le1 11672	. . . . . . . . . . . 12 ⊢ 0 ≤ 1
144	143	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 1)
145	141, 142, 126, 144	addge0d 11725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ (𝑗 + 1))
146	127, 131, 130, 133	leadd1dd 11763	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ ((𝑀 − 1) + 1))
147	2	nncnd 12173	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℂ)
148	147	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℂ)
149		1cnd 11139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℂ)
150	148, 149	npcand 11508	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
151	146, 150	breqtrd 5126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
152	151	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
153	113, 114, 140, 145, 152	elfzd 13443	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ (0...𝑀))
154	112, 153	ffvelcdmd 7039	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
155		simpll 767	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝜑)
156	135	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
157	116, 113, 114, 81	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
158	126, 156, 157	mpbir2and 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0..^𝑀))
159	155, 158, 101	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
160	139, 154, 159	ltled 11293	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
161	107, 111, 160	monoord 13967	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
162	28	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑀) = 𝐵)
163	161, 162	breqtrd 5126	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ 𝐵)
164	27, 33, 34, 105, 163	eliccd 45861	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (𝐴[,]𝐵))
165	164	ralrimiva 3130	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵))
166		fnfvrnss 7075	. . 3 ⊢ ((𝑄 Fn (0...𝑀) ∧ ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵)) → ran 𝑄 ⊆ (𝐴[,]𝐵))
167	15, 165, 166	syl2anc 585	. 2 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
168		df-f 6504	. 2 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) ↔ (𝑄 Fn (0...𝑀) ∧ ran 𝑄 ⊆ (𝐴[,]𝐵)))
169	15, 167, 168	sylanbrc 584	1 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 {crab 3401 Vcvv 3442 ⊆ wss 3903 class class class wbr 5100 ↦ cmpt 5181 ran crn 5633 Fn wfn 6495 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ↑_m cmap 8775 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 < clt 11178 ≤ cle 11179 − cmin 11376 ℕcn 12157 ℕ₀cn0 12413 ℤcz 12500 ℤ_≥cuz 12763 [,]cicc 13276 ...cfz 13435 ..^cfzo 13582

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-er 8645 df-map 8777 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-n0 12414 df-z 12501 df-uz 12764 df-icc 13280 df-fz 13436 df-fzo 13583

This theorem is referenced by: fourierdlem38 46500 fourierdlem50 46511 fourierdlem54 46515 fourierdlem63 46524 fourierdlem65 46526 fourierdlem69 46530 fourierdlem70 46531 fourierdlem74 46535 fourierdlem75 46536 fourierdlem76 46537 fourierdlem79 46540 fourierdlem81 46542 fourierdlem84 46545 fourierdlem85 46546 fourierdlem88 46549 fourierdlem89 46550 fourierdlem90 46551 fourierdlem91 46552 fourierdlem92 46553 fourierdlem93 46554 fourierdlem100 46561 fourierdlem101 46562 fourierdlem103 46564 fourierdlem104 46565 fourierdlem107 46568 fourierdlem111 46572 fourierdlem112 46573 fourierdlem113 46574

W3C validator