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 42474

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 7164	. . . . . . . . 9 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
5	4	oveq1d 7171	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
6	5	fveq2d 6674	. . . . . . 7 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
7	6	oveq1d 7171	. . . . . 6 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
8	3, 7	oveq12d 7174	. . . . 5 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
9	8	adantl 484	. . . 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 42465	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
22	21	simpld 497	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
23	22	simprd 498	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
24	22	simpld 497	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
25	17	fourierdlem2 42414	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
26	24, 25	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
27	23, 26	mpbid 234	. . . . . . 7 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
28	27	simpld 497	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
29		elmapi 8428	. . . . . 6 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
30	28, 29	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
31		fourierdlem63.j	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
32		fzofzp1 13135	. . . . . 6 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
34	30, 33	ffvelrnd 6852	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
35	11, 12, 13	fourierdlem11 42423	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
36	35	simp2d 1139	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℝ)
37	36, 34	resubcld 11068	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
38	35	simp1d 1138	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	36, 38	resubcld 11068	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
40	10, 39	eqeltrid 2917	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℝ)
41	35	simp3d 1140	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
42	38, 36	posdifd 11227	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
43	41, 42	mpbid 234	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
44	43, 10	breqtrrdi 5108	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑇)
45	44	gt0ne0d 11204	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ≠ 0)
46	37, 40, 45	redivcld 11468	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
47	46	flcld 13169	. . . . . . 7 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
48	47	zred 12088	. . . . . 6 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
49	48, 40	remulcld 10671	. . . . 5 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
50	34, 49	readdcld 10670	. . . 4 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
51	2, 9, 34, 50	fvmptd 6775	. . 3 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
52	51, 50	eqeltrd 2913	. 2 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
53	11	fourierdlem2 42414	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
54	12, 53	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
55	13, 54	mpbid 234	. . . . 5 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
56	55	simpld 497	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
57		elmapi 8428	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
58	56, 57	syl 17	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
59		fourierdlem63.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (0...𝑀))
60	58, 59	ffvelrnd 6852	. 2 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℝ)
61	14	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
62	15	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
63	38	rexrd 10691	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
64		iocssre 12817	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
65	63, 36, 64	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
66	38, 36, 41, 10, 1	fourierdlem4 42416	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
67		fourierdlem63.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))))
68		elfzofz 13054	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
69	31, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
70	30, 69	ffvelrnd 6852	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
71	34	rexrd 10691	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
72		elico2 12801	. . . . . . . . . . . . . . 15 ⊢ (((𝑆‘𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))))
73	70, 71, 72	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))))
74	67, 73	mpbid 234	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))
75	74	simp1d 1138	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ ℝ)
76	66, 75	ffvelrnd 6852	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑌) ∈ (𝐴(,]𝐵))
77	65, 76	sseldd 3968	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℝ)
78	77, 75	resubcld 11068	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℝ)
79	60, 78	resubcld 11068	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
80	79	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
81		icossicc 12825	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1)))
82	14	rexrd 10691	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
83	15	rexrd 10691	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
84	17, 24, 23	fourierdlem15 42427	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
85	82, 83, 84, 31	fourierdlem8 42420	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
86	81, 85	sstrid 3978	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
87	86, 67	sseldd 3968	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝐶[,]𝐷))
88		elicc2 12802	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
89	14, 15, 88	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
90	87, 89	mpbid 234	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))
91	90	simp2d 1139	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≤ 𝑌)
92	60, 77	resubcld 11068	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ)
93		fourierdlem63.eyltqk	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾))
94	77, 60	posdifd 11227	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘𝑌) < (𝑄‘𝐾) ↔ 0 < ((𝑄‘𝐾) − (𝐸‘𝑌))))
95	93, 94	mpbid 234	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((𝑄‘𝐾) − (𝐸‘𝑌)))
96	92, 95	elrpd 12429	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ⁺)
97	75, 96	ltaddrpd 12465	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 < (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
98	60	recnd 10669	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℂ)
99	77	recnd 10669	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℂ)
100	75	recnd 10669	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ ℂ)
101	98, 99, 100	subsub3d 11027	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) = (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)))
102	98, 100	addcomd 10842	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) + 𝑌) = (𝑌 + (𝑄‘𝐾)))
103	102	oveq1d 7171	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)) = ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)))
104	100, 98, 99	addsubassd 11017	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)) = (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
105	101, 103, 104	3eqtrrd 2861	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))) = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
106	97, 105	breqtrd 5092	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
107	14, 75, 79, 91, 106	lelttrd 10798	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
108	14, 79, 107	ltled 10788	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
109	108	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
110	34	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
111	60	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℝ)
112	52, 34	resubcld 11068	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113	112	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114	111, 113	resubcld 11068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
115	74	simp3d 1140	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 < (𝑆‘(𝐽 + 1)))
116	75, 34, 115	ltled 10788	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ≤ (𝑆‘(𝐽 + 1)))
117	38, 36, 41, 10, 1, 75, 34, 116	fourierdlem7 42419	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸‘𝑌) − 𝑌))
118	112, 78, 60, 117	lesub2dd 11257	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119	118	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
120	98	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℂ)
121	52	recnd 10669	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122	121	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123	110	recnd 10669	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124	120, 122, 123	subsubd 11025	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
125	98, 121	subcld 10997	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
126	34	recnd 10669	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127	125, 126	addcomd 10842	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128	127	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129	124, 128	eqtrd 2856	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130		simpr 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
131	52	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132	111, 131	sublt0d 11266	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133	130, 132	mpbird 259	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134	111, 131	resubcld 11068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135		ltaddneg 10855	. . . . . . . . . . . . 13 ⊢ ((((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
136	134, 110, 135	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
137	133, 136	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))
138	129, 137	eqbrtrd 5088	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
139	80, 114, 110, 119, 138	lelttrd 10798	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
140	84, 33	ffvelrnd 6852	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141		elicc2 12802	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
142	14, 15, 141	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
143	140, 142	mpbid 234	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))
144	143	simp3d 1140	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145	144	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
146	80, 110, 62, 139, 145	ltletrd 10800	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < 𝐷)
147	80, 62, 146	ltled 10788	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ 𝐷)
148	61, 62, 80, 109, 147	eliccd 41799	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
150		oveq2 7164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐵 − 𝑥) = (𝐵 − 𝑌))
151	150	oveq1d 7171	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑌) / 𝑇))
152	151	fveq2d 6674	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
153	152	oveq1d 7171	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
154	149, 153	oveq12d 7174	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
155	154	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
156	36, 75	resubcld 11068	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ)
157	156, 40, 45	redivcld 11468	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 − 𝑌) / 𝑇) ∈ ℝ)
158	157	flcld 13169	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℤ)
159	158	zred 12088	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℝ)
160	159, 40	remulcld 10671	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
161	75, 160	readdcld 10670	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
162	2, 155, 75, 161	fvmptd 6775	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑌) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
163	162	oveq1d 7171	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164	163	oveq1d 7171	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165	160	recnd 10669	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166	100, 165	pncan2d 10999	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
167	166	oveq1d 7171	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇))
168	159	recnd 10669	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℂ)
169	40	recnd 10669	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℂ)
170	168, 169, 45	divcan4d 11422	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
171	164, 167, 170	3eqtrd 2860	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
172	171, 158	eqeltrd 2913	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ)
173	78	recnd 10669	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℂ)
174	173, 169, 45	divcan1d 11417	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸‘𝑌) − 𝑌))
175	174	oveq2d 7172	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)))
176	98, 173	npcand 11001	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)) = (𝑄‘𝐾))
177	175, 176	eqtrd 2856	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄‘𝐾))
178		ffun 6517	. . . . . . . . . . 11 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
179	58, 178	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑄)
180	58	fdmd 6523	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
181	59, 180	eleqtrrd 2916	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ dom 𝑄)
182		fvelrn 6844	. . . . . . . . . 10 ⊢ ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) → (𝑄‘𝐾) ∈ ran 𝑄)
183	179, 181, 182	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ran 𝑄)
184	177, 183	eqeltrd 2913	. . . . . . . 8 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185		oveq1 7163	. . . . . . . . . . 11 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇))
186	185	oveq2d 7172	. . . . . . . . . 10 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)))
187	186	eleq1d 2897	. . . . . . . . 9 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → ((((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188	187	rspcev 3623	. . . . . . . 8 ⊢ (((((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189	172, 184, 188	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190	189	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191		oveq1 7163	. . . . . . . . 9 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192	191	eleq1d 2897	. . . . . . . 8 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193	192	rexbidv 3297	. . . . . . 7 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194	193	elrab 3680	. . . . . 6 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195	148, 190, 194	sylanbrc 585	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196		elun2 4153	. . . . 5 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197	195, 196	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198		fourierdlem63.x	. . . 4 ⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))
199	197, 198, 18	3eltr4g 2930	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 ∈ 𝐻)
200		elfzelz 12909	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201	200	ad2antlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202		elfzoelz 13039	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
203	31, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℤ)
204	203	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ)
205		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
206	21	simprd 498	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
207	206	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
208	69	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 ∈ (0...𝑁))
209		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑗 ∈ (0...𝑁))
210		isorel 7079	. . . . . . . . . . . 12 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
211	207, 208, 209, 210	syl12anc 834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
212	205, 211	mpbird 259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 < 𝑗)
213	212	adantrr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗)
214		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
215	206	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
216		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁))
217	33	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁))
218		isorel 7079	. . . . . . . . . . . 12 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
219	215, 216, 217, 218	syl12anc 834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
220	214, 219	mpbird 259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1))
221	220	adantrl 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1))
222		btwnnz 12059	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
223	204, 213, 221, 222	syl3anc 1367	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ)
224	201, 223	pm2.65da 815	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
225	224	adantlr 713	. . . . . 6 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
226	70	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ∈ ℝ)
227	75	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 ∈ ℝ)
228	30	ffvelrnda 6851	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘𝑗) ∈ ℝ)
229	228	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) ∈ ℝ)
230	74	simp2d 1139	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐽) ≤ 𝑌)
231	230	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ≤ 𝑌)
232	106, 198	breqtrrdi 5108	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 < 𝑋)
233	232	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < 𝑋)
234		eqcom 2828	. . . . . . . . . . . . 13 ⊢ (𝑋 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝑋)
235	234	biimpri 230	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗) = 𝑋 → 𝑋 = (𝑆‘𝑗))
236	235	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 = (𝑆‘𝑗))
237	233, 236	breqtrd 5092	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
238	237	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
239	226, 227, 229, 231, 238	lelttrd 10798	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
240	239	adantllr 717	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
241		simpr 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) = 𝑋)
242	198, 139	eqbrtrid 5101	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243	242	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244	241, 243	eqbrtrd 5088	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	244	adantlr 713	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
246	240, 245	jca 514	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
247	225, 246	mtand 814	. . . . 5 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆‘𝑗) = 𝑋)
248	247	nrexdv 3270	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
249		isof1o 7076	. . . . . . . . 9 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto→𝐻)
250	206, 249	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
251		f1ofo 6622	. . . . . . . 8 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)–onto→𝐻)
252	250, 251	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻)
253		foelrn 6872	. . . . . . 7 ⊢ ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
254	252, 253	sylan 582	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
255	234	rexbii 3247	. . . . . 6 ⊢ (∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
256	254, 255	sylib 220	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
257	256	adantlr 713	. . . 4 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
258	248, 257	mtand 814	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋 ∈ 𝐻)
259	199, 258	pm2.65da 815	. 2 ⊢ (𝜑 → ¬ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
260	52, 60, 259	nltled 10790	1 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ∀wral 3138 ∃wrex 3139 {crab 3142 ∪ cun 3934 ⊆ wss 3936 {cpr 4569 class class class wbr 5066 ↦ cmpt 5146 dom cdm 5555 ran crn 5556 ℩cio 6312 Fun wfun 6349 ⟶wf 6351 –onto→wfo 6353 –1-1-onto→wf1o 6354 ‘cfv 6355 Isom wiso 6356 (class class class)co 7156 ↑_m cmap 8406 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 ℝ^*cxr 10674 < clt 10675 ≤ cle 10676 − cmin 10870 / cdiv 11297 ℕcn 11638 ℤcz 11982 (,]cioc 12740 [,)cico 12741 [,]cicc 12742 ...cfz 12893 ..^cfzo 13034 ⌊cfl 13161 ♯chash 13691

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 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-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-oadd 8106 df-er 8289 df-map 8408 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-dju 9330 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-n0 11899 df-xnn0 11969 df-z 11983 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ioc 12744 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-seq 13371 df-exp 13431 df-hash 13692 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-rest 16696 df-topgen 16717 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-top 21502 df-topon 21519 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-nei 21706 df-lp 21744 df-cmp 21995

This theorem is referenced by: fourierdlem79 42490

W3C validator