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 40852

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 40843	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 222	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simprd 483	. . . . 5 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
8	7	simpld 482	. . . 4 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
9	8	simpld 482	. . 3 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
10	6	simpld 482	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)))
11		elmapi 8031	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
13		0red 10243	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
14	13	leidd 10796	. . . . 5 ⊢ (𝜑 → 0 ≤ 0)
15	2	nnred 11237	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
16	2	nngt0d 11266	. . . . . 6 ⊢ (𝜑 → 0 < 𝑀)
17	13, 15, 16	ltled 10387	. . . . 5 ⊢ (𝜑 → 0 ≤ 𝑀)
18		0zd 11591	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
19	2	nnzd 11683	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
20		elfz 12539	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0...𝑀) ↔ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
21	18, 18, 19, 20	syl3anc 1476	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑀) ↔ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
22	14, 17, 21	mpbir2and 692	. . . 4 ⊢ (𝜑 → 0 ∈ (0...𝑀))
23	12, 22	ffvelrnd 6503	. . 3 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
24	9, 23	eqeltrrd 2851	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
25	8	simprd 483	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
26	15	leidd 10796	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
27		elfz 12539	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ∈ (0...𝑀) ↔ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
28	19, 18, 19, 27	syl3anc 1476	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (0...𝑀) ↔ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
29	17, 26, 28	mpbir2and 692	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
30	12, 29	ffvelrnd 6503	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
31	25, 30	eqeltrrd 2851	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
32		0le1 10753	. . . . . 6 ⊢ 0 ≤ 1
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ 1)
34	2	nnge1d 11265	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
35		1zzd 11610	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
36		elfz 12539	. . . . . 6 ⊢ ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
37	35, 18, 19, 36	syl3anc 1476	. . . . 5 ⊢ (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
38	33, 34, 37	mpbir2and 692	. . . 4 ⊢ (𝜑 → 1 ∈ (0...𝑀))
39	12, 38	ffvelrnd 6503	. . 3 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
40		elfzo 12680	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 < 𝑀)))
41	18, 18, 19, 40	syl3anc 1476	. . . . . 6 ⊢ (𝜑 → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 < 𝑀)))
42	14, 16, 41	mpbir2and 692	. . . . 5 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
43		0re 10242	. . . . . 6 ⊢ 0 ∈ ℝ
44		eleq1 2838	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
45	44	anbi2d 614	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
46		fveq2 6332	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
47		oveq1 6800	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
48	47	fveq2d 6336	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
49	46, 48	breq12d 4799	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
50	45, 49	imbi12d 333	. . . . . . 7 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
51	7	simprd 483	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
52	51	r19.21bi 3081	. . . . . . 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 667	. . . 4 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
56		0p1e1 11334	. . . . . 6 ⊢ (0 + 1) = 1
57	56	a1i 11	. . . . 5 ⊢ (𝜑 → (0 + 1) = 1)
58	57	fveq2d 6336	. . . 4 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
59	55, 9, 58	3brtr3d 4817	. . 3 ⊢ (𝜑 → 𝐴 < (𝑄‘1))
60		nnuz 11925	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
61	2, 60	syl6eleq 2860	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
62	12	adantr 466	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
63		0red 10243	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℝ)
64		elfzelz 12549	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℤ)
65	64	zred 11684	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℝ)
66		1red 10257	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ∈ ℝ)
67		0lt1 10752	. . . . . . . . . . 11 ⊢ 0 < 1
68	67	a1i 11	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 1)
69		elfzle1 12551	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ≤ 𝑖)
70	63, 66, 65, 68, 69	ltletrd 10399	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 𝑖)
71	63, 65, 70	ltled 10387	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 0 ≤ 𝑖)
72		elfzle2 12552	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
73		0zd 11591	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℤ)
74		elfzel2 12547	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑀 ∈ ℤ)
75		elfz 12539	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
76	64, 73, 74, 75	syl3anc 1476	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
77	71, 72, 76	mpbir2and 692	. . . . . . 7 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ (0...𝑀))
78	77	adantl 467	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (0...𝑀))
79	62, 78	ffvelrnd 6503	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
80	12	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
81		0red 10243	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ∈ ℝ)
82		elfzelz 12549	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℤ)
83	82	zred 11684	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℝ)
84		1red 10257	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ∈ ℝ)
85	67	a1i 11	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 1)
86		elfzle1 12551	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ≤ 𝑖)
87	81, 84, 83, 85, 86	ltletrd 10399	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 𝑖)
88	81, 83, 87	ltled 10387	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ≤ 𝑖)
89	88	adantl 467	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ 𝑖)
90	83	adantl 467	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
91	15	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
92		peano2rem 10550	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
93	91, 92	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
94		elfzle2 12552	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ≤ (𝑀 − 1))
95	94	adantl 467	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ (𝑀 − 1))
96	91	ltm1d 11158	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
97	90, 93, 91, 95, 96	lelttrd 10397	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
98	90, 91, 97	ltled 10387	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ 𝑀)
99	82	adantl 467	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℤ)
100		0zd 11591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℤ)
101	19	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
102	99, 100, 101, 75	syl3anc 1476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
103	89, 98, 102	mpbir2and 692	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0...𝑀))
104	80, 103	ffvelrnd 6503	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ∈ ℝ)
105		0red 10243	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℝ)
106		peano2re 10411	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℝ → (𝑖 + 1) ∈ ℝ)
107	90, 106	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℝ)
108		1red 10257	. . . . . . . . . 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 11156	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 < (𝑖 + 1))
112	84, 83, 110, 86, 111	lelttrd 10397	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 < (𝑖 + 1))
113	112	adantl 467	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 < (𝑖 + 1))
114	105, 108, 107, 109, 113	lttrd 10400	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 < (𝑖 + 1))
115	105, 107, 114	ltled 10387	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ (𝑖 + 1))
116	90, 93, 108, 95	leadd1dd 10843	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ ((𝑀 − 1) + 1))
117	2	nncnd 11238	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
118		1cnd 10258	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 10598	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
120	119	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
121	116, 120	breqtrd 4812	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ 𝑀)
122	99	peano2zd 11687	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℤ)
123		elfz 12539	. . . . . . . . 9 ⊢ (((𝑖 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑖 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑀)))
124	122, 100, 101, 123	syl3anc 1476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑖 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑀)))
125	115, 121, 124	mpbir2and 692	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ (0...𝑀))
126	80, 125	ffvelrnd 6503	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
127		elfzo 12680	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
128	99, 100, 101, 127	syl3anc 1476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
129	89, 97, 128	mpbir2and 692	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀))
130	129, 52	syldan 579	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
131	104, 126, 130	ltled 10387	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1)))
132	61, 79, 131	monoord 13038	. . . 4 ⊢ (𝜑 → (𝑄‘1) ≤ (𝑄‘𝑀))
133	132, 25	breqtrd 4812	. . 3 ⊢ (𝜑 → (𝑄‘1) ≤ 𝐵)
134	24, 39, 31, 59, 133	ltletrd 10399	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
135	24, 31, 134	3jca 1122	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 ∀wral 3061 {crab 3065 class class class wbr 4786 ↦ cmpt 4863 ⟶wf 6027 ‘cfv 6031 (class class class)co 6793 ↑_𝑚 cmap 8009 ℝcr 10137 0cc0 10138 1c1 10139 + caddc 10141 < clt 10276 ≤ cle 10277 − cmin 10468 ℕcn 11222 ℤcz 11579 ℤ_≥cuz 11888 ...cfz 12533 ..^cfzo 12673

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 ax-cnex 10194 ax-resscn 10195 ax-1cn 10196 ax-icn 10197 ax-addcl 10198 ax-addrcl 10199 ax-mulcl 10200 ax-mulrcl 10201 ax-mulcom 10202 ax-addass 10203 ax-mulass 10204 ax-distr 10205 ax-i2m1 10206 ax-1ne0 10207 ax-1rid 10208 ax-rnegex 10209 ax-rrecex 10210 ax-cnre 10211 ax-pre-lttri 10212 ax-pre-lttrn 10213 ax-pre-ltadd 10214 ax-pre-mulgt0 10215

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-riota 6754 df-ov 6796 df-oprab 6797 df-mpt2 6798 df-om 7213 df-1st 7315 df-2nd 7316 df-wrecs 7559 df-recs 7621 df-rdg 7659 df-er 7896 df-map 8011 df-en 8110 df-dom 8111 df-sdom 8112 df-pnf 10278 df-mnf 10279 df-xr 10280 df-ltxr 10281 df-le 10282 df-sub 10470 df-neg 10471 df-nn 11223 df-n0 11495 df-z 11580 df-uz 11889 df-fz 12534 df-fzo 12674

This theorem is referenced by: fourierdlem37 40878 fourierdlem54 40894 fourierdlem63 40903 fourierdlem64 40904 fourierdlem65 40905 fourierdlem69 40909 fourierdlem79 40919 fourierdlem89 40929 fourierdlem90 40930 fourierdlem91 40931 fourierdlem107 40947 fourierdlem109 40949

W3C validator