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 42760

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 42751	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 235	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simprd 499	. . . . 5 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
8	7	simpld 498	. . . 4 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
9	8	simpld 498	. . 3 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
10	6	simpld 498	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
11		elmapi 8411	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
13		0red 10633	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
14	13	leidd 11195	. . . . 5 ⊢ (𝜑 → 0 ≤ 0)
15	2	nnred 11640	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
16	2	nngt0d 11674	. . . . . 6 ⊢ (𝜑 → 0 < 𝑀)
17	13, 15, 16	ltled 10777	. . . . 5 ⊢ (𝜑 → 0 ≤ 𝑀)
18		0zd 11981	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
19	2	nnzd 12074	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
20		elfz 12891	. . . . . 6 ⊢ ((0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0...𝑀) ↔ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
21	18, 18, 19, 20	syl3anc 1368	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑀) ↔ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
22	14, 17, 21	mpbir2and 712	. . . 4 ⊢ (𝜑 → 0 ∈ (0...𝑀))
23	12, 22	ffvelrnd 6829	. . 3 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
24	9, 23	eqeltrrd 2891	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
25	8	simprd 499	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
26	15	leidd 11195	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
27		elfz 12891	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ∈ (0...𝑀) ↔ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
28	19, 18, 19, 27	syl3anc 1368	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (0...𝑀) ↔ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
29	17, 26, 28	mpbir2and 712	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
30	12, 29	ffvelrnd 6829	. . 3 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
31	25, 30	eqeltrrd 2891	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
32		0le1 11152	. . . . . 6 ⊢ 0 ≤ 1
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ≤ 1)
34	2	nnge1d 11673	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
35		1zzd 12001	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
36		elfz 12891	. . . . . 6 ⊢ ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
37	35, 18, 19, 36	syl3anc 1368	. . . . 5 ⊢ (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
38	33, 34, 37	mpbir2and 712	. . . 4 ⊢ (𝜑 → 1 ∈ (0...𝑀))
39	12, 38	ffvelrnd 6829	. . 3 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
40		elfzo 13035	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 < 𝑀)))
41	18, 18, 19, 40	syl3anc 1368	. . . . . 6 ⊢ (𝜑 → (0 ∈ (0..^𝑀) ↔ (0 ≤ 0 ∧ 0 < 𝑀)))
42	14, 16, 41	mpbir2and 712	. . . . 5 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
43		0re 10632	. . . . . 6 ⊢ 0 ∈ ℝ
44		eleq1 2877	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
45	44	anbi2d 631	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
46		fveq2 6645	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
47		oveq1 7142	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
48	47	fveq2d 6649	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
49	46, 48	breq12d 5043	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
50	45, 49	imbi12d 348	. . . . . . 7 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
51	7	simprd 499	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
52	51	r19.21bi 3173	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
53	50, 52	vtoclg 3515	. . . . . 6 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
54	43, 53	ax-mp 5	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
55	42, 54	mpdan 686	. . . 4 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
56		0p1e1 11747	. . . . . 6 ⊢ (0 + 1) = 1
57	56	a1i 11	. . . . 5 ⊢ (𝜑 → (0 + 1) = 1)
58	57	fveq2d 6649	. . . 4 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
59	55, 9, 58	3brtr3d 5061	. . 3 ⊢ (𝜑 → 𝐴 < (𝑄‘1))
60		nnuz 12269	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
61	2, 60	eleqtrdi 2900	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
62	12	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
63		0red 10633	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℝ)
64		elfzelz 12902	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℤ)
65	64	zred 12075	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℝ)
66		1red 10631	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ∈ ℝ)
67		0lt1 11151	. . . . . . . . . . 11 ⊢ 0 < 1
68	67	a1i 11	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 1)
69		elfzle1 12905	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 1 ≤ 𝑖)
70	63, 66, 65, 68, 69	ltletrd 10789	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 < 𝑖)
71	63, 65, 70	ltled 10777	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 0 ≤ 𝑖)
72		elfzle2 12906	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
73		0zd 11981	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 0 ∈ ℤ)
74		elfzel2 12900	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑀) → 𝑀 ∈ ℤ)
75		elfz 12891	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
76	64, 73, 74, 75	syl3anc 1368	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑀) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
77	71, 72, 76	mpbir2and 712	. . . . . . 7 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ (0...𝑀))
78	77	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (0...𝑀))
79	62, 78	ffvelrnd 6829	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
80	12	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
81		0red 10633	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ∈ ℝ)
82		elfzelz 12902	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℤ)
83	82	zred 12075	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℝ)
84		1red 10631	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ∈ ℝ)
85	67	a1i 11	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 1)
86		elfzle1 12905	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 ≤ 𝑖)
87	81, 84, 83, 85, 86	ltletrd 10789	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 < 𝑖)
88	81, 83, 87	ltled 10777	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 0 ≤ 𝑖)
89	88	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ 𝑖)
90	83	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
91	15	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
92		peano2rem 10942	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
93	91, 92	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ)
94		elfzle2 12906	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ≤ (𝑀 − 1))
95	94	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ (𝑀 − 1))
96	91	ltm1d 11561	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑀 − 1) < 𝑀)
97	90, 93, 91, 95, 96	lelttrd 10787	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
98	90, 91, 97	ltled 10777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ≤ 𝑀)
99	82	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℤ)
100		0zd 11981	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℤ)
101	19	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
102	99, 100, 101, 75	syl3anc 1368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0...𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
103	89, 98, 102	mpbir2and 712	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0...𝑀))
104	80, 103	ffvelrnd 6829	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ∈ ℝ)
105		0red 10633	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ∈ ℝ)
106		peano2re 10802	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℝ → (𝑖 + 1) ∈ ℝ)
107	90, 106	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℝ)
108		1red 10631	. . . . . . . . . 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 11559	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 < (𝑖 + 1))
112	84, 83, 110, 86, 111	lelttrd 10787	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 1 < (𝑖 + 1))
113	112	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 1 < (𝑖 + 1))
114	105, 108, 107, 109, 113	lttrd 10790	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 < (𝑖 + 1))
115	105, 107, 114	ltled 10777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 0 ≤ (𝑖 + 1))
116	90, 93, 108, 95	leadd1dd 11243	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ ((𝑀 − 1) + 1))
117	2	nncnd 11641	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
118		1cnd 10625	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 10990	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
120	119	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
121	116, 120	breqtrd 5056	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ≤ 𝑀)
122	99	peano2zd 12078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ ℤ)
123		elfz 12891	. . . . . . . . 9 ⊢ (((𝑖 + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑖 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑀)))
124	122, 100, 101, 123	syl3anc 1368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((𝑖 + 1) ∈ (0...𝑀) ↔ (0 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑀)))
125	115, 121, 124	mpbir2and 712	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 + 1) ∈ (0...𝑀))
126	80, 125	ffvelrnd 6829	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
127		elfzo 13035	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
128	99, 100, 101, 127	syl3anc 1368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (0..^𝑀) ↔ (0 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
129	89, 97, 128	mpbir2and 712	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀))
130	129, 52	syldan 594	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
131	104, 126, 130	ltled 10777	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1)))
132	61, 79, 131	monoord 13396	. . . 4 ⊢ (𝜑 → (𝑄‘1) ≤ (𝑄‘𝑀))
133	132, 25	breqtrd 5056	. . 3 ⊢ (𝜑 → (𝑄‘1) ≤ 𝐵)
134	24, 39, 31, 59, 133	ltletrd 10789	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
135	24, 31, 134	3jca 1125	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∀wral 3106 {crab 3110 class class class wbr 5030 ↦ cmpt 5110 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 ↑_m cmap 8389 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 < clt 10664 ≤ cle 10665 − cmin 10859 ℕcn 11625 ℤcz 11969 ℤ_≥cuz 12231 ...cfz 12885 ..^cfzo 13028

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-nn 11626 df-n0 11886 df-z 11970 df-uz 12232 df-fz 12886 df-fzo 13029

This theorem is referenced by: fourierdlem37 42786 fourierdlem54 42802 fourierdlem63 42811 fourierdlem64 42812 fourierdlem65 42813 fourierdlem69 42817 fourierdlem79 42827 fourierdlem89 42837 fourierdlem90 42838 fourierdlem91 42839 fourierdlem107 42855 fourierdlem109 42857

W3C validator