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 47443

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	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem54.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem54.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem54.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem54.d	⊢ (𝜑 → 𝐷 ∈ ℝ)
fourierdlem54.cd	⊢ (𝜑 → 𝐶 < 𝐷)
fourierdlem54.o	⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (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 12768	. . . . . 6 ⊢ 2 ∈ ℤ
3	2	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
4		fourierdlem54.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5		prid1g 4723	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶, 𝐷})
6		elun1 4183	. . . . . . . . . 10 ⊢ (𝐶 ∈ {𝐶, 𝐷} → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
7	4, 5, 6	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
8		fourierdlem54.h	. . . . . . . . 9 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
9	7, 8	eleqtrrdi 2875	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝐻)
10	9	ne0d 4291	. . . . . . 7 ⊢ (𝜑 → 𝐻 ≠ ∅)
11		prfi 9353	. . . . . . . . . 10 ⊢ {𝐶, 𝐷} ∈ Fin
12		fourierdlem54.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
13		fourierdlem54.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		fourierdlem54.q	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
15	12, 13, 14	fourierdlem11 47401	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
16	15	simp1d 1160	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
17	15	simp2d 1161	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
18	15	simp3d 1162	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 < 𝐵)
19		fourierdlem54.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝐵 − 𝐴)
20	12, 13, 14	fourierdlem15 47405	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
21		frn 6747	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → ran 𝑄 ⊆ (𝐴[,]𝐵))
22	20, 21	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
23	12	fourierdlem2 47392	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
24	13, 23	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
25	14, 24	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
26	25	simpld 500	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
27		elmapi 8907	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
28		ffn 6739	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
29	26, 27, 28	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
30		fzfid 14156	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
31		fnfi 9231	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ (0...𝑀) ∈ Fin) → 𝑄 ∈ Fin)
32	29, 30, 31	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ Fin)
33		rnfi 9367	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ Fin → ran 𝑄 ∈ Fin)
34	32, 33	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
35	25	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
36	35	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
37	36	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
38	13	nnnn0d 12707	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
39		nn0uz 13043	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
40	38, 39	eleqtrdi 2874	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
41		eluzfz1 13704	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
42	40, 41	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ (0...𝑀))
43		fnfvelrn 7112	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄)
44	29, 42, 43	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ran 𝑄)
45	37, 44	eqeltrrd 2865	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ran 𝑄)
46	36	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
47		eluzfz2 13705	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
48	40, 47	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
49		fnfvelrn 7112	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄)
50	29, 48, 49	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
51	46, 50	eqeltrrd 2865	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ran 𝑄)
52		eqid 2763	. . . . . . . . . . 11 ⊢ (abs ∘ − ) = (abs ∘ − )
53		eqid 2763	. . . . . . . . . . 11 ⊢ ((ran 𝑄 × ran 𝑄) ∖ I ) = ((ran 𝑄 × ran 𝑄) ∖ I )
54		eqid 2763	. . . . . . . . . . 11 ⊢ ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )) = ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I ))
55		eqid 2763	. . . . . . . . . . 11 ⊢ inf(ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < ) = inf(ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < )
56		fourierdlem54.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
57		eqid 2763	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
58		eqid 2763	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶[,]𝐷)) = ((topGen‘ran (,)) ↾_t (𝐶[,]𝐷))
59		oveq1 7458	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝑥 + (𝑘 · 𝑇)) = (𝑤 + (𝑘 · 𝑇)))
60	59	eleq1d 2849	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
61	60	rexbidv 3190	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
62	61	cbvrabv 3426	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
63		oveq1 7458	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 · 𝑇) = (𝑗 · 𝑇))
64	63	oveq2d 7467	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → (𝑦 + (𝑖 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
65	64	eleq1d 2849	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
66	65	anbi1d 643	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄)))
67		oveq1 7458	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (𝑙 · 𝑇) = (𝑘 · 𝑇))
68	67	oveq2d 7467	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (𝑧 + (𝑙 · 𝑇)) = (𝑧 + (𝑘 · 𝑇)))
69	68	eleq1d 2849	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))
70	69	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → (((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)))
71	66, 70	cbvrex2vw 3249	. . . . . . . . . . . 12 ⊢ (∃𝑖 ∈ ℤ ∃𝑙 ∈ ℤ ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))
72	71	anbi2i 635	. . . . . . . . . . 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 47432	. . . . . . . . . 10 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin)
74		unfi 9224	. . . . . . . . . 10 ⊢ (({𝐶, 𝐷} ∈ Fin ∧ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
75	11, 73, 74	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
76	8, 75	eqeltrid 2868	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Fin)
77		hashnncl 14551	. . . . . . . 8 ⊢ (𝐻 ∈ Fin → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
78	76, 77	syl 18	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
79	10, 78	mpbird 260	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ)
80	79	nnzd 12759	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
81		fourierdlem54.cd	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < 𝐷)
82	4, 81	ltned 11485	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
83		hashprg 14580	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
84	4, 56, 83	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
85	82, 84	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) = 2)
86	85	eqcomd 2769	. . . . . 6 ⊢ (𝜑 → 2 = (♯‘{𝐶, 𝐷}))
87		ssun1 4179	. . . . . . . . 9 ⊢ {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
88	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
89	88, 8	sseqtrrdi 3954	. . . . . . 7 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ 𝐻)
90		hashssle 46587	. . . . . . 7 ⊢ ((𝐻 ∈ Fin ∧ {𝐶, 𝐷} ⊆ 𝐻) → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
91	76, 89, 90	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
92	86, 91	eqbrtrd 5133	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
93		eluz2 13011	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
94	3, 80, 92, 93	syl3anbrc 1362	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
95		uz2m1nn 13090	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
96	94, 95	syl 18	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
97	1, 96	eqeltrid 2868	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ)
98		prssg 4780	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
99	4, 56, 98	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
100	4, 56, 99	mpbi2and 725	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
101		ssrab2 4008	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
102	4, 56	iccssred 13605	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
103	101, 102	sstrid 3924	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
104	100, 103	unssd 4193	. . . . . . . . . 10 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
105	8, 104	eqsstrid 3951	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
106		fourierdlem54.s	. . . . . . . . 9 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
107	76, 105, 106, 1	fourierdlem36 47426	. . . . . . . 8 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
108		df-isom 6575	. . . . . . . 8 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) ↔ (𝑆:(0...𝑁)⟶1-1onto𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
109	107, 108	sylib 221	. . . . . . 7 ⊢ (𝜑 → (𝑆:(0...𝑁)⟶1-1onto𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
110	109	simpld 500	. . . . . 6 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶1-1onto𝐻)
111		f1of 6854	. . . . . 6 ⊢ (𝑆:(0...𝑁)⟶1-1onto𝐻 → 𝑆:(0...𝑁)⟶𝐻)
112	110, 111	syl 18	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝐻)
113	112, 105	fssd 6757	. . . 4 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
114		reex 11330	. . . . 5 ⊢ ℝ ∈ V
115		ovex 7484	. . . . . 6 ⊢ (0...𝑁) ∈ V
116	115	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑁) ∈ V)
117		elmapg 8897	. . . . 5 ⊢ ((ℝ ∈ V ∧ (0...𝑁) ∈ V) → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ))
118	114, 116, 117	sylancr 599	. . . 4 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ))
119	113, 118	mpbird 260	. . 3 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
120		df-f1o 6573	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)⟶1-1onto𝐻 ↔ (𝑆:(0...𝑁)⟶1-1𝐻 ∧ 𝑆:(0...𝑁)⟶onto𝐻))
121	110, 120	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆:(0...𝑁)⟶1-1𝐻 ∧ 𝑆:(0...𝑁)⟶onto𝐻))
122	121	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶onto𝐻)
123		dffo3 7134	. . . . . . . . 9 ⊢ (𝑆:(0...𝑁)⟶onto𝐻 ↔ (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
124	122, 123	sylib 221	. . . . . . . 8 ⊢ (𝜑 → (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
125	124	simprd 501	. . . . . . 7 ⊢ (𝜑 → ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))
126		eqeq1 2767	. . . . . . . . . 10 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ 𝐶 = (𝑆‘𝑦)))
127		eqcom 2770	. . . . . . . . . 10 ⊢ (𝐶 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶)
128	126, 127	bitrdi 290	. . . . . . . . 9 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶))
129	128	rexbidv 3190	. . . . . . . 8 ⊢ (ℎ = 𝐶 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
130	129	rspcv 3576	. . . . . . 7 ⊢ (𝐶 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
131	9, 125, 130	sylc 66	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)
132		fveq2 6916	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → (𝑆‘𝑦) = (𝑆‘0))
133	132	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ (𝑦 = 0 → (𝑆‘0) = (𝑆‘𝑦))
134	133	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = (𝑆‘𝑦))
135		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
136	134, 135	eqtrd 2798	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = 𝐶)
137	4	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → 𝐶 ∈ ℝ)
138	136, 137	eqeltrd 2864	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
139	138, 136	eqled 11452	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
140	139	3adantl2 1186	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
141	4	rexrd 11398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
142	56	rexrd 11398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
143	4, 56, 81	ltled 11497	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
144		lbicc2 13635	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
145	141, 142, 143, 144	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
146		ubicc2 13636	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
147	141, 142, 143, 146	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
148		prssg 4780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
149	145, 147, 148	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
150	145, 147, 149	mpbi2and 725	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
151	101	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
152	150, 151	unssd 4193	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
153	8, 152	eqsstrid 3951	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
154		nnm1nn0 12687	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐻) ∈ ℕ → ((♯‘𝐻) − 1) ∈ ℕ₀)
155	79, 154	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ₀)
156	1, 155	eqeltrid 2868	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
157	156, 39	eleqtrdi 2874	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
158		eluzfz1 13704	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑁))
159	157, 158	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑁))
160	112, 159	ffvelcdmd 7117	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘0) ∈ 𝐻)
161	153, 160	sseldd 3914	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘0) ∈ (𝐶[,]𝐷))
162	102, 161	sseldd 3914	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘0) ∈ ℝ)
163	162	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
164	163	3ad2antl1 1204	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
165	4	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ)
166	165	3ad2antl1 1204	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ)
167		elfzelz 13696	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℤ)
168	167	zred 12843	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℝ)
169	168	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ ℝ)
170		elfzle1 13700	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 0 ≤ 𝑦)
171	170	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 ≤ 𝑦)
172		neqne 2967	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑦 = 0 → 𝑦 ≠ 0)
173	172	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ≠ 0)
174	169, 171, 173	ne0gt0d 11486	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 < 𝑦)
175	174	3ad2antl2 1205	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 0 < 𝑦)
176		simpl1 1210	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝜑)
177		simpl2 1211	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ (0...𝑁))
178	109	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
179		breq1 5111	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦))
180		fveq2 6916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
181	180	breq1d 5118	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘0) < (𝑆‘𝑦)))
182	179, 181	bibi12d 348	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
183	182	ralbidv 3189	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
184	183	rspcv 3576	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
185	159, 178, 184	sylc 66	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
186	185	r19.21bi 3258	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
187	176, 177, 186	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
188	175, 187	mpbid 235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < (𝑆‘𝑦))
189		simpl3 1212	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
190	188, 189	breqtrd 5137	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < 𝐶)
191	164, 166, 190	ltled 11497	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
192	140, 191	pm2.61dan 825	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) → (𝑆‘0) ≤ 𝐶)
193	192	rexlimdv3a 3171	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶 → (𝑆‘0) ≤ 𝐶))
194	131, 193	mpd 16	. . . . 5 ⊢ (𝜑 → (𝑆‘0) ≤ 𝐶)
195		elicc2 13582	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)))
196	4, 56, 195	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)))
197	161, 196	mpbid 235	. . . . . 6 ⊢ (𝜑 → ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷))
198	197	simp2d 1161	. . . . 5 ⊢ (𝜑 → 𝐶 ≤ (𝑆‘0))
199	162, 4	letri3d 11491	. . . . 5 ⊢ (𝜑 → ((𝑆‘0) = 𝐶 ↔ ((𝑆‘0) ≤ 𝐶 ∧ 𝐶 ≤ (𝑆‘0))))
200	194, 198, 199	mpbir2and 726	. . . 4 ⊢ (𝜑 → (𝑆‘0) = 𝐶)
201		eluzfz2 13705	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 𝑁 ∈ (0...𝑁))
202	157, 201	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
203	112, 202	ffvelcdmd 7117	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝑁) ∈ 𝐻)
204	153, 203	sseldd 3914	. . . . . . 7 ⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐶[,]𝐷))
205		elicc2 13582	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
206	4, 56, 205	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
207	204, 206	mpbid 235	. . . . . 6 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))
208	207	simp3d 1162	. . . . 5 ⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐷)
209		prid2g 4724	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ → 𝐷 ∈ {𝐶, 𝐷})
210		elun1 4183	. . . . . . . . 9 ⊢ (𝐷 ∈ {𝐶, 𝐷} → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
211	56, 209, 210	3syl 19	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
212	211, 8	eleqtrrdi 2875	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝐻)
213		eqeq1 2767	. . . . . . . . . 10 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ 𝐷 = (𝑆‘𝑦)))
214		eqcom 2770	. . . . . . . . . 10 ⊢ (𝐷 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷)
215	213, 214	bitrdi 290	. . . . . . . . 9 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷))
216	215	rexbidv 3190	. . . . . . . 8 ⊢ (ℎ = 𝐷 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
217	216	rspcv 3576	. . . . . . 7 ⊢ (𝐷 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
218	212, 125, 217	sylc 66	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷)
219	214	biimpri 231	. . . . . . . . 9 ⊢ ((𝑆‘𝑦) = 𝐷 → 𝐷 = (𝑆‘𝑦))
220	219	3ad2ant3 1153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 = (𝑆‘𝑦))
221	113	ffvelcdmda 7116	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ∈ ℝ)
222	102, 204	sseldd 3914	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ)
223	222	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑁) ∈ ℝ)
224	168	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ∈ ℝ)
225		elfzel2 13694	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
226	225	zred 12843	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
227	226	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
228		elfzle2 13701	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ≤ 𝑁)
229	228	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ≤ 𝑁)
230	224, 227, 229	lensymd 11500	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ 𝑁 < 𝑦)
231		breq1 5111	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → (𝑥 < 𝑦 ↔ 𝑁 < 𝑦))
232		fveq2 6916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
233	232	breq1d 5118	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
234	231, 233	bibi12d 348	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
235	234	ralbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
236	235	rspcv 3576	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
237	202, 178, 236	sylc 66	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
238	237	r19.21bi 3258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
239	230, 238	mtbid 327	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ (𝑆‘𝑁) < (𝑆‘𝑦))
240	221, 223, 239	nltled 11499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
241	240	3adant3 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
242	220, 241	eqbrtrd 5133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 ≤ (𝑆‘𝑁))
243	242	rexlimdv3a 3171	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷 → 𝐷 ≤ (𝑆‘𝑁)))
244	218, 243	mpd 16	. . . . 5 ⊢ (𝜑 → 𝐷 ≤ (𝑆‘𝑁))
245	222, 56	letri3d 11491	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑁) = 𝐷 ↔ ((𝑆‘𝑁) ≤ 𝐷 ∧ 𝐷 ≤ (𝑆‘𝑁))))
246	208, 244, 245	mpbir2and 726	. . . 4 ⊢ (𝜑 → (𝑆‘𝑁) = 𝐷)
247		elfzoelz 13833	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℤ)
248	247	zred 12843	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℝ)
249	248	ltp1d 12287	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 < (𝑖 + 1))
250	249	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 < (𝑖 + 1))
251	178	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
252		elfzofz 13850	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0...𝑁))
253	252	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0...𝑁))
254		fzofzp1 13939	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁))
255	254	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁))
256		breq1 5111	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → (𝑥 < 𝑦 ↔ 𝑖 < 𝑦))
257		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑆‘𝑥) = (𝑆‘𝑖))
258	257	breq1d 5118	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘𝑦)))
259	256, 258	bibi12d 348	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦))))
260		breq2 5112	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → (𝑖 < 𝑦 ↔ 𝑖 < (𝑖 + 1)))
261		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑖 + 1) → (𝑆‘𝑦) = (𝑆‘(𝑖 + 1)))
262	261	breq2d 5120	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → ((𝑆‘𝑖) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
263	260, 262	bibi12d 348	. . . . . . . . 9 ⊢ (𝑦 = (𝑖 + 1) → ((𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)) ↔ (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
264	259, 263	rspc2v 3590	. . . . . . . 8 ⊢ ((𝑖 ∈ (0...𝑁) ∧ (𝑖 + 1) ∈ (0...𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
265	253, 255, 264	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
266	251, 265	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
267	250, 266	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
268	267	ralrimiva 3158	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
269	200, 246, 268	jca31 524	. . 3 ⊢ (𝜑 → (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
270		fourierdlem54.o	. . . . 5 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
271	270	fourierdlem2 47392	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
272	97, 271	syl 18	. . 3 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
273	119, 269, 272	mpbir2and 726	. 2 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
274	97, 273, 107	jca31 524	1 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∪ cun 4152 ∅c0 4281 {cpr 4590 class class class wbr 5108 ↦ cmpt 5192 I cid 5552 × cxp 5656 ran crn 5659 ↾ cres 5660 ∘ ccom 5662 ℩cio 6518 Fn wfn 6561 ⟶wf 6562 ⟶1-1wf1 6563 ⟶ontowfo 6564 ⟶1-1ontowf1o 6565 ‘cfv 6566 Isom wiso 6567 (class class class)co 7451 ↑_m cmap 8885 Fincfn 9011 infcinf 9470 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 ℝ^*cxr 11381 < clt 11382 ≤ cle 11383 − cmin 11580 ℕcn 12375 2c2 12437 ℕ₀cn0 12646 ℤcz 12733 ℤ_≥cuz 13005 (,)cioo 13516 [,]cicc 13519 ...cfz 13679 ..^cfzo 13828 ♯chash 14515 abscabs 15444 ↾_t crest 17641 topGenctg 17658

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-inf2 9679 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-oadd 8518 df-er 8755 df-map 8887 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fi 9440 df-sup 9471 df-inf 9472 df-oi 9541 df-dju 10019 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-n0 12647 df-xnn0 12720 df-z 12734 df-uz 13006 df-q 13116 df-rp 13161 df-xneg 13281 df-xadd 13282 df-xmul 13283 df-ioo 13520 df-icc 13523 df-fz 13680 df-fzo 13829 df-seq 14185 df-exp 14245 df-hash 14516 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-rest 17643 df-topgen 17664 df-psmet 21721 df-xmet 21722 df-met 21723 df-bl 21724 df-mopn 21725 df-top 23267 df-topon 23284 df-bases 23319 df-cld 23392 df-ntr 23393 df-cls 23394 df-nei 23471 df-lp 23509 df-cmp 23760

This theorem is used by: fourierdlem63 47452 fourierdlem64 47453 fourierdlem65 47454 fourierdlem79 47468 fourierdlem89 47478 fourierdlem90 47479 fourierdlem91 47480 fourierdlem100 47489 fourierdlem107 47496 fourierdlem109 47498 fourierdlem112 47501

W3C validator