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 45551

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 7422	. . . . . . . . 9 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
5	4	oveq1d 7429	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
6	5	fveq2d 6895	. . . . . . 7 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
7	6	oveq1d 7429	. . . . . 6 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
8	3, 7	oveq12d 7432	. . . . 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 45542	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
22	21	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
23	22	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
24	22	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
25	17	fourierdlem2 45491	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
26	24, 25	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
27	23, 26	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
28	27	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
29		elmapi 8861	. . . . . 6 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
30	28, 29	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
31		fourierdlem63.j	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
32		fzofzp1 13755	. . . . . 6 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
34	30, 33	ffvelcdmd 7089	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
35	11, 12, 13	fourierdlem11 45500	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
36	35	simp2d 1141	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℝ)
37	36, 34	resubcld 11666	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
38	35	simp1d 1140	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	36, 38	resubcld 11666	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
40	10, 39	eqeltrid 2833	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℝ)
41	35	simp3d 1142	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
42	38, 36	posdifd 11825	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
43	41, 42	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
44	43, 10	breqtrrdi 5184	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑇)
45	44	gt0ne0d 11802	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ≠ 0)
46	37, 40, 45	redivcld 12066	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
47	46	flcld 13789	. . . . . . 7 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
48	47	zred 12690	. . . . . 6 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
49	48, 40	remulcld 11268	. . . . 5 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
50	34, 49	readdcld 11267	. . . 4 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
51	2, 9, 34, 50	fvmptd 7006	. . 3 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
52	51, 50	eqeltrd 2829	. 2 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
53	11	fourierdlem2 45491	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
54	12, 53	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
55	13, 54	mpbid 231	. . . . 5 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
56	55	simpld 494	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
57		elmapi 8861	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
58	56, 57	syl 17	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
59		fourierdlem63.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (0...𝑀))
60	58, 59	ffvelcdmd 7089	. 2 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℝ)
61	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
62	15	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
63	38	rexrd 11288	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
64		iocssre 13430	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
65	63, 36, 64	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
66	38, 36, 41, 10, 1	fourierdlem4 45493	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
67		fourierdlem63.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))))
68		elfzofz 13674	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
69	31, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
70	30, 69	ffvelcdmd 7089	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
71	34	rexrd 11288	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
72		elico2 13414	. . . . . . . . . . . . . . 15 ⊢ (((𝑆‘𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))))
73	70, 71, 72	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))))
74	67, 73	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))
75	74	simp1d 1140	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ ℝ)
76	66, 75	ffvelcdmd 7089	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑌) ∈ (𝐴(,]𝐵))
77	65, 76	sseldd 3979	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℝ)
78	77, 75	resubcld 11666	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℝ)
79	60, 78	resubcld 11666	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
80	79	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ)
81		icossicc 13439	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1)))
82	14	rexrd 11288	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
83	15	rexrd 11288	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
84	17, 24, 23	fourierdlem15 45504	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
85	82, 83, 84, 31	fourierdlem8 45497	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
86	81, 85	sstrid 3989	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
87	86, 67	sseldd 3979	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝐶[,]𝐷))
88		elicc2 13415	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
89	14, 15, 88	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)))
90	87, 89	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))
91	90	simp2d 1141	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≤ 𝑌)
92	60, 77	resubcld 11666	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ)
93		fourierdlem63.eyltqk	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾))
94	77, 60	posdifd 11825	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘𝑌) < (𝑄‘𝐾) ↔ 0 < ((𝑄‘𝐾) − (𝐸‘𝑌))))
95	93, 94	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((𝑄‘𝐾) − (𝐸‘𝑌)))
96	92, 95	elrpd 13039	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ⁺)
97	75, 96	ltaddrpd 13075	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 < (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
98	60	recnd 11266	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ℂ)
99	77	recnd 11266	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑌) ∈ ℂ)
100	75	recnd 11266	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ ℂ)
101	98, 99, 100	subsub3d 11625	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) = (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)))
102	98, 100	addcomd 11440	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘𝐾) + 𝑌) = (𝑌 + (𝑄‘𝐾)))
103	102	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)) = ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)))
104	100, 98, 99	addsubassd 11615	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)) = (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))))
105	101, 103, 104	3eqtrrd 2773	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))) = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
106	97, 105	breqtrd 5168	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
107	14, 75, 79, 91, 106	lelttrd 11396	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
108	14, 79, 107	ltled 11386	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
109	108	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)))
110	34	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
111	60	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℝ)
112	52, 34	resubcld 11666	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113	112	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114	111, 113	resubcld 11666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
115	74	simp3d 1142	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 < (𝑆‘(𝐽 + 1)))
116	75, 34, 115	ltled 11386	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ≤ (𝑆‘(𝐽 + 1)))
117	38, 36, 41, 10, 1, 75, 34, 116	fourierdlem7 45496	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸‘𝑌) − 𝑌))
118	112, 78, 60, 117	lesub2dd 11855	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119	118	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
120	98	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℂ)
121	52	recnd 11266	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122	121	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123	110	recnd 11266	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124	120, 122, 123	subsubd 11623	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
125	98, 121	subcld 11595	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
126	34	recnd 11266	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127	125, 126	addcomd 11440	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128	127	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129	124, 128	eqtrd 2768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
131	52	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132	111, 131	sublt0d 11864	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133	130, 132	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134	111, 131	resubcld 11666	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135		ltaddneg 11453	. . . . . . . . . . . . 13 ⊢ ((((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
136	134, 110, 135	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
137	133, 136	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))
138	129, 137	eqbrtrd 5164	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
139	80, 114, 110, 119, 138	lelttrd 11396	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
140	84, 33	ffvelcdmd 7089	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141		elicc2 13415	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
142	14, 15, 141	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
143	140, 142	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))
144	143	simp3d 1142	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145	144	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
146	80, 110, 62, 139, 145	ltletrd 11398	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < 𝐷)
147	80, 62, 146	ltled 11386	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ 𝐷)
148	61, 62, 80, 109, 147	eliccd 44883	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
150		oveq2 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐵 − 𝑥) = (𝐵 − 𝑌))
151	150	oveq1d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑌) / 𝑇))
152	151	fveq2d 6895	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
153	152	oveq1d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
154	149, 153	oveq12d 7432	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
155	154	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
156	36, 75	resubcld 11666	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ)
157	156, 40, 45	redivcld 12066	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 − 𝑌) / 𝑇) ∈ ℝ)
158	157	flcld 13789	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℤ)
159	158	zred 12690	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℝ)
160	159, 40	remulcld 11268	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
161	75, 160	readdcld 11267	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
162	2, 155, 75, 161	fvmptd 7006	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑌) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)))
163	162	oveq1d 7429	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164	163	oveq1d 7429	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165	160	recnd 11266	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166	100, 165	pncan2d 11597	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))
167	166	oveq1d 7429	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇))
168	159	recnd 11266	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℂ)
169	40	recnd 11266	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℂ)
170	168, 169, 45	divcan4d 12020	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
171	164, 167, 170	3eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇)))
172	171, 158	eqeltrd 2829	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ)
173	78	recnd 11266	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℂ)
174	173, 169, 45	divcan1d 12015	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸‘𝑌) − 𝑌))
175	174	oveq2d 7430	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)))
176	98, 173	npcand 11599	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)) = (𝑄‘𝐾))
177	175, 176	eqtrd 2768	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄‘𝐾))
178		ffun 6719	. . . . . . . . . . 11 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
179	58, 178	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑄)
180	58	fdmd 6727	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
181	59, 180	eleqtrrd 2832	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ dom 𝑄)
182		fvelrn 7080	. . . . . . . . . 10 ⊢ ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) → (𝑄‘𝐾) ∈ ran 𝑄)
183	179, 181, 182	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐾) ∈ ran 𝑄)
184	177, 183	eqeltrd 2829	. . . . . . . 8 ⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185		oveq1 7421	. . . . . . . . . . 11 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇))
186	185	oveq2d 7430	. . . . . . . . . 10 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)))
187	186	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → ((((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188	187	rspcev 3608	. . . . . . . 8 ⊢ (((((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189	172, 184, 188	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190	189	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191		oveq1 7421	. . . . . . . . 9 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192	191	eleq1d 2814	. . . . . . . 8 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193	192	rexbidv 3174	. . . . . . 7 ⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194	193	elrab 3681	. . . . . 6 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195	148, 190, 194	sylanbrc 582	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196		elun2 4173	. . . . 5 ⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197	195, 196	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198		fourierdlem63.x	. . . 4 ⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))
199	197, 198, 18	3eltr4g 2846	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 ∈ 𝐻)
200		elfzelz 13527	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201	200	ad2antlr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202		elfzoelz 13658	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
203	31, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℤ)
204	203	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ)
205		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
206	21	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
207	206	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
208	69	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 ∈ (0...𝑁))
209		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑗 ∈ (0...𝑁))
210		isorel 7328	. . . . . . . . . . . 12 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
211	207, 208, 209, 210	syl12anc 836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
212	205, 211	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 < 𝑗)
213	212	adantrr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗)
214		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
215	206	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
216		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁))
217	33	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁))
218		isorel 7328	. . . . . . . . . . . 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 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1))
222		btwnnz 12662	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
223	204, 213, 221, 222	syl3anc 1369	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ)
224	201, 223	pm2.65da 816	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
225	224	adantlr 714	. . . . . 6 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
226	70	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ∈ ℝ)
227	75	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 ∈ ℝ)
228	30	ffvelcdmda 7088	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘𝑗) ∈ ℝ)
229	228	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) ∈ ℝ)
230	74	simp2d 1141	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆‘𝐽) ≤ 𝑌)
231	230	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ≤ 𝑌)
232	106, 198	breqtrrdi 5184	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 < 𝑋)
233	232	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < 𝑋)
234		eqcom 2735	. . . . . . . . . . . . 13 ⊢ (𝑋 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝑋)
235	234	biimpri 227	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗) = 𝑋 → 𝑋 = (𝑆‘𝑗))
236	235	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 = (𝑆‘𝑗))
237	233, 236	breqtrd 5168	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
238	237	adantlr 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗))
239	226, 227, 229, 231, 238	lelttrd 11396	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
240	239	adantllr 718	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗))
241		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) = 𝑋)
242	198, 139	eqbrtrid 5177	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243	242	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244	241, 243	eqbrtrd 5164	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	244	adantlr 714	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
246	240, 245	jca 511	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
247	225, 246	mtand 815	. . . . 5 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆‘𝑗) = 𝑋)
248	247	nrexdv 3145	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
249		isof1o 7325	. . . . . . . . 9 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto→𝐻)
250	206, 249	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
251		f1ofo 6840	. . . . . . . 8 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)–onto→𝐻)
252	250, 251	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻)
253		foelrn 7111	. . . . . . 7 ⊢ ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
254	252, 253	sylan 579	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗))
255	234	rexbii 3090	. . . . . 6 ⊢ (∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
256	254, 255	sylib 217	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
257	256	adantlr 714	. . . 4 ⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋)
258	248, 257	mtand 815	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋 ∈ 𝐻)
259	199, 258	pm2.65da 816	. 2 ⊢ (𝜑 → ¬ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
260	52, 60, 259	nltled 11388	1 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ∀wral 3057 ∃wrex 3066 {crab 3428 ∪ cun 3943 ⊆ wss 3945 {cpr 4626 class class class wbr 5142 ↦ cmpt 5225 dom cdm 5672 ran crn 5673 ℩cio 6492 Fun wfun 6536 ⟶wf 6538 –onto→wfo 6540 –1-1-onto→wf1o 6541 ‘cfv 6542 Isom wiso 6543 (class class class)co 7414 ↑_m cmap 8838 ℂcc 11130 ℝcr 11131 0cc0 11132 1c1 11133 + caddc 11135 · cmul 11137 ℝ^*cxr 11271 < clt 11272 ≤ cle 11273 − cmin 11468 / cdiv 11895 ℕcn 12236 ℤcz 12582 (,]cioc 13351 [,)cico 13352 [,]cicc 13353 ...cfz 13510 ..^cfzo 13653 ⌊cfl 13781 ♯chash 14315

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-inf2 9658 ax-cnex 11188 ax-resscn 11189 ax-1cn 11190 ax-icn 11191 ax-addcl 11192 ax-addrcl 11193 ax-mulcl 11194 ax-mulrcl 11195 ax-mulcom 11196 ax-addass 11197 ax-mulass 11198 ax-distr 11199 ax-i2m1 11200 ax-1ne0 11201 ax-1rid 11202 ax-rnegex 11203 ax-rrecex 11204 ax-cnre 11205 ax-pre-lttri 11206 ax-pre-lttrn 11207 ax-pre-ltadd 11208 ax-pre-mulgt0 11209 ax-pre-sup 11210

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-rmo 3372 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-iin 4994 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-oadd 8484 df-er 8718 df-map 8840 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fi 9428 df-sup 9459 df-inf 9460 df-oi 9527 df-dju 9918 df-card 9956 df-pnf 11274 df-mnf 11275 df-xr 11276 df-ltxr 11277 df-le 11278 df-sub 11470 df-neg 11471 df-div 11896 df-nn 12237 df-2 12299 df-3 12300 df-n0 12497 df-xnn0 12569 df-z 12583 df-uz 12847 df-q 12957 df-rp 13001 df-xneg 13118 df-xadd 13119 df-xmul 13120 df-ioo 13354 df-ioc 13355 df-ico 13356 df-icc 13357 df-fz 13511 df-fzo 13654 df-fl 13783 df-seq 13993 df-exp 14053 df-hash 14316 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-rest 17397 df-topgen 17418 df-psmet 21264 df-xmet 21265 df-met 21266 df-bl 21267 df-mopn 21268 df-top 22789 df-topon 22806 df-bases 22842 df-cld 22916 df-ntr 22917 df-cls 22918 df-nei 22995 df-lp 23033 df-cmp 23284

This theorem is referenced by: fourierdlem79 45567

W3C validator

	
		OSZAR »