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

Metamath Proof Explorer

Theorem fourierdlem80

Proof