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 47101

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 47088	. . . . . . 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 500	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
8		reex 11284	. . . . . 6 ⊢ ℝ ∈ V
9	8	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ∈ V)
10		ovex 7451	. . . . . 6 ⊢ (0...𝑀) ∈ V
11	10	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ V)
12	9, 11	elmapd 8853	. . . 4 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ))
13	7, 12	mpbid 235	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
14		ffn 6707	. . 3 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
15	13, 14	syl 18	. 2 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
16	6	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
17	16	simpld 500	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
18	17	simpld 500	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
19		nnnn0 12606	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
20		nn0uz 12996	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
21	19, 20	eleqtrdi 2871	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘0))
22	2, 21	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
23		eluzfz1 13657	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
24	22, 23	syl 18	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
25	13, 24	ffvelcdmd 7083	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
26	18, 25	eqeltrrd 2862	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ)
27	26	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ∈ ℝ)
28	17	simprd 501	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
29		eluzfz2 13658	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
30	22, 29	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
31	13, 30	ffvelcdmd 7083	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
32	28, 31	eqeltrrd 2862	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
33	32	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐵 ∈ ℝ)
34	13	ffvelcdmda 7082	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
35	18	eqcomd 2767	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
36	35	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 = (𝑄‘0))
37		elfzuz 13645	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ (ℤ_≥‘0))
38	37	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (ℤ_≥‘0))
39	13	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
40		0zd 12698	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ∈ ℤ)
41		elfzel2 13647	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
42	41	adantr 486	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℤ)
43		elfzelz 13649	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℤ)
44	43	adantl 487	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℤ)
45		elfzle1 13653	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 0 ≤ 𝑗)
46	45	adantl 487	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ≤ 𝑗)
47	43	zred 12796	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℝ)
48	47	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℝ)
49		elfzelz 13649	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
50	49	zred 12796	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
51	50	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ∈ ℝ)
52	41	zred 12796	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
53	52	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℝ)
54		elfzle2 13654	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ≤ 𝑖)
55	54	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑖)
56		elfzle2 13654	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
57	56	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ≤ 𝑀)
58	48, 51, 53, 55, 57	letrd 11460	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑀)
59	40, 42, 44, 46, 58	elfzd 13640	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
60	59	adantll 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
61	39, 60	ffvelcdmd 7083	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → (𝑄‘𝑗) ∈ ℝ)
62		simpll 779	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝜑)
63		elfzle1 13653	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 0 ≤ 𝑗)
64	63	adantl 487	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ≤ 𝑗)
65		elfzelz 13649	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℤ)
66	65	zred 12796	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℝ)
67	66	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℝ)
68	50	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ∈ ℝ)
69	52	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℝ)
70		peano2rem 11618	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
71	68, 70	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
72		elfzle2 13654	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
73	72	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
74	68	ltm1d 12242	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
75	67, 71, 68, 73, 74	lelttrd 11461	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑖)
76	56	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ≤ 𝑀)
77	67, 68, 69, 75, 76	ltletrd 11463	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑀)
78	65	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℤ)
79		0zd 12698	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ∈ ℤ)
80	41	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℤ)
81		elfzo 13788	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
82	78, 79, 80, 81	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
83	64, 77, 82	mpbir2and 726	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
84	83	adantll 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
85	13	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
86		elfzofz 13803	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀))
87	86	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
88	85, 87	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ)
89		fzofzp1 13892	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
90	89	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
91	85, 90	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
92		eleq1w 2844	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
93	92	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
94		fveq2 6883	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
95		oveq1 7425	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
96	95	fveq2d 6887	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
97	94, 96	breq12d 5116	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
98	93, 97	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
99	16	simprd 501	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
100	99	r19.21bi 3255	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
101	98, 100	chvarvv 2022	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
102	88, 91, 101	ltled 11451	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
103	62, 84, 102	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
104	38, 61, 103	monoord 14168	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
105	36, 104	eqbrtrd 5127	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ≤ (𝑄‘𝑖))
106		elfzuz3 13646	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ (ℤ_≥‘𝑖))
107	106	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (ℤ_≥‘𝑖))
108	13	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
109		fz0fzelfz0 13761	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
110	109	adantll 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
111	108, 110	ffvelcdmd 7083	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
112	13	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
113		0zd 12698	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℤ)
114	41	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℤ)
115		elfzelz 13649	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℤ)
116	115	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℤ)
117		0red 11304	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℝ)
118	50	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ∈ ℝ)
119	115	zred 12796	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℝ)
120	119	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
121		elfzle1 13653	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
122	121	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑖)
123		elfzle1 13653	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑖 ≤ 𝑗)
124	123	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ≤ 𝑗)
125	117, 118, 120, 122, 124	letrd 11460	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
126	125	adantll 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
127	119	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
128	2	nnred 12343	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
129	128	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℝ)
130		1red 11302	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
131	129, 130	resubcld 11737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
132		elfzle2 13654	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ≤ (𝑀 − 1))
133	132	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ (𝑀 − 1))
134	129	ltm1d 12242	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
135	127, 131, 129, 133, 134	lelttrd 11461	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
136	127, 129, 135	ltled 11451	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
137	136	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
138	113, 114, 116, 126, 137	elfzd 13640	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0...𝑀))
139	112, 138	ffvelcdmd 7083	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ∈ ℝ)
140	116	peano2zd 12799	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ ℤ)
141	119	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
142		1red 11302	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
143		0le1 11832	. . . . . . . . . . . 12 ⊢ 0 ≤ 1
144	143	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 1)
145	141, 142, 126, 144	addge0d 11885	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ (𝑗 + 1))
146	127, 131, 130, 133	leadd1dd 11923	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ ((𝑀 − 1) + 1))
147	2	nncnd 12344	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℂ)
148	147	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℂ)
149		1cnd 11295	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℂ)
150	148, 149	npcand 11666	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
151	146, 150	breqtrd 5131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
152	151	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
153	113, 114, 140, 145, 152	elfzd 13640	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ (0...𝑀))
154	112, 153	ffvelcdmd 7083	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
155		simpll 779	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝜑)
156	135	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
157	116, 113, 114, 81	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
158	126, 156, 157	mpbir2and 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0..^𝑀))
159	155, 158, 101	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
160	139, 154, 159	ltled 11451	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
161	107, 111, 160	monoord 14168	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
162	28	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑀) = 𝐵)
163	161, 162	breqtrd 5131	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ 𝐵)
164	27, 33, 34, 105, 163	eliccd 46485	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (𝐴[,]𝐵))
165	164	ralrimiva 3155	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵))
166		fnfvrnss 7119	. . 3 ⊢ ((𝑄 Fn (0...𝑀) ∧ ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵)) → ran 𝑄 ⊆ (𝐴[,]𝐵))
167	15, 165, 166	syl2anc 596	. 2 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
168		df-f 6541	. 2 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) ↔ (𝑄 Fn (0...𝑀) ∧ ran 𝑄 ⊆ (𝐴[,]𝐵)))
169	15, 167, 168	sylanbrc 595	1 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 {crab 3413 Vcvv 3451 ⊆ wss 3899 class class class wbr 5103 ↦ cmpt 5186 ran crn 5652 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 ↑_m cmap 8840 ℂcc 11191 ℝcr 11192 0cc0 11193 1c1 11194 + caddc 11196 < clt 11336 ≤ cle 11337 − cmin 11534 ℕcn 12328 ℕ₀cn0 12599 ℤcz 12686 ℤ_≥cuz 12958 [,]cicc 13472 ...cfz 13632 ..^cfzo 13781

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-er 8710 df-map 8842 df-en 8967 df-dom 8968 df-sdom 8969 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-nn 12329 df-n0 12600 df-z 12687 df-uz 12959 df-icc 13476 df-fz 13633 df-fzo 13782

This theorem is used by: fourierdlem38 47124 fourierdlem50 47135 fourierdlem54 47139 fourierdlem63 47148 fourierdlem65 47150 fourierdlem69 47154 fourierdlem70 47155 fourierdlem74 47159 fourierdlem75 47160 fourierdlem76 47161 fourierdlem79 47164 fourierdlem81 47166 fourierdlem84 47169 fourierdlem85 47170 fourierdlem88 47173 fourierdlem89 47174 fourierdlem90 47175 fourierdlem91 47176 fourierdlem92 47177 fourierdlem93 47178 fourierdlem100 47185 fourierdlem101 47186 fourierdlem103 47188 fourierdlem104 47189 fourierdlem107 47192 fourierdlem111 47196 fourierdlem112 47197 fourierdlem113 47198

W3C validator