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

Theorem cncfperiod 45267
Description: A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
cncfperiod.a (𝜑𝐴 ⊆ ℂ)
cncfperiod.t (𝜑𝑇 ∈ ℝ)
cncfperiod.b 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)}
cncfperiod.f (𝜑𝐹:dom 𝐹⟶ℂ)
cncfperiod.cssdmf (𝜑𝐵 ⊆ dom 𝐹)
cncfperiod.fper ((𝜑𝑥𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
cncfperiod.fcn (𝜑 → (𝐹𝐴) ∈ (𝐴cn→ℂ))
Assertion
Ref Expression
cncfperiod (𝜑 → (𝐹𝐵) ∈ (𝐵cn→ℂ))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑥,𝑇,𝑦   𝜑,𝑥,𝑦

Proof of Theorem cncfperiod
Dummy variables 𝑎 𝑏 𝑤 𝑧 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cncfperiod.f . . 3 (𝜑𝐹:dom 𝐹⟶ℂ)
2 cncfperiod.cssdmf . . 3 (𝜑𝐵 ⊆ dom 𝐹)
31, 2fssresd 6764 . 2 (𝜑 → (𝐹𝐵):𝐵⟶ℂ)
4 fvoveq1 7443 . . . . . . . . . . 11 (𝑎 = (𝑥𝑇) → (abs‘(𝑎𝑏)) = (abs‘((𝑥𝑇) − 𝑏)))
54breq1d 5158 . . . . . . . . . 10 (𝑎 = (𝑥𝑇) → ((abs‘(𝑎𝑏)) < 𝑧 ↔ (abs‘((𝑥𝑇) − 𝑏)) < 𝑧))
65imbrov2fvoveq 7445 . . . . . . . . 9 (𝑎 = (𝑥𝑇) → (((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤) ↔ ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)))
76rexralbidv 3217 . . . . . . . 8 (𝑎 = (𝑥𝑇) → (∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤) ↔ ∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)))
87ralbidv 3174 . . . . . . 7 (𝑎 = (𝑥𝑇) → (∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤) ↔ ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)))
9 cncfperiod.fcn . . . . . . . . . 10 (𝜑 → (𝐹𝐴) ∈ (𝐴cn→ℂ))
109adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝐹𝐴) ∈ (𝐴cn→ℂ))
11 cncfperiod.a . . . . . . . . . . 11 (𝜑𝐴 ⊆ ℂ)
1211adantr 480 . . . . . . . . . 10 ((𝜑𝑥𝐵) → 𝐴 ⊆ ℂ)
13 ssidd 4003 . . . . . . . . . 10 ((𝜑𝑥𝐵) → ℂ ⊆ ℂ)
14 elcncf 24822 . . . . . . . . . 10 ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐹𝐴) ∈ (𝐴cn→ℂ) ↔ ((𝐹𝐴):𝐴⟶ℂ ∧ ∀𝑎𝐴𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤))))
1512, 13, 14syl2anc 583 . . . . . . . . 9 ((𝜑𝑥𝐵) → ((𝐹𝐴) ∈ (𝐴cn→ℂ) ↔ ((𝐹𝐴):𝐴⟶ℂ ∧ ∀𝑎𝐴𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤))))
1610, 15mpbid 231 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝐹𝐴):𝐴⟶ℂ ∧ ∀𝑎𝐴𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤)))
1716simprd 495 . . . . . . 7 ((𝜑𝑥𝐵) → ∀𝑎𝐴𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤))
18 simpr 484 . . . . . . . . . . 11 ((𝜑𝑥𝐵) → 𝑥𝐵)
19 cncfperiod.b . . . . . . . . . . 11 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)}
2018, 19eleqtrdi 2839 . . . . . . . . . 10 ((𝜑𝑥𝐵) → 𝑥 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)})
21 rabid 3449 . . . . . . . . . 10 (𝑥 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)))
2220, 21sylib 217 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝑥 ∈ ℂ ∧ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)))
2322simprd 495 . . . . . . . 8 ((𝜑𝑥𝐵) → ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇))
24 oveq1 7427 . . . . . . . . . . . 12 (𝑥 = (𝑦 + 𝑇) → (𝑥𝑇) = ((𝑦 + 𝑇) − 𝑇))
25243ad2ant3 1133 . . . . . . . . . . 11 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → (𝑥𝑇) = ((𝑦 + 𝑇) − 𝑇))
2611sselda 3980 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
27 cncfperiod.t . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ ℝ)
2827recnd 11273 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℂ)
2928adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴) → 𝑇 ∈ ℂ)
3026, 29pncand 11603 . . . . . . . . . . . . 13 ((𝜑𝑦𝐴) → ((𝑦 + 𝑇) − 𝑇) = 𝑦)
3130adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑥𝐵) ∧ 𝑦𝐴) → ((𝑦 + 𝑇) − 𝑇) = 𝑦)
32313adant3 1130 . . . . . . . . . . 11 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → ((𝑦 + 𝑇) − 𝑇) = 𝑦)
3325, 32eqtrd 2768 . . . . . . . . . 10 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → (𝑥𝑇) = 𝑦)
34 simp2 1135 . . . . . . . . . 10 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → 𝑦𝐴)
3533, 34eqeltrd 2829 . . . . . . . . 9 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → (𝑥𝑇) ∈ 𝐴)
3635rexlimdv3a 3156 . . . . . . . 8 ((𝜑𝑥𝐵) → (∃𝑦𝐴 𝑥 = (𝑦 + 𝑇) → (𝑥𝑇) ∈ 𝐴))
3723, 36mpd 15 . . . . . . 7 ((𝜑𝑥𝐵) → (𝑥𝑇) ∈ 𝐴)
388, 17, 37rspcdva 3610 . . . . . 6 ((𝜑𝑥𝐵) → ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
3938adantrr 716 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
40 simprr 772 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → 𝑤 ∈ ℝ+)
41 rspa 3242 . . . . 5 ((∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤) ∧ 𝑤 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
4239, 40, 41syl2anc 583 . . . 4 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
43 simpl1l 1222 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) → 𝜑)
4443adantr 480 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → 𝜑)
45 simp1rl 1236 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) → 𝑥𝐵)
4645adantr 480 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) → 𝑥𝐵)
4746adantr 480 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → 𝑥𝐵)
48 simplr 768 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → 𝑣𝐵)
49 fvres 6916 . . . . . . . . . . . . . . 15 (𝑥𝐵 → ((𝐹𝐵)‘𝑥) = (𝐹𝑥))
5049adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → ((𝐹𝐵)‘𝑥) = (𝐹𝑥))
5119ssrab3 4078 . . . . . . . . . . . . . . . . . . 19 𝐵 ⊆ ℂ
5251sseli 3976 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵𝑥 ∈ ℂ)
5352adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐵) → 𝑥 ∈ ℂ)
5428adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐵) → 𝑇 ∈ ℂ)
5553, 54npcand 11606 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐵) → ((𝑥𝑇) + 𝑇) = 𝑥)
5655eqcomd 2734 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐵) → 𝑥 = ((𝑥𝑇) + 𝑇))
5756fveq2d 6901 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → (𝐹𝑥) = (𝐹‘((𝑥𝑇) + 𝑇)))
58 simpl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐵) → 𝜑)
5958, 37jca 511 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐵) → (𝜑 ∧ (𝑥𝑇) ∈ 𝐴))
60 eleq1 2817 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥𝑇) → (𝑦𝐴 ↔ (𝑥𝑇) ∈ 𝐴))
6160anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥𝑇) → ((𝜑𝑦𝐴) ↔ (𝜑 ∧ (𝑥𝑇) ∈ 𝐴)))
62 fvoveq1 7443 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥𝑇) + 𝑇)))
63 fveq2 6897 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥𝑇) → (𝐹𝑦) = (𝐹‘(𝑥𝑇)))
6462, 63eqeq12d 2744 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
6561, 64imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥𝑇) → (((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥𝑇) ∈ 𝐴) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))))
66 eleq1 2817 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
6766anbi2d 629 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝜑𝑥𝐴) ↔ (𝜑𝑦𝐴)))
68 fvoveq1 7443 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
69 fveq2 6897 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
7068, 69eqeq12d 2744 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
7167, 70imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
72 cncfperiod.fper . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
7371, 72chvarvv 1995 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
7465, 73vtoclg 3540 . . . . . . . . . . . . . . . 16 ((𝑥𝑇) ∈ 𝐴 → ((𝜑 ∧ (𝑥𝑇) ∈ 𝐴) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
7537, 59, 74sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐵) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))
7637fvresd 6917 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐵) → ((𝐹𝐴)‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
7775, 76eqtr4d 2771 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → (𝐹‘((𝑥𝑇) + 𝑇)) = ((𝐹𝐴)‘(𝑥𝑇)))
7850, 57, 773eqtrd 2772 . . . . . . . . . . . . 13 ((𝜑𝑥𝐵) → ((𝐹𝐵)‘𝑥) = ((𝐹𝐴)‘(𝑥𝑇)))
79783adant3 1130 . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑣𝐵) → ((𝐹𝐵)‘𝑥) = ((𝐹𝐴)‘(𝑥𝑇)))
80 eleq1 2817 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (𝑥𝐵𝑣𝐵))
8180anbi2d 629 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → ((𝜑𝑥𝐵) ↔ (𝜑𝑣𝐵)))
82 fveq2 6897 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → ((𝐹𝐵)‘𝑥) = ((𝐹𝐵)‘𝑣))
83 fvoveq1 7443 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → ((𝐹𝐴)‘(𝑥𝑇)) = ((𝐹𝐴)‘(𝑣𝑇)))
8482, 83eqeq12d 2744 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (((𝐹𝐵)‘𝑥) = ((𝐹𝐴)‘(𝑥𝑇)) ↔ ((𝐹𝐵)‘𝑣) = ((𝐹𝐴)‘(𝑣𝑇))))
8581, 84imbi12d 344 . . . . . . . . . . . . . 14 (𝑥 = 𝑣 → (((𝜑𝑥𝐵) → ((𝐹𝐵)‘𝑥) = ((𝐹𝐴)‘(𝑥𝑇))) ↔ ((𝜑𝑣𝐵) → ((𝐹𝐵)‘𝑣) = ((𝐹𝐴)‘(𝑣𝑇)))))
8685, 78chvarvv 1995 . . . . . . . . . . . . 13 ((𝜑𝑣𝐵) → ((𝐹𝐵)‘𝑣) = ((𝐹𝐴)‘(𝑣𝑇)))
87863adant2 1129 . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑣𝐵) → ((𝐹𝐵)‘𝑣) = ((𝐹𝐴)‘(𝑣𝑇)))
8879, 87oveq12d 7438 . . . . . . . . . . 11 ((𝜑𝑥𝐵𝑣𝐵) → (((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣)) = (((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇))))
8988fveq2d 6901 . . . . . . . . . 10 ((𝜑𝑥𝐵𝑣𝐵) → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) = (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))))
9044, 47, 48, 89syl3anc 1369 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) = (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))))
91 simpr 484 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(𝑥𝑣)) < 𝑧)
9222simpld 494 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐵) → 𝑥 ∈ ℂ)
9392adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → 𝑥 ∈ ℂ)
9451sseli 3976 . . . . . . . . . . . . . . . 16 (𝑣𝐵𝑣 ∈ ℂ)
9594adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → 𝑣 ∈ ℂ)
9654adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → 𝑇 ∈ ℂ)
9793, 95, 96nnncan2d 11637 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → ((𝑥𝑇) − (𝑣𝑇)) = (𝑥𝑣))
9897fveq2d 6901 . . . . . . . . . . . . 13 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → (abs‘((𝑥𝑇) − (𝑣𝑇))) = (abs‘(𝑥𝑣)))
9998adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑥𝐵) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘((𝑥𝑇) − (𝑣𝑇))) = (abs‘(𝑥𝑣)))
100 simpr 484 . . . . . . . . . . . 12 ((((𝜑𝑥𝐵) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(𝑥𝑣)) < 𝑧)
10199, 100eqbrtrd 5170 . . . . . . . . . . 11 ((((𝜑𝑥𝐵) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧)
10244, 47, 48, 91, 101syl1111anc 839 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧)
103 oveq2 7428 . . . . . . . . . . . . . 14 (𝑏 = (𝑣𝑇) → ((𝑥𝑇) − 𝑏) = ((𝑥𝑇) − (𝑣𝑇)))
104103fveq2d 6901 . . . . . . . . . . . . 13 (𝑏 = (𝑣𝑇) → (abs‘((𝑥𝑇) − 𝑏)) = (abs‘((𝑥𝑇) − (𝑣𝑇))))
105104breq1d 5158 . . . . . . . . . . . 12 (𝑏 = (𝑣𝑇) → ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 ↔ (abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧))
106 fveq2 6897 . . . . . . . . . . . . . . 15 (𝑏 = (𝑣𝑇) → ((𝐹𝐴)‘𝑏) = ((𝐹𝐴)‘(𝑣𝑇)))
107106oveq2d 7436 . . . . . . . . . . . . . 14 (𝑏 = (𝑣𝑇) → (((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏)) = (((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇))))
108107fveq2d 6901 . . . . . . . . . . . . 13 (𝑏 = (𝑣𝑇) → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) = (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))))
109108breq1d 5158 . . . . . . . . . . . 12 (𝑏 = (𝑣𝑇) → ((abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤 ↔ (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))) < 𝑤))
110105, 109imbi12d 344 . . . . . . . . . . 11 (𝑏 = (𝑣𝑇) → (((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤) ↔ ((abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))) < 𝑤)))
111 simpll3 1212 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
112 oveq1 7427 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (𝑥𝑇) = (𝑣𝑇))
113112eleq1d 2814 . . . . . . . . . . . . . 14 (𝑥 = 𝑣 → ((𝑥𝑇) ∈ 𝐴 ↔ (𝑣𝑇) ∈ 𝐴))
11481, 113imbi12d 344 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (((𝜑𝑥𝐵) → (𝑥𝑇) ∈ 𝐴) ↔ ((𝜑𝑣𝐵) → (𝑣𝑇) ∈ 𝐴)))
115114, 37chvarvv 1995 . . . . . . . . . . . 12 ((𝜑𝑣𝐵) → (𝑣𝑇) ∈ 𝐴)
11644, 48, 115syl2anc 583 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (𝑣𝑇) ∈ 𝐴)
117110, 111, 116rspcdva 3610 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → ((abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))) < 𝑤))
118102, 117mpd 15 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))) < 𝑤)
11990, 118eqbrtrd 5170 . . . . . . . 8 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤)
120119ex 412 . . . . . . 7 ((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) → ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))
121120ralrimiva 3143 . . . . . 6 (((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) → ∀𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))
1221213exp 1117 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → (𝑧 ∈ ℝ+ → (∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤) → ∀𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))))
123122reximdvai 3162 . . . 4 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → (∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤) → ∃𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤)))
12442, 123mpd 15 . . 3 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))
125124ralrimivva 3197 . 2 (𝜑 → ∀𝑥𝐵𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))
12651a1i 11 . . 3 (𝜑𝐵 ⊆ ℂ)
127 ssidd 4003 . . 3 (𝜑 → ℂ ⊆ ℂ)
128 elcncf 24822 . . 3 ((𝐵 ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐹𝐵) ∈ (𝐵cn→ℂ) ↔ ((𝐹𝐵):𝐵⟶ℂ ∧ ∀𝑥𝐵𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))))
129126, 127, 128syl2anc 583 . 2 (𝜑 → ((𝐹𝐵) ∈ (𝐵cn→ℂ) ↔ ((𝐹𝐵):𝐵⟶ℂ ∧ ∀𝑥𝐵𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))))
1303, 125, 129mpbir2and 712 1 (𝜑 → (𝐹𝐵) ∈ (𝐵cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wral 3058  wrex 3067  {crab 3429  wss 3947   class class class wbr 5148  dom cdm 5678  cres 5680  wf 6544  cfv 6548  (class class class)co 7420  cc 11137  cr 11138   + caddc 11142   < clt 11279  cmin 11475  +crp 13007  abscabs 15214  cnccncf 24809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11195  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11281  df-mnf 11282  df-ltxr 11284  df-sub 11477  df-cncf 24811
This theorem is referenced by:  itgperiod  45369  fourierdlem81  45575
  Copyright terms: Public domain W3C validator