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 42402

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	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (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 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 42393	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 234	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simprd 498	. . . . 5 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
8	7	simpld 497	. . . 4 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
9	8	simpld 497	. . 3 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
10	6	simpld 497	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
11		elmapi 8427	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
13		0red 10643	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
14	13	leidd 11205	. . . . 5 ⊢ (𝜑 → 0 ≤ 0)
15	2	nnred 11652	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
16	2	nngt0d 11685	. . . . . 6 ⊢ (𝜑 → 0 < 𝑀)
17	13, 15, 16	ltled 10787	. . . . 5 ⊢ (𝜑 → 0 ≤ 𝑀)
18		0zd 11992	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
19	2	nnzd 12085	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
20		elfz 12897	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0...𝑀) ↔ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
21	18, 18, 19, 20	syl3anc 1367	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑀) ↔ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
22	14, 17, 21	mpbir2and 711	. . . 4 ⊢ (𝜑 → 0 ∈ (0...𝑀))
23	12, 22	ffvelrnd 6851	. . 3 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
24	9, 23	eqeltrrd 2914	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
25	8	simprd 498	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
26	15	leidd 11205	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
27		elfz 12897	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ∈ (0...𝑀) ↔ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
28	19, 18, 19, 27	syl3anc 1367	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (0...𝑀) ↔ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
29	17, 26, 28	mpbir2and 711	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
30	12, 29	ffvelrnd 6851	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
31	25, 30	eqeltrrd 2914	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
32		0le1 11162	. . . . . 6 ⊢ 0 ≤ 1
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ 1)
34	2	nnge1d 11684	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
35		1zzd 12012	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
36		elfz 12897	. . . . . 6 ⊢ ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
37	35, 18, 19, 36	syl3anc 1367	. . . . 5 ⊢ (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
38	33, 34, 37	mpbir2and 711	. . . 4 ⊢ (𝜑 → 1 ∈ (0...𝑀))
39	12, 38	ffvelrnd 6851	. . 3 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
40		elfzo 13039	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 < 𝑀)))
41	18, 18, 19, 40	syl3anc 1367	. . . . . 6 ⊢ (𝜑 → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 < 𝑀)))
42	14, 16, 41	mpbir2and 711	. . . . 5 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
43		0re 10642	. . . . . 6 ⊢ 0 ∈ ℝ
44		eleq1 2900	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
45	44	anbi2d 630	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
46		fveq2 6669	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
47		oveq1 7162	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
48	47	fveq2d 6673	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
49	46, 48	breq12d 5078	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
50	45, 49	imbi12d 347	. . . . . . 7 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
51	7	simprd 498	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
52	51	r19.21bi 3208	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
53	50, 52	vtoclg 3567	. . . . . 6 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
54	43, 53	ax-mp 5	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
55	42, 54	mpdan 685	. . . 4 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
56		0p1e1 11758	. . . . . 6 ⊢ (0 + 1) = 1
57	56	a1i 11	. . . . 5 ⊢ (𝜑 → (0 + 1) = 1)
58	57	fveq2d 6673	. . . 4 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
59	55, 9, 58	3brtr3d 5096	. . 3 ⊢ (𝜑 → 𝐴 < (𝑄‘1))
60		nnuz 12280	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
61	2, 60	eleqtrdi 2923	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
62	12	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
63		0red 10643	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℝ)
64		elfzelz 12907	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℤ)
65	64	zred 12086	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℝ)
66		1red 10641	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ∈ ℝ)
67		0lt1 11161	. . . . . . . . . . 11 ⊢ 0 < 1
68	67	a1i 11	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 1)
69		elfzle1 12909	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ≤ 𝑖)
70	63, 66, 65, 68, 69	ltletrd 10799	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 𝑖)
71	63, 65, 70	ltled 10787	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 0 ≤ 𝑖)
72		elfzle2 12910	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
73		0zd 11992	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℤ)
74		elfzel2 12905	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑀 ∈ ℤ)
75		elfz 12897	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
76	64, 73, 74, 75	syl3anc 1367	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
77	71, 72, 76	mpbir2and 711	. . . . . . 7 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ (0...𝑀))
78	77	adantl 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (0...𝑀))
79	62, 78	ffvelrnd 6851	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
80	12	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
81		0red 10643	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ∈ ℝ)
82		elfzelz 12907	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℤ)
83	82	zred 12086	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℝ)
84		1red 10641	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ∈ ℝ)
85	67	a1i 11	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 1)
86		elfzle1 12909	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ≤ 𝑖)
87	81, 84, 83, 85, 86	ltletrd 10799	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 𝑖)
88	81, 83, 87	ltled 10787	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ≤ 𝑖)
89	88	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ 𝑖)
90	83	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
91	15	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
92		peano2rem 10952	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
93	91, 92	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
94		elfzle2 12910	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ≤ (𝑀 − 1))
95	94	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ (𝑀 − 1))
96	91	ltm1d 11571	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
97	90, 93, 91, 95, 96	lelttrd 10797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
98	90, 91, 97	ltled 10787	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ 𝑀)
99	82	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℤ)
100		0zd 11992	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℤ)
101	19	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
102	99, 100, 101, 75	syl3anc 1367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
103	89, 98, 102	mpbir2and 711	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0...𝑀))
104	80, 103	ffvelrnd 6851	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ∈ ℝ)
105		0red 10643	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℝ)
106		peano2re 10812	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℝ → (𝑖 + 1) ∈ ℝ)
107	90, 106	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℝ)
108		1red 10641	. . . . . . . . . 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 11569	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 < (𝑖 + 1))
112	84, 83, 110, 86, 111	lelttrd 10797	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 < (𝑖 + 1))
113	112	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 < (𝑖 + 1))
114	105, 108, 107, 109, 113	lttrd 10800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 < (𝑖 + 1))
115	105, 107, 114	ltled 10787	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ (𝑖 + 1))
116	90, 93, 108, 95	leadd1dd 11253	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ ((𝑀 − 1) + 1))
117	2	nncnd 11653	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
118		1cnd 10635	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 11000	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
120	119	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
121	116, 120	breqtrd 5091	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ 𝑀)
122	99	peano2zd 12089	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℤ)
123		elfz 12897	. . . . . . . . 9 ⊢ (((𝑖 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑖 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑀)))
124	122, 100, 101, 123	syl3anc 1367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑖 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑀)))
125	115, 121, 124	mpbir2and 711	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ (0...𝑀))
126	80, 125	ffvelrnd 6851	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
127		elfzo 13039	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
128	99, 100, 101, 127	syl3anc 1367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
129	89, 97, 128	mpbir2and 711	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀))
130	129, 52	syldan 593	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
131	104, 126, 130	ltled 10787	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1)))
132	61, 79, 131	monoord 13399	. . . 4 ⊢ (𝜑 → (𝑄‘1) ≤ (𝑄‘𝑀))
133	132, 25	breqtrd 5091	. . 3 ⊢ (𝜑 → (𝑄‘1) ≤ 𝐵)
134	24, 39, 31, 59, 133	ltletrd 10799	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
135	24, 31, 134	3jca 1124	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 {crab 3142 class class class wbr 5065 ↦ cmpt 5145 ⟶wf 6350 ‘cfv 6354 (class class class)co 7155 ↑_m cmap 8405 ℝcr 10535 0cc0 10536 1c1 10537 + caddc 10539 < clt 10674 ≤ cle 10675 − cmin 10869 ℕcn 11637 ℤcz 11980 ℤ_≥cuz 12242 ...cfz 12891 ..^cfzo 13032

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460 ax-cnex 10592 ax-resscn 10593 ax-1cn 10594 ax-icn 10595 ax-addcl 10596 ax-addrcl 10597 ax-mulcl 10598 ax-mulrcl 10599 ax-mulcom 10600 ax-addass 10601 ax-mulass 10602 ax-distr 10603 ax-i2m1 10604 ax-1ne0 10605 ax-1rid 10606 ax-rnegex 10607 ax-rrecex 10608 ax-cnre 10609 ax-pre-lttri 10610 ax-pre-lttrn 10611 ax-pre-ltadd 10612 ax-pre-mulgt0 10613

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-iun 4920 df-br 5066 df-opab 5128 df-mpt 5146 df-tr 5172 df-id 5459 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-we 5515 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-pred 6147 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7580 df-1st 7688 df-2nd 7689 df-wrecs 7946 df-recs 8007 df-rdg 8045 df-er 8288 df-map 8407 df-en 8509 df-dom 8510 df-sdom 8511 df-pnf 10676 df-mnf 10677 df-xr 10678 df-ltxr 10679 df-le 10680 df-sub 10871 df-neg 10872 df-nn 11638 df-n0 11897 df-z 11981 df-uz 12243 df-fz 12892 df-fzo 13033

This theorem is referenced by: fourierdlem37 42428 fourierdlem54 42444 fourierdlem63 42453 fourierdlem64 42454 fourierdlem65 42455 fourierdlem69 42459 fourierdlem79 42469 fourierdlem89 42479 fourierdlem90 42480 fourierdlem91 42481 fourierdlem107 42497 fourierdlem109 42499

W3C validator