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

Metamath Proof Explorer

Theorem fourierdlem80

Proof