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 42410

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 42401	. . . . . . . 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 8431	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
13		0red 10647	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
14	13	leidd 11209	. . . . 5 ⊢ (𝜑 → 0 ≤ 0)
15	2	nnred 11656	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
16	2	nngt0d 11689	. . . . . 6 ⊢ (𝜑 → 0 < 𝑀)
17	13, 15, 16	ltled 10791	. . . . 5 ⊢ (𝜑 → 0 ≤ 𝑀)
18		0zd 11996	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
19	2	nnzd 12089	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
20		elfz 12901	. . . . . 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 6855	. . 3 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
24	9, 23	eqeltrrd 2917	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
25	8	simprd 498	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
26	15	leidd 11209	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
27		elfz 12901	. . . . . 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 6855	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
31	25, 30	eqeltrrd 2917	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
32		0le1 11166	. . . . . 6 ⊢ 0 ≤ 1
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ 1)
34	2	nnge1d 11688	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
35		1zzd 12016	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
36		elfz 12901	. . . . . 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 6855	. . 3 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
40		elfzo 13043	. . . . . . 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 10646	. . . . . 6 ⊢ 0 ∈ ℝ
44		eleq1 2903	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
45	44	anbi2d 630	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
46		fveq2 6673	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
47		oveq1 7166	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
48	47	fveq2d 6677	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
49	46, 48	breq12d 5082	. . . . . . . 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 3211	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
53	50, 52	vtoclg 3570	. . . . . 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 11762	. . . . . 6 ⊢ (0 + 1) = 1
57	56	a1i 11	. . . . 5 ⊢ (𝜑 → (0 + 1) = 1)
58	57	fveq2d 6677	. . . 4 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
59	55, 9, 58	3brtr3d 5100	. . 3 ⊢ (𝜑 → 𝐴 < (𝑄‘1))
60		nnuz 12284	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
61	2, 60	eleqtrdi 2926	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
62	12	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
63		0red 10647	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℝ)
64		elfzelz 12911	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℤ)
65	64	zred 12090	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℝ)
66		1red 10645	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ∈ ℝ)
67		0lt1 11165	. . . . . . . . . . 11 ⊢ 0 < 1
68	67	a1i 11	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 1)
69		elfzle1 12913	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ≤ 𝑖)
70	63, 66, 65, 68, 69	ltletrd 10803	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 𝑖)
71	63, 65, 70	ltled 10791	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 0 ≤ 𝑖)
72		elfzle2 12914	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
73		0zd 11996	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℤ)
74		elfzel2 12909	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑀 ∈ ℤ)
75		elfz 12901	. . . . . . . . 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 6855	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
80	12	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
81		0red 10647	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ∈ ℝ)
82		elfzelz 12911	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℤ)
83	82	zred 12090	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℝ)
84		1red 10645	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ∈ ℝ)
85	67	a1i 11	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 1)
86		elfzle1 12913	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ≤ 𝑖)
87	81, 84, 83, 85, 86	ltletrd 10803	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 𝑖)
88	81, 83, 87	ltled 10791	. . . . . . . . 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 10956	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
93	91, 92	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
94		elfzle2 12914	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ≤ (𝑀 − 1))
95	94	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ (𝑀 − 1))
96	91	ltm1d 11575	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
97	90, 93, 91, 95, 96	lelttrd 10801	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
98	90, 91, 97	ltled 10791	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ 𝑀)
99	82	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℤ)
100		0zd 11996	. . . . . . . . 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 6855	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ∈ ℝ)
105		0red 10647	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℝ)
106		peano2re 10816	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℝ → (𝑖 + 1) ∈ ℝ)
107	90, 106	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℝ)
108		1red 10645	. . . . . . . . . 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 11573	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 < (𝑖 + 1))
112	84, 83, 110, 86, 111	lelttrd 10801	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 < (𝑖 + 1))
113	112	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 < (𝑖 + 1))
114	105, 108, 107, 109, 113	lttrd 10804	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 < (𝑖 + 1))
115	105, 107, 114	ltled 10791	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ (𝑖 + 1))
116	90, 93, 108, 95	leadd1dd 11257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ ((𝑀 − 1) + 1))
117	2	nncnd 11657	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
118		1cnd 10639	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 11004	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
120	119	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
121	116, 120	breqtrd 5095	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ 𝑀)
122	99	peano2zd 12093	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℤ)
123		elfz 12901	. . . . . . . . 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 6855	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
127		elfzo 13043	. . . . . . . . 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 10791	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1)))
132	61, 79, 131	monoord 13403	. . . 4 ⊢ (𝜑 → (𝑄‘1) ≤ (𝑄‘𝑀))
133	132, 25	breqtrd 5095	. . 3 ⊢ (𝜑 → (𝑄‘1) ≤ 𝐵)
134	24, 39, 31, 59, 133	ltletrd 10803	. 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 1536 ∈ wcel 2113 ∀wral 3141 {crab 3145 class class class wbr 5069 ↦ cmpt 5149 ⟶wf 6354 ‘cfv 6358 (class class class)co 7159 ↑_m cmap 8409 ℝcr 10539 0cc0 10540 1c1 10541 + caddc 10543 < clt 10678 ≤ cle 10679 − cmin 10873 ℕcn 11641 ℤcz 11984 ℤ_≥cuz 12246 ...cfz 12895 ..^cfzo 13036

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-cnex 10596 ax-resscn 10597 ax-1cn 10598 ax-icn 10599 ax-addcl 10600 ax-addrcl 10601 ax-mulcl 10602 ax-mulrcl 10603 ax-mulcom 10604 ax-addass 10605 ax-mulass 10606 ax-distr 10607 ax-i2m1 10608 ax-1ne0 10609 ax-1rid 10610 ax-rnegex 10611 ax-rrecex 10612 ax-cnre 10613 ax-pre-lttri 10614 ax-pre-lttrn 10615 ax-pre-ltadd 10616 ax-pre-mulgt0 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-nel 3127 df-ral 3146 df-rex 3147 df-reu 3148 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-riota 7117 df-ov 7162 df-oprab 7163 df-mpo 7164 df-om 7584 df-1st 7692 df-2nd 7693 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-map 8411 df-en 8513 df-dom 8514 df-sdom 8515 df-pnf 10680 df-mnf 10681 df-xr 10682 df-ltxr 10683 df-le 10684 df-sub 10875 df-neg 10876 df-nn 11642 df-n0 11901 df-z 11985 df-uz 12247 df-fz 12896 df-fzo 13037

This theorem is referenced by: fourierdlem37 42436 fourierdlem54 42452 fourierdlem63 42461 fourierdlem64 42462 fourierdlem65 42463 fourierdlem69 42467 fourierdlem79 42477 fourierdlem89 42487 fourierdlem90 42488 fourierdlem91 42489 fourierdlem107 42505 fourierdlem109 42507

W3C validator