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

Metamath Proof Explorer

Theorem fourierdlem80

Proof