Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem61 Structured version   Visualization version   GIF version

Theorem fourierdlem61 39717
 Description: Given a differentiable function 𝐹, with finite limit of the derivative at 𝐴 the derived function 𝐻 has a limit at 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem61.a (𝜑𝐴 ∈ ℝ)
fourierdlem61.b (𝜑𝐵 ∈ ℝ)
fourierdlem61.altb (𝜑𝐴 < 𝐵)
fourierdlem61.f (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
fourierdlem61.y (𝜑𝑌 ∈ (𝐹 lim 𝐴))
fourierdlem61.g 𝐺 = (ℝ D 𝐹)
fourierdlem61.domg (𝜑 → dom 𝐺 = (𝐴(,)𝐵))
fourierdlem61.e (𝜑𝐸 ∈ (𝐺 lim 𝐴))
fourierdlem61.h 𝐻 = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠))
fourierdlem61.n 𝑁 = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))
fourierdlem61.d 𝐷 = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠)
Assertion
Ref Expression
fourierdlem61 (𝜑𝐸 ∈ (𝐻 lim 0))
Distinct variable groups:   𝐴,𝑠   𝐵,𝑠   𝐷,𝑠   𝐸,𝑠   𝐹,𝑠   𝐺,𝑠   𝑁,𝑠   𝑌,𝑠   𝜑,𝑠
Allowed substitution hint:   𝐻(𝑠)

