fourierdlem80

Description: The derivative of O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem80.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem80.xre	$⊢ φ \to X \in ℝ$
	fourierdlem80.a	$⊢ φ \to A \in ℝ$
	fourierdlem80.b	$⊢ φ \to B \in ℝ$
	fourierdlem80.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
	fourierdlem80.n0	$⊢ φ \to \neg 0 \in [A, B]$
	fourierdlem80.c	$⊢ φ \to C \in ℝ$
	fourierdlem80.o	$⊢ O = (s \in [A, B] ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
	fourierdlem80.i	$⊢ I = (X + S (j), X + S (j + 1))$
	fourierdlem80.fbdioo	$⊢ (φ \land j \in (0 ..^N)) \to \exists w \in ℝ \forall t \in I \|F (t)\| \leq w$
	fourierdlem80.fdvbdioo	$⊢ (φ \land j \in (0 ..^N)) \to \exists z \in ℝ \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z$
	fourierdlem80.sf	$⊢ φ \to S : (0 \dots N) ⟶ [A, B]$
	fourierdlem80.slt	$⊢ (φ \land j \in (0 ..^N)) \to S (j) < S (j + 1)$
	fourierdlem80.sjss	$⊢ (φ \land j \in (0 ..^N)) \to [S (j), S (j + 1)] \subseteq [A, B]$
	fourierdlem80.relioo	$⊢ ((φ \land r \in [A, B]) \land \neg r \in ran S) \to \exists k \in (0 ..^N) r \in (S (k), S (k + 1))$
	fdv	$⊢ (φ \land j \in (0 ..^N)) \to {({F ↾}_{I})}_{ℝ}^{'} : I ⟶ ℝ$
	fourierdlem80.y	$⊢ Y = (s \in (S (j), S (j + 1)) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
	fourierdlem80.ch	$⊢ χ \leftrightarrow (((((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ) \land \forall t \in I \|F (t)\| \leq w) \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)$
Assertion	fourierdlem80	$⊢ φ \to \exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|O_{ℝ}^{'} (s)\| \leq b$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem80.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem80.xre	$⊢ φ \to X \in ℝ$
3		fourierdlem80.a	$⊢ φ \to A \in ℝ$
4		fourierdlem80.b	$⊢ φ \to B \in ℝ$
5		fourierdlem80.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
6		fourierdlem80.n0	$⊢ φ \to \neg 0 \in [A, B]$
7		fourierdlem80.c	$⊢ φ \to C \in ℝ$
8		fourierdlem80.o	$⊢ O = (s \in [A, B] ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
9		fourierdlem80.i	$⊢ I = (X + S (j), X + S (j + 1))$
10		fourierdlem80.fbdioo	$⊢ (φ \land j \in (0 ..^N)) \to \exists w \in ℝ \forall t \in I \|F (t)\| \leq w$
11		fourierdlem80.fdvbdioo	$⊢ (φ \land j \in (0 ..^N)) \to \exists z \in ℝ \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z$
12		fourierdlem80.sf	$⊢ φ \to S : (0 \dots N) ⟶ [A, B]$
13		fourierdlem80.slt	$⊢ (φ \land j \in (0 ..^N)) \to S (j) < S (j + 1)$
14		fourierdlem80.sjss	$⊢ (φ \land j \in (0 ..^N)) \to [S (j), S (j + 1)] \subseteq [A, B]$
15		fourierdlem80.relioo	$⊢ ((φ \land r \in [A, B]) \land \neg r \in ran S) \to \exists k \in (0 ..^N) r \in (S (k), S (k + 1))$
16		fdv	$⊢ (φ \land j \in (0 ..^N)) \to {({F ↾}_{I})}_{ℝ}^{'} : I ⟶ ℝ$
17		fourierdlem80.y	$⊢ Y = (s \in (S (j), S (j + 1)) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
18		fourierdlem80.ch	$⊢ χ \leftrightarrow (((((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ) \land \forall t \in I \|F (t)\| \leq w) \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)$
19		oveq2	$⊢ s = t \to X + s = X + t$
20	19	fveq2d	$⊢ s = t \to F (X + s) = F (X + t)$
21	20	oveq1d	$⊢ s = t \to F (X + s) - C = F (X + t) - C$
22		oveq1	$⊢ s = t \to \frac{s}{2} = \frac{t}{2}$
23	22	fveq2d	$⊢ s = t \to \sin (\frac{s}{2}) = \sin (\frac{t}{2})$
24	23	oveq2d	$⊢ s = t \to 2 \sin (\frac{s}{2}) = 2 \sin (\frac{t}{2})$
25	21 24	oveq12d	$⊢ s = t \to \frac{F (X + s) - C}{2 \sin (\frac{s}{2})} = \frac{F (X + t) - C}{2 \sin (\frac{t}{2})}$
26	25	cbvmptv	$⊢ (s \in [A, B] ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})}) = (t \in [A, B] ⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})$
27	8 26	eqtr2i	$⊢ (t \in [A, B] ⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})}) = O$
28	27	oveq2i	$⊢ \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t} = ℝ D O$
29	28	dmeqi	$⊢ dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t} = dom O_{ℝ}^{'}$
30	29	ineq2i	$⊢ ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t} = ran S \cap dom O_{ℝ}^{'}$
31	30	sneqi	$⊢ \{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} = \{ran S \cap dom O_{ℝ}^{'}\}$
32	31	uneq1i	$⊢ \{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) = \{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
33		snfi	$⊢ \{ran S \cap dom O_{ℝ}^{'}\} \in Fin$
34		fzofi	$⊢ (0 ..^N) \in Fin$
35		eqid	$⊢ (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) = (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
36	35	rnmptfi	$⊢ (0 ..^N) \in Fin \to ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \in Fin$
37	34 36	ax-mp	$⊢ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \in Fin$
38		unfi	$⊢ (\{ran S \cap dom O_{ℝ}^{'}\} \in Fin \land ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \in Fin) \to \{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \in Fin$
39	33 37 38	mp2an	$⊢ \{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \in Fin$
40	39	a1i	$⊢ φ \to \{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \in Fin$
41	32 40	eqeltrid	$⊢ φ \to \{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \in Fin$
42		id	$⊢ s \in ⋃ (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to s \in ⋃ (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
43	32	unieqi	$⊢ ⋃ (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) = ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
44	42 43	eleqtrdi	$⊢ s \in ⋃ (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
45		simpl	$⊢ (φ \land s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to φ$
46		uniun	$⊢ ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) = ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \cup ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
47	46	eleq2i	$⊢ s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \leftrightarrow s \in (⋃ \{ran S \cap dom O_{ℝ}^{'}\} \cup ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
48		elun	$⊢ s \in (⋃ \{ran S \cap dom O_{ℝ}^{'}\} \cup ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \leftrightarrow (s \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \lor s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
49	47 48	sylbb	$⊢ s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to (s \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \lor s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
50	49	adantl	$⊢ (φ \land s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to (s \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \lor s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
51		ovex	$⊢ (0 \dots N) \in V$
52	51	a1i	$⊢ φ \to (0 \dots N) \in V$
53		fex	$⊢ (S : (0 \dots N) ⟶ [A, B] \land (0 \dots N) \in V) \to S \in V$
54	12 52 53	syl2anc	$⊢ φ \to S \in V$
55		rnexg	$⊢ S \in V \to ran S \in V$
56	54 55	syl	$⊢ φ \to ran S \in V$
57		inex1g	$⊢ ran S \in V \to ran S \cap dom O_{ℝ}^{'} \in V$
58	56 57	syl	$⊢ φ \to ran S \cap dom O_{ℝ}^{'} \in V$
59		unisng	$⊢ ran S \cap dom O_{ℝ}^{'} \in V \to ⋃ \{ran S \cap dom O_{ℝ}^{'}\} = ran S \cap dom O_{ℝ}^{'}$
60	58 59	syl	$⊢ φ \to ⋃ \{ran S \cap dom O_{ℝ}^{'}\} = ran S \cap dom O_{ℝ}^{'}$
61	60	eleq2d	$⊢ φ \to (s \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \leftrightarrow s \in (ran S \cap dom O_{ℝ}^{'}))$
62	61	adantr	$⊢ (φ \land s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to (s \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \leftrightarrow s \in (ran S \cap dom O_{ℝ}^{'}))$
63	62	orbi1d	$⊢ (φ \land s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to ((s \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \lor s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \leftrightarrow (s \in (ran S \cap dom O_{ℝ}^{'}) \lor s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))))$
64	50 63	mpbid	$⊢ (φ \land s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to (s \in (ran S \cap dom O_{ℝ}^{'}) \lor s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
65		dvf	$⊢ O_{ℝ}^{'} : dom O_{ℝ}^{'} ⟶ ℂ$
66	65	a1i	$⊢ s \in (ran S \cap dom O_{ℝ}^{'}) \to O_{ℝ}^{'} : dom O_{ℝ}^{'} ⟶ ℂ$
67		elinel2	$⊢ s \in (ran S \cap dom O_{ℝ}^{'}) \to s \in dom O_{ℝ}^{'}$
68	66 67	ffvelrnd	$⊢ s \in (ran S \cap dom O_{ℝ}^{'}) \to O_{ℝ}^{'} (s) \in ℂ$
69	68	adantl	$⊢ (φ \land s \in (ran S \cap dom O_{ℝ}^{'})) \to O_{ℝ}^{'} (s) \in ℂ$
70		ovex	$⊢ (S (j), S (j + 1)) \in V$
71	70	dfiun3	$⊢ ⋃_{j \in (0 ..^N)} (S (j), S (j + 1)) = ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
72	71	eleq2i	$⊢ s \in ⋃_{j \in (0 ..^N)} (S (j), S (j + 1)) \leftrightarrow s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
73	72	biimpri	$⊢ s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \to s \in ⋃_{j \in (0 ..^N)} (S (j), S (j + 1))$
74	73	adantl	$⊢ (φ \land s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to s \in ⋃_{j \in (0 ..^N)} (S (j), S (j + 1))$
75		eliun	$⊢ s \in ⋃_{j \in (0 ..^N)} (S (j), S (j + 1)) \leftrightarrow \exists j \in (0 ..^N) s \in (S (j), S (j + 1))$
76	74 75	sylib	$⊢ (φ \land s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to \exists j \in (0 ..^N) s \in (S (j), S (j + 1))$
77		nfv	$⊢ Ⅎ j φ$
78		nfmpt1	$⊢ \underline{Ⅎ} j (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
79	78	nfrn	$⊢ \underline{Ⅎ} j ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
80	79	nfuni	$⊢ \underline{Ⅎ} j ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
81	80	nfcri	$⊢ Ⅎ j s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
82	77 81	nfan	$⊢ Ⅎ j (φ \land s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
83		nfv	$⊢ Ⅎ j O_{ℝ}^{'} (s) \in ℂ$
84	65	a1i	$⊢ (φ \land j \in (0 ..^N) \land s \in (S (j), S (j + 1))) \to O_{ℝ}^{'} : dom O_{ℝ}^{'} ⟶ ℂ$
85	8	reseq1i	$⊢ {O ↾}_{(S (j), S (j + 1))} = {(s \in [A, B] ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})}) ↾}_{(S (j), S (j + 1))}$
86		ioossicc	$⊢ (S (j), S (j + 1)) \subseteq [S (j), S (j + 1)]$
87	86 14	sstrid	$⊢ (φ \land j \in (0 ..^N)) \to (S (j), S (j + 1)) \subseteq [A, B]$
88	87	resmptd	$⊢ (φ \land j \in (0 ..^N)) \to {(s \in [A, B] ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})}) ↾}_{(S (j), S (j + 1))} = (s \in (S (j), S (j + 1)) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
89	85 88	syl5eq	$⊢ (φ \land j \in (0 ..^N)) \to {O ↾}_{(S (j), S (j + 1))} = (s \in (S (j), S (j + 1)) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
90	89 17	syl6reqr	$⊢ (φ \land j \in (0 ..^N)) \to Y = {O ↾}_{(S (j), S (j + 1))}$
91	90	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to ℝ D Y = ℝ D ({O ↾}_{(S (j), S (j + 1))})$
92		ax-resscn	$⊢ ℝ \subseteq ℂ$
93	92	a1i	$⊢ φ \to ℝ \subseteq ℂ$
94	1	adantr	$⊢ (φ \land s \in [A, B]) \to F : ℝ ⟶ ℝ$
95	2	adantr	$⊢ (φ \land s \in [A, B]) \to X \in ℝ$
96	3 4	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
97	96	sselda	$⊢ (φ \land s \in [A, B]) \to s \in ℝ$
98	95 97	readdcld	$⊢ (φ \land s \in [A, B]) \to X + s \in ℝ$
99	94 98	ffvelrnd	$⊢ (φ \land s \in [A, B]) \to F (X + s) \in ℝ$
100	99	recnd	$⊢ (φ \land s \in [A, B]) \to F (X + s) \in ℂ$
101	7	recnd	$⊢ φ \to C \in ℂ$
102	101	adantr	$⊢ (φ \land s \in [A, B]) \to C \in ℂ$
103	100 102	subcld	$⊢ (φ \land s \in [A, B]) \to F (X + s) - C \in ℂ$
104		2cnd	$⊢ (φ \land s \in [A, B]) \to 2 \in ℂ$
105	96 93	sstrd	$⊢ φ \to [A, B] \subseteq ℂ$
106	105	sselda	$⊢ (φ \land s \in [A, B]) \to s \in ℂ$
107	106	halfcld	$⊢ (φ \land s \in [A, B]) \to \frac{s}{2} \in ℂ$
108	107	sincld	$⊢ (φ \land s \in [A, B]) \to \sin (\frac{s}{2}) \in ℂ$
109	104 108	mulcld	$⊢ (φ \land s \in [A, B]) \to 2 \sin (\frac{s}{2}) \in ℂ$
110		2ne0	$⊢ 2 \neq 0$
111	110	a1i	$⊢ (φ \land s \in [A, B]) \to 2 \neq 0$
112	5	sselda	$⊢ (φ \land s \in [A, B]) \to s \in [- π, π]$
113		eqcom	$⊢ s = 0 \leftrightarrow 0 = s$
114	113	biimpi	$⊢ s = 0 \to 0 = s$
115	114	adantl	$⊢ (s \in [A, B] \land s = 0) \to 0 = s$
116		simpl	$⊢ (s \in [A, B] \land s = 0) \to s \in [A, B]$
117	115 116	eqeltrd	$⊢ (s \in [A, B] \land s = 0) \to 0 \in [A, B]$
118	117	adantll	$⊢ ((φ \land s \in [A, B]) \land s = 0) \to 0 \in [A, B]$
119	6	ad2antrr	$⊢ ((φ \land s \in [A, B]) \land s = 0) \to \neg 0 \in [A, B]$
120	118 119	pm2.65da	$⊢ (φ \land s \in [A, B]) \to \neg s = 0$
121	120	neqned	$⊢ (φ \land s \in [A, B]) \to s \neq 0$
122		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
123	112 121 122	syl2anc	$⊢ (φ \land s \in [A, B]) \to \sin (\frac{s}{2}) \neq 0$
124	104 108 111 123	mulne0d	$⊢ (φ \land s \in [A, B]) \to 2 \sin (\frac{s}{2}) \neq 0$
125	103 109 124	divcld	$⊢ (φ \land s \in [A, B]) \to \frac{F (X + s) - C}{2 \sin (\frac{s}{2})} \in ℂ$
126	125 8	fmptd	$⊢ φ \to O : [A, B] ⟶ ℂ$
127		ioossre	$⊢ (S (j), S (j + 1)) \subseteq ℝ$
128	127	a1i	$⊢ φ \to (S (j), S (j + 1)) \subseteq ℝ$
129		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
130	129	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
131	129 130	dvres	$⊢ ((ℝ \subseteq ℂ \land O : [A, B] ⟶ ℂ) \land ([A, B] \subseteq ℝ \land (S (j), S (j + 1)) \subseteq ℝ)) \to ℝ D ({O ↾}_{(S (j), S (j + 1))}) = {O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))}$
132	93 126 96 128 131	syl22anc	$⊢ φ \to ℝ D ({O ↾}_{(S (j), S (j + 1))}) = {O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))}$
133		ioontr	$⊢ int (topGen (ran (.))) ((S (j), S (j + 1))) = (S (j), S (j + 1))$
134	133	reseq2i	$⊢ {O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))} = {O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}$
135	132 134	syl6eq	$⊢ φ \to ℝ D ({O ↾}_{(S (j), S (j + 1))}) = {O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}$
136	135	adantr	$⊢ (φ \land j \in (0 ..^N)) \to ℝ D ({O ↾}_{(S (j), S (j + 1))}) = {O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}$
137	91 136	eqtr2d	$⊢ (φ \land j \in (0 ..^N)) \to {O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))} = ℝ D Y$
138	137	dmeqd	$⊢ (φ \land j \in (0 ..^N)) \to dom ({O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}) = dom Y_{ℝ}^{'}$
139	1	adantr	$⊢ (φ \land j \in (0 ..^N)) \to F : ℝ ⟶ ℝ$
140	2	adantr	$⊢ (φ \land j \in (0 ..^N)) \to X \in ℝ$
141	96	adantr	$⊢ (φ \land j \in (0 ..^N)) \to [A, B] \subseteq ℝ$
142	12	adantr	$⊢ (φ \land j \in (0 ..^N)) \to S : (0 \dots N) ⟶ [A, B]$
143		elfzofz	$⊢ j \in (0 ..^N) \to j \in (0 \dots N)$
144	143	adantl	$⊢ (φ \land j \in (0 ..^N)) \to j \in (0 \dots N)$
145	142 144	ffvelrnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in [A, B]$
146	141 145	sseldd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in ℝ$
147		fzofzp1	$⊢ j \in (0 ..^N) \to j + 1 \in (0 \dots N)$
148	147	adantl	$⊢ (φ \land j \in (0 ..^N)) \to j + 1 \in (0 \dots N)$
149	142 148	ffvelrnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in [A, B]$
150	141 149	sseldd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in ℝ$
151	9	feq2i	$⊢ {({F ↾}_{I})}_{ℝ}^{'} : I ⟶ ℝ \leftrightarrow {({F ↾}_{I})}_{ℝ}^{'} : (X + S (j), X + S (j + 1)) ⟶ ℝ$
152	16 151	sylib	$⊢ (φ \land j \in (0 ..^N)) \to {({F ↾}_{I})}_{ℝ}^{'} : (X + S (j), X + S (j + 1)) ⟶ ℝ$
153	9	reseq2i	$⊢ {F ↾}_{I} = {F ↾}_{(X + S (j), X + S (j + 1))}$
154	153	oveq2i	$⊢ ℝ D ({F ↾}_{I}) = ℝ D ({F ↾}_{(X + S (j), X + S (j + 1))})$
155	154	feq1i	$⊢ {({F ↾}_{I})}_{ℝ}^{'} : (X + S (j), X + S (j + 1)) ⟶ ℝ \leftrightarrow {({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} : (X + S (j), X + S (j + 1)) ⟶ ℝ$
156	152 155	sylib	$⊢ (φ \land j \in (0 ..^N)) \to {({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} : (X + S (j), X + S (j + 1)) ⟶ ℝ$
157	5	adantr	$⊢ (φ \land j \in (0 ..^N)) \to [A, B] \subseteq [- π, π]$
158	87 157	sstrd	$⊢ (φ \land j \in (0 ..^N)) \to (S (j), S (j + 1)) \subseteq [- π, π]$
159	6	adantr	$⊢ (φ \land j \in (0 ..^N)) \to \neg 0 \in [A, B]$
160	87 159	ssneldd	$⊢ (φ \land j \in (0 ..^N)) \to \neg 0 \in (S (j), S (j + 1))$
161	7	adantr	$⊢ (φ \land j \in (0 ..^N)) \to C \in ℝ$
162	139 140 146 150 156 158 160 161 17	fourierdlem57	$⊢ (((φ \land j \in (0 ..^N)) \to (Y_{ℝ}^{'} : (S (j), S (j + 1)) ⟶ ℝ \land ℝ D Y = (s \in (S (j), S (j + 1)) ⟼ \frac{{({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}))) \land \frac{d (s \in (S (j), S (j + 1))⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (S (j), S (j + 1)) ⟼ \cos (\frac{s}{2})))$
163	162	simpli	$⊢ (φ \land j \in (0 ..^N)) \to (Y_{ℝ}^{'} : (S (j), S (j + 1)) ⟶ ℝ \land ℝ D Y = (s \in (S (j), S (j + 1)) ⟼ \frac{{({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}))$
164	163	simpld	$⊢ (φ \land j \in (0 ..^N)) \to Y_{ℝ}^{'} : (S (j), S (j + 1)) ⟶ ℝ$
165		fdm	$⊢ Y_{ℝ}^{'} : (S (j), S (j + 1)) ⟶ ℝ \to dom Y_{ℝ}^{'} = (S (j), S (j + 1))$
166	164 165	syl	$⊢ (φ \land j \in (0 ..^N)) \to dom Y_{ℝ}^{'} = (S (j), S (j + 1))$
167	138 166	eqtr2d	$⊢ (φ \land j \in (0 ..^N)) \to (S (j), S (j + 1)) = dom ({O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))})$
168		resss	$⊢ {O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))} \subseteq ℝ D O$
169		dmss	$⊢ {O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))} \subseteq ℝ D O \to dom ({O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}) \subseteq dom O_{ℝ}^{'}$
170	168 169	mp1i	$⊢ (φ \land j \in (0 ..^N)) \to dom ({O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}) \subseteq dom O_{ℝ}^{'}$
171	167 170	eqsstrd	$⊢ (φ \land j \in (0 ..^N)) \to (S (j), S (j + 1)) \subseteq dom O_{ℝ}^{'}$
172	171	3adant3	$⊢ (φ \land j \in (0 ..^N) \land s \in (S (j), S (j + 1))) \to (S (j), S (j + 1)) \subseteq dom O_{ℝ}^{'}$
173		simp3	$⊢ (φ \land j \in (0 ..^N) \land s \in (S (j), S (j + 1))) \to s \in (S (j), S (j + 1))$
174	172 173	sseldd	$⊢ (φ \land j \in (0 ..^N) \land s \in (S (j), S (j + 1))) \to s \in dom O_{ℝ}^{'}$
175	84 174	ffvelrnd	$⊢ (φ \land j \in (0 ..^N) \land s \in (S (j), S (j + 1))) \to O_{ℝ}^{'} (s) \in ℂ$
176	175	3exp	$⊢ φ \to (j \in (0 ..^N) \to (s \in (S (j), S (j + 1)) \to O_{ℝ}^{'} (s) \in ℂ))$
177	176	adantr	$⊢ (φ \land s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to (j \in (0 ..^N) \to (s \in (S (j), S (j + 1)) \to O_{ℝ}^{'} (s) \in ℂ))$
178	82 83 177	rexlimd	$⊢ (φ \land s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to (\exists j \in (0 ..^N) s \in (S (j), S (j + 1)) \to O_{ℝ}^{'} (s) \in ℂ)$
179	76 178	mpd	$⊢ (φ \land s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to O_{ℝ}^{'} (s) \in ℂ$
180	69 179	jaodan	$⊢ (φ \land (s \in (ran S \cap dom O_{ℝ}^{'}) \lor s \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to O_{ℝ}^{'} (s) \in ℂ$
181	45 64 180	syl2anc	$⊢ (φ \land s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to O_{ℝ}^{'} (s) \in ℂ$
182	181	abscld	$⊢ (φ \land s \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to \|O_{ℝ}^{'} (s)\| \in ℝ$
183	44 182	sylan2	$⊢ (φ \land s \in ⋃ (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to \|O_{ℝ}^{'} (s)\| \in ℝ$
184		id	$⊢ r \in (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to r \in (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
185	184 32	eleqtrdi	$⊢ r \in (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to r \in (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
186		elsni	$⊢ r \in \{ran S \cap dom O_{ℝ}^{'}\} \to r = ran S \cap dom O_{ℝ}^{'}$
187		simpr	$⊢ (φ \land r = ran S \cap dom O_{ℝ}^{'}) \to r = ran S \cap dom O_{ℝ}^{'}$
188		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
189		rnffi	$⊢ (S : (0 \dots N) ⟶ [A, B] \land (0 \dots N) \in Fin) \to ran S \in Fin$
190	12 188 189	syl2anc	$⊢ φ \to ran S \in Fin$
191		infi	$⊢ ran S \in Fin \to ran S \cap dom O_{ℝ}^{'} \in Fin$
192	190 191	syl	$⊢ φ \to ran S \cap dom O_{ℝ}^{'} \in Fin$
193	192	adantr	$⊢ (φ \land r = ran S \cap dom O_{ℝ}^{'}) \to ran S \cap dom O_{ℝ}^{'} \in Fin$
194	187 193	eqeltrd	$⊢ (φ \land r = ran S \cap dom O_{ℝ}^{'}) \to r \in Fin$
195		nfv	$⊢ Ⅎ s φ$
196		nfcv	$⊢ \underline{Ⅎ} s ran S$
197		nfcv	$⊢ \underline{Ⅎ} s ℝ$
198		nfcv	$⊢ \underline{Ⅎ} s D$
199		nfmpt1	$⊢ \underline{Ⅎ} s (s \in [A, B] ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
200	8 199	nfcxfr	$⊢ \underline{Ⅎ} s O$
201	197 198 200	nfov	$⊢ \underline{Ⅎ} s O_{ℝ}^{'}$
202	201	nfdm	$⊢ \underline{Ⅎ} s dom O_{ℝ}^{'}$
203	196 202	nfin	$⊢ \underline{Ⅎ} s (ran S \cap dom O_{ℝ}^{'})$
204	203	nfeq2	$⊢ Ⅎ s r = ran S \cap dom O_{ℝ}^{'}$
205	195 204	nfan	$⊢ Ⅎ s (φ \land r = ran S \cap dom O_{ℝ}^{'})$
206		simpr	$⊢ (r = ran S \cap dom O_{ℝ}^{'} \land s \in r) \to s \in r$
207		simpl	$⊢ (r = ran S \cap dom O_{ℝ}^{'} \land s \in r) \to r = ran S \cap dom O_{ℝ}^{'}$
208	206 207	eleqtrd	$⊢ (r = ran S \cap dom O_{ℝ}^{'} \land s \in r) \to s \in (ran S \cap dom O_{ℝ}^{'})$
209	208 67	syl	$⊢ (r = ran S \cap dom O_{ℝ}^{'} \land s \in r) \to s \in dom O_{ℝ}^{'}$
210	209	adantll	$⊢ ((φ \land r = ran S \cap dom O_{ℝ}^{'}) \land s \in r) \to s \in dom O_{ℝ}^{'}$
211	65	ffvelrni	$⊢ s \in dom O_{ℝ}^{'} \to O_{ℝ}^{'} (s) \in ℂ$
212	211	abscld	$⊢ s \in dom O_{ℝ}^{'} \to \|O_{ℝ}^{'} (s)\| \in ℝ$
213	210 212	syl	$⊢ ((φ \land r = ran S \cap dom O_{ℝ}^{'}) \land s \in r) \to \|O_{ℝ}^{'} (s)\| \in ℝ$
214	213	ex	$⊢ (φ \land r = ran S \cap dom O_{ℝ}^{'}) \to (s \in r \to \|O_{ℝ}^{'} (s)\| \in ℝ)$
215	205 214	ralrimi	$⊢ (φ \land r = ran S \cap dom O_{ℝ}^{'}) \to \forall s \in r \|O_{ℝ}^{'} (s)\| \in ℝ$
216		fimaxre3	$⊢ (r \in Fin \land \forall s \in r \|O_{ℝ}^{'} (s)\| \in ℝ) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
217	194 215 216	syl2anc	$⊢ (φ \land r = ran S \cap dom O_{ℝ}^{'}) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
218	186 217	sylan2	$⊢ (φ \land r \in \{ran S \cap dom O_{ℝ}^{'}\}) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
219	218	adantlr	$⊢ ((φ \land r \in (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \land r \in \{ran S \cap dom O_{ℝ}^{'}\}) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
220		simpll	$⊢ ((φ \land r \in (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \land \neg r \in \{ran S \cap dom O_{ℝ}^{'}\}) \to φ$
221		elunnel1	$⊢ (r \in (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \land \neg r \in \{ran S \cap dom O_{ℝ}^{'}\}) \to r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
222	221	adantll	$⊢ ((φ \land r \in (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \land \neg r \in \{ran S \cap dom O_{ℝ}^{'}\}) \to r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
223		vex	$⊢ r \in V$
224	35	elrnmpt	$⊢ r \in V \to (r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \leftrightarrow \exists j \in (0 ..^N) r = (S (j), S (j + 1)))$
225	223 224	ax-mp	$⊢ r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \leftrightarrow \exists j \in (0 ..^N) r = (S (j), S (j + 1))$
226	225	biimpi	$⊢ r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \to \exists j \in (0 ..^N) r = (S (j), S (j + 1))$
227	226	adantl	$⊢ (φ \land r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to \exists j \in (0 ..^N) r = (S (j), S (j + 1))$
228	79	nfcri	$⊢ Ⅎ j r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
229	77 228	nfan	$⊢ Ⅎ j (φ \land r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
230		nfv	$⊢ Ⅎ j \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
231		reeanv	$⊢ \exists w \in ℝ \exists z \in ℝ (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z) \leftrightarrow (\exists w \in ℝ \forall t \in I \|F (t)\| \leq w \land \exists z \in ℝ \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)$
232	10 11 231	sylanbrc	$⊢ (φ \land j \in (0 ..^N)) \to \exists w \in ℝ \exists z \in ℝ (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)$
233		simp1	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to (φ \land j \in (0 ..^N))$
234		simp2l	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to w \in ℝ$
235		simp2r	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to z \in ℝ$
236	233 234 235	jca31	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to (((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ)$
237		simp3l	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to \forall t \in I \|F (t)\| \leq w$
238		simp3r	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z$
239	236 237 238	jca31	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to (((((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ) \land \forall t \in I \|F (t)\| \leq w) \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)$
240	239 18	sylibr	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to χ$
241	18	biimpi	$⊢ χ \to (((((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ) \land \forall t \in I \|F (t)\| \leq w) \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)$
242		simp-5l	$⊢ (((((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ) \land \forall t \in I \|F (t)\| \leq w) \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z) \to φ$
243	241 242	syl	$⊢ χ \to φ$
244	243 1	syl	$⊢ χ \to F : ℝ ⟶ ℝ$
245	243 2	syl	$⊢ χ \to X \in ℝ$
246		simp-4l	$⊢ (((((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ) \land \forall t \in I \|F (t)\| \leq w) \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z) \to (φ \land j \in (0 ..^N))$
247	241 246	syl	$⊢ χ \to (φ \land j \in (0 ..^N))$
248	247 146	syl	$⊢ χ \to S (j) \in ℝ$
249	247 150	syl	$⊢ χ \to S (j + 1) \in ℝ$
250	247 13	syl	$⊢ χ \to S (j) < S (j + 1)$
251	14 157	sstrd	$⊢ (φ \land j \in (0 ..^N)) \to [S (j), S (j + 1)] \subseteq [- π, π]$
252	247 251	syl	$⊢ χ \to [S (j), S (j + 1)] \subseteq [- π, π]$
253	14 159	ssneldd	$⊢ (φ \land j \in (0 ..^N)) \to \neg 0 \in [S (j), S (j + 1)]$
254	247 253	syl	$⊢ χ \to \neg 0 \in [S (j), S (j + 1)]$
255	247 156	syl	$⊢ χ \to {({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} : (X + S (j), X + S (j + 1)) ⟶ ℝ$
256		simp-4r	$⊢ (((((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ) \land \forall t \in I \|F (t)\| \leq w) \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z) \to w \in ℝ$
257	241 256	syl	$⊢ χ \to w \in ℝ$
258	241	simplrd	$⊢ χ \to \forall t \in I \|F (t)\| \leq w$
259		id	$⊢ t \in (X + S (j), X + S (j + 1)) \to t \in (X + S (j), X + S (j + 1))$
260	259 9	eleqtrrdi	$⊢ t \in (X + S (j), X + S (j + 1)) \to t \in I$
261		rspa	$⊢ (\forall t \in I \|F (t)\| \leq w \land t \in I) \to \|F (t)\| \leq w$
262	258 260 261	syl2an	$⊢ (χ \land t \in (X + S (j), X + S (j + 1))) \to \|F (t)\| \leq w$
263		simpllr	$⊢ (((((φ \land j \in (0 ..^N)) \land w \in ℝ) \land z \in ℝ) \land \forall t \in I \|F (t)\| \leq w) \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z) \to z \in ℝ$
264	241 263	syl	$⊢ χ \to z \in ℝ$
265	154	fveq1i	$⊢ {({F ↾}_{I})}_{ℝ}^{'} (t) = {({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} (t)$
266	265	fveq2i	$⊢ \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| = \|{({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} (t)\|$
267	241	simprd	$⊢ χ \to \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z$
268	267	r19.21bi	$⊢ (χ \land t \in I) \to \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z$
269	266 268	eqbrtrrid	$⊢ (χ \land t \in I) \to \|{({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} (t)\| \leq z$
270	260 269	sylan2	$⊢ (χ \land t \in (X + S (j), X + S (j + 1))) \to \|{({F ↾}_{(X + S (j), X + S (j + 1))})}_{ℝ}^{'} (t)\| \leq z$
271	243 7	syl	$⊢ χ \to C \in ℝ$
272	244 245 248 249 250 252 254 255 257 262 264 270 271 17	fourierdlem68	$⊢ χ \to (dom Y_{ℝ}^{'} = (S (j), S (j + 1)) \land \exists y \in ℝ \forall s \in dom Y_{ℝ}^{'} \|Y_{ℝ}^{'} (s)\| \leq y)$
273	272	simprd	$⊢ χ \to \exists y \in ℝ \forall s \in dom Y_{ℝ}^{'} \|Y_{ℝ}^{'} (s)\| \leq y$
274	272	simpld	$⊢ χ \to dom Y_{ℝ}^{'} = (S (j), S (j + 1))$
275	274	raleqdv	$⊢ χ \to (\forall s \in dom Y_{ℝ}^{'} \|Y_{ℝ}^{'} (s)\| \leq y \leftrightarrow \forall s \in (S (j), S (j + 1)) \|Y_{ℝ}^{'} (s)\| \leq y)$
276	275	rexbidv	$⊢ χ \to (\exists y \in ℝ \forall s \in dom Y_{ℝ}^{'} \|Y_{ℝ}^{'} (s)\| \leq y \leftrightarrow \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|Y_{ℝ}^{'} (s)\| \leq y)$
277	273 276	mpbid	$⊢ χ \to \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|Y_{ℝ}^{'} (s)\| \leq y$
278	133	eqcomi	$⊢ (S (j), S (j + 1)) = int (topGen (ran (.))) ((S (j), S (j + 1)))$
279	278	reseq2i	$⊢ {O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))} = {O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))}$
280	279	fveq1i	$⊢ ({O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}) (s) = ({O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))}) (s)$
281		fvres	$⊢ s \in (S (j), S (j + 1)) \to ({O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}) (s) = O_{ℝ}^{'} (s)$
282	281	adantl	$⊢ (χ \land s \in (S (j), S (j + 1))) \to ({O_{ℝ}^{'} ↾}_{(S (j), S (j + 1))}) (s) = O_{ℝ}^{'} (s)$
283	247 87	syl	$⊢ χ \to (S (j), S (j + 1)) \subseteq [A, B]$
284	283	resmptd	$⊢ χ \to {(s \in [A, B] ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})}) ↾}_{(S (j), S (j + 1))} = (s \in (S (j), S (j + 1)) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
285	85 284	syl5eq	$⊢ χ \to {O ↾}_{(S (j), S (j + 1))} = (s \in (S (j), S (j + 1)) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
286	285 17	syl6reqr	$⊢ χ \to Y = {O ↾}_{(S (j), S (j + 1))}$
287	286	oveq2d	$⊢ χ \to ℝ D Y = ℝ D ({O ↾}_{(S (j), S (j + 1))})$
288	287	fveq1d	$⊢ χ \to Y_{ℝ}^{'} (s) = {({O ↾}_{(S (j), S (j + 1))})}_{ℝ}^{'} (s)$
289	132	fveq1d	$⊢ φ \to {({O ↾}_{(S (j), S (j + 1))})}_{ℝ}^{'} (s) = ({O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))}) (s)$
290	243 289	syl	$⊢ χ \to {({O ↾}_{(S (j), S (j + 1))})}_{ℝ}^{'} (s) = ({O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))}) (s)$
291	288 290	eqtr2d	$⊢ χ \to ({O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))}) (s) = Y_{ℝ}^{'} (s)$
292	291	adantr	$⊢ (χ \land s \in (S (j), S (j + 1))) \to ({O_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((S (j), S (j + 1)))}) (s) = Y_{ℝ}^{'} (s)$
293	280 282 292	3eqtr3a	$⊢ (χ \land s \in (S (j), S (j + 1))) \to O_{ℝ}^{'} (s) = Y_{ℝ}^{'} (s)$
294	293	fveq2d	$⊢ (χ \land s \in (S (j), S (j + 1))) \to \|O_{ℝ}^{'} (s)\| = \|Y_{ℝ}^{'} (s)\|$
295	294	breq1d	$⊢ (χ \land s \in (S (j), S (j + 1))) \to (\|O_{ℝ}^{'} (s)\| \leq y \leftrightarrow \|Y_{ℝ}^{'} (s)\| \leq y)$
296	295	ralbidva	$⊢ χ \to (\forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y \leftrightarrow \forall s \in (S (j), S (j + 1)) \|Y_{ℝ}^{'} (s)\| \leq y)$
297	296	rexbidv	$⊢ χ \to (\exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y \leftrightarrow \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|Y_{ℝ}^{'} (s)\| \leq y)$
298	277 297	mpbird	$⊢ χ \to \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y$
299	240 298	syl	$⊢ ((φ \land j \in (0 ..^N)) \land (w \in ℝ \land z \in ℝ) \land (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z)) \to \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y$
300	299	3exp	$⊢ (φ \land j \in (0 ..^N)) \to ((w \in ℝ \land z \in ℝ) \to ((\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z) \to \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y))$
301	300	rexlimdvv	$⊢ (φ \land j \in (0 ..^N)) \to (\exists w \in ℝ \exists z \in ℝ (\forall t \in I \|F (t)\| \leq w \land \forall t \in I \|{({F ↾}_{I})}_{ℝ}^{'} (t)\| \leq z) \to \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y)$
302	232 301	mpd	$⊢ (φ \land j \in (0 ..^N)) \to \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y$
303	302	3adant3	$⊢ (φ \land j \in (0 ..^N) \land r = (S (j), S (j + 1))) \to \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y$
304		raleq	$⊢ r = (S (j), S (j + 1)) \to (\forall s \in r \|O_{ℝ}^{'} (s)\| \leq y \leftrightarrow \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y)$
305	304	3ad2ant3	$⊢ (φ \land j \in (0 ..^N) \land r = (S (j), S (j + 1))) \to (\forall s \in r \|O_{ℝ}^{'} (s)\| \leq y \leftrightarrow \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y)$
306	305	rexbidv	$⊢ (φ \land j \in (0 ..^N) \land r = (S (j), S (j + 1))) \to (\exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y \leftrightarrow \exists y \in ℝ \forall s \in (S (j), S (j + 1)) \|O_{ℝ}^{'} (s)\| \leq y)$
307	303 306	mpbird	$⊢ (φ \land j \in (0 ..^N) \land r = (S (j), S (j + 1))) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
308	307	3exp	$⊢ φ \to (j \in (0 ..^N) \to (r = (S (j), S (j + 1)) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y))$
309	308	adantr	$⊢ (φ \land r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to (j \in (0 ..^N) \to (r = (S (j), S (j + 1)) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y))$
310	229 230 309	rexlimd	$⊢ (φ \land r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to (\exists j \in (0 ..^N) r = (S (j), S (j + 1)) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y)$
311	227 310	mpd	$⊢ (φ \land r \in ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
312	220 222 311	syl2anc	$⊢ ((φ \land r \in (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \land \neg r \in \{ran S \cap dom O_{ℝ}^{'}\}) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
313	219 312	pm2.61dan	$⊢ (φ \land r \in (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
314	185 313	sylan2	$⊢ (φ \land r \in (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))) \to \exists y \in ℝ \forall s \in r \|O_{ℝ}^{'} (s)\| \leq y$
315		pm3.22	$⊢ (r \in dom O_{ℝ}^{'} \land r \in ran S) \to (r \in ran S \land r \in dom O_{ℝ}^{'})$
316		elin	$⊢ r \in (ran S \cap dom O_{ℝ}^{'}) \leftrightarrow (r \in ran S \land r \in dom O_{ℝ}^{'})$
317	315 316	sylibr	$⊢ (r \in dom O_{ℝ}^{'} \land r \in ran S) \to r \in (ran S \cap dom O_{ℝ}^{'})$
318	317	adantll	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land r \in ran S) \to r \in (ran S \cap dom O_{ℝ}^{'})$
319	60	eqcomd	$⊢ φ \to ran S \cap dom O_{ℝ}^{'} = ⋃ \{ran S \cap dom O_{ℝ}^{'}\}$
320	319	ad2antrr	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land r \in ran S) \to ran S \cap dom O_{ℝ}^{'} = ⋃ \{ran S \cap dom O_{ℝ}^{'}\}$
321	318 320	eleqtrd	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land r \in ran S) \to r \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\}$
322	321	orcd	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land r \in ran S) \to (r \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \lor r \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
323		simpll	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land \neg r \in ran S) \to φ$
324	92	a1i	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to ℝ \subseteq ℂ$
325	126	adantr	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to O : [A, B] ⟶ ℂ$
326	3	adantr	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to A \in ℝ$
327	4	adantr	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to B \in ℝ$
328	326 327	iccssred	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to [A, B] \subseteq ℝ$
329	324 325 328	dvbss	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to dom O_{ℝ}^{'} \subseteq [A, B]$
330		simpr	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to r \in dom O_{ℝ}^{'}$
331	329 330	sseldd	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to r \in [A, B]$
332	331	adantr	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land \neg r \in ran S) \to r \in [A, B]$
333		simpr	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land \neg r \in ran S) \to \neg r \in ran S$
334		fveq2	$⊢ j = k \to S (j) = S (k)$
335		oveq1	$⊢ j = k \to j + 1 = k + 1$
336	335	fveq2d	$⊢ j = k \to S (j + 1) = S (k + 1)$
337	334 336	oveq12d	$⊢ j = k \to (S (j), S (j + 1)) = (S (k), S (k + 1))$
338		ovex	$⊢ (S (k), S (k + 1)) \in V$
339	337 35 338	fvmpt	$⊢ k \in (0 ..^N) \to (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k) = (S (k), S (k + 1))$
340	339	eleq2d	$⊢ k \in (0 ..^N) \to (r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k) \leftrightarrow r \in (S (k), S (k + 1)))$
341	340	rexbiia	$⊢ \exists k \in (0 ..^N) r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k) \leftrightarrow \exists k \in (0 ..^N) r \in (S (k), S (k + 1))$
342	15 341	sylibr	$⊢ ((φ \land r \in [A, B]) \land \neg r \in ran S) \to \exists k \in (0 ..^N) r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k)$
343	70 35	dmmpti	$⊢ dom (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) = (0 ..^N)$
344	343	rexeqi	$⊢ \exists k \in dom (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k) \leftrightarrow \exists k \in (0 ..^N) r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k)$
345	342 344	sylibr	$⊢ ((φ \land r \in [A, B]) \land \neg r \in ran S) \to \exists k \in dom (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k)$
346	323 332 333 345	syl21anc	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land \neg r \in ran S) \to \exists k \in dom (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k)$
347		funmpt	$⊢ Fun (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
348		elunirn	$⊢ Fun (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \to (r \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \leftrightarrow \exists k \in dom (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k))$
349	347 348	mp1i	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land \neg r \in ran S) \to (r \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) \leftrightarrow \exists k \in dom (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) r \in (j \in (0 ..^N) ⟼ (S (j), S (j + 1))) (k))$
350	346 349	mpbird	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land \neg r \in ran S) \to r \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))$
351	350	olcd	$⊢ ((φ \land r \in dom O_{ℝ}^{'}) \land \neg r \in ran S) \to (r \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \lor r \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
352	322 351	pm2.61dan	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to (r \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \lor r \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
353		elun	$⊢ r \in (⋃ \{ran S \cap dom O_{ℝ}^{'}\} \cup ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \leftrightarrow (r \in ⋃ \{ran S \cap dom O_{ℝ}^{'}\} \lor r \in ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
354	352 353	sylibr	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to r \in (⋃ \{ran S \cap dom O_{ℝ}^{'}\} \cup ⋃ ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
355	354 46	eleqtrrdi	$⊢ (φ \land r \in dom O_{ℝ}^{'}) \to r \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
356	355	ralrimiva	$⊢ φ \to \forall r \in dom O_{ℝ}^{'} r \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
357		dfss3	$⊢ dom O_{ℝ}^{'} \subseteq ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1)))) \leftrightarrow \forall r \in dom O_{ℝ}^{'} r \in ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
358	356 357	sylibr	$⊢ φ \to dom O_{ℝ}^{'} \subseteq ⋃ (\{ran S \cap dom O_{ℝ}^{'}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
359	358 43	sseqtrrdi	$⊢ φ \to dom O_{ℝ}^{'} \subseteq ⋃ (\{ran S \cap dom \frac{d (t \in [A, B]⟼ \frac{F (X + t) - C}{2 \sin (\frac{t}{2})})}{d_{ℝ} t}\} \cup ran (j \in (0 ..^N) ⟼ (S (j), S (j + 1))))$
360	41 183 314 359	ssfiunibd	$⊢ φ \to \exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|O_{ℝ}^{'} (s)\| \leq b$

Metamath Proof Explorer

Theorem fourierdlem80

Proof