fourierdlem63 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem63 46167

Description: The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem63.t	⊢ 𝑇 = (𝐵 − 𝐴)
fourierdlem63.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem63.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem63.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem63.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem63.d	⊢ (𝜑 → 𝐷 ∈ ℝ)
fourierdlem63.cltd	⊢ (𝜑 → 𝐶 < 𝐷)
fourierdlem63.o	⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem63.h	⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem63.n	⊢ 𝑁 = ((♯‘𝐻) − 1)
fourierdlem63.s	⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem63.e	⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
fourierdlem63.k	⊢ (𝜑 → 𝐾 ∈ (0...𝑀))
fourierdlem63.j	⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
fourierdlem63.y	⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))))
fourierdlem63.eyltqk	⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾))
fourierdlem63.x	⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))

**Assertion**
Ref	Expression
fourierdlem63	⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾))

Distinct variable groups: 𝐴,𝑖,𝑚,𝑝 𝑥,𝐴,𝑖 𝐵,𝑖,𝑚,𝑝 𝑥,𝐵 𝐶,𝑖,𝑚,𝑝 𝑥,𝐶 𝐷,𝑖,𝑚,𝑝 𝑥,𝐷 𝑘,𝐸,𝑥 𝑓,𝐻 𝑥,𝐻 𝑘,𝐽,𝑥 𝑘,𝐾,𝑥 𝑖,𝑀,𝑚,𝑝 𝑓,𝑁 𝑖,𝑁,𝑚,𝑝 𝑥,𝑁 𝑄,𝑖,𝑘,𝑥 𝑄,𝑝 𝑆,𝑓 𝑆,𝑖,𝑘,𝑥 𝑆,𝑝 𝑇,𝑖,𝑘,𝑥 𝑘,𝑌,𝑥 𝜑,𝑓 𝜑,𝑖,𝑘,𝑥 Allowed substitution hints: 𝜑(𝑚,𝑝) 𝐴(𝑓,𝑘) 𝐵(𝑓,𝑘) 𝐶(𝑓,𝑘) 𝐷(𝑓,𝑘) 𝑃(𝑥,𝑓,𝑖,𝑘,𝑚,𝑝) 𝑄(𝑓,𝑚) 𝑆(𝑚) 𝑇(𝑓,𝑚,𝑝) 𝐸(𝑓,𝑖,𝑚,𝑝) 𝐻(𝑖,𝑘,𝑚,𝑝) 𝐽(𝑓,𝑖,𝑚,𝑝) 𝐾(𝑓,𝑖,𝑚,𝑝) 𝑀(𝑥,𝑓,𝑘) 𝑁(𝑘) 𝑂(𝑥,𝑓,𝑖,𝑘,𝑚,𝑝) 𝑋(𝑥,𝑓,𝑖,𝑘,𝑚,𝑝) 𝑌(𝑓,𝑖,𝑚,𝑝)

