fourierdlem54

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

	Ref	Expression
Hypotheses	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	fourierdlem54	⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem54.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
2		fourierdlem54.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑_m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3		fourierdlem54.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4		fourierdlem54.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5		fourierdlem54.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6		fourierdlem54.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
7		fourierdlem54.cd	⊢ ( 𝜑 → 𝐶 < 𝐷 )
8		fourierdlem54.o	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑_m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
9		fourierdlem54.h	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
10		fourierdlem54.n	⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
11		fourierdlem54.s	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
12		2z	⊢ 2 ∈ ℤ
13	12	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
14		prid1g	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ { 𝐶 , 𝐷 } )
15		elun1	⊢ ( 𝐶 ∈ { 𝐶 , 𝐷 } → 𝐶 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
16	5 14 15	3syl	⊢ ( 𝜑 → 𝐶 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
17	16 9	eleqtrrdi	⊢ ( 𝜑 → 𝐶 ∈ 𝐻 )
18	17	ne0d	⊢ ( 𝜑 → 𝐻 ≠ ∅ )
19		prfi	⊢ { 𝐶 , 𝐷 } ∈ Fin
20	2 3 4	fourierdlem11	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
21	20	simp1d	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
22	20	simp2d	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
23	20	simp3d	⊢ ( 𝜑 → 𝐴 < 𝐵 )
24	2 3 4	fourierdlem15	⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
25		frn	⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) → ran 𝑄 ⊆ ( 𝐴 [,] 𝐵 ) )
26	24 25	syl	⊢ ( 𝜑 → ran 𝑄 ⊆ ( 𝐴 [,] 𝐵 ) )
27	2	fourierdlem2	⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑_m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
28	3 27	syl	⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑_m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
29	4 28	mpbid	⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑_m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
30	29	simpld	⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑_m ( 0 ... 𝑀 ) ) )
31		elmapi	⊢ ( 𝑄 ∈ ( ℝ ↑_m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
32		ffn	⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → 𝑄 Fn ( 0 ... 𝑀 ) )
33	30 31 32	3syl	⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) )
34		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
35		fnfi	⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ ( 0 ... 𝑀 ) ∈ Fin ) → 𝑄 ∈ Fin )
36	33 34 35	syl2anc	⊢ ( 𝜑 → 𝑄 ∈ Fin )
37		rnfi	⊢ ( 𝑄 ∈ Fin → ran 𝑄 ∈ Fin )
38	36 37	syl	⊢ ( 𝜑 → ran 𝑄 ∈ Fin )
39	29	simprd	⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
40	39	simpld	⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
41	40	simpld	⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
42	3	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
43		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
44	42 43	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ_≥ ‘ 0 ) )
45		eluzfz1	⊢ ( 𝑀 ∈ ( ℤ_≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
46	44 45	syl	⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
47		fnfvelrn	⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 0 ) ∈ ran 𝑄 )
48	33 46 47	syl2anc	⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ran 𝑄 )
49	41 48	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ ran 𝑄 )
50	40	simprd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
51		eluzfz2	⊢ ( 𝑀 ∈ ( ℤ_≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
52	44 51	syl	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
53		fnfvelrn	⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ 𝑀 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 )
54	33 52 53	syl2anc	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 )
55	50 54	eqeltrrd	⊢ ( 𝜑 → 𝐵 ∈ ran 𝑄 )
56		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
57		eqid	⊢ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) = ( ( ran 𝑄 × ran 𝑄 ) ∖ I )
58		eqid	⊢ ran ( ( abs ∘ − ) ↾ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) ) = ran ( ( abs ∘ − ) ↾ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) )
59		eqid	⊢ inf ( ran ( ( abs ∘ − ) ↾ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) ) , ℝ , < ) = inf ( ran ( ( abs ∘ − ) ↾ ( ( ran 𝑄 × ran 𝑄 ) ∖ I ) ) , ℝ , < )
60		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
61		eqid	⊢ ( ( topGen ‘ ran (,) ) ↾_t ( 𝐶 [,] 𝐷 ) ) = ( ( topGen ‘ ran (,) ) ↾_t ( 𝐶 [,] 𝐷 ) )
62		oveq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( 𝑤 + ( 𝑘 · 𝑇 ) ) )
63	62	eleq1d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
64	63	rexbidv	⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
65	64	cbvrabv	⊢ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
66		oveq1	⊢ ( 𝑖 = 𝑗 → ( 𝑖 · 𝑇 ) = ( 𝑗 · 𝑇 ) )
67	66	oveq2d	⊢ ( 𝑖 = 𝑗 → ( 𝑦 + ( 𝑖 · 𝑇 ) ) = ( 𝑦 + ( 𝑗 · 𝑇 ) ) )
68	67	eleq1d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑦 + ( 𝑖 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ) )
69	68	anbi1d	⊢ ( 𝑖 = 𝑗 → ( ( ( 𝑦 + ( 𝑖 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ↔ ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ) )
70		oveq1	⊢ ( 𝑙 = 𝑘 → ( 𝑙 · 𝑇 ) = ( 𝑘 · 𝑇 ) )
71	70	oveq2d	⊢ ( 𝑙 = 𝑘 → ( 𝑧 + ( 𝑙 · 𝑇 ) ) = ( 𝑧 + ( 𝑘 · 𝑇 ) ) )
72	71	eleq1d	⊢ ( 𝑙 = 𝑘 → ( ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑧 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
73	72	anbi2d	⊢ ( 𝑙 = 𝑘 → ( ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ↔ ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ) )
74	69 73	cbvrex2vw	⊢ ( ∃ 𝑖 ∈ ℤ ∃ 𝑙 ∈ ℤ ( ( 𝑦 + ( 𝑖 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ↔ ∃ 𝑗 ∈ ℤ ∃ 𝑘 ∈ ℤ ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
75	74	anbi2i	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧 ) ) ∧ ∃ 𝑖 ∈ ℤ ∃ 𝑙 ∈ ℤ ( ( 𝑦 + ( 𝑖 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧 ) ) ∧ ∃ 𝑗 ∈ ℤ ∃ 𝑘 ∈ ℤ ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ∧ ( 𝑧 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ) )
76	21 22 23 1 26 38 49 55 56 57 58 59 5 6 60 61 65 75	fourierdlem42	⊢ ( 𝜑 → { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ∈ Fin )
77		unfi	⊢ ( ( { 𝐶 , 𝐷 } ∈ Fin ∧ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ∈ Fin ) → ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ∈ Fin )
78	19 76 77	sylancr	⊢ ( 𝜑 → ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ∈ Fin )
79	9 78	eqeltrid	⊢ ( 𝜑 → 𝐻 ∈ Fin )
80		hashnncl	⊢ ( 𝐻 ∈ Fin → ( ( ♯ ‘ 𝐻 ) ∈ ℕ ↔ 𝐻 ≠ ∅ ) )
81	79 80	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) ∈ ℕ ↔ 𝐻 ≠ ∅ ) )
82	18 81	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ )
83	82	nnzd	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℤ )
84	5 7	ltned	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
85		hashprg	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 ≠ 𝐷 ↔ ( ♯ ‘ { 𝐶 , 𝐷 } ) = 2 ) )
86	5 6 85	syl2anc	⊢ ( 𝜑 → ( 𝐶 ≠ 𝐷 ↔ ( ♯ ‘ { 𝐶 , 𝐷 } ) = 2 ) )
87	84 86	mpbid	⊢ ( 𝜑 → ( ♯ ‘ { 𝐶 , 𝐷 } ) = 2 )
88	87	eqcomd	⊢ ( 𝜑 → 2 = ( ♯ ‘ { 𝐶 , 𝐷 } ) )
89		ssun1	⊢ { 𝐶 , 𝐷 } ⊆ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
90	89	a1i	⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
91	90 9	sseqtrrdi	⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ 𝐻 )
92		hashssle	⊢ ( ( 𝐻 ∈ Fin ∧ { 𝐶 , 𝐷 } ⊆ 𝐻 ) → ( ♯ ‘ { 𝐶 , 𝐷 } ) ≤ ( ♯ ‘ 𝐻 ) )
93	79 91 92	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ { 𝐶 , 𝐷 } ) ≤ ( ♯ ‘ 𝐻 ) )
94	88 93	eqbrtrd	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐻 ) )
95		eluz2	⊢ ( ( ♯ ‘ 𝐻 ) ∈ ( ℤ_≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ♯ ‘ 𝐻 ) ∈ ℤ ∧ 2 ≤ ( ♯ ‘ 𝐻 ) ) )
96	13 83 94 95	syl3anbrc	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ( ℤ_≥ ‘ 2 ) )
97		uz2m1nn	⊢ ( ( ♯ ‘ 𝐻 ) ∈ ( ℤ_≥ ‘ 2 ) → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ )
98	96 97	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ )
99	10 98	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
100		prssg	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ↔ { 𝐶 , 𝐷 } ⊆ ℝ ) )
101	5 6 100	syl2anc	⊢ ( 𝜑 → ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ↔ { 𝐶 , 𝐷 } ⊆ ℝ ) )
102	5 6 101	mpbi2and	⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ ℝ )
103		ssrab2	⊢ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ( 𝐶 [,] 𝐷 )
104	5 6	iccssred	⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
105	103 104	sstrid	⊢ ( 𝜑 → { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ℝ )
106	102 105	unssd	⊢ ( 𝜑 → ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ⊆ ℝ )
107	9 106	eqsstrid	⊢ ( 𝜑 → 𝐻 ⊆ ℝ )
108	79 107 11 10	fourierdlem36	⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
109		df-isom	⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
110	108 109	sylib	⊢ ( 𝜑 → ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
111	110	simpld	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 )
112		f1of	⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝐻 )
113	111 112	syl	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝐻 )
114	113 107	fssd	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
115		reex	⊢ ℝ ∈ V
116		ovex	⊢ ( 0 ... 𝑁 ) ∈ V
117	116	a1i	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
118		elmapg	⊢ ( ( ℝ ∈ V ∧ ( 0 ... 𝑁 ) ∈ V ) → ( 𝑆 ∈ ( ℝ ↑_m ( 0 ... 𝑁 ) ) ↔ 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ ) )
119	115 117 118	sylancr	⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑_m ( 0 ... 𝑁 ) ) ↔ 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ ) )
120	114 119	mpbird	⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑_m ( 0 ... 𝑁 ) ) )
121		df-f1o	⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 ↔ ( 𝑆 : ( 0 ... 𝑁 ) –1-1→ 𝐻 ∧ 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 ) )
122	111 121	sylib	⊢ ( 𝜑 → ( 𝑆 : ( 0 ... 𝑁 ) –1-1→ 𝐻 ∧ 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 ) )
123	122	simprd	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 )
124		dffo3	⊢ ( 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 ↔ ( 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝐻 ∧ ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ) )
125	123 124	sylib	⊢ ( 𝜑 → ( 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝐻 ∧ ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ) )
126	125	simprd	⊢ ( 𝜑 → ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) )
127		eqeq1	⊢ ( ℎ = 𝐶 → ( ℎ = ( 𝑆 ‘ 𝑦 ) ↔ 𝐶 = ( 𝑆 ‘ 𝑦 ) ) )
128		eqcom	⊢ ( 𝐶 = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑦 ) = 𝐶 )
129	127 128	bitrdi	⊢ ( ℎ = 𝐶 → ( ℎ = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) )
130	129	rexbidv	⊢ ( ℎ = 𝐶 → ( ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐶 ) )
131	130	rspcv	⊢ ( 𝐶 ∈ 𝐻 → ( ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) → ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐶 ) )
132	17 126 131	sylc	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐶 )
133		fveq2	⊢ ( 𝑦 = 0 → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 0 ) )
134	133	eqcomd	⊢ ( 𝑦 = 0 → ( 𝑆 ‘ 0 ) = ( 𝑆 ‘ 𝑦 ) )
135	134	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) = ( 𝑆 ‘ 𝑦 ) )
136		simplr	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 𝑦 ) = 𝐶 )
137	135 136	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) = 𝐶 )
138	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → 𝐶 ∈ ℝ )
139	137 138	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ∈ ℝ )
140	139 137	eqled	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ≤ 𝐶 )
141	140	3adantl2	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ≤ 𝐶 )
142	5	rexrd	⊢ ( 𝜑 → 𝐶 ∈ ℝ^* )
143	6	rexrd	⊢ ( 𝜑 → 𝐷 ∈ ℝ^* )
144	5 6 7	ltled	⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
145		lbicc2	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷 ) → 𝐶 ∈ ( 𝐶 [,] 𝐷 ) )
146	142 143 144 145	syl3anc	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐶 [,] 𝐷 ) )
147		ubicc2	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷 ) → 𝐷 ∈ ( 𝐶 [,] 𝐷 ) )
148	142 143 144 147	syl3anc	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 [,] 𝐷 ) )
149		prssg	⊢ ( ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) → ( ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) ↔ { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) ) )
150	146 148 149	syl2anc	⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) ↔ { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) ) )
151	146 148 150	mpbi2and	⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) )
152	103	a1i	⊢ ( 𝜑 → { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ( 𝐶 [,] 𝐷 ) )
153	151 152	unssd	⊢ ( 𝜑 → ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ⊆ ( 𝐶 [,] 𝐷 ) )
154	9 153	eqsstrid	⊢ ( 𝜑 → 𝐻 ⊆ ( 𝐶 [,] 𝐷 ) )
155		nnm1nn0	⊢ ( ( ♯ ‘ 𝐻 ) ∈ ℕ → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ₀ )
156	82 155	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) − 1 ) ∈ ℕ₀ )
157	10 156	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
158	157 43	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 0 ) )
159		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑁 ) )
160	158 159	syl	⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
161	113 160	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ 𝐻 )
162	154 161	sseldd	⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ ( 𝐶 [,] 𝐷 ) )
163	104 162	sseldd	⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ ℝ )
164	163	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ∈ ℝ )
165	164	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ∈ ℝ )
166	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑦 = 0 ) → 𝐶 ∈ ℝ )
167	166	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → 𝐶 ∈ ℝ )
168		elfzelz	⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑦 ∈ ℤ )
169	168	zred	⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑦 ∈ ℝ )
170	169	adantr	⊢ ( ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝑦 = 0 ) → 𝑦 ∈ ℝ )
171		elfzle1	⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑦 )
172	171	adantr	⊢ ( ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝑦 = 0 ) → 0 ≤ 𝑦 )
173		neqne	⊢ ( ¬ 𝑦 = 0 → 𝑦 ≠ 0 )
174	173	adantl	⊢ ( ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝑦 = 0 ) → 𝑦 ≠ 0 )
175	170 172 174	ne0gt0d	⊢ ( ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝑦 = 0 ) → 0 < 𝑦 )
176	175	3ad2antl2	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → 0 < 𝑦 )
177		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → 𝜑 )
178		simpl2	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → 𝑦 ∈ ( 0 ... 𝑁 ) )
179	110	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) )
180		breq1	⊢ ( 𝑥 = 0 → ( 𝑥 < 𝑦 ↔ 0 < 𝑦 ) )
181		fveq2	⊢ ( 𝑥 = 0 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 0 ) )
182	181	breq1d	⊢ ( 𝑥 = 0 → ( ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) )
183	180 182	bibi12d	⊢ ( 𝑥 = 0 → ( ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
184	183	ralbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
185	184	rspcv	⊢ ( 0 ∈ ( 0 ... 𝑁 ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
186	160 179 185	sylc	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) )
187	186	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) )
188	177 178 187	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 0 < 𝑦 ↔ ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) ) )
189	176 188	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) < ( 𝑆 ‘ 𝑦 ) )
190		simpl3	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 𝑦 ) = 𝐶 )
191	189 190	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) < 𝐶 )
192	165 167 191	ltled	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) ∧ ¬ 𝑦 = 0 ) → ( 𝑆 ‘ 0 ) ≤ 𝐶 )
193	141 192	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐶 ) → ( 𝑆 ‘ 0 ) ≤ 𝐶 )
194	193	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐶 → ( 𝑆 ‘ 0 ) ≤ 𝐶 ) )
195	132 194	mpd	⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ≤ 𝐶 )
196		elicc2	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ 0 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 0 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 0 ) ∧ ( 𝑆 ‘ 0 ) ≤ 𝐷 ) ) )
197	5 6 196	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 ‘ 0 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 0 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 0 ) ∧ ( 𝑆 ‘ 0 ) ≤ 𝐷 ) ) )
198	162 197	mpbid	⊢ ( 𝜑 → ( ( 𝑆 ‘ 0 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 0 ) ∧ ( 𝑆 ‘ 0 ) ≤ 𝐷 ) )
199	198	simp2d	⊢ ( 𝜑 → 𝐶 ≤ ( 𝑆 ‘ 0 ) )
200	163 5	letri3d	⊢ ( 𝜑 → ( ( 𝑆 ‘ 0 ) = 𝐶 ↔ ( ( 𝑆 ‘ 0 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝑆 ‘ 0 ) ) ) )
201	195 199 200	mpbir2and	⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) = 𝐶 )
202		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 0 ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
203	158 202	syl	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
204	113 203	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ∈ 𝐻 )
205	154 204	sseldd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ∈ ( 𝐶 [,] 𝐷 ) )
206		elicc2	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ 𝑁 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 𝑁 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ) ) )
207	5 6 206	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑁 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 𝑁 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ) ) )
208	205 207	mpbid	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑁 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑁 ) ∧ ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ) )
209	208	simp3d	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 )
210		prid2g	⊢ ( 𝐷 ∈ ℝ → 𝐷 ∈ { 𝐶 , 𝐷 } )
211		elun1	⊢ ( 𝐷 ∈ { 𝐶 , 𝐷 } → 𝐷 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
212	6 210 211	3syl	⊢ ( 𝜑 → 𝐷 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
213	212 9	eleqtrrdi	⊢ ( 𝜑 → 𝐷 ∈ 𝐻 )
214		eqeq1	⊢ ( ℎ = 𝐷 → ( ℎ = ( 𝑆 ‘ 𝑦 ) ↔ 𝐷 = ( 𝑆 ‘ 𝑦 ) ) )
215		eqcom	⊢ ( 𝐷 = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑦 ) = 𝐷 )
216	214 215	bitrdi	⊢ ( ℎ = 𝐷 → ( ℎ = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) )
217	216	rexbidv	⊢ ( ℎ = 𝐷 → ( ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐷 ) )
218	217	rspcv	⊢ ( 𝐷 ∈ 𝐻 → ( ∀ ℎ ∈ 𝐻 ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ℎ = ( 𝑆 ‘ 𝑦 ) → ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐷 ) )
219	213 126 218	sylc	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐷 )
220	215	biimpri	⊢ ( ( 𝑆 ‘ 𝑦 ) = 𝐷 → 𝐷 = ( 𝑆 ‘ 𝑦 ) )
221	220	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) → 𝐷 = ( 𝑆 ‘ 𝑦 ) )
222	114	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 𝑦 ) ∈ ℝ )
223	104 205	sseldd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ∈ ℝ )
224	223	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 𝑁 ) ∈ ℝ )
225	169	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → 𝑦 ∈ ℝ )
226		elfzel2	⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
227	226	zred	⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℝ )
228	227	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
229		elfzle2	⊢ ( 𝑦 ∈ ( 0 ... 𝑁 ) → 𝑦 ≤ 𝑁 )
230	229	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → 𝑦 ≤ 𝑁 )
231	225 228 230	lensymd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ¬ 𝑁 < 𝑦 )
232		breq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 < 𝑦 ↔ 𝑁 < 𝑦 ) )
233		fveq2	⊢ ( 𝑥 = 𝑁 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑁 ) )
234	233	breq1d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) )
235	232 234	bibi12d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
236	235	ralbidv	⊢ ( 𝑥 = 𝑁 → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
237	236	rspcv	⊢ ( 𝑁 ∈ ( 0 ... 𝑁 ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
238	203 179 237	sylc	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) )
239	238	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 < 𝑦 ↔ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) ) )
240	231 239	mtbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝑆 ‘ 𝑁 ) < ( 𝑆 ‘ 𝑦 ) )
241	222 224 240	nltled	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 𝑦 ) ≤ ( 𝑆 ‘ 𝑁 ) )
242	241	3adant3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) → ( 𝑆 ‘ 𝑦 ) ≤ ( 𝑆 ‘ 𝑁 ) )
243	221 242	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑆 ‘ 𝑦 ) = 𝐷 ) → 𝐷 ≤ ( 𝑆 ‘ 𝑁 ) )
244	243	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑦 ) = 𝐷 → 𝐷 ≤ ( 𝑆 ‘ 𝑁 ) ) )
245	219 244	mpd	⊢ ( 𝜑 → 𝐷 ≤ ( 𝑆 ‘ 𝑁 ) )
246	223 6	letri3d	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑁 ) = 𝐷 ↔ ( ( 𝑆 ‘ 𝑁 ) ≤ 𝐷 ∧ 𝐷 ≤ ( 𝑆 ‘ 𝑁 ) ) ) )
247	209 245 246	mpbir2and	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) = 𝐷 )
248		elfzoelz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ℤ )
249	248	zred	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ℝ )
250	249	ltp1d	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 < ( 𝑖 + 1 ) )
251	250	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 < ( 𝑖 + 1 ) )
252	179	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) )
253		elfzofz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
254	253	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
255		fzofzp1	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) )
256	255	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) )
257		breq1	⊢ ( 𝑥 = 𝑖 → ( 𝑥 < 𝑦 ↔ 𝑖 < 𝑦 ) )
258		fveq2	⊢ ( 𝑥 = 𝑖 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑖 ) )
259	258	breq1d	⊢ ( 𝑥 = 𝑖 → ( ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑦 ) ) )
260	257 259	bibi12d	⊢ ( 𝑥 = 𝑖 → ( ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑖 < 𝑦 ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑦 ) ) ) )
261		breq2	⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( 𝑖 < 𝑦 ↔ 𝑖 < ( 𝑖 + 1 ) ) )
262		fveq2	⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
263	262	breq2d	⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑦 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
264	261 263	bibi12d	⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( ( 𝑖 < 𝑦 ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
265	260 264	rspc2v	⊢ ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) → ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
266	254 256 265	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( 𝑥 < 𝑦 ↔ ( 𝑆 ‘ 𝑥 ) < ( 𝑆 ‘ 𝑦 ) ) → ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
267	252 266	mpd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 < ( 𝑖 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
268	251 267	mpbid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
269	268	ralrimiva	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
270	201 247 269	jca31	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
271	8	fourierdlem2	⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑_m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
272	99 271	syl	⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑_m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
273	120 270 272	mpbir2and	⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
274	99 273 108	jca31	⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )

Metamath Proof Explorer

Theorem fourierdlem54

Proof