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 46184

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 7439	. . . . . . . . 9 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
5	4	oveq1d 7446	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
6	5	fveq2d 6910	. . . . . . 7 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
7	6	oveq1d 7446	. . . . . 6 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
8	3, 7	oveq12d 7449	. . . . 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 46175	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
22	21	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
23	22	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
24	22	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
25	17	fourierdlem2 46124	. . . . . . . . 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 8889	. . . . . 6 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
30	28, 29	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
31		fourierdlem63.j	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
32		fzofzp1 13803	. . . . . 6 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
34	30, 33	ffvelcdmd 7105	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
35	11, 12, 13	fourierdlem11 46133	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
36	35	simp2d 1144	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℝ)
37	36, 34	resubcld 11691	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
38	35	simp1d 1143	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	36, 38	resubcld 11691	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
40	10, 39	eqeltrid 2845	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℝ)
41	35	simp3d 1145	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
42	38, 36	posdifd 11850	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
43	41, 42	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
44	43, 10	breqtrrdi 5185	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑇)
45	44	gt0ne0d 11827	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ≠ 0)
46	37, 40, 45	redivcld 12095	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
47	46	flcld 13838	. . . . . . 7 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
48	47	zred 12722	. . . . . 6 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
49	48, 40	remulcld 11291	. . . . 5 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
50	34, 49	readdcld 11290	. . . 4 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
51	2, 9, 34, 50	fvmptd 7023	. . 3 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
52	51, 50	eqeltrd 2841	. 2 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
53	11	fourierdlem2 46124	. . . . . . 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 8889	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
58	56, 57	syl 17	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
59		fourierdlem63.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (0...𝑀))
60	58, 59	ffvelcdmd 7105	. 2 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℝ)
61	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
62	15	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
63	38	rexrd 11311	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
64		iocssre 13467	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
65	63, 36, 64	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
66	38, 36, 41, 10, 1	fourierdlem4 46126	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
67		fourierdlem63.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))))
68		elfzofz 13715	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
69	31, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
70	30, 69	ffvelcdmd 7105	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
71	34	rexrd 11311	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
72		elico2 13451	. . . . . . . . . . . . . . 15 ⊢ (((𝑆‘𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))))
73	70, 71, 72	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))))
74	67, 73	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))
75	74	simp1d 1143	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ ℝ)
76	66, 75	ffvelcdmd 7105	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑌) ∈ (𝐴(,]𝐵))
77	65, 76	sseldd 3984	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℝ)
78	77, 75	resubcld 11691	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℝ)
79	60, 78	resubcld 11691	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
80	79	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
81		icossicc 13476	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1)))
82	14	rexrd 11311	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
83	15	rexrd 11311	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
84	17, 24, 23	fourierdlem15 46137	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
85	82, 83, 84, 31	fourierdlem8 46130	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
86	81, 85	sstrid 3995	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
87	86, 67	sseldd 3984	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝐶[,]𝐷))
88		elicc2 13452	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
89	14, 15, 88	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
90	87, 89	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))
91	90	simp2d 1144	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≤ 𝑌)
92	60, 77	resubcld 11691	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ)
93		fourierdlem63.eyltqk	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾))
94	77, 60	posdifd 11850	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘𝑌) < (𝑄‘𝐾) ↔ 0 < ((𝑄‘𝐾) − (𝐸‘𝑌))))
95	93, 94	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((𝑄‘𝐾) − (𝐸‘𝑌)))
96	92, 95	elrpd 13074	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ⁺)
97	75, 96	ltaddrpd 13110	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 < (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
98	60	recnd 11289	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℂ)
99	77	recnd 11289	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℂ)
100	75	recnd 11289	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ ℂ)
101	98, 99, 100	subsub3d 11650	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) = (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)))
102	98, 100	addcomd 11463	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) + 𝑌) = (𝑌 + (𝑄‘𝐾)))
103	102	oveq1d 7446	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)) = ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)))
104	100, 98, 99	addsubassd 11640	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)) = (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
105	101, 103, 104	3eqtrrd 2782	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))) = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
106	97, 105	breqtrd 5169	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
107	14, 75, 79, 91, 106	lelttrd 11419	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
108	14, 79, 107	ltled 11409	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
109	108	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
110	34	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
111	60	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℝ)
112	52, 34	resubcld 11691	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113	112	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114	111, 113	resubcld 11691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
115	74	simp3d 1145	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 < (𝑆‘(𝐽 + 1)))
116	75, 34, 115	ltled 11409	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ≤ (𝑆‘(𝐽 + 1)))
117	38, 36, 41, 10, 1, 75, 34, 116	fourierdlem7 46129	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸‘𝑌) − 𝑌))
118	112, 78, 60, 117	lesub2dd 11880	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119	118	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
120	98	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℂ)
121	52	recnd 11289	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122	121	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123	110	recnd 11289	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124	120, 122, 123	subsubd 11648	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
125	98, 121	subcld 11620	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
126	34	recnd 11289	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127	125, 126	addcomd 11463	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128	127	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129	124, 128	eqtrd 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
131	52	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132	111, 131	sublt0d 11889	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133	130, 132	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134	111, 131	resubcld 11691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135		ltaddneg 11477	. . . . . . . . . . . . 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 5165	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
139	80, 114, 110, 119, 138	lelttrd 11419	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
140	84, 33	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141		elicc2 13452	. . . . . . . . . . . . 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 1145	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145	144	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
146	80, 110, 62, 139, 145	ltletrd 11421	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < 𝐷)
147	80, 62, 146	ltled 11409	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ 𝐷)
148	61, 62, 80, 109, 147	eliccd 45517	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
150		oveq2 7439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐵 − 𝑥) = (𝐵 − 𝑌))
151	150	oveq1d 7446	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑌) / 𝑇))
152	151	fveq2d 6910	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
153	152	oveq1d 7446	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
154	149, 153	oveq12d 7449	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
155	154	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
156	36, 75	resubcld 11691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ)
157	156, 40, 45	redivcld 12095	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 − 𝑌) / 𝑇) ∈ ℝ)
158	157	flcld 13838	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℤ)
159	158	zred 12722	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℝ)
160	159, 40	remulcld 11291	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
161	75, 160	readdcld 11290	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
162	2, 155, 75, 161	fvmptd 7023	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑌) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
163	162	oveq1d 7446	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164	163	oveq1d 7446	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165	160	recnd 11289	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166	100, 165	pncan2d 11622	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
167	166	oveq1d 7446	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇))
168	159	recnd 11289	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℂ)
169	40	recnd 11289	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℂ)
170	168, 169, 45	divcan4d 12049	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
171	164, 167, 170	3eqtrd 2781	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
172	171, 158	eqeltrd 2841	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ)
173	78	recnd 11289	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℂ)
174	173, 169, 45	divcan1d 12044	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸‘𝑌) − 𝑌))
175	174	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)))
176	98, 173	npcand 11624	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)) = (𝑄‘𝐾))
177	175, 176	eqtrd 2777	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄‘𝐾))
178		ffun 6739	. . . . . . . . . . 11 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
179	58, 178	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑄)
180	58	fdmd 6746	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
181	59, 180	eleqtrrd 2844	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ dom 𝑄)
182		fvelrn 7096	. . . . . . . . . 10 ⊢ ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) → (𝑄‘𝐾) ∈ ran 𝑄)
183	179, 181, 182	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ran 𝑄)
184	177, 183	eqeltrd 2841	. . . . . . . 8 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185		oveq1 7438	. . . . . . . . . . 11 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇))
186	185	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)))
187	186	eleq1d 2826	. . . . . . . . 9 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → ((((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188	187	rspcev 3622	. . . . . . . 8 ⊢ (((((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189	172, 184, 188	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190	189	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191		oveq1 7438	. . . . . . . . 9 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192	191	eleq1d 2826	. . . . . . . 8 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193	192	rexbidv 3179	. . . . . . 7 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194	193	elrab 3692	. . . . . 6 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195	148, 190, 194	sylanbrc 583	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196		elun2 4183	. . . . 5 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197	195, 196	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198		fourierdlem63.x	. . . 4 ⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))
199	197, 198, 18	3eltr4g 2858	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 ∈ 𝐻)
200		elfzelz 13564	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201	200	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202		elfzoelz 13699	. . . . . . . . . . 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 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑗 ∈ (0...𝑁))
210		isorel 7346	. . . . . . . . . . . 12 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
211	207, 208, 209, 210	syl12anc 837	. . . . . . . . . . 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 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁))
217	33	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁))
218		isorel 7346	. . . . . . . . . . . 12 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
219	215, 216, 217, 218	syl12anc 837	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
220	214, 219	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1))
221	220	adantrl 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1))
222		btwnnz 12694	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
223	204, 213, 221, 222	syl3anc 1373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ)
224	201, 223	pm2.65da 817	. . . . . . 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 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘𝑗) ∈ ℝ)
229	228	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) ∈ ℝ)
230	74	simp2d 1144	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐽) ≤ 𝑌)
231	230	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ≤ 𝑌)
232	106, 198	breqtrrdi 5185	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 < 𝑋)
233	232	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < 𝑋)
234		eqcom 2744	. . . . . . . . . . . . 13 ⊢ (𝑋 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝑋)
235	234	biimpri 228	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗) = 𝑋 → 𝑋 = (𝑆‘𝑗))
236	235	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 = (𝑆‘𝑗))
237	233, 236	breqtrd 5169	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
238	237	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
239	226, 227, 229, 231, 238	lelttrd 11419	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
240	239	adantllr 719	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
241		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) = 𝑋)
242	198, 139	eqbrtrid 5178	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243	242	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244	241, 243	eqbrtrd 5165	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	244	adantlr 715	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
246	240, 245	jca 511	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
247	225, 246	mtand 816	. . . . 5 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆‘𝑗) = 𝑋)
248	247	nrexdv 3149	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
249		isof1o 7343	. . . . . . . . 9 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto→𝐻)
250	206, 249	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
251		f1ofo 6855	. . . . . . . 8 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)–onto→𝐻)
252	250, 251	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻)
253		foelrn 7127	. . . . . . 7 ⊢ ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
254	252, 253	sylan 580	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
255	234	rexbii 3094	. . . . . 6 ⊢ (∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
256	254, 255	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
257	256	adantlr 715	. . . 4 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
258	248, 257	mtand 816	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋 ∈ 𝐻)
259	199, 258	pm2.65da 817	. 2 ⊢ (𝜑 → ¬ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
260	52, 60, 259	nltled 11411	1 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 {crab 3436 ∪ cun 3949 ⊆ wss 3951 {cpr 4628 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ran crn 5686 ℩cio 6512 Fun wfun 6555 ⟶wf 6557 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 Isom wiso 6562 (class class class)co 7431 ↑_m cmap 8866 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 / cdiv 11920 ℕcn 12266 ℤcz 12613 (,]cioc 13388 [,)cico 13389 [,]cicc 13390 ...cfz 13547 ..^cfzo 13694 ⌊cfl 13830 ♯chash 14369

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 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-er 8745 df-map 8868 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-ioc 13392 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-rest 17467 df-topgen 17488 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-top 22900 df-topon 22917 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-cmp 23395

This theorem is referenced by: fourierdlem79 46200

W3C validator