fourierdlem11 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem11 40904

Description: If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem11.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem11.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem11.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))

**Assertion**
Ref	Expression
fourierdlem11	⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))

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

**Proof of Theorem fourierdlem11**
Step	Hyp	Ref	Expression
1		fourierdlem11.q	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
2		fourierdlem11.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3		fourierdlem11.p	. . . . . . . . 9 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 40895	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 223	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simprd 489	. . . . 5 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
8	7	simpld 488	. . . 4 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
9	8	simpld 488	. . 3 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
10	6	simpld 488	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)))
11		elmapi 8081	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
13		0red 10296	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
14	13	leidd 10847	. . . . 5 ⊢ (𝜑 → 0 ≤ 0)
15	2	nnred 11290	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
16	2	nngt0d 11320	. . . . . 6 ⊢ (𝜑 → 0 < 𝑀)
17	13, 15, 16	ltled 10438	. . . . 5 ⊢ (𝜑 → 0 ≤ 𝑀)
18		0zd 11635	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
19	2	nnzd 11727	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
20		elfz 12538	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0...𝑀) ↔ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
21	18, 18, 19, 20	syl3anc 1490	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑀) ↔ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
22	14, 17, 21	mpbir2and 704	. . . 4 ⊢ (𝜑 → 0 ∈ (0...𝑀))
23	12, 22	ffvelrnd 6549	. . 3 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
24	9, 23	eqeltrrd 2844	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
25	8	simprd 489	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
26	15	leidd 10847	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
27		elfz 12538	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ∈ (0...𝑀) ↔ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
28	19, 18, 19, 27	syl3anc 1490	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (0...𝑀) ↔ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
29	17, 26, 28	mpbir2and 704	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
30	12, 29	ffvelrnd 6549	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
31	25, 30	eqeltrrd 2844	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
32		0le1 10804	. . . . . 6 ⊢ 0 ≤ 1
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ 1)
34	2	nnge1d 11319	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
35		1zzd 11654	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
36		elfz 12538	. . . . . 6 ⊢ ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
37	35, 18, 19, 36	syl3anc 1490	. . . . 5 ⊢ (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
38	33, 34, 37	mpbir2and 704	. . . 4 ⊢ (𝜑 → 1 ∈ (0...𝑀))
39	12, 38	ffvelrnd 6549	. . 3 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
40		elfzo 12679	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 < 𝑀)))
41	18, 18, 19, 40	syl3anc 1490	. . . . . 6 ⊢ (𝜑 → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 < 𝑀)))
42	14, 16, 41	mpbir2and 704	. . . . 5 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
43		0re 10294	. . . . . 6 ⊢ 0 ∈ ℝ
44		eleq1 2831	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
45	44	anbi2d 622	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
46		fveq2 6374	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
47		oveq1 6848	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
48	47	fveq2d 6378	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
49	46, 48	breq12d 4821	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
50	45, 49	imbi12d 335	. . . . . . 7 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
51	7	simprd 489	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
52	51	r19.21bi 3078	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
53	50, 52	vtoclg 3417	. . . . . 6 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
54	43, 53	ax-mp 5	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
55	42, 54	mpdan 678	. . . 4 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
56		0p1e1 11400	. . . . . 6 ⊢ (0 + 1) = 1
57	56	a1i 11	. . . . 5 ⊢ (𝜑 → (0 + 1) = 1)
58	57	fveq2d 6378	. . . 4 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
59	55, 9, 58	3brtr3d 4839	. . 3 ⊢ (𝜑 → 𝐴 < (𝑄‘1))
60		nnuz 11922	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
61	2, 60	syl6eleq 2853	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
62	12	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
63		0red 10296	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℝ)
64		elfzelz 12548	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℤ)
65	64	zred 11728	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℝ)
66		1red 10293	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ∈ ℝ)
67		0lt1 10803	. . . . . . . . . . 11 ⊢ 0 < 1
68	67	a1i 11	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 1)
69		elfzle1 12550	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ≤ 𝑖)
70	63, 66, 65, 68, 69	ltletrd 10450	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 𝑖)
71	63, 65, 70	ltled 10438	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 0 ≤ 𝑖)
72		elfzle2 12551	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
73		0zd 11635	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℤ)
74		elfzel2 12546	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑀 ∈ ℤ)
75		elfz 12538	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
76	64, 73, 74, 75	syl3anc 1490	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
77	71, 72, 76	mpbir2and 704	. . . . . . 7 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ (0...𝑀))
78	77	adantl 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (0...𝑀))
79	62, 78	ffvelrnd 6549	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
80	12	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
81		0red 10296	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ∈ ℝ)
82		elfzelz 12548	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℤ)
83	82	zred 11728	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℝ)
84		1red 10293	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ∈ ℝ)
85	67	a1i 11	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 1)
86		elfzle1 12550	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ≤ 𝑖)
87	81, 84, 83, 85, 86	ltletrd 10450	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 𝑖)
88	81, 83, 87	ltled 10438	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ≤ 𝑖)
89	88	adantl 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ 𝑖)
90	83	adantl 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
91	15	adantr 472	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
92		peano2rem 10601	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
93	91, 92	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
94		elfzle2 12551	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ≤ (𝑀 − 1))
95	94	adantl 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ (𝑀 − 1))
96	91	ltm1d 11209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
97	90, 93, 91, 95, 96	lelttrd 10448	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
98	90, 91, 97	ltled 10438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ 𝑀)
99	82	adantl 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℤ)
100		0zd 11635	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℤ)
101	19	adantr 472	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
102	99, 100, 101, 75	syl3anc 1490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
103	89, 98, 102	mpbir2and 704	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0...𝑀))
104	80, 103	ffvelrnd 6549	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ∈ ℝ)
105		0red 10296	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℝ)
106		peano2re 10462	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℝ → (𝑖 + 1) ∈ ℝ)
107	90, 106	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℝ)
108		1red 10293	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 ∈ ℝ)
109	67	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 < 1)
110	83, 106	syl 17	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → (𝑖 + 1) ∈ ℝ)
111	83	ltp1d 11207	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 < (𝑖 + 1))
112	84, 83, 110, 86, 111	lelttrd 10448	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 < (𝑖 + 1))
113	112	adantl 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 < (𝑖 + 1))
114	105, 108, 107, 109, 113	lttrd 10451	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 < (𝑖 + 1))
115	105, 107, 114	ltled 10438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ (𝑖 + 1))
116	90, 93, 108, 95	leadd1dd 10894	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ ((𝑀 − 1) + 1))
117	2	nncnd 11291	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
118		1cnd 10287	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 10649	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
120	119	adantr 472	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
121	116, 120	breqtrd 4834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ 𝑀)
122	99	peano2zd 11731	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℤ)
123		elfz 12538	. . . . . . . . 9 ⊢ (((𝑖 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑖 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑀)))
124	122, 100, 101, 123	syl3anc 1490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑖 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑀)))
125	115, 121, 124	mpbir2and 704	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ (0...𝑀))
126	80, 125	ffvelrnd 6549	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
127		elfzo 12679	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
128	99, 100, 101, 127	syl3anc 1490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
129	89, 97, 128	mpbir2and 704	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀))
130	129, 52	syldan 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
131	104, 126, 130	ltled 10438	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1)))
132	61, 79, 131	monoord 13037	. . . 4 ⊢ (𝜑 → (𝑄‘1) ≤ (𝑄‘𝑀))
133	132, 25	breqtrd 4834	. . 3 ⊢ (𝜑 → (𝑄‘1) ≤ 𝐵)
134	24, 39, 31, 59, 133	ltletrd 10450	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
135	24, 31, 134	3jca 1158	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1107 = wceq 1652 ∈ wcel 2155 ∀wral 3054 {crab 3058 class class class wbr 4808 ↦ cmpt 4887 ⟶wf 6063 ‘cfv 6067 (class class class)co 6841 ↑_𝑚 cmap 8059 ℝcr 10187 0cc0 10188 1c1 10189 + caddc 10191 < clt 10327 ≤ cle 10328 − cmin 10519 ℕcn 11273 ℤcz 11623 ℤ_≥cuz 11885 ...cfz 12532 ..^cfzo 12672

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2069 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2349 ax-ext 2742 ax-sep 4940 ax-nul 4948 ax-pow 5000 ax-pr 5061 ax-un 7146 ax-cnex 10244 ax-resscn 10245 ax-1cn 10246 ax-icn 10247 ax-addcl 10248 ax-addrcl 10249 ax-mulcl 10250 ax-mulrcl 10251 ax-mulcom 10252 ax-addass 10253 ax-mulass 10254 ax-distr 10255 ax-i2m1 10256 ax-1ne0 10257 ax-1rid 10258 ax-rnegex 10259 ax-rrecex 10260 ax-cnre 10261 ax-pre-lttri 10262 ax-pre-lttrn 10263 ax-pre-ltadd 10264 ax-pre-mulgt0 10265

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2062 df-mo 2564 df-eu 2581 df-clab 2751 df-cleq 2757 df-clel 2760 df-nfc 2895 df-ne 2937 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3351 df-sbc 3596 df-csb 3691 df-dif 3734 df-un 3736 df-in 3738 df-ss 3745 df-pss 3747 df-nul 4079 df-if 4243 df-pw 4316 df-sn 4334 df-pr 4336 df-tp 4338 df-op 4340 df-uni 4594 df-iun 4677 df-br 4809 df-opab 4871 df-mpt 4888 df-tr 4911 df-id 5184 df-eprel 5189 df-po 5197 df-so 5198 df-fr 5235 df-we 5237 df-xp 5282 df-rel 5283 df-cnv 5284 df-co 5285 df-dm 5286 df-rn 5287 df-res 5288 df-ima 5289 df-pred 5864 df-ord 5910 df-on 5911 df-lim 5912 df-suc 5913 df-iota 6030 df-fun 6069 df-fn 6070 df-f 6071 df-f1 6072 df-fo 6073 df-f1o 6074 df-fv 6075 df-riota 6802 df-ov 6844 df-oprab 6845 df-mpt2 6846 df-om 7263 df-1st 7365 df-2nd 7366 df-wrecs 7609 df-recs 7671 df-rdg 7709 df-er 7946 df-map 8061 df-en 8160 df-dom 8161 df-sdom 8162 df-pnf 10329 df-mnf 10330 df-xr 10331 df-ltxr 10332 df-le 10333 df-sub 10521 df-neg 10522 df-nn 11274 df-n0 11538 df-z 11624 df-uz 11886 df-fz 12533 df-fzo 12673

This theorem is referenced by: fourierdlem37 40930 fourierdlem54 40946 fourierdlem63 40955 fourierdlem64 40956 fourierdlem65 40957 fourierdlem69 40961 fourierdlem79 40971 fourierdlem89 40981 fourierdlem90 40982 fourierdlem91 40983 fourierdlem107 40999 fourierdlem109 41001

W3C validator