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 46198

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 7413	. . . . . . . . 9 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
5	4	oveq1d 7420	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
6	5	fveq2d 6880	. . . . . . 7 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
7	6	oveq1d 7420	. . . . . 6 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
8	3, 7	oveq12d 7423	. . . . 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 46189	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
22	21	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
23	22	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
24	22	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
25	17	fourierdlem2 46138	. . . . . . . . 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 8863	. . . . . 6 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
30	28, 29	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
31		fourierdlem63.j	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
32		fzofzp1 13780	. . . . . 6 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
34	30, 33	ffvelcdmd 7075	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
35	11, 12, 13	fourierdlem11 46147	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
36	35	simp2d 1143	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℝ)
37	36, 34	resubcld 11665	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
38	35	simp1d 1142	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	36, 38	resubcld 11665	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
40	10, 39	eqeltrid 2838	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℝ)
41	35	simp3d 1144	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
42	38, 36	posdifd 11824	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
43	41, 42	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
44	43, 10	breqtrrdi 5161	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑇)
45	44	gt0ne0d 11801	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ≠ 0)
46	37, 40, 45	redivcld 12069	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
47	46	flcld 13815	. . . . . . 7 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
48	47	zred 12697	. . . . . 6 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
49	48, 40	remulcld 11265	. . . . 5 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
50	34, 49	readdcld 11264	. . . 4 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
51	2, 9, 34, 50	fvmptd 6993	. . 3 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
52	51, 50	eqeltrd 2834	. 2 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
53	11	fourierdlem2 46138	. . . . . . 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 8863	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
58	56, 57	syl 17	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
59		fourierdlem63.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (0...𝑀))
60	58, 59	ffvelcdmd 7075	. 2 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℝ)
61	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
62	15	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
63	38	rexrd 11285	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
64		iocssre 13444	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
65	63, 36, 64	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
66	38, 36, 41, 10, 1	fourierdlem4 46140	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
67		fourierdlem63.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))))
68		elfzofz 13692	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
69	31, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
70	30, 69	ffvelcdmd 7075	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
71	34	rexrd 11285	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
72		elico2 13427	. . . . . . . . . . . . . . 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 7075	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑌) ∈ (𝐴(,]𝐵))
77	65, 76	sseldd 3959	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℝ)
78	77, 75	resubcld 11665	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℝ)
79	60, 78	resubcld 11665	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
80	79	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
81		icossicc 13453	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1)))
82	14	rexrd 11285	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
83	15	rexrd 11285	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
84	17, 24, 23	fourierdlem15 46151	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
85	82, 83, 84, 31	fourierdlem8 46144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
86	81, 85	sstrid 3970	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
87	86, 67	sseldd 3959	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝐶[,]𝐷))
88		elicc2 13428	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
89	14, 15, 88	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
90	87, 89	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))
91	90	simp2d 1143	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≤ 𝑌)
92	60, 77	resubcld 11665	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ)
93		fourierdlem63.eyltqk	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾))
94	77, 60	posdifd 11824	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘𝑌) < (𝑄‘𝐾) ↔ 0 < ((𝑄‘𝐾) − (𝐸‘𝑌))))
95	93, 94	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((𝑄‘𝐾) − (𝐸‘𝑌)))
96	92, 95	elrpd 13048	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ⁺)
97	75, 96	ltaddrpd 13084	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 < (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
98	60	recnd 11263	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℂ)
99	77	recnd 11263	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℂ)
100	75	recnd 11263	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ ℂ)
101	98, 99, 100	subsub3d 11624	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) = (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)))
102	98, 100	addcomd 11437	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) + 𝑌) = (𝑌 + (𝑄‘𝐾)))
103	102	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)) = ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)))
104	100, 98, 99	addsubassd 11614	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)) = (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
105	101, 103, 104	3eqtrrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))) = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
106	97, 105	breqtrd 5145	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
107	14, 75, 79, 91, 106	lelttrd 11393	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
108	14, 79, 107	ltled 11383	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
109	108	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
110	34	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
111	60	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℝ)
112	52, 34	resubcld 11665	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113	112	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114	111, 113	resubcld 11665	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
115	74	simp3d 1144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 < (𝑆‘(𝐽 + 1)))
116	75, 34, 115	ltled 11383	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ≤ (𝑆‘(𝐽 + 1)))
117	38, 36, 41, 10, 1, 75, 34, 116	fourierdlem7 46143	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸‘𝑌) − 𝑌))
118	112, 78, 60, 117	lesub2dd 11854	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119	118	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
120	98	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℂ)
121	52	recnd 11263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122	121	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123	110	recnd 11263	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124	120, 122, 123	subsubd 11622	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
125	98, 121	subcld 11594	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
126	34	recnd 11263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127	125, 126	addcomd 11437	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128	127	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129	124, 128	eqtrd 2770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
131	52	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132	111, 131	sublt0d 11863	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133	130, 132	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134	111, 131	resubcld 11665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135		ltaddneg 11451	. . . . . . . . . . . . 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 5141	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
139	80, 114, 110, 119, 138	lelttrd 11393	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
140	84, 33	ffvelcdmd 7075	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141		elicc2 13428	. . . . . . . . . . . . 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 11395	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < 𝐷)
147	80, 62, 146	ltled 11383	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ 𝐷)
148	61, 62, 80, 109, 147	eliccd 45533	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
150		oveq2 7413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐵 − 𝑥) = (𝐵 − 𝑌))
151	150	oveq1d 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑌) / 𝑇))
152	151	fveq2d 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
153	152	oveq1d 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
154	149, 153	oveq12d 7423	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
155	154	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
156	36, 75	resubcld 11665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ)
157	156, 40, 45	redivcld 12069	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 − 𝑌) / 𝑇) ∈ ℝ)
158	157	flcld 13815	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℤ)
159	158	zred 12697	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℝ)
160	159, 40	remulcld 11265	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
161	75, 160	readdcld 11264	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
162	2, 155, 75, 161	fvmptd 6993	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑌) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
163	162	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164	163	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165	160	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166	100, 165	pncan2d 11596	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
167	166	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇))
168	159	recnd 11263	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℂ)
169	40	recnd 11263	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℂ)
170	168, 169, 45	divcan4d 12023	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
171	164, 167, 170	3eqtrd 2774	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
172	171, 158	eqeltrd 2834	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ)
173	78	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℂ)
174	173, 169, 45	divcan1d 12018	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸‘𝑌) − 𝑌))
175	174	oveq2d 7421	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)))
176	98, 173	npcand 11598	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)) = (𝑄‘𝐾))
177	175, 176	eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄‘𝐾))
178		ffun 6709	. . . . . . . . . . 11 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
179	58, 178	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑄)
180	58	fdmd 6716	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
181	59, 180	eleqtrrd 2837	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ dom 𝑄)
182		fvelrn 7066	. . . . . . . . . 10 ⊢ ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) → (𝑄‘𝐾) ∈ ran 𝑄)
183	179, 181, 182	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ran 𝑄)
184	177, 183	eqeltrd 2834	. . . . . . . 8 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185		oveq1 7412	. . . . . . . . . . 11 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇))
186	185	oveq2d 7421	. . . . . . . . . 10 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)))
187	186	eleq1d 2819	. . . . . . . . 9 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → ((((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188	187	rspcev 3601	. . . . . . . 8 ⊢ (((((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189	172, 184, 188	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190	189	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191		oveq1 7412	. . . . . . . . 9 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192	191	eleq1d 2819	. . . . . . . 8 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193	192	rexbidv 3164	. . . . . . 7 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194	193	elrab 3671	. . . . . 6 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195	148, 190, 194	sylanbrc 583	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196		elun2 4158	. . . . 5 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197	195, 196	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198		fourierdlem63.x	. . . 4 ⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))
199	197, 198, 18	3eltr4g 2851	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 ∈ 𝐻)
200		elfzelz 13541	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201	200	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202		elfzoelz 13676	. . . . . . . . . . 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 7319	. . . . . . . . . . . 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 7319	. . . . . . . . . . . 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 12669	. . . . . . . . 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 7074	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘𝑗) ∈ ℝ)
229	228	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) ∈ ℝ)
230	74	simp2d 1143	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐽) ≤ 𝑌)
231	230	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ≤ 𝑌)
232	106, 198	breqtrrdi 5161	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 < 𝑋)
233	232	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < 𝑋)
234		eqcom 2742	. . . . . . . . . . . . 13 ⊢ (𝑋 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝑋)
235	234	biimpri 228	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗) = 𝑋 → 𝑋 = (𝑆‘𝑗))
236	235	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 = (𝑆‘𝑗))
237	233, 236	breqtrd 5145	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
238	237	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
239	226, 227, 229, 231, 238	lelttrd 11393	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
240	239	adantllr 719	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
241		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) = 𝑋)
242	198, 139	eqbrtrid 5154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243	242	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244	241, 243	eqbrtrd 5141	. . . . . . . 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 3135	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
249		isof1o 7316	. . . . . . . . 9 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto→𝐻)
250	206, 249	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
251		f1ofo 6825	. . . . . . . 8 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)–onto→𝐻)
252	250, 251	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻)
253		foelrn 7097	. . . . . . 7 ⊢ ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
254	252, 253	sylan 580	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
255	234	rexbii 3083	. . . . . 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 11385	1 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∀wral 3051 ∃wrex 3060 {crab 3415 ∪ cun 3924 ⊆ wss 3926 {cpr 4603 class class class wbr 5119 ↦ cmpt 5201 dom cdm 5654 ran crn 5655 ℩cio 6482 Fun wfun 6525 ⟶wf 6527 –onto→wfo 6529 –1-1-onto→wf1o 6530 ‘cfv 6531 Isom wiso 6532 (class class class)co 7405 ↑_m cmap 8840 ℂcc 11127 ℝcr 11128 0cc0 11129 1c1 11130 + caddc 11132 · cmul 11134 ℝ^*cxr 11268 < clt 11269 ≤ cle 11270 − cmin 11466 / cdiv 11894 ℕcn 12240 ℤcz 12588 (,]cioc 13363 [,)cico 13364 [,]cicc 13365 ...cfz 13524 ..^cfzo 13671 ⌊cfl 13807 ♯chash 14348

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-inf2 9655 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207

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 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-oadd 8484 df-er 8719 df-map 8842 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-fi 9423 df-sup 9454 df-inf 9455 df-oi 9524 df-dju 9915 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-3 12304 df-n0 12502 df-xnn0 12575 df-z 12589 df-uz 12853 df-q 12965 df-rp 13009 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ioo 13366 df-ioc 13367 df-ico 13368 df-icc 13369 df-fz 13525 df-fzo 13672 df-fl 13809 df-seq 14020 df-exp 14080 df-hash 14349 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-rest 17436 df-topgen 17457 df-psmet 21307 df-xmet 21308 df-met 21309 df-bl 21310 df-mopn 21311 df-top 22832 df-topon 22849 df-bases 22884 df-cld 22957 df-ntr 22958 df-cls 22959 df-nei 23036 df-lp 23074 df-cmp 23325

This theorem is referenced by: fourierdlem79 46214

W3C validator