Theorem fourierdlem40

Description: H is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem40.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem40.a	⊢ ( 𝜑 → 𝐴 ∈ ( - π [,] π ) )
	fourierdlem40.b	⊢ ( 𝜑 → 𝐵 ∈ ( - π [,] π ) )
	fourierdlem40.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem40.nxelab	⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
	fourierdlem40.fcn	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ∈ ( ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) –cn→ ℂ ) )
	fourierdlem40.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	fourierdlem40.w	⊢ ( 𝜑 → 𝑊 ∈ ℝ )
	fourierdlem40.h	⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
Assertion	fourierdlem40	⊢ ( 𝜑 → ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem40.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem40.a	⊢ ( 𝜑 → 𝐴 ∈ ( - π [,] π ) )
3		fourierdlem40.b	⊢ ( 𝜑 → 𝐵 ∈ ( - π [,] π ) )
4		fourierdlem40.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5		fourierdlem40.nxelab	⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
6		fourierdlem40.fcn	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ∈ ( ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) –cn→ ℂ ) )
7		fourierdlem40.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
8		fourierdlem40.w	⊢ ( 𝜑 → 𝑊 ∈ ℝ )
9		fourierdlem40.h	⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
10	9	reseq1i	⊢ ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) )
11	10	a1i	⊢ ( 𝜑 → ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) )
12		pire	⊢ π ∈ ℝ
13	12	renegcli	⊢ - π ∈ ℝ
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - π ∈ ℝ )
15	12	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → π ∈ ℝ )
16		elioore	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
18	13	a1i	⊢ ( 𝜑 → - π ∈ ℝ )
19	12	a1i	⊢ ( 𝜑 → π ∈ ℝ )
20	18 19	iccssred	⊢ ( 𝜑 → ( - π [,] π ) ⊆ ℝ )
21	20 2	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
23	13 12	elicc2i	⊢ ( 𝐴 ∈ ( - π [,] π ) ↔ ( 𝐴 ∈ ℝ ∧ - π ≤ 𝐴 ∧ 𝐴 ≤ π ) )
24	23	simp2bi	⊢ ( 𝐴 ∈ ( - π [,] π ) → - π ≤ 𝐴 )
25	2 24	syl	⊢ ( 𝜑 → - π ≤ 𝐴 )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - π ≤ 𝐴 )
27	22	rexrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
28	20 3	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
29	28	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
32		ioogtlb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
33	27 30 31 32	syl3anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
34	14 22 17 26 33	lelttrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - π < 𝑠 )
35	14 17 34	ltled	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - π ≤ 𝑠 )
36	28	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
37		iooltub	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
38	27 30 31 37	syl3anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
39	13 12	elicc2i	⊢ ( 𝐵 ∈ ( - π [,] π ) ↔ ( 𝐵 ∈ ℝ ∧ - π ≤ 𝐵 ∧ 𝐵 ≤ π ) )
40	39	simp3bi	⊢ ( 𝐵 ∈ ( - π [,] π ) → 𝐵 ≤ π )
41	3 40	syl	⊢ ( 𝜑 → 𝐵 ≤ π )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ≤ π )
43	17 36 15 38 42	ltletrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < π )
44	17 15 43	ltled	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≤ π )
45	14 15 17 35 44	eliccd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( - π [,] π ) )
46	45	ex	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ( - π [,] π ) ) )
47	46	ssrdv	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( - π [,] π ) )
48	47	resmptd	⊢ ( 𝜑 → ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) )
49		eleq1	⊢ ( 𝑠 = 0 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↔ 0 ∈ ( 𝐴 (,) 𝐵 ) ) )
50	49	biimpac	⊢ ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
51	50	adantll	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
52	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
53	51 52	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑠 = 0 )
54	53	iffalsed	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) )
55	1	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
56	4	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℝ )
57	56 17	readdcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
58	55 57	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
59	7 8	ifcld	⊢ ( 𝜑 → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
60	59	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
61	58 60	resubcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℝ )
62	61	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℂ )
63	17	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℂ )
64	53	neqned	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≠ 0 )
65	62 63 64	divrecd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) )
66	54 65	eqtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) )
67	66	mpteq2dva	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) ) )
68	11 48 67	3eqtrd	⊢ ( 𝜑 → ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) ) )
69	58	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
70	60	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
71	69 70	negsubd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) + - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) )
72	71	eqcomd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) + - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) )
73	72	mpteq2dva	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) + - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) )
74	21 4	readdcld	⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ )
75	74	rexrd	⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ* )
76	75	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 + 𝑋 ) ∈ ℝ* )
77	28 4	readdcld	⊢ ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ )
78	77	rexrd	⊢ ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ* )
79	78	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐵 + 𝑋 ) ∈ ℝ* )
80	21	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
81	4	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
82	80 81	addcomd	⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) = ( 𝑋 + 𝐴 ) )
83	82	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 + 𝑋 ) = ( 𝑋 + 𝐴 ) )
84	22 17 56 33	ltadd2dd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) < ( 𝑋 + 𝑠 ) )
85	83 84	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 + 𝑋 ) < ( 𝑋 + 𝑠 ) )
86	17 36 56 38	ltadd2dd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + 𝐵 ) )
87	28	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
88	81 87	addcomd	⊢ ( 𝜑 → ( 𝑋 + 𝐵 ) = ( 𝐵 + 𝑋 ) )
89	88	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐵 ) = ( 𝐵 + 𝑋 ) )
90	86 89	breqtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) < ( 𝐵 + 𝑋 ) )
91	76 79 57 85 90	eliood	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) )
92		fvres	⊢ ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) → ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
93	91 92	syl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
94	93	eqcomd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
95	94	mpteq2dva	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
96		ioosscn	⊢ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ⊆ ℂ
97	96	a1i	⊢ ( 𝜑 → ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ⊆ ℂ )
98		ioosscn	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
99	98	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
100	97 6 99 81 91	fourierdlem23	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ↾ ( ( 𝐴 + 𝑋 ) (,) ( 𝐵 + 𝑋 ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
101	95 100	eqeltrd	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
102		0red	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
103	21	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
104	16	adantl	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
105		simplr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ 𝐴 )
106	33	adantlr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
107	102 103 104 105 106	lelttrd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < 𝑠 )
108	107	iftrued	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑌 )
109	108	negeqd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = - 𝑌 )
110	109	mpteq2dva	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑌 ) )
111	7	renegcld	⊢ ( 𝜑 → - 𝑌 ∈ ℝ )
112	111	recnd	⊢ ( 𝜑 → - 𝑌 ∈ ℂ )
113		ssid	⊢ ℂ ⊆ ℂ
114	113	a1i	⊢ ( 𝜑 → ℂ ⊆ ℂ )
115	99 112 114	constcncfg	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑌 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
116	115	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑌 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
117	110 116	eqeltrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
118	21	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
119	118	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 𝐴 ∈ ℝ* )
120	29	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 𝐵 ∈ ℝ* )
121		0red	⊢ ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 0 ∈ ℝ )
122		simpr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → ¬ 0 ≤ 𝐴 )
123	21	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
124		0red	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → 0 ∈ ℝ )
125	123 124	ltnled	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → ( 𝐴 < 0 ↔ ¬ 0 ≤ 𝐴 ) )
126	122 125	mpbird	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → 𝐴 < 0 )
127	126	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 𝐴 < 0 )
128		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → ¬ 𝐵 ≤ 0 )
129		0red	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → 0 ∈ ℝ )
130	28	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → 𝐵 ∈ ℝ )
131	129 130	ltnled	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → ( 0 < 𝐵 ↔ ¬ 𝐵 ≤ 0 ) )
132	128 131	mpbird	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 0 ) → 0 < 𝐵 )
133	132	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 0 < 𝐵 )
134	119 120 121 127 133	eliood	⊢ ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
135	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) ∧ ¬ 𝐵 ≤ 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
136	134 135	condan	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → 𝐵 ≤ 0 )
137	16	adantl	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
138		0red	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
139	28	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
140	38	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
141		simplr	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ≤ 0 )
142	137 139 138 140 141	ltletrd	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 0 )
143	137 138 142	ltnsymd	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 < 𝑠 )
144	143	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑊 )
145	144	negeqd	⊢ ( ( ( 𝜑 ∧ 𝐵 ≤ 0 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = - 𝑊 )
146	145	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑊 ) )
147	8	recnd	⊢ ( 𝜑 → 𝑊 ∈ ℂ )
148	147	negcld	⊢ ( 𝜑 → - 𝑊 ∈ ℂ )
149	99 148 114	constcncfg	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑊 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
150	149	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - 𝑊 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
151	146 150	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
152	136 151	syldan	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐴 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
153	117 152	pm2.61dan	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
154	101 153	addcncf	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) + - if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
155	73 154	eqeltrd	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
156		eqid	⊢ ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑠 ) ) = ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑠 ) )
157		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
158	156	cdivcncf	⊢ ( 1 ∈ ℂ → ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑠 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
159	157 158	syl	⊢ ( 𝜑 → ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑠 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
160		velsn	⊢ ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
161	53 160	sylnibr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑠 ∈ { 0 } )
162	63 161	eldifd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( ℂ ∖ { 0 } ) )
163	162	ralrimiva	⊢ ( 𝜑 → ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) 𝑠 ∈ ( ℂ ∖ { 0 } ) )
164		dfss3	⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( ℂ ∖ { 0 } ) ↔ ∀ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) 𝑠 ∈ ( ℂ ∖ { 0 } ) )
165	163 164	sylibr	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( ℂ ∖ { 0 } ) )
166	17 64	rereccld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 𝑠 ) ∈ ℝ )
167	166	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 𝑠 ) ∈ ℂ )
168	156 159 165 114 167	cncfmptssg	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑠 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
169	155 168	mulcncf	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( 1 / 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
170	68 169	eqeltrd	⊢ ( 𝜑 → ( 𝐻 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )