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 41976

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	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (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 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 41963	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 233	. . . . 5 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simpld 495	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)))
8		reex 10479	. . . . . 6 ⊢ ℝ ∈ V
9	8	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ∈ V)
10		ovex 7053	. . . . . 6 ⊢ (0...𝑀) ∈ V
11	10	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ V)
12	9, 11	elmapd 8275	. . . 4 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ))
13	7, 12	mpbid 233	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
14		ffn 6387	. . 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 11757	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
20		nn0uz 12134	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
21	19, 20	syl6eleq 2893	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘0))
22	2, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
23		eluzfz1 12769	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
24	22, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
25	13, 24	ffvelrnd 6722	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
26	18, 25	eqeltrrd 2884	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ)
27	26	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ∈ ℝ)
28	17	simprd 496	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
29		eluzfz2 12770	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
30	22, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
31	13, 30	ffvelrnd 6722	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
32	28, 31	eqeltrrd 2884	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
33	32	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐵 ∈ ℝ)
34	13	ffvelrnda 6721	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
35	18	eqcomd 2801	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
36	35	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 = (𝑄‘0))
37		elfzuz 12759	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ (ℤ_≥‘0))
38	37	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (ℤ_≥‘0))
39	13	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
40		elfzle1 12765	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑖) → 0 ≤ 𝑗)
41	40	adantl 482	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ≤ 𝑗)
42		elfzelz 12763	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℤ)
43	42	zred 11941	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℝ)
44	43	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℝ)
45		elfzelz 12763	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
46	45	zred 11941	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
47	46	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ∈ ℝ)
48		elfzel2 12761	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
49	48	zred 11941	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
50	49	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℝ)
51		elfzle2 12766	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ≤ 𝑖)
52	51	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑖)
53		elfzle2 12766	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
54	53	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ≤ 𝑀)
55	44, 47, 50, 52, 54	letrd 10649	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑀)
56	42	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℤ)
57		0zd 11846	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ∈ ℤ)
58	48	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℤ)
59		elfz 12753	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ∈ (0...𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀)))
60	56, 57, 58, 59	syl3anc 1364	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → (𝑗 ∈ (0...𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀)))
61	41, 55, 60	mpbir2and 709	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
62	61	adantll 710	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀))
63	39, 62	ffvelrnd 6722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → (𝑄‘𝑗) ∈ ℝ)
64		simpll 763	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝜑)
65		elfzle1 12765	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 0 ≤ 𝑗)
66	65	adantl 482	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ≤ 𝑗)
67		elfzelz 12763	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℤ)
68	67	zred 11941	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℝ)
69	68	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℝ)
70	46	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ∈ ℝ)
71	49	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℝ)
72		peano2rem 10806	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
73	70, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
74		elfzle2 12766	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
75	74	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
76	70	ltm1d 11425	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
77	69, 73, 70, 75, 76	lelttrd 10650	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑖)
78	53	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ≤ 𝑀)
79	69, 70, 71, 77, 78	ltletrd 10652	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑀)
80	67	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℤ)
81		0zd 11846	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ∈ ℤ)
82	48	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℤ)
83		elfzo 12895	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
84	80, 81, 82, 83	syl3anc 1364	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
85	66, 79, 84	mpbir2and 709	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
86	85	adantll 710	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀))
87	13	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
88		elfzofz 12908	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀))
89	88	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
90	87, 89	ffvelrnd 6722	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ)
91		fzofzp1 12989	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
92	91	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
93	87, 92	ffvelrnd 6722	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
94		eleq1w 2865	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
95	94	anbi2d 628	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
96		fveq2 6543	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
97		oveq1 7028	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
98	97	fveq2d 6547	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
99	96, 98	breq12d 4979	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
100	95, 99	imbi12d 346	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
101	16	simprd 496	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
102	101	r19.21bi 3175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
103	100, 102	chvarv 2370	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
104	90, 93, 103	ltled 10640	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
105	64, 86, 104	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
106	38, 63, 105	monoord 13255	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
107	36, 106	eqbrtrd 4988	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ≤ (𝑄‘𝑖))
108		elfzuz3 12760	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ (ℤ_≥‘𝑖))
109	108	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (ℤ_≥‘𝑖))
110	13	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
111		fz0fzelfz0 12868	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
112	111	adantll 710	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀))
113	110, 112	ffvelrnd 6722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
114	13	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
115		0red 10495	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℝ)
116	46	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ∈ ℝ)
117		elfzelz 12763	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℤ)
118	117	zred 11941	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℝ)
119	118	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
120		elfzle1 12765	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
121	120	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑖)
122		elfzle1 12765	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑖 ≤ 𝑗)
123	122	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ≤ 𝑗)
124	115, 116, 119, 121, 123	letrd 10649	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
125	124	adantll 710	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗)
126	118	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
127	2	nnred 11506	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
128	127	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℝ)
129		1red 10493	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
130	128, 129	resubcld 10921	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
131		elfzle2 12766	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ≤ (𝑀 − 1))
132	131	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ (𝑀 − 1))
133	128	ltm1d 11425	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
134	126, 130, 128, 132, 133	lelttrd 10650	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
135	126, 128, 134	ltled 10640	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
136	135	adantlr 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀)
137	117	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℤ)
138		0zd 11846	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈ ℤ)
139	48	ad2antlr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℤ)
140	137, 138, 139, 59	syl3anc 1364	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 ∈ (0...𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀)))
141	125, 136, 140	mpbir2and 709	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0...𝑀))
142	114, 141	ffvelrnd 6722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ∈ ℝ)
143	118	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ)
144		1red 10493	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℝ)
145		0le1 11016	. . . . . . . . . . . 12 ⊢ 0 ≤ 1
146	145	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 1)
147	143, 144, 125, 146	addge0d 11069	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ (𝑗 + 1))
148	126, 130, 129, 132	leadd1dd 11107	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ ((𝑀 − 1) + 1))
149	2	nncnd 11507	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℂ)
150	149	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℂ)
151		1cnd 10487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈ ℂ)
152	150, 151	npcand 10854	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
153	148, 152	breqtrd 4992	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
154	153	adantlr 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀)
155	137	peano2zd 11944	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ ℤ)
156		elfz 12753	. . . . . . . . . . 11 ⊢ (((𝑗 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑗 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑀)))
157	155, 138, 139, 156	syl3anc 1364	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → ((𝑗 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑀)))
158	147, 154, 157	mpbir2and 709	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ (0...𝑀))
159	114, 158	ffvelrnd 6722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
160		simpll 763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝜑)
161	134	adantlr 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀)
162	137, 138, 139, 83	syl3anc 1364	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀)))
163	125, 161, 162	mpbir2and 709	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0..^𝑀))
164	160, 163, 103	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
165	142, 159, 164	ltled 10640	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1)))
166	109, 113, 165	monoord 13255	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
167	28	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑀) = 𝐵)
168	166, 167	breqtrd 4992	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ 𝐵)
169	27, 33, 34, 107, 168	eliccd 41347	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (𝐴[,]𝐵))
170	169	ralrimiva 3149	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵))
171		fnfvrnss 6752	. . 3 ⊢ ((𝑄 Fn (0...𝑀) ∧ ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵)) → ran 𝑄 ⊆ (𝐴[,]𝐵))
172	15, 170, 171	syl2anc 584	. 2 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
173		df-f 6234	. 2 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) ↔ (𝑄 Fn (0...𝑀) ∧ ran 𝑄 ⊆ (𝐴[,]𝐵)))
174	15, 172, 173	sylanbrc 583	1 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∀wral 3105 {crab 3109 Vcvv 3437 ⊆ wss 3863 class class class wbr 4966 ↦ cmpt 5045 ran crn 5449 Fn wfn 6225 ⟶wf 6226 ‘cfv 6230 (class class class)co 7021 ↑_𝑚 cmap 8261 ℂcc 10386 ℝcr 10387 0cc0 10388 1c1 10389 + caddc 10391 < clt 10526 ≤ cle 10527 − cmin 10722 ℕcn 11491 ℕ₀cn0 11750 ℤcz 11834 ℤ_≥cuz 12098 [,]cicc 12596 ...cfz 12747 ..^cfzo 12888

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-cnex 10444 ax-resscn 10445 ax-1cn 10446 ax-icn 10447 ax-addcl 10448 ax-addrcl 10449 ax-mulcl 10450 ax-mulrcl 10451 ax-mulcom 10452 ax-addass 10453 ax-mulass 10454 ax-distr 10455 ax-i2m1 10456 ax-1ne0 10457 ax-1rid 10458 ax-rnegex 10459 ax-rrecex 10460 ax-cnre 10461 ax-pre-lttri 10462 ax-pre-lttrn 10463 ax-pre-ltadd 10464 ax-pre-mulgt0 10465

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-pss 3880 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-tp 4481 df-op 4483 df-uni 4750 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-tr 5069 df-id 5353 df-eprel 5358 df-po 5367 df-so 5368 df-fr 5407 df-we 5409 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-pred 6028 df-ord 6074 df-on 6075 df-lim 6076 df-suc 6077 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-riota 6982 df-ov 7024 df-oprab 7025 df-mpo 7026 df-om 7442 df-1st 7550 df-2nd 7551 df-wrecs 7803 df-recs 7865 df-rdg 7903 df-er 8144 df-map 8263 df-en 8363 df-dom 8364 df-sdom 8365 df-pnf 10528 df-mnf 10529 df-xr 10530 df-ltxr 10531 df-le 10532 df-sub 10724 df-neg 10725 df-nn 11492 df-n0 11751 df-z 11835 df-uz 12099 df-icc 12600 df-fz 12748 df-fzo 12889

This theorem is referenced by: fourierdlem38 41999 fourierdlem50 42010 fourierdlem54 42014 fourierdlem63 42023 fourierdlem65 42025 fourierdlem69 42029 fourierdlem70 42030 fourierdlem74 42034 fourierdlem75 42035 fourierdlem76 42036 fourierdlem79 42039 fourierdlem81 42041 fourierdlem84 42044 fourierdlem85 42045 fourierdlem88 42048 fourierdlem89 42049 fourierdlem90 42050 fourierdlem91 42051 fourierdlem92 42052 fourierdlem93 42053 fourierdlem100 42060 fourierdlem101 42061 fourierdlem103 42063 fourierdlem104 42064 fourierdlem107 42067 fourierdlem111 42071 fourierdlem112 42072 fourierdlem113 42073

W3C validator