Theorem limciccioolb 37273

Description: The limit of a function at the lower bound of a closed interval only depends on the values in the inner open interval (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
limciccioolb.1	|- ( ph -> A e. RR )
limciccioolb.2	|- ( ph -> B e. RR )
limciccioolb.3	|- ( ph -> A < B )
limciccioolb.4	|- ( ph -> F : ( A [,] B ) --> CC )

Assertion

Ref	Expression
limciccioolb	|- ( ph -> ( ( F |` ( A (,) B ) ) lim CC A ) = ( F lim CC A ) )

Proof of Theorem limciccioolb

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		limciccioolb.4	. 2 |- ( ph -> F : ( A [,] B ) --> CC )
2		ioossicc 11720	. . 3 |- ( A (,) B ) C_ ( A [,] B )
3	2	a1i 11	. 2 |- ( ph -> ( A (,) B ) C_ ( A [,] B ) )
4		limciccioolb.1	. . . 4 |- ( ph -> A e. RR )
5		limciccioolb.2	. . . 4 |- ( ph -> B e. RR )
6	4, 5	iccssred 37187	. . 3 |- ( ph -> ( A [,] B ) C_ RR )
7		ax-resscn 9595	. . 3 |- RR C_ CC
8	6, 7	syl6ss 3482	. 2 |- ( ph -> ( A [,] B ) C_ CC )
9		eqid 2429	. 2 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
10		eqid 2429	. 2 |- ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) )
11		retop 21693	. . . . . . . . 9 |- ( topGen ` ran (,) ) e. Top
12	11	a1i 11	. . . . . . . 8 |- ( ph -> ( topGen ` ran (,) ) e. Top )
13	5	rexrd 9689	. . . . . . . . . . 11 |- ( ph -> B e. RR* )
14		icossre 11715	. . . . . . . . . . 11 |- ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) C_ RR )
15	4, 13, 14	syl2anc 665	. . . . . . . . . 10 |- ( ph -> ( A [,) B ) C_ RR )
16		difssd 3599	. . . . . . . . . 10 |- ( ph -> ( RR \ ( A [,] B ) ) C_ RR )
17	15, 16	unssd 3648	. . . . . . . . 9 |- ( ph -> ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
18		uniretop 21694	. . . . . . . . 9 |- RR = U. ( topGen ` ran (,) )
19	17, 18	syl6sseq 3516	. . . . . . . 8 |- ( ph -> ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ U. ( topGen ` ran (,) ) )
20		elioore 11666	. . . . . . . . . . . . . . 15 |- ( x e. ( -oo (,) B ) -> x e. RR )
21	20	ad2antlr 731	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> x e. RR )
22		simpr 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> A <_ x )
23		simpr 462	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> x e. ( -oo (,) B ) )
24		mnfxr 11414	. . . . . . . . . . . . . . . . . . 19 |- -oo e. RR*
25	24	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> -oo e. RR* )
26	13	adantr 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> B e. RR* )
27		elioo2 11677	. . . . . . . . . . . . . . . . . 18 |- ( ( -oo e. RR* /\ B e. RR* ) -> ( x e. ( -oo (,) B ) <-> ( x e. RR /\ -oo < x /\ x < B ) ) )
28	25, 26, 27	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> ( x e. ( -oo (,) B ) <-> ( x e. RR /\ -oo < x /\ x < B ) ) )
29	23, 28	mpbid 213	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> ( x e. RR /\ -oo < x /\ x < B ) )
30	29	simp3d 1019	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> x < B )
31	30	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> x < B )
32	4	ad2antrr 730	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> A e. RR )
33	13	ad2antrr 730	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> B e. RR* )
34		elico2 11698	. . . . . . . . . . . . . . 15 |- ( ( A e. RR /\ B e. RR* ) -> ( x e. ( A [,) B ) <-> ( x e. RR /\ A <_ x /\ x < B ) ) )
35	32, 33, 34	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> ( x e. ( A [,) B ) <-> ( x e. RR /\ A <_ x /\ x < B ) ) )
36	21, 22, 31, 35	mpbir3and 1188	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> x e. ( A [,) B ) )
37	36	orcd 393	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
38	20	ad2antlr 731	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> x e. RR )
39		simpr 462	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> -. A <_ x )
40	39	intnanrd 925	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> -. ( A <_ x /\ x <_ B ) )
41	4	rexrd 9689	. . . . . . . . . . . . . . . . 17 |- ( ph -> A e. RR* )
42	41	ad2antrr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> A e. RR* )
43	13	ad2antrr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> B e. RR* )
44	38	rexrd 9689	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> x e. RR* )
45		elicc4 11701	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR* /\ B e. RR* /\ x e. RR* ) -> ( x e. ( A [,] B ) <-> ( A <_ x /\ x <_ B ) ) )
46	42, 43, 44, 45	syl3anc 1264	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> ( x e. ( A [,] B ) <-> ( A <_ x /\ x <_ B ) ) )
47	40, 46	mtbird 302	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> -. x e. ( A [,] B ) )
48	38, 47	eldifd 3453	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> x e. ( RR \ ( A [,] B ) ) )
49	48	olcd 394	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
50	37, 49	pm2.61dan 798	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
51		elun 3612	. . . . . . . . . . 11 |- ( x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) <-> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
52	50, 51	sylibr 215	. . . . . . . . . 10 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
53	52	ralrimiva 2846	. . . . . . . . 9 |- ( ph -> A. x e. ( -oo (,) B ) x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
54		dfss3 3460	. . . . . . . . 9 |- ( ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) <-> A. x e. ( -oo (,) B ) x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
55	53, 54	sylibr 215	. . . . . . . 8 |- ( ph -> ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
56		eqid 2429	. . . . . . . . 9 |- U. ( topGen ` ran (,) ) = U. ( topGen ` ran (,) )
57	56	ntrss 20001	. . . . . . . 8 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ U. ( topGen ` ran (,) ) /\ ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
58	12, 19, 55, 57	syl3anc 1264	. . . . . . 7 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
59	24	a1i 11	. . . . . . . . 9 |- ( ph -> -oo e. RR* )
60	4	mnfltd 11426	. . . . . . . . 9 |- ( ph -> -oo < A )
61		limciccioolb.3	. . . . . . . . 9 |- ( ph -> A < B )
62	59, 13, 4, 60, 61	eliood 37180	. . . . . . . 8 |- ( ph -> A e. ( -oo (,) B ) )
63		iooretop 21697	. . . . . . . . . 10 |- ( -oo (,) B ) e. ( topGen ` ran (,) )
64	63	a1i 11	. . . . . . . . 9 |- ( ph -> ( -oo (,) B ) e. ( topGen ` ran (,) ) )
65		isopn3i 20029	. . . . . . . . 9 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) = ( -oo (,) B ) )
66	12, 64, 65	syl2anc 665	. . . . . . . 8 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) = ( -oo (,) B ) )
67	62, 66	eleqtrrd 2520	. . . . . . 7 |- ( ph -> A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) )
68	58, 67	sseldd 3471	. . . . . 6 |- ( ph -> A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
69	4	leidd 10179	. . . . . . 7 |- ( ph -> A <_ A )
70	4, 5, 61	ltled 9782	. . . . . . 7 |- ( ph -> A <_ B )
71	4, 5, 4, 69, 70	eliccd 37186	. . . . . 6 |- ( ph -> A e. ( A [,] B ) )
72	68, 71	elind 3656	. . . . 5 |- ( ph -> A e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
73		icossicc 11721	. . . . . . 7 |- ( A [,) B ) C_ ( A [,] B )
74	73	a1i 11	. . . . . 6 |- ( ph -> ( A [,) B ) C_ ( A [,] B ) )
75		eqid 2429	. . . . . . 7 |- ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) )
76	18, 75	restntr 20129	. . . . . 6 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) C_ RR /\ ( A [,) B ) C_ ( A [,] B ) ) -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
77	12, 6, 74, 76	syl3anc 1264	. . . . 5 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
78	72, 77	eleqtrrd 2520	. . . 4 |- ( ph -> A e. ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) )
79		eqid 2429	. . . . . . . . 9 |- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
80	9, 79	rerest 21733	. . . . . . . 8 |- ( ( A [,] B ) C_ RR -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) )
81	6, 80	syl 17	. . . . . . 7 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) )
82	81	eqcomd 2437	. . . . . 6 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
83	82	fveq2d 5885	. . . . 5 |- ( ph -> ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) )
84	83	fveq1d 5883	. . . 4 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) )
85	78, 84	eleqtrd 2519	. . 3 |- ( ph -> A e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) )
86	71	snssd 4148	. . . . . . . 8 |- ( ph -> { A } C_ ( A [,] B ) )
87		ssequn2 3645	. . . . . . . 8 |- ( { A } C_ ( A [,] B ) <-> ( ( A [,] B ) u. { A } ) = ( A [,] B ) )
88	86, 87	sylib 199	. . . . . . 7 |- ( ph -> ( ( A [,] B ) u. { A } ) = ( A [,] B ) )
89	88	eqcomd 2437	. . . . . 6 |- ( ph -> ( A [,] B ) = ( ( A [,] B ) u. { A } ) )
90	89	oveq2d 6321	. . . . 5 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) )
91	90	fveq2d 5885	. . . 4 |- ( ph -> ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) ) )
92		uncom 3616	. . . . 5 |- ( ( A (,) B ) u. { A } ) = ( { A } u. ( A (,) B ) )
93		snunioo 11756	. . . . . 6 |- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )
94	41, 13, 61, 93	syl3anc 1264	. . . . 5 |- ( ph -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )
95	92, 94	syl5req 2483	. . . 4 |- ( ph -> ( A [,) B ) = ( ( A (,) B ) u. { A } ) )
96	91, 95	fveq12d 5887	. . 3 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) ) ` ( ( A (,) B ) u. { A } ) ) )
97	85, 96	eleqtrd 2519	. 2 |- ( ph -> A e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) ) ` ( ( A (,) B ) u. { A } ) ) )
98	1, 3, 8, 9, 10, 97	limcres 22718	1 |- ( ph -> ( ( F |` ( A (,) B ) ) lim CC A ) = ( F lim CC A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1870   A.wral 2782   \ cdif 3439   u. cun 3440   i^i cin 3441   C_ wss 3442   {csn 4002   U.cuni 4222   class class class wbr 4426   ran crn 4855   |` cres 4856   -->wf 5597   ` cfv 5601  (class class class)co 6305   CCcc 9536   RRcr 9537   -oocmnf 9672   RR*cxr 9673   < clt 9674   <_ cle 9675   (,)cioo 11635   [,)cico 11637   [,]cicc 11638   ↾_t crest 15278   TopOpenctopn 15279   topGenctg 15295  ℂ_fldccnfld 18905   Topctop 19848   intcnt 19963   lim CC climc 22694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-pre-sup 9616

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-map 7482  df-pm 7483  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-fi 7931  df-sup 7962  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ico 11641  df-icc 11642  df-fz 11783  df-seq 12211  df-exp 12270  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-struct 15086  df-ndx 15087  df-slot 15088  df-base 15089  df-plusg 15165  df-mulr 15166  df-starv 15167  df-tset 15171  df-ple 15172  df-ds 15174  df-unif 15175  df-rest 15280  df-topn 15281  df-topgen 15301  df-psmet 18897  df-xmet 18898  df-met 18899  df-bl 18900  df-mopn 18901  df-cnfld 18906  df-top 19852  df-bases 19853  df-topon 19854  df-topsp 19855  df-cld 19965  df-ntr 19966  df-cls 19967  df-cnp 20175  df-xms 21266  df-ms 21267  df-limc 22698

This theorem is referenced by:  cncfiooicclem1  37343  fourierdlem82  37620  fourierdlem93  37631  fourierdlem111  37649