Proof of Theorem fourierdlem63 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem63.e	. . . . 5 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
2	1	a1i 11	. . . 4 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
3		id 22	. . . . . 6 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1)))
4		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
5	4	oveq1d 7402	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
6	5	fveq2d 6862	. . . . . . 7 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
7	6	oveq1d 7402	. . . . . 6 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
8	3, 7	oveq12d 7405	. . . . 5 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
9	8	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = (𝑆‘(𝐽 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
10		fourierdlem63.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝐵 − 𝐴)
11		fourierdlem63.p	. . . . . . . . . . 11 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
12		fourierdlem63.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
13		fourierdlem63.q	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
14		fourierdlem63.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℝ)
15		fourierdlem63.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
16		fourierdlem63.cltd	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 < 𝐷)
17		fourierdlem63.o	. . . . . . . . . . 11 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
18		fourierdlem63.h	. . . . . . . . . . 11 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
19		fourierdlem63.n	. . . . . . . . . . 11 ⊢ 𝑁 = ((♯‘𝐻) − 1)
20		fourierdlem63.s	. . . . . . . . . . 11 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
21	10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20	fourierdlem54 46158	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
22	21	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
23	22	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
24	22	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
25	17	fourierdlem2 46107	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
26	24, 25	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
27	23, 26	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
28	27	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
29		elmapi 8822	. . . . . 6 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
30	28, 29	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
31		fourierdlem63.j	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
32		fzofzp1 13725	. . . . . 6 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
34	30, 33	ffvelcdmd 7057	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
35	11, 12, 13	fourierdlem11 46116	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
36	35	simp2d 1143	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℝ)
37	36, 34	resubcld 11606	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
38	35	simp1d 1142	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	36, 38	resubcld 11606	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
40	10, 39	eqeltrid 2832	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℝ)
41	35	simp3d 1144	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
42	38, 36	posdifd 11765	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
43	41, 42	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
44	43, 10	breqtrrdi 5149	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑇)
45	44	gt0ne0d 11742	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ≠ 0)
46	37, 40, 45	redivcld 12010	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
47	46	flcld 13760	. . . . . . 7 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
48	47	zred 12638	. . . . . 6 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
49	48, 40	remulcld 11204	. . . . 5 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
50	34, 49	readdcld 11203	. . . 4 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
51	2, 9, 34, 50	fvmptd 6975	. . 3 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
52	51, 50	eqeltrd 2828	. 2 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
53	11	fourierdlem2 46107	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
54	12, 53	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
55	13, 54	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
56	55	simpld 494	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
57		elmapi 8822	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
58	56, 57	syl 17	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
59		fourierdlem63.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (0...𝑀))
60	58, 59	ffvelcdmd 7057	. 2 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℝ)
61	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
62	15	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
63	38	rexrd 11224	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
64		iocssre 13388	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
65	63, 36, 64	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
66	38, 36, 41, 10, 1	fourierdlem4 46109	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
67		fourierdlem63.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))))
68		elfzofz 13636	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
69	31, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
70	30, 69	ffvelcdmd 7057	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
71	34	rexrd 11224	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
72		elico2 13371	. . . . . . . . . . . . . . 15 ⊢ (((𝑆‘𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))))
73	70, 71, 72	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))))
74	67, 73	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))
75	74	simp1d 1142	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ ℝ)
76	66, 75	ffvelcdmd 7057	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑌) ∈ (𝐴(,]𝐵))
77	65, 76	sseldd 3947	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℝ)
78	77, 75	resubcld 11606	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℝ)
79	60, 78	resubcld 11606	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
80	79	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
81		icossicc 13397	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1)))
82	14	rexrd 11224	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
83	15	rexrd 11224	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
84	17, 24, 23	fourierdlem15 46120	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
85	82, 83, 84, 31	fourierdlem8 46113	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
86	81, 85	sstrid 3958	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
87	86, 67	sseldd 3947	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝐶[,]𝐷))
88		elicc2 13372	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
89	14, 15, 88	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
90	87, 89	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))
91	90	simp2d 1143	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≤ 𝑌)
92	60, 77	resubcld 11606	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ)
93		fourierdlem63.eyltqk	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾))
94	77, 60	posdifd 11765	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘𝑌) < (𝑄‘𝐾) ↔ 0 < ((𝑄‘𝐾) − (𝐸‘𝑌))))
95	93, 94	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((𝑄‘𝐾) − (𝐸‘𝑌)))
96	92, 95	elrpd 12992	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ⁺)
97	75, 96	ltaddrpd 13028	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 < (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
98	60	recnd 11202	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℂ)
99	77	recnd 11202	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℂ)
100	75	recnd 11202	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ ℂ)
101	98, 99, 100	subsub3d 11563	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) = (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)))
102	98, 100	addcomd 11376	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) + 𝑌) = (𝑌 + (𝑄‘𝐾)))
103	102	oveq1d 7402	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)) = ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)))
104	100, 98, 99	addsubassd 11553	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)) = (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
105	101, 103, 104	3eqtrrd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))) = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
106	97, 105	breqtrd 5133	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
107	14, 75, 79, 91, 106	lelttrd 11332	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
108	14, 79, 107	ltled 11322	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
109	108	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
110	34	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
111	60	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℝ)
112	52, 34	resubcld 11606	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113	112	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114	111, 113	resubcld 11606	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
115	74	simp3d 1144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 < (𝑆‘(𝐽 + 1)))
116	75, 34, 115	ltled 11322	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ≤ (𝑆‘(𝐽 + 1)))
117	38, 36, 41, 10, 1, 75, 34, 116	fourierdlem7 46112	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸‘𝑌) − 𝑌))
118	112, 78, 60, 117	lesub2dd 11795	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119	118	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
120	98	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℂ)
121	52	recnd 11202	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122	121	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123	110	recnd 11202	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124	120, 122, 123	subsubd 11561	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
125	98, 121	subcld 11533	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
126	34	recnd 11202	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127	125, 126	addcomd 11376	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128	127	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129	124, 128	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
131	52	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132	111, 131	sublt0d 11804	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133	130, 132	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134	111, 131	resubcld 11606	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135		ltaddneg 11390	. . . . . . . . . . . . 13 ⊢ ((((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
136	134, 110, 135	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
137	133, 136	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))
138	129, 137	eqbrtrd 5129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
139	80, 114, 110, 119, 138	lelttrd 11332	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
140	84, 33	ffvelcdmd 7057	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141		elicc2 13372	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
142	14, 15, 141	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
143	140, 142	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))
144	143	simp3d 1144	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145	144	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
146	80, 110, 62, 139, 145	ltletrd 11334	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < 𝐷)
147	80, 62, 146	ltled 11322	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ 𝐷)
148	61, 62, 80, 109, 147	eliccd 45502	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
150		oveq2 7395	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐵 − 𝑥) = (𝐵 − 𝑌))
151	150	oveq1d 7402	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑌) / 𝑇))
152	151	fveq2d 6862	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
153	152	oveq1d 7402	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
154	149, 153	oveq12d 7405	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
155	154	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
156	36, 75	resubcld 11606	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ)
157	156, 40, 45	redivcld 12010	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 − 𝑌) / 𝑇) ∈ ℝ)
158	157	flcld 13760	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℤ)
159	158	zred 12638	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℝ)
160	159, 40	remulcld 11204	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
161	75, 160	readdcld 11203	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
162	2, 155, 75, 161	fvmptd 6975	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑌) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
163	162	oveq1d 7402	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164	163	oveq1d 7402	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165	160	recnd 11202	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166	100, 165	pncan2d 11535	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
167	166	oveq1d 7402	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇))
168	159	recnd 11202	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℂ)
169	40	recnd 11202	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℂ)
170	168, 169, 45	divcan4d 11964	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
171	164, 167, 170	3eqtrd 2768	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
172	171, 158	eqeltrd 2828	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ)
173	78	recnd 11202	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℂ)
174	173, 169, 45	divcan1d 11959	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸‘𝑌) − 𝑌))
175	174	oveq2d 7403	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)))
176	98, 173	npcand 11537	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)) = (𝑄‘𝐾))
177	175, 176	eqtrd 2764	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄‘𝐾))
178		ffun 6691	. . . . . . . . . . 11 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
179	58, 178	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑄)
180	58	fdmd 6698	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
181	59, 180	eleqtrrd 2831	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ dom 𝑄)
182		fvelrn 7048	. . . . . . . . . 10 ⊢ ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) → (𝑄‘𝐾) ∈ ran 𝑄)
183	179, 181, 182	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ran 𝑄)
184	177, 183	eqeltrd 2828	. . . . . . . 8 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185		oveq1 7394	. . . . . . . . . . 11 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇))
186	185	oveq2d 7403	. . . . . . . . . 10 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)))
187	186	eleq1d 2813	. . . . . . . . 9 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → ((((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188	187	rspcev 3588	. . . . . . . 8 ⊢ (((((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189	172, 184, 188	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190	189	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191		oveq1 7394	. . . . . . . . 9 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192	191	eleq1d 2813	. . . . . . . 8 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193	192	rexbidv 3157	. . . . . . 7 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194	193	elrab 3659	. . . . . 6 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195	148, 190, 194	sylanbrc 583	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196		elun2 4146	. . . . 5 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197	195, 196	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198		fourierdlem63.x	. . . 4 ⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))
199	197, 198, 18	3eltr4g 2845	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 ∈ 𝐻)
200		elfzelz 13485	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201	200	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202		elfzoelz 13620	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
203	31, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℤ)
204	203	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ)
205		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
206	21	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
207	206	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
208	69	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 ∈ (0...𝑁))
209		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑗 ∈ (0...𝑁))
210		isorel 7301	. . . . . . . . . . . 12 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
211	207, 208, 209, 210	syl12anc 836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
212	205, 211	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 < 𝑗)
213	212	adantrr 717	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗)
214		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
215	206	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
216		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁))
217	33	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁))
218		isorel 7301	. . . . . . . . . . . 12 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
219	215, 216, 217, 218	syl12anc 836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
220	214, 219	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1))
221	220	adantrl 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1))
222		btwnnz 12610	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
223	204, 213, 221, 222	syl3anc 1373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ)
224	201, 223	pm2.65da 816	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
225	224	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
226	70	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ∈ ℝ)
227	75	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 ∈ ℝ)
228	30	ffvelcdmda 7056	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘𝑗) ∈ ℝ)
229	228	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) ∈ ℝ)
230	74	simp2d 1143	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐽) ≤ 𝑌)
231	230	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ≤ 𝑌)
232	106, 198	breqtrrdi 5149	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 < 𝑋)
233	232	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < 𝑋)
234		eqcom 2736	. . . . . . . . . . . . 13 ⊢ (𝑋 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝑋)
235	234	biimpri 228	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗) = 𝑋 → 𝑋 = (𝑆‘𝑗))
236	235	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 = (𝑆‘𝑗))
237	233, 236	breqtrd 5133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
238	237	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
239	226, 227, 229, 231, 238	lelttrd 11332	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
240	239	adantllr 719	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
241		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) = 𝑋)
242	198, 139	eqbrtrid 5142	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243	242	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244	241, 243	eqbrtrd 5129	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	244	adantlr 715	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
246	240, 245	jca 511	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
247	225, 246	mtand 815	. . . . 5 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆‘𝑗) = 𝑋)
248	247	nrexdv 3128	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
249		isof1o 7298	. . . . . . . . 9 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto→𝐻)
250	206, 249	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
251		f1ofo 6807	. . . . . . . 8 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)–onto→𝐻)
252	250, 251	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻)
253		foelrn 7079	. . . . . . 7 ⊢ ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
254	252, 253	sylan 580	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
255	234	rexbii 3076	. . . . . 6 ⊢ (∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
256	254, 255	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
257	256	adantlr 715	. . . 4 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
258	248, 257	mtand 815	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋 ∈ 𝐻)
259	199, 258	pm2.65da 816	. 2 ⊢ (𝜑 → ¬ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
260	52, 60, 259	nltled 11324	1 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 {crab 3405 ∪ cun 3912 ⊆ wss 3914 {cpr 4591 class class class wbr 5107 ↦ cmpt 5188 dom cdm 5638 ran crn 5639 ℩cio 6462 Fun wfun 6505 ⟶wf 6507 –onto→wfo 6509 –1-1-onto→wf1o 6510 ‘cfv 6511 Isom wiso 6512 (class class class)co 7387 ↑_m cmap 8799 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 ℝ^*cxr 11207 < clt 11208 ≤ cle 11209 − cmin 11405 / cdiv 11835 ℕcn 12186 ℤcz 12529 (,]cioc 13307 [,)cico 13308 [,]cicc 13309 ...cfz 13468 ..^cfzo 13615 ⌊cfl 13752 ♯chash 14295

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 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-oadd 8438 df-er 8671 df-map 8801 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fi 9362 df-sup 9393 df-inf 9394 df-oi 9463 df-dju 9854 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-xnn0 12516 df-z 12530 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ioo 13310 df-ioc 13311 df-ico 13312 df-icc 13313 df-fz 13469 df-fzo 13616 df-fl 13754 df-seq 13967 df-exp 14027 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-rest 17385 df-topgen 17406 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-top 22781 df-topon 22798 df-bases 22833 df-cld 22906 df-ntr 22907 df-cls 22908 df-nei 22985 df-lp 23023 df-cmp 23274

This theorem is referenced by: fourierdlem79 46183

W3C validator