Proof of Theorem fourierdlem61
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 0red 9993 . . 3 (𝜑 → 0 ∈ ℝ)
2 fourierdlem61.b . . . . 5 (𝜑𝐵 ∈ ℝ)
3 fourierdlem61.a . . . . 5 (𝜑𝐴 ∈ ℝ)
42, 3resubcld 10410 . . . 4 (𝜑 → (𝐵𝐴) ∈ ℝ)
54rexrd 10041 . . 3 (𝜑 → (𝐵𝐴) ∈ ℝ*)
6 fourierdlem61.altb . . . 4 (𝜑𝐴 < 𝐵)
73, 2posdifd 10566 . . . 4 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
86, 7mpbid 222 . . 3 (𝜑 → 0 < (𝐵𝐴))
9 fourierdlem61.f . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
109adantr 481 . . . . . 6 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
113rexrd 10041 . . . . . . . 8 (𝜑𝐴 ∈ ℝ*)
1211adantr 481 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝐴 ∈ ℝ*)
132rexrd 10041 . . . . . . . 8 (𝜑𝐵 ∈ ℝ*)
1413adantr 481 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝐵 ∈ ℝ*)
153adantr 481 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝐴 ∈ ℝ)
16 elioore 12155 . . . . . . . . 9 (𝑠 ∈ (0(,)(𝐵𝐴)) → 𝑠 ∈ ℝ)
1716adantl 482 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝑠 ∈ ℝ)
1815, 17readdcld 10021 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴 + 𝑠) ∈ ℝ)
193recnd 10020 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
2019addid1d 10188 . . . . . . . . . 10 (𝜑 → (𝐴 + 0) = 𝐴)
2120eqcomd 2627 . . . . . . . . 9 (𝜑𝐴 = (𝐴 + 0))
2221adantr 481 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝐴 = (𝐴 + 0))
23 0red 9993 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 0 ∈ ℝ)
24 0xr 10038 . . . . . . . . . . 11 0 ∈ ℝ*
2524a1i 11 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 0 ∈ ℝ*)
265adantr 481 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐵𝐴) ∈ ℝ*)
27 simpr 477 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝑠 ∈ (0(,)(𝐵𝐴)))
28 ioogtlb 39159 . . . . . . . . . 10 ((0 ∈ ℝ* ∧ (𝐵𝐴) ∈ ℝ*𝑠 ∈ (0(,)(𝐵𝐴))) → 0 < 𝑠)
2925, 26, 27, 28syl3anc 1323 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 0 < 𝑠)
3023, 17, 15, 29ltadd2dd 10148 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴 + 0) < (𝐴 + 𝑠))
3122, 30eqbrtrd 4640 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝐴 < (𝐴 + 𝑠))
324adantr 481 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐵𝐴) ∈ ℝ)
33 iooltub 39177 . . . . . . . . . 10 ((0 ∈ ℝ* ∧ (𝐵𝐴) ∈ ℝ*𝑠 ∈ (0(,)(𝐵𝐴))) → 𝑠 < (𝐵𝐴))
3425, 26, 27, 33syl3anc 1323 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝑠 < (𝐵𝐴))
3517, 32, 15, 34ltadd2dd 10148 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴 + 𝑠) < (𝐴 + (𝐵𝐴)))
362recnd 10020 . . . . . . . . . 10 (𝜑𝐵 ∈ ℂ)
3719, 36pncan3d 10347 . . . . . . . . 9 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
3837adantr 481 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴 + (𝐵𝐴)) = 𝐵)
3935, 38breqtrd 4644 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴 + 𝑠) < 𝐵)
4012, 14, 18, 31, 39eliood 39162 . . . . . 6 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴 + 𝑠) ∈ (𝐴(,)𝐵))
4110, 40ffvelrnd 6321 . . . . 5 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐹‘(𝐴 + 𝑠)) ∈ ℝ)
42 ioossre 12185 . . . . . . . . 9 (𝐴(,)𝐵) ⊆ ℝ
4342a1i 11 . . . . . . . 8 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
44 ax-resscn 9945 . . . . . . . 8 ℝ ⊆ ℂ
4543, 44syl6ss 3599 . . . . . . 7 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
46 eqid 2621 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4746, 13, 3, 6lptioo1cn 39310 . . . . . . 7 (𝜑𝐴 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴(,)𝐵)))
48 fourierdlem61.y . . . . . . 7 (𝜑𝑌 ∈ (𝐹 lim 𝐴))
499, 45, 47, 48limcrecl 39293 . . . . . 6 (𝜑𝑌 ∈ ℝ)
5049adantr 481 . . . . 5 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝑌 ∈ ℝ)
5141, 50resubcld 10410 . . . 4 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((𝐹‘(𝐴 + 𝑠)) − 𝑌) ∈ ℝ)
52 fourierdlem61.n . . . 4 𝑁 = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))
5351, 52fmptd 6346 . . 3 (𝜑𝑁:(0(,)(𝐵𝐴))⟶ℝ)
54 fourierdlem61.d . . . 4 𝐷 = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠)
5517, 54fmptd 6346 . . 3 (𝜑𝐷:(0(,)(𝐵𝐴))⟶ℝ)
5652oveq2i 6621 . . . . . 6 (ℝ D 𝑁) = (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)))
5756a1i 11 . . . . 5 (𝜑 → (ℝ D 𝑁) = (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))))
5857dmeqd 5291 . . . 4 (𝜑 → dom (ℝ D 𝑁) = dom (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))))
59 reelprrecn 9980 . . . . . . . 8 ℝ ∈ {ℝ, ℂ}
6059a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ {ℝ, ℂ})
6141recnd 10020 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐹‘(𝐴 + 𝑠)) ∈ ℂ)
62 dvfre 23637 . . . . . . . . . . 11 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
639, 43, 62syl2anc 692 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
64 fourierdlem61.g . . . . . . . . . . . 12 𝐺 = (ℝ D 𝐹)
6564a1i 11 . . . . . . . . . . 11 (𝜑𝐺 = (ℝ D 𝐹))
6665feq1d 5992 . . . . . . . . . 10 (𝜑 → (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ))
6763, 66mpbird 247 . . . . . . . . 9 (𝜑𝐺:dom (ℝ D 𝐹)⟶ℝ)
6867adantr 481 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
6965eqcomd 2627 . . . . . . . . . . . 12 (𝜑 → (ℝ D 𝐹) = 𝐺)
7069dmeqd 5291 . . . . . . . . . . 11 (𝜑 → dom (ℝ D 𝐹) = dom 𝐺)
71 fourierdlem61.domg . . . . . . . . . . 11 (𝜑 → dom 𝐺 = (𝐴(,)𝐵))
7270, 71eqtr2d 2656 . . . . . . . . . 10 (𝜑 → (𝐴(,)𝐵) = dom (ℝ D 𝐹))
7372adantr 481 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴(,)𝐵) = dom (ℝ D 𝐹))
7440, 73eleqtrd 2700 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴 + 𝑠) ∈ dom (ℝ D 𝐹))
7568, 74ffvelrnd 6321 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐺‘(𝐴 + 𝑠)) ∈ ℝ)
76 1red 10007 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 1 ∈ ℝ)
779ffvelrnda 6320 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐹𝑥) ∈ ℝ)
7877recnd 10020 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐹𝑥) ∈ ℂ)
7972feq2d 5993 . . . . . . . . . . 11 (𝜑 → (𝐺:(𝐴(,)𝐵)⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ))
8067, 79mpbird 247 . . . . . . . . . 10 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
8180ffvelrnda 6320 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐺𝑥) ∈ ℝ)
8219adantr 481 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝐴 ∈ ℂ)
8319adantr 481 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℝ) → 𝐴 ∈ ℂ)
84 0red 9993 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℝ) → 0 ∈ ℝ)
8560, 19dvmptc 23644 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝐴)) = (𝑠 ∈ ℝ ↦ 0))
86 ioossre 12185 . . . . . . . . . . . . 13 (0(,)(𝐵𝐴)) ⊆ ℝ
8786a1i 11 . . . . . . . . . . . 12 (𝜑 → (0(,)(𝐵𝐴)) ⊆ ℝ)
8846tgioo2 22529 . . . . . . . . . . . 12 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
89 iooretop 22492 . . . . . . . . . . . . 13 (0(,)(𝐵𝐴)) ∈ (topGen‘ran (,))
9089a1i 11 . . . . . . . . . . . 12 (𝜑 → (0(,)(𝐵𝐴)) ∈ (topGen‘ran (,)))
9160, 83, 84, 85, 87, 88, 46, 90dvmptres 23649 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝐴)) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 0))
9217recnd 10020 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝑠 ∈ ℂ)
93 recn 9978 . . . . . . . . . . . . 13 (𝑠 ∈ ℝ → 𝑠 ∈ ℂ)
9493adantl 482 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℝ) → 𝑠 ∈ ℂ)
95 1red 10007 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℝ) → 1 ∈ ℝ)
9660dvmptid 23643 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑠)) = (𝑠 ∈ ℝ ↦ 1))
9760, 94, 95, 96, 87, 88, 46, 90dvmptres 23649 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠)) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1))
9860, 82, 23, 91, 92, 76, 97dvmptadd 23646 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (0 + 1)))
99 0p1e1 11084 . . . . . . . . . . 11 (0 + 1) = 1
10099mpteq2i 4706 . . . . . . . . . 10 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (0 + 1)) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1)
10198, 100syl6eq 2671 . . . . . . . . 9 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1))
1029feqmptd 6211 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)))
103102eqcomd 2627 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) = 𝐹)
104103oveq2d 6626 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥))) = (ℝ D 𝐹))
10580feqmptd 6211 . . . . . . . . . 10 (𝜑𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)))
106104, 69, 1053eqtrd 2659 . . . . . . . . 9 (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)))
107 fveq2 6153 . . . . . . . . 9 (𝑥 = (𝐴 + 𝑠) → (𝐹𝑥) = (𝐹‘(𝐴 + 𝑠)))
108 fveq2 6153 . . . . . . . . 9 (𝑥 = (𝐴 + 𝑠) → (𝐺𝑥) = (𝐺‘(𝐴 + 𝑠)))
10960, 60, 40, 76, 78, 81, 101, 106, 107, 108dvmptco 23658 . . . . . . . 8 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐹‘(𝐴 + 𝑠)))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) · 1)))
11075recnd 10020 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐺‘(𝐴 + 𝑠)) ∈ ℂ)
111110mulid1d 10009 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((𝐺‘(𝐴 + 𝑠)) · 1) = (𝐺‘(𝐴 + 𝑠)))
112111mpteq2dva 4709 . . . . . . . 8 (𝜑 → (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) · 1)) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))))
113109, 112eqtrd 2655 . . . . . . 7 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐹‘(𝐴 + 𝑠)))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))))
114 limccl 23562 . . . . . . . . 9 (𝐹 lim 𝐴) ⊆ ℂ
115114, 48sseldi 3585 . . . . . . . 8 (𝜑𝑌 ∈ ℂ)
116115adantr 481 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 𝑌 ∈ ℂ)
117115adantr 481 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ) → 𝑌 ∈ ℂ)
11860, 115dvmptc 23644 . . . . . . . 8 (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑌)) = (𝑠 ∈ ℝ ↦ 0))
11960, 117, 84, 118, 87, 88, 46, 90dvmptres 23649 . . . . . . 7 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑌)) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 0))
12060, 61, 75, 113, 116, 25, 119dvmptsub 23653 . . . . . 6 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) − 0)))
121110subid1d 10333 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((𝐺‘(𝐴 + 𝑠)) − 0) = (𝐺‘(𝐴 + 𝑠)))
122121mpteq2dva 4709 . . . . . 6 (𝜑 → (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) − 0)) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))))
123120, 122eqtrd 2655 . . . . 5 (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))))
124123dmeqd 5291 . . . 4 (𝜑 → dom (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = dom (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))))
12575ralrimiva 2961 . . . . 5 (𝜑 → ∀𝑠 ∈ (0(,)(𝐵𝐴))(𝐺‘(𝐴 + 𝑠)) ∈ ℝ)
126 dmmptg 5596 . . . . 5 (∀𝑠 ∈ (0(,)(𝐵𝐴))(𝐺‘(𝐴 + 𝑠)) ∈ ℝ → dom (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (0(,)(𝐵𝐴)))
127125, 126syl 17 . . . 4 (𝜑 → dom (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (0(,)(𝐵𝐴)))
12858, 124, 1273eqtrd 2659 . . 3 (𝜑 → dom (ℝ D 𝑁) = (0(,)(𝐵𝐴)))
12954a1i 11 . . . . . . 7 (𝜑𝐷 = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠))
130129oveq2d 6626 . . . . . 6 (𝜑 → (ℝ D 𝐷) = (ℝ D (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠)))
131130, 97eqtrd 2655 . . . . 5 (𝜑 → (ℝ D 𝐷) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1))
132131dmeqd 5291 . . . 4 (𝜑 → dom (ℝ D 𝐷) = dom (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1))
13376ralrimiva 2961 . . . . 5 (𝜑 → ∀𝑠 ∈ (0(,)(𝐵𝐴))1 ∈ ℝ)
134 dmmptg 5596 . . . . 5 (∀𝑠 ∈ (0(,)(𝐵𝐴))1 ∈ ℝ → dom (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1) = (0(,)(𝐵𝐴)))
135133, 134syl 17 . . . 4 (𝜑 → dom (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1) = (0(,)(𝐵𝐴)))
136132, 135eqtrd 2655 . . 3 (𝜑 → dom (ℝ D 𝐷) = (0(,)(𝐵𝐴)))
137 eqid 2621 . . . . 5 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐹‘(𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐹‘(𝐴 + 𝑠)))
138 eqid 2621 . . . . 5 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑌) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑌)
139 eqid 2621 . . . . 5 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))
14040adantrr 752 . . . . . 6 ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐴 + 𝑠) ≠ 𝐴)) → (𝐴 + 𝑠) ∈ (𝐴(,)𝐵))
141 eqid 2621 . . . . . . . 8 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝐴) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝐴)
142 eqid 2621 . . . . . . . 8 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠)
143 eqid 2621 . . . . . . . 8 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐴 + 𝑠)) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐴 + 𝑠))
14487, 44syl6ss 3599 . . . . . . . . 9 (𝜑 → (0(,)(𝐵𝐴)) ⊆ ℂ)
1451recnd 10020 . . . . . . . . 9 (𝜑 → 0 ∈ ℂ)
146141, 144, 19, 145constlimc 39288 . . . . . . . 8 (𝜑𝐴 ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝐴) lim 0))
147144, 142, 145idlimc 39290 . . . . . . . 8 (𝜑 → 0 ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠) lim 0))
148141, 142, 143, 82, 92, 146, 147addlimc 39312 . . . . . . 7 (𝜑 → (𝐴 + 0) ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐴 + 𝑠)) lim 0))
14921, 148eqeltrd 2698 . . . . . 6 (𝜑𝐴 ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐴 + 𝑠)) lim 0))
150102oveq1d 6625 . . . . . . 7 (𝜑 → (𝐹 lim 𝐴) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) lim 𝐴))
15148, 150eleqtrd 2700 . . . . . 6 (𝜑𝑌 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) lim 𝐴))
152 simplrr 800 . . . . . . 7 (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐹‘(𝐴 + 𝑠)) = 𝑌) → (𝐴 + 𝑠) = 𝐴)
15315, 31gtned 10124 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐴 + 𝑠) ≠ 𝐴)
154153neneqd 2795 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ¬ (𝐴 + 𝑠) = 𝐴)
155154adantrr 752 . . . . . . . 8 ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → ¬ (𝐴 + 𝑠) = 𝐴)
156155adantr 481 . . . . . . 7 (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐹‘(𝐴 + 𝑠)) = 𝑌) → ¬ (𝐴 + 𝑠) = 𝐴)
157152, 156condan 834 . . . . . 6 ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → (𝐹‘(𝐴 + 𝑠)) = 𝑌)
158140, 78, 149, 151, 107, 157limcco 23580 . . . . 5 (𝜑𝑌 ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐹‘(𝐴 + 𝑠))) lim 0))
159138, 144, 115, 145constlimc 39288 . . . . 5 (𝜑𝑌 ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑌) lim 0))
160137, 138, 139, 61, 116, 158, 159sublimc 39316 . . . 4 (𝜑 → (𝑌𝑌) ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) lim 0))
161115subidd 10332 . . . 4 (𝜑 → (𝑌𝑌) = 0)
16252eqcomi 2630 . . . . . 6 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) = 𝑁
163162oveq1i 6620 . . . . 5 ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) lim 0) = (𝑁 lim 0)
164163a1i 11 . . . 4 (𝜑 → ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) lim 0) = (𝑁 lim 0))
165160, 161, 1643eltr3d 2712 . . 3 (𝜑 → 0 ∈ (𝑁 lim 0))
166144, 54, 145idlimc 39290 . . 3 (𝜑 → 0 ∈ (𝐷 lim 0))
167 lbioo 12156 . . . . 5 ¬ 0 ∈ (0(,)(𝐵𝐴))
168167a1i 11 . . . 4 (𝜑 → ¬ 0 ∈ (0(,)(𝐵𝐴)))
169 mptresid 5420 . . . . . . 7 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 𝑠) = ( I ↾ (0(,)(𝐵𝐴)))
170129, 169syl6eq 2671 . . . . . 6 (𝜑𝐷 = ( I ↾ (0(,)(𝐵𝐴))))
171170rneqd 5318 . . . . 5 (𝜑 → ran 𝐷 = ran ( I ↾ (0(,)(𝐵𝐴))))
172 rnresi 5443 . . . . 5 ran ( I ↾ (0(,)(𝐵𝐴))) = (0(,)(𝐵𝐴))
173171, 172syl6req 2672 . . . 4 (𝜑 → (0(,)(𝐵𝐴)) = ran 𝐷)
174168, 173neleqtrd 2719 . . 3 (𝜑 → ¬ 0 ∈ ran 𝐷)
175 0ne1 11040 . . . . . 6 0 ≠ 1
176175neii 2792 . . . . 5 ¬ 0 = 1
177 elsng 4167 . . . . . 6 (0 ∈ ℝ → (0 ∈ {1} ↔ 0 = 1))
1781, 177syl 17 . . . . 5 (𝜑 → (0 ∈ {1} ↔ 0 = 1))
179176, 178mtbiri 317 . . . 4 (𝜑 → ¬ 0 ∈ {1})
180131rneqd 5318 . . . . 5 (𝜑 → ran (ℝ D 𝐷) = ran (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1))
181 eqid 2621 . . . . . 6 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1)
18224a1i 11 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
183 ioon0 12151 . . . . . . . 8 ((0 ∈ ℝ* ∧ (𝐵𝐴) ∈ ℝ*) → ((0(,)(𝐵𝐴)) ≠ ∅ ↔ 0 < (𝐵𝐴)))
184182, 5, 183syl2anc 692 . . . . . . 7 (𝜑 → ((0(,)(𝐵𝐴)) ≠ ∅ ↔ 0 < (𝐵𝐴)))
1858, 184mpbird 247 . . . . . 6 (𝜑 → (0(,)(𝐵𝐴)) ≠ ∅)
186181, 76, 185rnmptc 38858 . . . . 5 (𝜑 → ran (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1) = {1})
187180, 186eqtr2d 2656 . . . 4 (𝜑 → {1} = ran (ℝ D 𝐷))
188179, 187neleqtrd 2719 . . 3 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐷))
18981recnd 10020 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐺𝑥) ∈ ℂ)
190 fourierdlem61.e . . . . . 6 (𝜑𝐸 ∈ (𝐺 lim 𝐴))
191105oveq1d 6625 . . . . . 6 (𝜑 → (𝐺 lim 𝐴) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)) lim 𝐴))
192190, 191eleqtrd 2700 . . . . 5 (𝜑𝐸 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)) lim 𝐴))
193 simplrr 800 . . . . . 6 (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐺‘(𝐴 + 𝑠)) = 𝐸) → (𝐴 + 𝑠) = 𝐴)
194155adantr 481 . . . . . 6 (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐺‘(𝐴 + 𝑠)) = 𝐸) → ¬ (𝐴 + 𝑠) = 𝐴)
195193, 194condan 834 . . . . 5 ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → (𝐺‘(𝐴 + 𝑠)) = 𝐸)
196140, 189, 149, 192, 108, 195limcco 23580 . . . 4 (𝜑𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) lim 0))
197110div1d 10745 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((𝐺‘(𝐴 + 𝑠)) / 1) = (𝐺‘(𝐴 + 𝑠)))
19856, 123syl5eq 2667 . . . . . . . . . . 11 (𝜑 → (ℝ D 𝑁) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))))
199198adantr 481 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (ℝ D 𝑁) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))))
200199fveq1d 6155 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((ℝ D 𝑁)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠))
201 eqid 2621 . . . . . . . . . . 11 (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))
202201fvmpt2 6253 . . . . . . . . . 10 ((𝑠 ∈ (0(,)(𝐵𝐴)) ∧ (𝐺‘(𝐴 + 𝑠)) ∈ ℝ) → ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠) = (𝐺‘(𝐴 + 𝑠)))
20327, 75, 202syl2anc 692 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠) = (𝐺‘(𝐴 + 𝑠)))
204200, 203eqtr2d 2656 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐺‘(𝐴 + 𝑠)) = ((ℝ D 𝑁)‘𝑠))
205131fveq1d 6155 . . . . . . . . . 10 (𝜑 → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1)‘𝑠))
206205adantr 481 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1)‘𝑠))
207181fvmpt2 6253 . . . . . . . . . 10 ((𝑠 ∈ (0(,)(𝐵𝐴)) ∧ 1 ∈ ℝ) → ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1)‘𝑠) = 1)
20827, 76, 207syl2anc 692 . . . . . . . . 9 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ 1)‘𝑠) = 1)
209206, 208eqtr2d 2656 . . . . . . . 8 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → 1 = ((ℝ D 𝐷)‘𝑠))
210204, 209oveq12d 6628 . . . . . . 7 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((𝐺‘(𝐴 + 𝑠)) / 1) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠)))
211197, 210eqtr3d 2657 . . . . . 6 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐺‘(𝐴 + 𝑠)) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠)))
212211mpteq2dva 4709 . . . . 5 (𝜑 → (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))))
213212oveq1d 6625 . . . 4 (𝜑 → ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) lim 0) = ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) lim 0))
214196, 213eleqtrd 2700 . . 3 (𝜑𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) lim 0))
2151, 5, 8, 53, 55, 128, 136, 165, 166, 174, 188, 214lhop1 23698 . 2 (𝜑𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝑁𝑠) / (𝐷𝑠))) lim 0))
21652fvmpt2 6253 . . . . . . 7 ((𝑠 ∈ (0(,)(𝐵𝐴)) ∧ ((𝐹‘(𝐴 + 𝑠)) − 𝑌) ∈ ℝ) → (𝑁𝑠) = ((𝐹‘(𝐴 + 𝑠)) − 𝑌))
21727, 51, 216syl2anc 692 . . . . . 6 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝑁𝑠) = ((𝐹‘(𝐴 + 𝑠)) − 𝑌))
21854fvmpt2 6253 . . . . . . 7 ((𝑠 ∈ (0(,)(𝐵𝐴)) ∧ 𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐷𝑠) = 𝑠)
21927, 27, 218syl2anc 692 . . . . . 6 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → (𝐷𝑠) = 𝑠)
220217, 219oveq12d 6628 . . . . 5 ((𝜑𝑠 ∈ (0(,)(𝐵𝐴))) → ((𝑁𝑠) / (𝐷𝑠)) = (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠))
221220mpteq2dva 4709 . . . 4 (𝜑 → (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝑁𝑠) / (𝐷𝑠))) = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠)))
222 fourierdlem61.h . . . 4 𝐻 = (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠))
223221, 222syl6eqr 2673 . . 3 (𝜑 → (𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝑁𝑠) / (𝐷𝑠))) = 𝐻)
224223oveq1d 6625 . 2 (𝜑 → ((𝑠 ∈ (0(,)(𝐵𝐴)) ↦ ((𝑁𝑠) / (𝐷𝑠))) lim 0) = (𝐻 lim 0))
225215, 224eleqtrd 2700 1 (𝜑𝐸 ∈ (𝐻 lim 0))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907   ⊆ wss 3559  ∅c0 3896  {csn 4153  {cpr 4155   class class class wbr 4618   ↦ cmpt 4678   I cid 4989  dom cdm 5079  ran crn 5080   ↾ cres 5081  ⟶wf 5848  ‘cfv 5852  (class class class)co 6610  ℂcc 9886  ℝcr 9887  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893  ℝ*cxr 10025   < clt 10026   − cmin 10218   / cdiv 10636  (,)cioo 12125  TopOpenctopn 16014  topGenctg 16030  ℂfldccnfld 19678   limℂ climc 23549   D cdv 23550 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966  ax-addf 9967  ax-mulf 9968 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7861  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-fsupp 8228  df-fi 8269  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-z 11330  df-dec 11446  df-uz 11640  df-q 11741  df-rp 11785  df-xneg 11898  df-xadd 11899  df-xmul 11900  df-ioo 12129  df-ioc 12130  df-ico 12131  df-icc 12132  df-fz 12277  df-fzo 12415  df-seq 12750  df-exp 12809  df-hash 13066  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-struct 15794  df-ndx 15795  df-slot 15796  df-base 15797  df-sets 15798  df-ress 15799  df-plusg 15886  df-mulr 15887  df-starv 15888  df-sca 15889  df-vsca 15890  df-ip 15891  df-tset 15892  df-ple 15893  df-ds 15896  df-unif 15897  df-hom 15898  df-cco 15899  df-rest 16015  df-topn 16016  df-0g 16034  df-gsum 16035  df-topgen 16036  df-pt 16037  df-prds 16040  df-xrs 16094  df-qtop 16099  df-imas 16100  df-xps 16102  df-mre 16178  df-mrc 16179  df-acs 16181  df-mgm 17174  df-sgrp 17216  df-mnd 17227  df-submnd 17268  df-mulg 17473  df-cntz 17682  df-cmn 18127  df-psmet 19670  df-xmet 19671  df-met 19672  df-bl 19673  df-mopn 19674  df-fbas 19675  df-fg 19676  df-cnfld 19679  df-top 20631  df-topon 20648  df-topsp 20661  df-bases 20674  df-cld 20746  df-ntr 20747  df-cls 20748  df-nei 20825  df-lp 20863  df-perf 20864  df-cn 20954  df-cnp 20955  df-haus 21042  df-cmp 21113  df-tx 21288  df-hmeo 21481  df-fil 21573  df-fm 21665  df-flim 21666  df-flf 21667  df-xms 22048  df-ms 22049  df-tms 22050  df-cncf 22604  df-limc 23553  df-dv 23554 This theorem is referenced by:  fourierdlem75  39731
 Copyright terms: Public domain W3C validator