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 46175

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 12649	. . . . . 6 ⊢ 2 ∈ ℤ
3	2	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
4		fourierdlem54.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5		prid1g 4760	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶, 𝐷})
6		elun1 4182	. . . . . . . . . 10 ⊢ (𝐶 ∈ {𝐶, 𝐷} → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
7	4, 5, 6	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
8		fourierdlem54.h	. . . . . . . . 9 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
9	7, 8	eleqtrrdi 2852	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝐻)
10	9	ne0d 4342	. . . . . . 7 ⊢ (𝜑 → 𝐻 ≠ ∅)
11		prfi 9363	. . . . . . . . . 10 ⊢ {𝐶, 𝐷} ∈ Fin
12		fourierdlem54.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
13		fourierdlem54.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		fourierdlem54.q	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
15	12, 13, 14	fourierdlem11 46133	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
16	15	simp1d 1143	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
17	15	simp2d 1144	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
18	15	simp3d 1145	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 < 𝐵)
19		fourierdlem54.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝐵 − 𝐴)
20	12, 13, 14	fourierdlem15 46137	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
21		frn 6743	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → ran 𝑄 ⊆ (𝐴[,]𝐵))
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵))
23	12	fourierdlem2 46124	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
24	13, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
25	14, 24	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
26	25	simpld 494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
27		elmapi 8889	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
28		ffn 6736	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
29	26, 27, 28	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
30		fzfid 14014	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
31		fnfi 9218	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ (0...𝑀) ∈ Fin) → 𝑄 ∈ Fin)
32	29, 30, 31	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ Fin)
33		rnfi 9380	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ Fin → ran 𝑄 ∈ Fin)
34	32, 33	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
35	25	simprd 495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
36	35	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
37	36	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
38	13	nnnn0d 12587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
39		nn0uz 12920	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
40	38, 39	eleqtrdi 2851	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
41		eluzfz1 13571	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
42	40, 41	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ (0...𝑀))
43		fnfvelrn 7100	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄)
44	29, 42, 43	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ran 𝑄)
45	37, 44	eqeltrrd 2842	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ran 𝑄)
46	36	simprd 495	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
47		eluzfz2 13572	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
48	40, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
49		fnfvelrn 7100	. . . . . . . . . . . . 13 ⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄)
50	29, 48, 49	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
51	46, 50	eqeltrrd 2842	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ran 𝑄)
52		eqid 2737	. . . . . . . . . . 11 ⊢ (abs ∘ − ) = (abs ∘ − )
53		eqid 2737	. . . . . . . . . . 11 ⊢ ((ran 𝑄 × ran 𝑄) ∖ I ) = ((ran 𝑄 × ran 𝑄) ∖ I )
54		eqid 2737	. . . . . . . . . . 11 ⊢ ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )) = ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I ))
55		eqid 2737	. . . . . . . . . . 11 ⊢ inf(ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < ) = inf(ran ((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < )
56		fourierdlem54.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
57		eqid 2737	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
58		eqid 2737	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶[,]𝐷)) = ((topGen‘ran (,)) ↾_t (𝐶[,]𝐷))
59		oveq1 7438	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝑥 + (𝑘 · 𝑇)) = (𝑤 + (𝑘 · 𝑇)))
60	59	eleq1d 2826	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
61	60	rexbidv 3179	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄))
62	61	cbvrabv 3447	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
63		oveq1 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 · 𝑇) = (𝑗 · 𝑇))
64	63	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → (𝑦 + (𝑖 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
65	64	eleq1d 2826	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
66	65	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄)))
67		oveq1 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑘 → (𝑙 · 𝑇) = (𝑘 · 𝑇))
68	67	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑘 → (𝑧 + (𝑙 · 𝑇)) = (𝑧 + (𝑘 · 𝑇)))
69	68	eleq1d 2826	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))
70	69	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → (((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)))
71	66, 70	cbvrex2vw 3242	. . . . . . . . . . . 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 46164	. . . . . . . . . 10 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin)
74		unfi 9211	. . . . . . . . . 10 ⊢ (({𝐶, 𝐷} ∈ Fin ∧ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
75	11, 73, 74	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin)
76	8, 75	eqeltrid 2845	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Fin)
77		hashnncl 14405	. . . . . . . 8 ⊢ (𝐻 ∈ Fin → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
78	76, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
79	10, 78	mpbird 257	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ)
80	79	nnzd 12640	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
81		fourierdlem54.cd	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 < 𝐷)
82	4, 81	ltned 11397	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
83		hashprg 14434	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
84	4, 56, 83	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2))
85	82, 84	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) = 2)
86	85	eqcomd 2743	. . . . . 6 ⊢ (𝜑 → 2 = (♯‘{𝐶, 𝐷}))
87		ssun1 4178	. . . . . . . . 9 ⊢ {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
88	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
89	88, 8	sseqtrrdi 4025	. . . . . . 7 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ 𝐻)
90		hashssle 45310	. . . . . . 7 ⊢ ((𝐻 ∈ Fin ∧ {𝐶, 𝐷} ⊆ 𝐻) → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
91	76, 89, 90	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻))
92	86, 91	eqbrtrd 5165	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
93		eluz2 12884	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
94	3, 80, 92, 93	syl3anbrc 1344	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
95		uz2m1nn 12965	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
96	94, 95	syl 17	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
97	1, 96	eqeltrid 2845	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ)
98		prssg 4819	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
99	4, 56, 98	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ))
100	4, 56, 99	mpbi2and 712	. . . . . . . . . . 11 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
101		ssrab2 4080	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
102	4, 56	iccssred 13474	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
103	101, 102	sstrid 3995	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
104	100, 103	unssd 4192	. . . . . . . . . 10 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
105	8, 104	eqsstrid 4022	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
106		fourierdlem54.s	. . . . . . . . 9 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
107	76, 105, 106, 1	fourierdlem36 46158	. . . . . . . 8 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
108		df-isom 6570	. . . . . . . 8 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) ↔ (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
109	107, 108	sylib 218	. . . . . . 7 ⊢ (𝜑 → (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))))
110	109	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻)
111		f1of 6848	. . . . . 6 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)⟶𝐻)
112	110, 111	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝐻)
113	112, 105	fssd 6753	. . . 4 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
114		reex 11246	. . . . 5 ⊢ ℝ ∈ V
115		ovex 7464	. . . . . 6 ⊢ (0...𝑁) ∈ V
116	115	a1i 11	. . . . 5 ⊢ (𝜑 → (0...𝑁) ∈ V)
117		elmapg 8879	. . . . 5 ⊢ ((ℝ ∈ V ∧ (0...𝑁) ∈ V) → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ))
118	114, 116, 117	sylancr 587	. . . 4 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ))
119	113, 118	mpbird 257	. . 3 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
120		df-f1o 6568	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 ↔ (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻))
121	110, 120	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻))
122	121	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻)
123		dffo3 7122	. . . . . . . . 9 ⊢ (𝑆:(0...𝑁)–onto→𝐻 ↔ (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
124	122, 123	sylib 218	. . . . . . . 8 ⊢ (𝜑 → (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)))
125	124	simprd 495	. . . . . . 7 ⊢ (𝜑 → ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))
126		eqeq1 2741	. . . . . . . . . 10 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ 𝐶 = (𝑆‘𝑦)))
127		eqcom 2744	. . . . . . . . . 10 ⊢ (𝐶 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶)
128	126, 127	bitrdi 287	. . . . . . . . 9 ⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶))
129	128	rexbidv 3179	. . . . . . . 8 ⊢ (ℎ = 𝐶 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
130	129	rspcv 3618	. . . . . . 7 ⊢ (𝐶 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶))
131	9, 125, 130	sylc 65	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)
132		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → (𝑆‘𝑦) = (𝑆‘0))
133	132	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ (𝑦 = 0 → (𝑆‘0) = (𝑆‘𝑦))
134	133	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = (𝑆‘𝑦))
135		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
136	134, 135	eqtrd 2777	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = 𝐶)
137	4	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → 𝐶 ∈ ℝ)
138	136, 137	eqeltrd 2841	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
139	138, 136	eqled 11364	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
140	139	3adantl2 1168	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
141	4	rexrd 11311	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
142	56	rexrd 11311	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
143	4, 56, 81	ltled 11409	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
144		lbicc2 13504	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
145	141, 142, 143, 144	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
146		ubicc2 13505	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
147	141, 142, 143, 146	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
148		prssg 4819	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
149	145, 147, 148	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
150	145, 147, 149	mpbi2and 712	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
151	101	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
152	150, 151	unssd 4192	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
153	8, 152	eqsstrid 4022	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
154		nnm1nn0 12567	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐻) ∈ ℕ → ((♯‘𝐻) − 1) ∈ ℕ₀)
155	79, 154	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ₀)
156	1, 155	eqeltrid 2845	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
157	156, 39	eleqtrdi 2851	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
158		eluzfz1 13571	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑁))
159	157, 158	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑁))
160	112, 159	ffvelcdmd 7105	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘0) ∈ 𝐻)
161	153, 160	sseldd 3984	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘0) ∈ (𝐶[,]𝐷))
162	102, 161	sseldd 3984	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘0) ∈ ℝ)
163	162	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
164	163	3ad2antl1 1186	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ)
165	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ)
166	165	3ad2antl1 1186	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ)
167		elfzelz 13564	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℤ)
168	167	zred 12722	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℝ)
169	168	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ ℝ)
170		elfzle1 13567	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 0 ≤ 𝑦)
171	170	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 ≤ 𝑦)
172		neqne 2948	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑦 = 0 → 𝑦 ≠ 0)
173	172	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ≠ 0)
174	169, 171, 173	ne0gt0d 11398	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 < 𝑦)
175	174	3ad2antl2 1187	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 0 < 𝑦)
176		simpl1 1192	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝜑)
177		simpl2 1193	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ (0...𝑁))
178	109	simprd 495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
179		breq1 5146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦))
180		fveq2 6906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
181	180	breq1d 5153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘0) < (𝑆‘𝑦)))
182	179, 181	bibi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
183	182	ralbidv 3178	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
184	183	rspcv 3618	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))))
185	159, 178, 184	sylc 65	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
186	185	r19.21bi 3251	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
187	176, 177, 186	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))
188	175, 187	mpbid 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < (𝑆‘𝑦))
189		simpl3 1194	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶)
190	188, 189	breqtrd 5169	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < 𝐶)
191	164, 166, 190	ltled 11409	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶)
192	140, 191	pm2.61dan 813	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) → (𝑆‘0) ≤ 𝐶)
193	192	rexlimdv3a 3159	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶 → (𝑆‘0) ≤ 𝐶))
194	131, 193	mpd 15	. . . . 5 ⊢ (𝜑 → (𝑆‘0) ≤ 𝐶)
195		elicc2 13452	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)))
196	4, 56, 195	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)))
197	161, 196	mpbid 232	. . . . . 6 ⊢ (𝜑 → ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷))
198	197	simp2d 1144	. . . . 5 ⊢ (𝜑 → 𝐶 ≤ (𝑆‘0))
199	162, 4	letri3d 11403	. . . . 5 ⊢ (𝜑 → ((𝑆‘0) = 𝐶 ↔ ((𝑆‘0) ≤ 𝐶 ∧ 𝐶 ≤ (𝑆‘0))))
200	194, 198, 199	mpbir2and 713	. . . 4 ⊢ (𝜑 → (𝑆‘0) = 𝐶)
201		eluzfz2 13572	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 𝑁 ∈ (0...𝑁))
202	157, 201	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
203	112, 202	ffvelcdmd 7105	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝑁) ∈ 𝐻)
204	153, 203	sseldd 3984	. . . . . . 7 ⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐶[,]𝐷))
205		elicc2 13452	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
206	4, 56, 205	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)))
207	204, 206	mpbid 232	. . . . . 6 ⊢ (𝜑 → ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))
208	207	simp3d 1145	. . . . 5 ⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐷)
209		prid2g 4761	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ → 𝐷 ∈ {𝐶, 𝐷})
210		elun1 4182	. . . . . . . . 9 ⊢ (𝐷 ∈ {𝐶, 𝐷} → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
211	56, 209, 210	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
212	211, 8	eleqtrrdi 2852	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝐻)
213		eqeq1 2741	. . . . . . . . . 10 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ 𝐷 = (𝑆‘𝑦)))
214		eqcom 2744	. . . . . . . . . 10 ⊢ (𝐷 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷)
215	213, 214	bitrdi 287	. . . . . . . . 9 ⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷))
216	215	rexbidv 3179	. . . . . . . 8 ⊢ (ℎ = 𝐷 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
217	216	rspcv 3618	. . . . . . 7 ⊢ (𝐷 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷))
218	212, 125, 217	sylc 65	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷)
219	214	biimpri 228	. . . . . . . . 9 ⊢ ((𝑆‘𝑦) = 𝐷 → 𝐷 = (𝑆‘𝑦))
220	219	3ad2ant3 1136	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 = (𝑆‘𝑦))
221	113	ffvelcdmda 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ∈ ℝ)
222	102, 204	sseldd 3984	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ)
223	222	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑁) ∈ ℝ)
224	168	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ∈ ℝ)
225		elfzel2 13562	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
226	225	zred 12722	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
227	226	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
228		elfzle2 13568	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ≤ 𝑁)
229	228	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ≤ 𝑁)
230	224, 227, 229	lensymd 11412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ 𝑁 < 𝑦)
231		breq1 5146	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → (𝑥 < 𝑦 ↔ 𝑁 < 𝑦))
232		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
233	232	breq1d 5153	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
234	231, 233	bibi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
235	234	ralbidv 3178	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
236	235	rspcv 3618	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))))
237	202, 178, 236	sylc 65	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
238	237	r19.21bi 3251	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))
239	230, 238	mtbid 324	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ (𝑆‘𝑁) < (𝑆‘𝑦))
240	221, 223, 239	nltled 11411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
241	240	3adant3 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → (𝑆‘𝑦) ≤ (𝑆‘𝑁))
242	220, 241	eqbrtrd 5165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 ≤ (𝑆‘𝑁))
243	242	rexlimdv3a 3159	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷 → 𝐷 ≤ (𝑆‘𝑁)))
244	218, 243	mpd 15	. . . . 5 ⊢ (𝜑 → 𝐷 ≤ (𝑆‘𝑁))
245	222, 56	letri3d 11403	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑁) = 𝐷 ↔ ((𝑆‘𝑁) ≤ 𝐷 ∧ 𝐷 ≤ (𝑆‘𝑁))))
246	208, 244, 245	mpbir2and 713	. . . 4 ⊢ (𝜑 → (𝑆‘𝑁) = 𝐷)
247		elfzoelz 13699	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℤ)
248	247	zred 12722	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℝ)
249	248	ltp1d 12198	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 < (𝑖 + 1))
250	249	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 < (𝑖 + 1))
251	178	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))
252		elfzofz 13715	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0...𝑁))
253	252	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0...𝑁))
254		fzofzp1 13803	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁))
255	254	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁))
256		breq1 5146	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → (𝑥 < 𝑦 ↔ 𝑖 < 𝑦))
257		fveq2 6906	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑆‘𝑥) = (𝑆‘𝑖))
258	257	breq1d 5153	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘𝑦)))
259	256, 258	bibi12d 345	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦))))
260		breq2 5147	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → (𝑖 < 𝑦 ↔ 𝑖 < (𝑖 + 1)))
261		fveq2 6906	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑖 + 1) → (𝑆‘𝑦) = (𝑆‘(𝑖 + 1)))
262	261	breq2d 5155	. . . . . . . . . 10 ⊢ (𝑦 = (𝑖 + 1) → ((𝑆‘𝑖) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
263	260, 262	bibi12d 345	. . . . . . . . 9 ⊢ (𝑦 = (𝑖 + 1) → ((𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)) ↔ (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
264	259, 263	rspc2v 3633	. . . . . . . 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 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
268	267	ralrimiva 3146	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
269	200, 246, 268	jca31 514	. . 3 ⊢ (𝜑 → (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))
270		fourierdlem54.o	. . . . 5 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
271	270	fourierdlem2 46124	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
272	97, 271	syl 17	. . 3 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
273	119, 269, 272	mpbir2and 713	. 2 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
274	97, 273, 107	jca31 514	1 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3436 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ⊆ wss 3951 ∅c0 4333 {cpr 4628 class class class wbr 5143 ↦ cmpt 5225 I cid 5577 × cxp 5683 ran crn 5686 ↾ cres 5687 ∘ ccom 5689 ℩cio 6512 Fn wfn 6556 ⟶wf 6557 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 Isom wiso 6562 (class class class)co 7431 ↑_m cmap 8866 Fincfn 8985 infcinf 9481 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 ℕcn 12266 2c2 12321 ℕ₀cn0 12526 ℤcz 12613 ℤ_≥cuz 12878 (,)cioo 13387 [,]cicc 13390 ...cfz 13547 ..^cfzo 13694 ♯chash 14369 abscabs 15273 ↾_t crest 17465 topGenctg 17482

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-er 8745 df-map 8868 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-icc 13394 df-fz 13548 df-fzo 13695 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-rest 17467 df-topgen 17488 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-top 22900 df-topon 22917 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-cmp 23395

This theorem is referenced by: fourierdlem63 46184 fourierdlem64 46185 fourierdlem65 46186 fourierdlem79 46200 fourierdlem89 46210 fourierdlem90 46211 fourierdlem91 46212 fourierdlem100 46221 fourierdlem107 46228 fourierdlem109 46230 fourierdlem112 46233

W3C validator