fourierdlem54 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem54 40946

Description: Given a partition 𝑄 and an arbitrary interval [𝐶, 𝐷], a partition 𝑆 on [𝐶, 𝐷] is built such that it preserves any periodic function piecewise continuous on 𝑄 will be piecewise continuous on 𝑆, with the same limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem54.t	⊢ 𝑇 = (𝐵 − 𝐴)
fourierdlem54.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem54.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem54.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem54.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem54.d	⊢ (𝜑 → 𝐷 ∈ ℝ)
fourierdlem54.cd	⊢ (𝜑 → 𝐶 < 𝐷)
fourierdlem54.o	⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem54.h	⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem54.n	⊢ 𝑁 = ((♯‘𝐻) − 1)
fourierdlem54.s	⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))

**Assertion**
Ref	Expression
fourierdlem54	⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))

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

Proof of Theorem fourierdlem54 Dummy variables 𝑤 ℎ 𝑦 𝑧 𝑗 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem54.n	. . 3 ⊢ 𝑁 = ((♯‘𝐻) − 1)
2		2z 11656	. . . . . 6 ⊢ 2 ∈ ℤ
3	2	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
4		fourierdlem54.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5		prid1g 4450	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶, 𝐷})
6		elun1 3942	. . . . . . . . . 10 ⊢ (𝐶 ∈ {𝐶, 𝐷} → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
7	4, 5, 6	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
8		fourierdlem54.h	. . . . . . . . 9 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
9	7, 8	syl6eleqr 2855	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝐻)
10	9	ne0d 4086	. . . . . . 7 ⊢ (𝜑 → 𝐻 ≠ ∅)
11		prfi 8442	. . . . . . . . . 10 ⊢ {𝐶, 𝐷} ∈ Fin
12		fourierdlem54.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
13		fourierdlem54.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		fourierdlem54.q	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
15	12, 13, 14	fourierdlem11 40904	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
16	15	simp1d 1172	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
17	15	simp2d 1173	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
18	15	simp3d 1174	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 < 𝐵)
19		fourierdlem54.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝐵 − 𝐴)
20	12, 13, 14	fourierdlem15 40908	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
21		frn 6229	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → ran 𝑄 ⊆ (𝐴[,]𝐵))
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
23	12	fourierdlem2 40895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
24	13, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
25	14, 24	mpbid 223	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
26	25	simpld 488	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)))
27		elmapi 8082	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
28		ffn 6223	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
29	26, 27, 28	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
30		fzfid 12980	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
31		fnfi 8445	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ (0...𝑀) ∈ Fin) → 𝑄 ∈ Fin)
32	29, 30, 31	syl2anc 579	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ Fin)
33		rnfi 8456	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ Fin → ran 𝑄 ∈ Fin)
34	32, 33	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
35	25	simprd 489	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
36	35	simpld 488	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
37	36	simpld 488	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
38	13	nnnn0d 11598	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
39		nn0uz 11922	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
40	38, 39	syl6eleq 2854	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
41		eluzfz1 12555	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
42	40, 41	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ (0...𝑀))
43		fnfvelrn 6546	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄)
44	29, 42, 43	syl2anc 579	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ran 𝑄)
45	37, 44	eqeltrrd 2845	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ran 𝑄)
46	36	simprd 489	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
47		eluzfz2 12556	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
48	40, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
49		fnfvelrn 6546	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄)
50	29, 48, 49	syl2anc 579	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
51	46, 50	eqeltrrd 2845	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ran 𝑄)
52		eqid 2765	. . . . . . . . . . 11 ⊢ (abs ∘ − ) = (abs ∘ − )
53		eqid 2765	. . . . . . . . . . 11 ⊢ ((ran 𝑄 × ran 𝑄) ∖ I ) = ((ran 𝑄 × ran 𝑄) ∖ I )
54		eqid 2765	. . . . . . . . . . 11 ⊢ ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )) = ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I ))
55		eqid 2765	. . . . . . . . . . 11 ⊢ inf(ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < ) = inf(ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < )
56		fourierdlem54.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
57		eqid 2765	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
58		eqid 2765	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶[,]𝐷)) = ((topGen‘ran (,)) ↾_t (𝐶[,]𝐷))
59		oveq1 6849	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝑥 + (𝑘 · 𝑇)) = (𝑤 + (𝑘 · 𝑇)))
60	59	eleq1d 2829	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
61	60	rexbidv 3199	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
62	61	cbvrabv 3348	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
63		oveq1 6849	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 · 𝑇) = (𝑗 · 𝑇))
64	63	oveq2d 6858	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → (𝑦 + (𝑖 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
65	64	eleq1d 2829	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
66	65	anbi1d 623	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄)))
67		oveq1 6849	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (𝑙 · 𝑇) = (𝑘 · 𝑇))
68	67	oveq2d 6858	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (𝑧 + (𝑙 · 𝑇)) = (𝑧 + (𝑘 · 𝑇)))
69	68	eleq1d 2829	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))
70	69	anbi2d 622	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → (((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)))
71	66, 70	cbvrex2v 3328	. . . . . . . . . . . 12 ⊢ (∃𝑖 ∈ ℤ ∃𝑙 ∈ ℤ ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))
72	71	anbi2i 616	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧)) ∧ ∃𝑖 ∈ ℤ ∃𝑙 ∈ ℤ ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄)) ↔ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧)) ∧ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)))
73	16, 17, 18, 19, 22, 34, 45, 51, 52, 53, 54, 55, 4, 56, 57, 58, 62, 72	fourierdlem42 40935	. . . . . . . . . 10 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin)
74		unfi 8434	. . . . . . . . . 10 ⊢ (({𝐶, 𝐷} ∈ Fin ∧ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
75	11, 73, 74	sylancr 581	. . . . . . . . 9 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
76	8, 75	syl5eqel 2848	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Fin)
77		hashnncl 13359	. . . . . . . 8 ⊢ (𝐻 ∈ Fin → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
78	76, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
79	10, 78	mpbird 248	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ)
80	79	nnzd 11728	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
81		fourierdlem54.cd	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < 𝐷)
82	4, 81	ltned 10427	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
83		hashprg 13384	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
84	4, 56, 83	syl2anc 579	. . . . . . . 8 ⊢ (𝜑 → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
85	82, 84	mpbid 223	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) = 2)
86	85	eqcomd 2771	. . . . . 6 ⊢ (𝜑 → 2 = (♯‘{𝐶, 𝐷}))
87		ssun1 3938	. . . . . . . . 9 ⊢ {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
88	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
89	88, 8	syl6sseqr 3812	. . . . . . 7 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ 𝐻)
90		hashssle 40083	. . . . . . 7 ⊢ ((𝐻 ∈ Fin ∧ {𝐶, 𝐷} ⊆ 𝐻) → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
91	76, 89, 90	syl2anc 579	. . . . . 6 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
92	86, 91	eqbrtrd 4831	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
93		eluz2 11892	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
94	3, 80, 92, 93	syl3anbrc 1443	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
95		uz2m1nn 11964	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
96	94, 95	syl 17	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
97	1, 96	syl5eqel 2848	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ)
98		prssg 4504	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
99	4, 56, 98	syl2anc 579	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
100	4, 56, 99	mpbi2and 703	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
101		ssrab2 3847	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
102	4, 56	iccssred 40301	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
103	101, 102	syl5ss 3772	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
104	100, 103	unssd 3951	. . . . . . . . . 10 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
105	8, 104	syl5eqss 3809	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
106		fourierdlem54.s	. . . . . . . . 9 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
107	76, 105, 106, 1	fourierdlem36 40929	. . . . . . . 8 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
108		df-isom 6077	. . . . . . . 8 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) ↔ (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
109	107, 108	sylib 209	. . . . . . 7 ⊢ (𝜑 → (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
110	109	simpld 488	. . . . . 6 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
111		f1of 6320	. . . . . 6 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)⟶𝐻)
112	110, 111	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝐻)
113	112, 105	fssd 6237	. . . 4 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
114		reex 10280	. . . . 5 ⊢ ℝ ∈ V
115		ovex 6874	. . . . . 6 ⊢ (0...𝑁) ∈ V
116	115	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑁) ∈ V)
117		elmapg 8073	. . . . 5 ⊢ ((ℝ ∈ V ∧ (0...𝑁) ∈ V) → (𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ))
118	114, 116, 117	sylancr 581	. . . 4 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ))
119	113, 118	mpbird 248	. . 3 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)))
120		df-f1o 6075	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 ↔ (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻))
121	110, 120	sylib 209	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻))
122	121	simprd 489	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻)
123		dffo3 6564	. . . . . . . . 9 ⊢ (𝑆:(0...𝑁)–onto→𝐻 ↔ (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
124	122, 123	sylib 209	. . . . . . . 8 ⊢ (𝜑 → (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
125	124	simprd 489	. . . . . . 7 ⊢ (𝜑 → ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))
126		eqeq1 2769	. . . . . . . . . 10 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ 𝐶 = (𝑆‘𝑦)))
127		eqcom 2772	. . . . . . . . . 10 ⊢ (𝐶 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶)
128	126, 127	syl6bb 278	. . . . . . . . 9 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶))
129	128	rexbidv 3199	. . . . . . . 8 ⊢ (ℎ = 𝐶 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
130	129	rspcv 3457	. . . . . . 7 ⊢ (𝐶 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
131	9, 125, 130	sylc 65	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)
132		fveq2 6375	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → (𝑆‘𝑦) = (𝑆‘0))
133	132	eqcomd 2771	. . . . . . . . . . . . 13 ⊢ (𝑦 = 0 → (𝑆‘0) = (𝑆‘𝑦))
134	133	adantl 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = (𝑆‘𝑦))
135		simplr 785	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
136	134, 135	eqtrd 2799	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = 𝐶)
137	4	ad2antrr 717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → 𝐶 ∈ ℝ)
138	136, 137	eqeltrd 2844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
139	138, 136	eqled 10394	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
140	139	3adantl2 1208	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
141	4	rexrd 10343	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
142	56	rexrd 10343	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
143	4, 56, 81	ltled 10439	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
144		lbicc2 12492	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
145	141, 142, 143, 144	syl3anc 1490	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
146		ubicc2 12493	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
147	141, 142, 143, 146	syl3anc 1490	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
148		prssg 4504	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
149	145, 147, 148	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
150	145, 147, 149	mpbi2and 703	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
151	101	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
152	150, 151	unssd 3951	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
153	8, 152	syl5eqss 3809	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
154		nnm1nn0 11581	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐻) ∈ ℕ → ((♯‘𝐻) − 1) ∈ ℕ₀)
155	79, 154	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ₀)
156	1, 155	syl5eqel 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
157	156, 39	syl6eleq 2854	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
158		eluzfz1 12555	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑁))
159	157, 158	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑁))
160	112, 159	ffvelrnd 6550	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘0) ∈ 𝐻)
161	153, 160	sseldd 3762	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘0) ∈ (𝐶[,]𝐷))
162	102, 161	sseldd 3762	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘0) ∈ ℝ)
163	162	adantr 472	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
164	163	3ad2antl1 1236	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
165	4	adantr 472	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ)
166	165	3ad2antl1 1236	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ)
167		elfzelz 12549	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℤ)
168	167	zred 11729	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℝ)
169	168	adantr 472	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ ℝ)
170		elfzle1 12551	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 0 ≤ 𝑦)
171	170	adantr 472	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 ≤ 𝑦)
172		neqne 2945	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑦 = 0 → 𝑦 ≠ 0)
173	172	adantl 473	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ≠ 0)
174	169, 171, 173	ne0gt0d 10428	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 < 𝑦)
175	174	3ad2antl2 1237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 0 < 𝑦)
176		simpl1 1242	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝜑)
177		simpl2 1244	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ (0...𝑁))
178	109	simprd 489	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
179		breq1 4812	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦))
180		fveq2 6375	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
181	180	breq1d 4819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘0) < (𝑆‘𝑦)))
182	179, 181	bibi12d 336	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
183	182	ralbidv 3133	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
184	183	rspcv 3457	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
185	159, 178, 184	sylc 65	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
186	185	r19.21bi 3079	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
187	176, 177, 186	syl2anc 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
188	175, 187	mpbid 223	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < (𝑆‘𝑦))
189		simpl3 1246	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
190	188, 189	breqtrd 4835	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < 𝐶)
191	164, 166, 190	ltled 10439	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
192	140, 191	pm2.61dan 847	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) → (𝑆‘0) ≤ 𝐶)
193	192	rexlimdv3a 3180	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶 → (𝑆‘0) ≤ 𝐶))
194	131, 193	mpd 15	. . . . 5 ⊢ (𝜑 → (𝑆‘0) ≤ 𝐶)
195		elicc2 12440	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)))
196	4, 56, 195	syl2anc 579	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)))
197	161, 196	mpbid 223	. . . . . 6 ⊢ (𝜑 → ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷))
198	197	simp2d 1173	. . . . 5 ⊢ (𝜑 → 𝐶 ≤ (𝑆‘0))
199	162, 4	letri3d 10433	. . . . 5 ⊢ (𝜑 → ((𝑆‘0) = 𝐶 ↔ ((𝑆‘0) ≤ 𝐶 ∧ 𝐶 ≤ (𝑆‘0))))
200	194, 198, 199	mpbir2and 704	. . . 4 ⊢ (𝜑 → (𝑆‘0) = 𝐶)
201		eluzfz2 12556	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 𝑁 ∈ (0...𝑁))
202	157, 201	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
203	112, 202	ffvelrnd 6550	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝑁) ∈ 𝐻)
204	153, 203	sseldd 3762	. . . . . . 7 ⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐶[,]𝐷))
205		elicc2 12440	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
206	4, 56, 205	syl2anc 579	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
207	204, 206	mpbid 223	. . . . . 6 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))
208	207	simp3d 1174	. . . . 5 ⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐷)
209		prid2g 4451	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ → 𝐷 ∈ {𝐶, 𝐷})
210		elun1 3942	. . . . . . . . 9 ⊢ (𝐷 ∈ {𝐶, 𝐷} → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
211	56, 209, 210	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
212	211, 8	syl6eleqr 2855	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝐻)
213		eqeq1 2769	. . . . . . . . . 10 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ 𝐷 = (𝑆‘𝑦)))
214		eqcom 2772	. . . . . . . . . 10 ⊢ (𝐷 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷)
215	213, 214	syl6bb 278	. . . . . . . . 9 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷))
216	215	rexbidv 3199	. . . . . . . 8 ⊢ (ℎ = 𝐷 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
217	216	rspcv 3457	. . . . . . 7 ⊢ (𝐷 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
218	212, 125, 217	sylc 65	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷)
219	214	biimpri 219	. . . . . . . . 9 ⊢ ((𝑆‘𝑦) = 𝐷 → 𝐷 = (𝑆‘𝑦))
220	219	3ad2ant3 1165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 = (𝑆‘𝑦))
221	113	ffvelrnda 6549	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ∈ ℝ)
222	102, 204	sseldd 3762	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ)
223	222	adantr 472	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑁) ∈ ℝ)
224	168	adantl 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ∈ ℝ)
225		elfzel2 12547	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
226	225	zred 11729	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
227	226	adantl 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
228		elfzle2 12552	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ≤ 𝑁)
229	228	adantl 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ≤ 𝑁)
230	224, 227, 229	lensymd 10442	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ 𝑁 < 𝑦)
231		breq1 4812	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → (𝑥 < 𝑦 ↔ 𝑁 < 𝑦))
232		fveq2 6375	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
233	232	breq1d 4819	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
234	231, 233	bibi12d 336	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
235	234	ralbidv 3133	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
236	235	rspcv 3457	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
237	202, 178, 236	sylc 65	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
238	237	r19.21bi 3079	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
239	230, 238	mtbid 315	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ (𝑆‘𝑁) < (𝑆‘𝑦))
240	221, 223, 239	nltled 10441	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
241	240	3adant3 1162	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
242	220, 241	eqbrtrd 4831	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 ≤ (𝑆‘𝑁))
243	242	rexlimdv3a 3180	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷 → 𝐷 ≤ (𝑆‘𝑁)))
244	218, 243	mpd 15	. . . . 5 ⊢ (𝜑 → 𝐷 ≤ (𝑆‘𝑁))
245	222, 56	letri3d 10433	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑁) = 𝐷 ↔ ((𝑆‘𝑁) ≤ 𝐷 ∧ 𝐷 ≤ (𝑆‘𝑁))))
246	208, 244, 245	mpbir2and 704	. . . 4 ⊢ (𝜑 → (𝑆‘𝑁) = 𝐷)
247		elfzoelz 12678	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℤ)
248	247	zred 11729	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℝ)
249	248	ltp1d 11208	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 < (𝑖 + 1))
250	249	adantl 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 < (𝑖 + 1))
251	178	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
252		elfzofz 12693	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0...𝑁))
253	252	adantl 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0...𝑁))
254		fzofzp1 12773	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁))
255	254	adantl 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁))
256		breq1 4812	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → (𝑥 < 𝑦 ↔ 𝑖 < 𝑦))
257		fveq2 6375	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑆‘𝑥) = (𝑆‘𝑖))
258	257	breq1d 4819	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘𝑦)))
259	256, 258	bibi12d 336	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦))))
260		breq2 4813	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → (𝑖 < 𝑦 ↔ 𝑖 < (𝑖 + 1)))
261		fveq2 6375	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑖 + 1) → (𝑆‘𝑦) = (𝑆‘(𝑖 + 1)))
262	261	breq2d 4821	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → ((𝑆‘𝑖) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
263	260, 262	bibi12d 336	. . . . . . . . 9 ⊢ (𝑦 = (𝑖 + 1) → ((𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)) ↔ (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
264	259, 263	rspc2v 3474	. . . . . . . 8 ⊢ ((𝑖 ∈ (0...𝑁) ∧ (𝑖 + 1) ∈ (0...𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
265	253, 255, 264	syl2anc 579	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
266	251, 265	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
267	250, 266	mpbid 223	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
268	267	ralrimiva 3113	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
269	200, 246, 268	jca31 510	. . 3 ⊢ (𝜑 → (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
270		fourierdlem54.o	. . . . 5 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
271	270	fourierdlem2 40895	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
272	97, 271	syl 17	. . 3 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
273	119, 269, 272	mpbir2and 704	. 2 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
274	97, 273, 107	jca31 510	1 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1107 = wceq 1652 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 ∃wrex 3056 {crab 3059 Vcvv 3350 ∖ cdif 3729 ∪ cun 3730 ⊆ wss 3732 ∅c0 4079 {cpr 4336 class class class wbr 4809 ↦ cmpt 4888 I cid 5184 × cxp 5275 ran crn 5278 ↾ cres 5279 ∘ ccom 5281 ℩cio 6029 Fn wfn 6063 ⟶wf 6064 –1-1→wf1 6065 –onto→wfo 6066 –1-1-onto→wf1o 6067 ‘cfv 6068 Isom wiso 6069 (class class class)co 6842 ↑_𝑚 cmap 8060 Fincfn 8160 infcinf 8554 ℝcr 10188 0cc0 10189 1c1 10190 + caddc 10192 · cmul 10194 ℝ^*cxr 10327 < clt 10328 ≤ cle 10329 − cmin 10520 ℕcn 11274 2c2 11327 ℕ₀cn0 11538 ℤcz 11624 ℤ_≥cuz 11886 (,)cioo 12377 [,]cicc 12380 ...cfz 12533 ..^cfzo 12673 ♯chash 13321 abscabs 14261 ↾_t crest 16349 topGenctg 16366

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4930 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147 ax-inf2 8753 ax-cnex 10245 ax-resscn 10246 ax-1cn 10247 ax-icn 10248 ax-addcl 10249 ax-addrcl 10250 ax-mulcl 10251 ax-mulrcl 10252 ax-mulcom 10253 ax-addass 10254 ax-mulass 10255 ax-distr 10256 ax-i2m1 10257 ax-1ne0 10258 ax-1rid 10259 ax-rnegex 10260 ax-rrecex 10261 ax-cnre 10262 ax-pre-lttri 10263 ax-pre-lttrn 10264 ax-pre-ltadd 10265 ax-pre-mulgt0 10266 ax-pre-sup 10267

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3597 df-csb 3692 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-pss 3748 df-nul 4080 df-if 4244 df-pw 4317 df-sn 4335 df-pr 4337 df-tp 4339 df-op 4341 df-uni 4595 df-int 4634 df-iun 4678 df-iin 4679 df-br 4810 df-opab 4872 df-mpt 4889 df-tr 4912 df-id 5185 df-eprel 5190 df-po 5198 df-so 5199 df-fr 5236 df-se 5237 df-we 5238 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-pred 5865 df-ord 5911 df-on 5912 df-lim 5913 df-suc 5914 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073 df-fo 6074 df-f1o 6075 df-fv 6076 df-isom 6077 df-riota 6803 df-ov 6845 df-oprab 6846 df-mpt2 6847 df-om 7264 df-1st 7366 df-2nd 7367 df-wrecs 7610 df-recs 7672 df-rdg 7710 df-1o 7764 df-oadd 7768 df-er 7947 df-map 8062 df-en 8161 df-dom 8162 df-sdom 8163 df-fin 8164 df-fi 8524 df-sup 8555 df-inf 8556 df-oi 8622 df-card 9016 df-cda 9243 df-pnf 10330 df-mnf 10331 df-xr 10332 df-ltxr 10333 df-le 10334 df-sub 10522 df-neg 10523 df-div 10939 df-nn 11275 df-2 11335 df-3 11336 df-n0 11539 df-xnn0 11611 df-z 11625 df-uz 11887 df-q 11990 df-rp 12029 df-xneg 12146 df-xadd 12147 df-xmul 12148 df-ioo 12381 df-icc 12384 df-fz 12534 df-fzo 12674 df-seq 13009 df-exp 13068 df-hash 13322 df-cj 14126 df-re 14127 df-im 14128 df-sqrt 14262 df-abs 14263 df-rest 16351 df-topgen 16372 df-psmet 20011 df-xmet 20012 df-met 20013 df-bl 20014 df-mopn 20015 df-top 20978 df-topon 20995 df-bases 21030 df-cld 21103 df-ntr 21104 df-cls 21105 df-nei 21182 df-lp 21220 df-cmp 21470

This theorem is referenced by: fourierdlem63 40955 fourierdlem64 40956 fourierdlem65 40957 fourierdlem79 40971 fourierdlem89 40981 fourierdlem90 40982 fourierdlem91 40983 fourierdlem100 40992 fourierdlem107 40999 fourierdlem109 41001 fourierdlem112 41004

W3C validator