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 44391

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 12535	. . . . . 6 ⊢ 2 ∈ ℤ
3	2	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
4		fourierdlem54.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5		prid1g 4721	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶, 𝐷})
6		elun1 4136	. . . . . . . . . 10 ⊢ (𝐶 ∈ {𝐶, 𝐷} → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
7	4, 5, 6	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
8		fourierdlem54.h	. . . . . . . . 9 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
9	7, 8	eleqtrrdi 2849	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝐻)
10	9	ne0d 4295	. . . . . . 7 ⊢ (𝜑 → 𝐻 ≠ ∅)
11		prfi 9266	. . . . . . . . . 10 ⊢ {𝐶, 𝐷} ∈ Fin
12		fourierdlem54.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
13		fourierdlem54.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		fourierdlem54.q	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
15	12, 13, 14	fourierdlem11 44349	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
16	15	simp1d 1142	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
17	15	simp2d 1143	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
18	15	simp3d 1144	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 < 𝐵)
19		fourierdlem54.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝐵 − 𝐴)
20	12, 13, 14	fourierdlem15 44353	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
21		frn 6675	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → ran 𝑄 ⊆ (𝐴[,]𝐵))
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
23	12	fourierdlem2 44340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
24	13, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
25	14, 24	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
26	25	simpld 495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
27		elmapi 8787	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
28		ffn 6668	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
29	26, 27, 28	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
30		fzfid 13878	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
31		fnfi 9125	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ (0...𝑀) ∈ Fin) → 𝑄 ∈ Fin)
32	29, 30, 31	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ Fin)
33		rnfi 9279	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ Fin → ran 𝑄 ∈ Fin)
34	32, 33	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
35	25	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
36	35	simpld 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
37	36	simpld 495	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
38	13	nnnn0d 12473	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
39		nn0uz 12805	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
40	38, 39	eleqtrdi 2848	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
41		eluzfz1 13448	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
42	40, 41	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ (0...𝑀))
43		fnfvelrn 7031	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄)
44	29, 42, 43	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ran 𝑄)
45	37, 44	eqeltrrd 2839	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ran 𝑄)
46	36	simprd 496	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
47		eluzfz2 13449	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
48	40, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
49		fnfvelrn 7031	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄)
50	29, 48, 49	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
51	46, 50	eqeltrrd 2839	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ran 𝑄)
52		eqid 2736	. . . . . . . . . . 11 ⊢ (abs ∘ − ) = (abs ∘ − )
53		eqid 2736	. . . . . . . . . . 11 ⊢ ((ran 𝑄 × ran 𝑄) ∖ I ) = ((ran 𝑄 × ran 𝑄) ∖ I )
54		eqid 2736	. . . . . . . . . . 11 ⊢ ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )) = ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I ))
55		eqid 2736	. . . . . . . . . . 11 ⊢ inf(ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < ) = inf(ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < )
56		fourierdlem54.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
57		eqid 2736	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
58		eqid 2736	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶[,]𝐷)) = ((topGen‘ran (,)) ↾_t (𝐶[,]𝐷))
59		oveq1 7364	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝑥 + (𝑘 · 𝑇)) = (𝑤 + (𝑘 · 𝑇)))
60	59	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
61	60	rexbidv 3175	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
62	61	cbvrabv 3417	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
63		oveq1 7364	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 · 𝑇) = (𝑗 · 𝑇))
64	63	oveq2d 7373	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → (𝑦 + (𝑖 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
65	64	eleq1d 2822	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
66	65	anbi1d 630	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄)))
67		oveq1 7364	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (𝑙 · 𝑇) = (𝑘 · 𝑇))
68	67	oveq2d 7373	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (𝑧 + (𝑙 · 𝑇)) = (𝑧 + (𝑘 · 𝑇)))
69	68	eleq1d 2822	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))
70	69	anbi2d 629	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → (((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)))
71	66, 70	cbvrex2vw 3228	. . . . . . . . . . . 12 ⊢ (∃𝑖 ∈ ℤ ∃𝑙 ∈ ℤ ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))
72	71	anbi2i 623	. . . . . . . . . . 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 44380	. . . . . . . . . 10 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin)
74		unfi 9116	. . . . . . . . . 10 ⊢ (({𝐶, 𝐷} ∈ Fin ∧ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
75	11, 73, 74	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
76	8, 75	eqeltrid 2842	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Fin)
77		hashnncl 14266	. . . . . . . 8 ⊢ (𝐻 ∈ Fin → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
78	76, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
79	10, 78	mpbird 256	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ)
80	79	nnzd 12526	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
81		fourierdlem54.cd	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < 𝐷)
82	4, 81	ltned 11291	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
83		hashprg 14295	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
84	4, 56, 83	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
85	82, 84	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) = 2)
86	85	eqcomd 2742	. . . . . 6 ⊢ (𝜑 → 2 = (♯‘{𝐶, 𝐷}))
87		ssun1 4132	. . . . . . . . 9 ⊢ {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
88	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
89	88, 8	sseqtrrdi 3995	. . . . . . 7 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ 𝐻)
90		hashssle 43522	. . . . . . 7 ⊢ ((𝐻 ∈ Fin ∧ {𝐶, 𝐷} ⊆ 𝐻) → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
91	76, 89, 90	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
92	86, 91	eqbrtrd 5127	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
93		eluz2 12769	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
94	3, 80, 92, 93	syl3anbrc 1343	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
95		uz2m1nn 12848	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
96	94, 95	syl 17	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
97	1, 96	eqeltrid 2842	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ)
98		prssg 4779	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
99	4, 56, 98	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
100	4, 56, 99	mpbi2and 710	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
101		ssrab2 4037	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
102	4, 56	iccssred 13351	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
103	101, 102	sstrid 3955	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
104	100, 103	unssd 4146	. . . . . . . . . 10 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
105	8, 104	eqsstrid 3992	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
106		fourierdlem54.s	. . . . . . . . 9 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
107	76, 105, 106, 1	fourierdlem36 44374	. . . . . . . 8 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
108		df-isom 6505	. . . . . . . 8 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) ↔ (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
109	107, 108	sylib 217	. . . . . . 7 ⊢ (𝜑 → (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
110	109	simpld 495	. . . . . 6 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
111		f1of 6784	. . . . . 6 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)⟶𝐻)
112	110, 111	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝐻)
113	112, 105	fssd 6686	. . . 4 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
114		reex 11142	. . . . 5 ⊢ ℝ ∈ V
115		ovex 7390	. . . . . 6 ⊢ (0...𝑁) ∈ V
116	115	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑁) ∈ V)
117		elmapg 8778	. . . . 5 ⊢ ((ℝ ∈ V ∧ (0...𝑁) ∈ V) → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ))
118	114, 116, 117	sylancr 587	. . . 4 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ))
119	113, 118	mpbird 256	. . 3 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
120		df-f1o 6503	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 ↔ (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻))
121	110, 120	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻))
122	121	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻)
123		dffo3 7052	. . . . . . . . 9 ⊢ (𝑆:(0...𝑁)–onto→𝐻 ↔ (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
124	122, 123	sylib 217	. . . . . . . 8 ⊢ (𝜑 → (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
125	124	simprd 496	. . . . . . 7 ⊢ (𝜑 → ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))
126		eqeq1 2740	. . . . . . . . . 10 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ 𝐶 = (𝑆‘𝑦)))
127		eqcom 2743	. . . . . . . . . 10 ⊢ (𝐶 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶)
128	126, 127	bitrdi 286	. . . . . . . . 9 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶))
129	128	rexbidv 3175	. . . . . . . 8 ⊢ (ℎ = 𝐶 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
130	129	rspcv 3577	. . . . . . 7 ⊢ (𝐶 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
131	9, 125, 130	sylc 65	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)
132		fveq2 6842	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → (𝑆‘𝑦) = (𝑆‘0))
133	132	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (𝑦 = 0 → (𝑆‘0) = (𝑆‘𝑦))
134	133	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = (𝑆‘𝑦))
135		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
136	134, 135	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = 𝐶)
137	4	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → 𝐶 ∈ ℝ)
138	136, 137	eqeltrd 2838	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
139	138, 136	eqled 11258	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
140	139	3adantl2 1167	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
141	4	rexrd 11205	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
142	56	rexrd 11205	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
143	4, 56, 81	ltled 11303	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
144		lbicc2 13381	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
145	141, 142, 143, 144	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
146		ubicc2 13382	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
147	141, 142, 143, 146	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
148		prssg 4779	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
149	145, 147, 148	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
150	145, 147, 149	mpbi2and 710	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
151	101	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
152	150, 151	unssd 4146	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
153	8, 152	eqsstrid 3992	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
154		nnm1nn0 12454	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐻) ∈ ℕ → ((♯‘𝐻) − 1) ∈ ℕ₀)
155	79, 154	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ₀)
156	1, 155	eqeltrid 2842	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
157	156, 39	eleqtrdi 2848	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
158		eluzfz1 13448	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑁))
159	157, 158	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑁))
160	112, 159	ffvelcdmd 7036	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘0) ∈ 𝐻)
161	153, 160	sseldd 3945	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘0) ∈ (𝐶[,]𝐷))
162	102, 161	sseldd 3945	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘0) ∈ ℝ)
163	162	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
164	163	3ad2antl1 1185	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
165	4	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ)
166	165	3ad2antl1 1185	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ)
167		elfzelz 13441	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℤ)
168	167	zred 12607	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℝ)
169	168	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ ℝ)
170		elfzle1 13444	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 0 ≤ 𝑦)
171	170	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 ≤ 𝑦)
172		neqne 2951	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑦 = 0 → 𝑦 ≠ 0)
173	172	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ≠ 0)
174	169, 171, 173	ne0gt0d 11292	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 < 𝑦)
175	174	3ad2antl2 1186	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 0 < 𝑦)
176		simpl1 1191	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝜑)
177		simpl2 1192	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ (0...𝑁))
178	109	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
179		breq1 5108	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦))
180		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
181	180	breq1d 5115	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘0) < (𝑆‘𝑦)))
182	179, 181	bibi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
183	182	ralbidv 3174	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
184	183	rspcv 3577	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
185	159, 178, 184	sylc 65	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
186	185	r19.21bi 3234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
187	176, 177, 186	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
188	175, 187	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < (𝑆‘𝑦))
189		simpl3 1193	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
190	188, 189	breqtrd 5131	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < 𝐶)
191	164, 166, 190	ltled 11303	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
192	140, 191	pm2.61dan 811	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) → (𝑆‘0) ≤ 𝐶)
193	192	rexlimdv3a 3156	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶 → (𝑆‘0) ≤ 𝐶))
194	131, 193	mpd 15	. . . . 5 ⊢ (𝜑 → (𝑆‘0) ≤ 𝐶)
195		elicc2 13329	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)))
196	4, 56, 195	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)))
197	161, 196	mpbid 231	. . . . . 6 ⊢ (𝜑 → ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷))
198	197	simp2d 1143	. . . . 5 ⊢ (𝜑 → 𝐶 ≤ (𝑆‘0))
199	162, 4	letri3d 11297	. . . . 5 ⊢ (𝜑 → ((𝑆‘0) = 𝐶 ↔ ((𝑆‘0) ≤ 𝐶 ∧ 𝐶 ≤ (𝑆‘0))))
200	194, 198, 199	mpbir2and 711	. . . 4 ⊢ (𝜑 → (𝑆‘0) = 𝐶)
201		eluzfz2 13449	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 𝑁 ∈ (0...𝑁))
202	157, 201	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
203	112, 202	ffvelcdmd 7036	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝑁) ∈ 𝐻)
204	153, 203	sseldd 3945	. . . . . . 7 ⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐶[,]𝐷))
205		elicc2 13329	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
206	4, 56, 205	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
207	204, 206	mpbid 231	. . . . . 6 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))
208	207	simp3d 1144	. . . . 5 ⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐷)
209		prid2g 4722	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ → 𝐷 ∈ {𝐶, 𝐷})
210		elun1 4136	. . . . . . . . 9 ⊢ (𝐷 ∈ {𝐶, 𝐷} → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
211	56, 209, 210	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
212	211, 8	eleqtrrdi 2849	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝐻)
213		eqeq1 2740	. . . . . . . . . 10 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ 𝐷 = (𝑆‘𝑦)))
214		eqcom 2743	. . . . . . . . . 10 ⊢ (𝐷 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷)
215	213, 214	bitrdi 286	. . . . . . . . 9 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷))
216	215	rexbidv 3175	. . . . . . . 8 ⊢ (ℎ = 𝐷 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
217	216	rspcv 3577	. . . . . . 7 ⊢ (𝐷 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
218	212, 125, 217	sylc 65	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷)
219	214	biimpri 227	. . . . . . . . 9 ⊢ ((𝑆‘𝑦) = 𝐷 → 𝐷 = (𝑆‘𝑦))
220	219	3ad2ant3 1135	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 = (𝑆‘𝑦))
221	113	ffvelcdmda 7035	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ∈ ℝ)
222	102, 204	sseldd 3945	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ)
223	222	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑁) ∈ ℝ)
224	168	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ∈ ℝ)
225		elfzel2 13439	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
226	225	zred 12607	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
227	226	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
228		elfzle2 13445	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ≤ 𝑁)
229	228	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ≤ 𝑁)
230	224, 227, 229	lensymd 11306	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ 𝑁 < 𝑦)
231		breq1 5108	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → (𝑥 < 𝑦 ↔ 𝑁 < 𝑦))
232		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
233	232	breq1d 5115	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
234	231, 233	bibi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
235	234	ralbidv 3174	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
236	235	rspcv 3577	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
237	202, 178, 236	sylc 65	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
238	237	r19.21bi 3234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
239	230, 238	mtbid 323	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ (𝑆‘𝑁) < (𝑆‘𝑦))
240	221, 223, 239	nltled 11305	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
241	240	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
242	220, 241	eqbrtrd 5127	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 ≤ (𝑆‘𝑁))
243	242	rexlimdv3a 3156	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷 → 𝐷 ≤ (𝑆‘𝑁)))
244	218, 243	mpd 15	. . . . 5 ⊢ (𝜑 → 𝐷 ≤ (𝑆‘𝑁))
245	222, 56	letri3d 11297	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑁) = 𝐷 ↔ ((𝑆‘𝑁) ≤ 𝐷 ∧ 𝐷 ≤ (𝑆‘𝑁))))
246	208, 244, 245	mpbir2and 711	. . . 4 ⊢ (𝜑 → (𝑆‘𝑁) = 𝐷)
247		elfzoelz 13572	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℤ)
248	247	zred 12607	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℝ)
249	248	ltp1d 12085	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 < (𝑖 + 1))
250	249	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 < (𝑖 + 1))
251	178	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
252		elfzofz 13588	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0...𝑁))
253	252	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0...𝑁))
254		fzofzp1 13669	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁))
255	254	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁))
256		breq1 5108	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → (𝑥 < 𝑦 ↔ 𝑖 < 𝑦))
257		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑆‘𝑥) = (𝑆‘𝑖))
258	257	breq1d 5115	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘𝑦)))
259	256, 258	bibi12d 345	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦))))
260		breq2 5109	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → (𝑖 < 𝑦 ↔ 𝑖 < (𝑖 + 1)))
261		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑖 + 1) → (𝑆‘𝑦) = (𝑆‘(𝑖 + 1)))
262	261	breq2d 5117	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → ((𝑆‘𝑖) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
263	260, 262	bibi12d 345	. . . . . . . . 9 ⊢ (𝑦 = (𝑖 + 1) → ((𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)) ↔ (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
264	259, 263	rspc2v 3590	. . . . . . . 8 ⊢ ((𝑖 ∈ (0...𝑁) ∧ (𝑖 + 1) ∈ (0...𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
265	253, 255, 264	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
266	251, 265	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
267	250, 266	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
268	267	ralrimiva 3143	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
269	200, 246, 268	jca31 515	. . 3 ⊢ (𝜑 → (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
270		fourierdlem54.o	. . . . 5 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
271	270	fourierdlem2 44340	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
272	97, 271	syl 17	. . 3 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
273	119, 269, 272	mpbir2and 711	. 2 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
274	97, 273, 107	jca31 515	1 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 {crab 3407 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 ⊆ wss 3910 ∅c0 4282 {cpr 4588 class class class wbr 5105 ↦ cmpt 5188 I cid 5530 × cxp 5631 ran crn 5634 ↾ cres 5635 ∘ ccom 5637 ℩cio 6446 Fn wfn 6491 ⟶wf 6492 –1-1→wf1 6493 –onto→wfo 6494 –1-1-onto→wf1o 6495 ‘cfv 6496 Isom wiso 6497 (class class class)co 7357 ↑_m cmap 8765 Fincfn 8883 infcinf 9377 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 ℝ^*cxr 11188 < clt 11189 ≤ cle 11190 − cmin 11385 ℕcn 12153 2c2 12208 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 (,)cioo 13264 [,]cicc 13267 ...cfz 13424 ..^cfzo 13567 ♯chash 14230 abscabs 15119 ↾_t crest 17302 topGenctg 17319

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-oadd 8416 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9347 df-sup 9378 df-inf 9379 df-oi 9446 df-dju 9837 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-xnn0 12486 df-z 12500 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-icc 13271 df-fz 13425 df-fzo 13568 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-rest 17304 df-topgen 17325 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-top 22243 df-topon 22260 df-bases 22296 df-cld 22370 df-ntr 22371 df-cls 22372 df-nei 22449 df-lp 22487 df-cmp 22738

This theorem is referenced by: fourierdlem63 44400 fourierdlem64 44401 fourierdlem65 44402 fourierdlem79 44416 fourierdlem89 44426 fourierdlem90 44427 fourierdlem91 44428 fourierdlem100 44437 fourierdlem107 44444 fourierdlem109 44446 fourierdlem112 44449

W3C validator