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 46932

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 12641	. . . . . 6 ⊢ 2 ∈ ℤ
3	2	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
4		fourierdlem54.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5		prid1g 4728	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶, 𝐷})
6		elun1 4135	. . . . . . . . . 10 ⊢ (𝐶 ∈ {𝐶, 𝐷} → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
7	4, 5, 6	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
8		fourierdlem54.h	. . . . . . . . 9 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
9	7, 8	eleqtrrdi 2876	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝐻)
10	9	ne0d 4295	. . . . . . 7 ⊢ (𝜑 → 𝐻 ≠ ∅)
11		prfi 9290	. . . . . . . . . 10 ⊢ {𝐶, 𝐷} ∈ Fin
12		fourierdlem54.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
13		fourierdlem54.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		fourierdlem54.q	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
15	12, 13, 14	fourierdlem11 46890	. . . . . . . . . . . 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 46894	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
21		frn 6717	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → ran 𝑄 ⊆ (𝐴[,]𝐵))
22	20, 21	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
23	12	fourierdlem2 46881	. . . . . . . . . . . . . . . . 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 8852	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
28		ffn 6709	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
29	26, 27, 28	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
30		fzfid 14027	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
31		fnfi 9169	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ (0...𝑀) ∈ Fin) → 𝑄 ∈ Fin)
32	29, 30, 31	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ Fin)
33		rnfi 9304	. . . . . . . . . . . 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 12580	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
39		nn0uz 12916	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
40	38, 39	eleqtrdi 2875	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
41		eluzfz1 13575	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
42	40, 41	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ (0...𝑀))
43		fnfvelrn 7079	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄)
44	29, 42, 43	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ran 𝑄)
45	37, 44	eqeltrrd 2866	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ran 𝑄)
46	36	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
47		eluzfz2 13576	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
48	40, 47	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
49		fnfvelrn 7079	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄)
50	29, 48, 49	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
51	46, 50	eqeltrrd 2866	. . . . . . . . . . 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 7426	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝑥 + (𝑘 · 𝑇)) = (𝑤 + (𝑘 · 𝑇)))
60	59	eleq1d 2850	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
61	60	rexbidv 3191	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
62	61	cbvrabv 3428	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
63		oveq1 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 · 𝑇) = (𝑗 · 𝑇))
64	63	oveq2d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → (𝑦 + (𝑖 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
65	64	eleq1d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
66	65	anbi1d 643	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄)))
67		oveq1 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (𝑙 · 𝑇) = (𝑘 · 𝑇))
68	67	oveq2d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (𝑧 + (𝑙 · 𝑇)) = (𝑧 + (𝑘 · 𝑇)))
69	68	eleq1d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))
70	69	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → (((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)))
71	66, 70	cbvrex2vw 3250	. . . . . . . . . . . 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 46921	. . . . . . . . . 10 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin)
74		unfi 9162	. . . . . . . . . 10 ⊢ (({𝐶, 𝐷} ∈ Fin ∧ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
75	11, 73, 74	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
76	8, 75	eqeltrid 2869	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Fin)
77		hashnncl 14420	. . . . . . . 8 ⊢ (𝐻 ∈ Fin → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
78	76, 77	syl 18	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
79	10, 78	mpbird 260	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ)
80	79	nnzd 12632	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
81		fourierdlem54.cd	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < 𝐷)
82	4, 81	ltned 11361	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
83		hashprg 14449	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
84	4, 56, 83	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
85	82, 84	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) = 2)
86	85	eqcomd 2771	. . . . . 6 ⊢ (𝜑 → 2 = (♯‘{𝐶, 𝐷}))
87		ssun1 4131	. . . . . . . . 9 ⊢ {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
88	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
89	88, 8	sseqtrrdi 3979	. . . . . . 7 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ 𝐻)
90		hashssle 46075	. . . . . . 7 ⊢ ((𝐻 ∈ Fin ∧ {𝐶, 𝐷} ⊆ 𝐻) → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
91	76, 89, 90	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
92	86, 91	eqbrtrd 5135	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
93		eluz2 12884	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
94	3, 80, 92, 93	syl3anbrc 1362	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
95		uz2m1nn 12963	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
96	94, 95	syl 18	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
97	1, 96	eqeltrid 2869	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ)
98		prssg 4787	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
99	4, 56, 98	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
100	4, 56, 99	mpbi2and 725	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
101		ssrab2 4035	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
102	4, 56	iccssred 13477	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
103	101, 102	sstrid 3949	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
104	100, 103	unssd 4145	. . . . . . . . . 10 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
105	8, 104	eqsstrid 3976	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
106		fourierdlem54.s	. . . . . . . . 9 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
107	76, 105, 106, 1	fourierdlem36 46915	. . . . . . . 8 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
108		df-isom 6549	. . . . . . . 8 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) ↔ (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
109	107, 108	sylib 221	. . . . . . 7 ⊢ (𝜑 → (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
110	109	simpld 500	. . . . . 6 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
111		f1of 6824	. . . . . 6 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)⟶𝐻)
112	110, 111	syl 18	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝐻)
113	112, 105	fssd 6727	. . . 4 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
114		reex 11206	. . . . 5 ⊢ ℝ ∈ V
115		ovex 7452	. . . . . 6 ⊢ (0...𝑁) ∈ V
116	115	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑁) ∈ V)
117		elmapg 8842	. . . . 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 6547	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 ↔ (𝑆:(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 7101	. . . . . . . . 9 ⊢ (𝑆:(0...𝑁)–onto→𝐻 ↔ (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
124	122, 123	sylib 221	. . . . . . . 8 ⊢ (𝜑 → (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
125	124	simprd 501	. . . . . . 7 ⊢ (𝜑 → ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))
126		eqeq1 2769	. . . . . . . . . 10 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ 𝐶 = (𝑆‘𝑦)))
127		eqcom 2772	. . . . . . . . . 10 ⊢ (𝐶 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶)
128	126, 127	bitrdi 290	. . . . . . . . 9 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶))
129	128	rexbidv 3191	. . . . . . . 8 ⊢ (ℎ = 𝐶 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
130	129	rspcv 3579	. . . . . . 7 ⊢ (𝐶 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
131	9, 125, 130	sylc 66	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)
132		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → (𝑆‘𝑦) = (𝑆‘0))
133	132	eqcomd 2771	. . . . . . . . . . . . 13 ⊢ (𝑦 = 0 → (𝑆‘0) = (𝑆‘𝑦))
134	133	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = (𝑆‘𝑦))
135		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
136	134, 135	eqtrd 2800	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = 𝐶)
137	4	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → 𝐶 ∈ ℝ)
138	136, 137	eqeltrd 2865	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
139	138, 136	eqled 11328	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
140	139	3adantl2 1186	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
141	4	rexrd 11274	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
142	56	rexrd 11274	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
143	4, 56, 81	ltled 11373	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
144		lbicc2 13507	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
145	141, 142, 143, 144	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
146		ubicc2 13508	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
147	141, 142, 143, 146	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
148		prssg 4787	. . . . . . . . . . . . . . . . 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 4145	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
153	8, 152	eqsstrid 3976	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
154		nnm1nn0 12560	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐻) ∈ ℕ → ((♯‘𝐻) − 1) ∈ ℕ₀)
155	79, 154	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ₀)
156	1, 155	eqeltrid 2869	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
157	156, 39	eleqtrdi 2875	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
158		eluzfz1 13575	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑁))
159	157, 158	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑁))
160	112, 159	ffvelcdmd 7084	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘0) ∈ 𝐻)
161	153, 160	sseldd 3939	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘0) ∈ (𝐶[,]𝐷))
162	102, 161	sseldd 3939	. . . . . . . . . . 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 13568	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℤ)
168	167	zred 12716	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℝ)
169	168	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ ℝ)
170		elfzle1 13571	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 0 ≤ 𝑦)
171	170	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 ≤ 𝑦)
172		neqne 2968	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑦 = 0 → 𝑦 ≠ 0)
173	172	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ≠ 0)
174	169, 171, 173	ne0gt0d 11362	. . . . . . . . . . . 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 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦))
180		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
181	180	breq1d 5121	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘0) < (𝑆‘𝑦)))
182	179, 181	bibi12d 348	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
183	182	ralbidv 3190	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
184	183	rspcv 3579	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
185	159, 178, 184	sylc 66	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
186	185	r19.21bi 3259	. . . . . . . . . . . 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 5139	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < 𝐶)
191	164, 166, 190	ltled 11373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
192	140, 191	pm2.61dan 825	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) → (𝑆‘0) ≤ 𝐶)
193	192	rexlimdv3a 3172	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶 → (𝑆‘0) ≤ 𝐶))
194	131, 193	mpd 16	. . . . 5 ⊢ (𝜑 → (𝑆‘0) ≤ 𝐶)
195		elicc2 13454	. . . . . . . 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 11367	. . . . 5 ⊢ (𝜑 → ((𝑆‘0) = 𝐶 ↔ ((𝑆‘0) ≤ 𝐶 ∧ 𝐶 ≤ (𝑆‘0))))
200	194, 198, 199	mpbir2and 726	. . . 4 ⊢ (𝜑 → (𝑆‘0) = 𝐶)
201		eluzfz2 13576	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 𝑁 ∈ (0...𝑁))
202	157, 201	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
203	112, 202	ffvelcdmd 7084	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝑁) ∈ 𝐻)
204	153, 203	sseldd 3939	. . . . . . 7 ⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐶[,]𝐷))
205		elicc2 13454	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
206	4, 56, 205	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
207	204, 206	mpbid 235	. . . . . 6 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))
208	207	simp3d 1162	. . . . 5 ⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐷)
209		prid2g 4729	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ → 𝐷 ∈ {𝐶, 𝐷})
210		elun1 4135	. . . . . . . . 9 ⊢ (𝐷 ∈ {𝐶, 𝐷} → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
211	56, 209, 210	3syl 19	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
212	211, 8	eleqtrrdi 2876	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝐻)
213		eqeq1 2769	. . . . . . . . . 10 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ 𝐷 = (𝑆‘𝑦)))
214		eqcom 2772	. . . . . . . . . 10 ⊢ (𝐷 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷)
215	213, 214	bitrdi 290	. . . . . . . . 9 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷))
216	215	rexbidv 3191	. . . . . . . 8 ⊢ (ℎ = 𝐷 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
217	216	rspcv 3579	. . . . . . 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 7083	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ∈ ℝ)
222	102, 204	sseldd 3939	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ)
223	222	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑁) ∈ ℝ)
224	168	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ∈ ℝ)
225		elfzel2 13566	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
226	225	zred 12716	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
227	226	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
228		elfzle2 13572	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ≤ 𝑁)
229	228	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ≤ 𝑁)
230	224, 227, 229	lensymd 11376	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ 𝑁 < 𝑦)
231		breq1 5114	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → (𝑥 < 𝑦 ↔ 𝑁 < 𝑦))
232		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
233	232	breq1d 5121	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
234	231, 233	bibi12d 348	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
235	234	ralbidv 3190	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
236	235	rspcv 3579	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
237	202, 178, 236	sylc 66	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
238	237	r19.21bi 3259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
239	230, 238	mtbid 327	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ (𝑆‘𝑁) < (𝑆‘𝑦))
240	221, 223, 239	nltled 11375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
241	240	3adant3 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
242	220, 241	eqbrtrd 5135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 ≤ (𝑆‘𝑁))
243	242	rexlimdv3a 3172	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷 → 𝐷 ≤ (𝑆‘𝑁)))
244	218, 243	mpd 16	. . . . 5 ⊢ (𝜑 → 𝐷 ≤ (𝑆‘𝑁))
245	222, 56	letri3d 11367	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑁) = 𝐷 ↔ ((𝑆‘𝑁) ≤ 𝐷 ∧ 𝐷 ≤ (𝑆‘𝑁))))
246	208, 244, 245	mpbir2and 726	. . . 4 ⊢ (𝜑 → (𝑆‘𝑁) = 𝐷)
247		elfzoelz 13704	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℤ)
248	247	zred 12716	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℝ)
249	248	ltp1d 12160	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 < (𝑖 + 1))
250	249	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 < (𝑖 + 1))
251	178	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
252		elfzofz 13721	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0...𝑁))
253	252	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0...𝑁))
254		fzofzp1 13810	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁))
255	254	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁))
256		breq1 5114	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → (𝑥 < 𝑦 ↔ 𝑖 < 𝑦))
257		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑆‘𝑥) = (𝑆‘𝑖))
258	257	breq1d 5121	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘𝑦)))
259	256, 258	bibi12d 348	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦))))
260		breq2 5115	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → (𝑖 < 𝑦 ↔ 𝑖 < (𝑖 + 1)))
261		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑖 + 1) → (𝑆‘𝑦) = (𝑆‘(𝑖 + 1)))
262	261	breq2d 5123	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → ((𝑆‘𝑖) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
263	260, 262	bibi12d 348	. . . . . . . . 9 ⊢ (𝑦 = (𝑖 + 1) → ((𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)) ↔ (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
264	259, 263	rspc2v 3594	. . . . . . . 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 3159	. . . 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 46881	. . . 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 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 {crab 3418 Vcvv 3457 ∖ cdif 3903 ∪ cun 3904 ⊆ wss 3906 ∅c0 4286 {cpr 4593 class class class wbr 5111 ↦ cmpt 5194 I cid 5557 × cxp 5661 ran crn 5664 ↾ cres 5665 ∘ ccom 5667 ℩cio 6494 Fn wfn 6535 ⟶wf 6536 –1-1→wf1 6537 –onto→wfo 6538 –1-1-onto→wf1o 6539 ‘cfv 6540 Isom wiso 6541 (class class class)co 7419 ↑_m cmap 8830 Fincfn 8949 infcinf 9408 ℝcr 11114 0cc0 11115 1c1 11116 + caddc 11118 · cmul 11120 ℝ^*cxr 11257 < clt 11258 ≤ cle 11259 − cmin 11456 ℕcn 12248 2c2 12310 ℕ₀cn0 12519 ℤcz 12606 ℤ_≥cuz 12878 (,)cioo 13388 [,]cicc 13391 ...cfz 13551 ..^cfzo 13699 ♯chash 14384 abscabs 15309 ↾_t crest 17495 topGenctg 17512

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 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192 ax-pre-sup 11193

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 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-er 8700 df-map 8832 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fi 9378 df-sup 9409 df-inf 9410 df-oi 9479 df-dju 9903 df-card 9941 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-div 11887 df-nn 12249 df-2 12318 df-3 12319 df-n0 12520 df-xnn0 12593 df-z 12607 df-uz 12879 df-q 12989 df-rp 13033 df-xneg 13153 df-xadd 13154 df-xmul 13155 df-ioo 13392 df-icc 13395 df-fz 13552 df-fzo 13700 df-seq 14056 df-exp 14116 df-hash 14385 df-cj 15174 df-re 15175 df-im 15176 df-sqrt 15310 df-abs 15311 df-rest 17497 df-topgen 17518 df-psmet 21564 df-xmet 21565 df-met 21566 df-bl 21567 df-mopn 21568 df-top 23101 df-topon 23118 df-bases 23153 df-cld 23226 df-ntr 23227 df-cls 23228 df-nei 23305 df-lp 23343 df-cmp 23594

This theorem is used by: fourierdlem63 46941 fourierdlem64 46942 fourierdlem65 46943 fourierdlem79 46957 fourierdlem89 46967 fourierdlem90 46968 fourierdlem91 46969 fourierdlem100 46978 fourierdlem107 46985 fourierdlem109 46987 fourierdlem112 46990

W3C validator