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

Theorem cncfperiod 42915
 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 6534 . 2 (𝜑 → (𝐹𝐵):𝐵⟶ℂ)
4 fvoveq1 7178 . . . . . . . . . . 11 (𝑎 = (𝑥𝑇) → (abs‘(𝑎𝑏)) = (abs‘((𝑥𝑇) − 𝑏)))
54breq1d 5045 . . . . . . . . . 10 (𝑎 = (𝑥𝑇) → ((abs‘(𝑎𝑏)) < 𝑧 ↔ (abs‘((𝑥𝑇) − 𝑏)) < 𝑧))
65imbrov2fvoveq 7180 . . . . . . . . 9 (𝑎 = (𝑥𝑇) → (((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤) ↔ ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)))
76rexralbidv 3225 . . . . . . . 8 (𝑎 = (𝑥𝑇) → (∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤) ↔ ∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)))
87ralbidv 3126 . . . . . . 7 (𝑎 = (𝑥𝑇) → (∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤) ↔ ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)))
9 cncfperiod.fcn . . . . . . . . . 10 (𝜑 → (𝐹𝐴) ∈ (𝐴cn→ℂ))
109adantr 484 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝐹𝐴) ∈ (𝐴cn→ℂ))
11 cncfperiod.a . . . . . . . . . . 11 (𝜑𝐴 ⊆ ℂ)
1211adantr 484 . . . . . . . . . 10 ((𝜑𝑥𝐵) → 𝐴 ⊆ ℂ)
13 ssidd 3917 . . . . . . . . . 10 ((𝜑𝑥𝐵) → ℂ ⊆ ℂ)
14 elcncf 23595 . . . . . . . . . 10 ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐹𝐴) ∈ (𝐴cn→ℂ) ↔ ((𝐹𝐴):𝐴⟶ℂ ∧ ∀𝑎𝐴𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤))))
1512, 13, 14syl2anc 587 . . . . . . . . 9 ((𝜑𝑥𝐵) → ((𝐹𝐴) ∈ (𝐴cn→ℂ) ↔ ((𝐹𝐴):𝐴⟶ℂ ∧ ∀𝑎𝐴𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤))))
1610, 15mpbid 235 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝐹𝐴):𝐴⟶ℂ ∧ ∀𝑎𝐴𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤)))
1716simprd 499 . . . . . . 7 ((𝜑𝑥𝐵) → ∀𝑎𝐴𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘(𝑎𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘𝑎) − ((𝐹𝐴)‘𝑏))) < 𝑤))
18 simpr 488 . . . . . . . . . . 11 ((𝜑𝑥𝐵) → 𝑥𝐵)
19 cncfperiod.b . . . . . . . . . . 11 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)}
2018, 19eleqtrdi 2862 . . . . . . . . . 10 ((𝜑𝑥𝐵) → 𝑥 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)})
21 rabid 3296 . . . . . . . . . 10 (𝑥 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)))
2220, 21sylib 221 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝑥 ∈ ℂ ∧ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)))
2322simprd 499 . . . . . . . 8 ((𝜑𝑥𝐵) → ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇))
24 oveq1 7162 . . . . . . . . . . . 12 (𝑥 = (𝑦 + 𝑇) → (𝑥𝑇) = ((𝑦 + 𝑇) − 𝑇))
25243ad2ant3 1132 . . . . . . . . . . 11 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → (𝑥𝑇) = ((𝑦 + 𝑇) − 𝑇))
2611sselda 3894 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴) → 𝑦 ∈ ℂ)
27 cncfperiod.t . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ ℝ)
2827recnd 10712 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℂ)
2928adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴) → 𝑇 ∈ ℂ)
3026, 29pncand 11041 . . . . . . . . . . . . 13 ((𝜑𝑦𝐴) → ((𝑦 + 𝑇) − 𝑇) = 𝑦)
3130adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑥𝐵) ∧ 𝑦𝐴) → ((𝑦 + 𝑇) − 𝑇) = 𝑦)
32313adant3 1129 . . . . . . . . . . 11 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → ((𝑦 + 𝑇) − 𝑇) = 𝑦)
3325, 32eqtrd 2793 . . . . . . . . . 10 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → (𝑥𝑇) = 𝑦)
34 simp2 1134 . . . . . . . . . 10 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → 𝑦𝐴)
3533, 34eqeltrd 2852 . . . . . . . . 9 (((𝜑𝑥𝐵) ∧ 𝑦𝐴𝑥 = (𝑦 + 𝑇)) → (𝑥𝑇) ∈ 𝐴)
3635rexlimdv3a 3210 . . . . . . . 8 ((𝜑𝑥𝐵) → (∃𝑦𝐴 𝑥 = (𝑦 + 𝑇) → (𝑥𝑇) ∈ 𝐴))
3723, 36mpd 15 . . . . . . 7 ((𝜑𝑥𝐵) → (𝑥𝑇) ∈ 𝐴)
388, 17, 37rspcdva 3545 . . . . . 6 ((𝜑𝑥𝐵) → ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
3938adantrr 716 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
40 simprr 772 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → 𝑤 ∈ ℝ+)
41 rspa 3135 . . . . 5 ((∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤) ∧ 𝑤 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
4239, 40, 41syl2anc 587 . . . 4 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
43 simpl1l 1221 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) → 𝜑)
4443adantr 484 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → 𝜑)
45 simp1rl 1235 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) → 𝑥𝐵)
4645adantr 484 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) → 𝑥𝐵)
4746adantr 484 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → 𝑥𝐵)
48 simplr 768 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → 𝑣𝐵)
49 fvres 6681 . . . . . . . . . . . . . . 15 (𝑥𝐵 → ((𝐹𝐵)‘𝑥) = (𝐹𝑥))
5049adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → ((𝐹𝐵)‘𝑥) = (𝐹𝑥))
5119ssrab3 3988 . . . . . . . . . . . . . . . . . . 19 𝐵 ⊆ ℂ
5251sseli 3890 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵𝑥 ∈ ℂ)
5352adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐵) → 𝑥 ∈ ℂ)
5428adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐵) → 𝑇 ∈ ℂ)
5553, 54npcand 11044 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐵) → ((𝑥𝑇) + 𝑇) = 𝑥)
5655eqcomd 2764 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐵) → 𝑥 = ((𝑥𝑇) + 𝑇))
5756fveq2d 6666 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → (𝐹𝑥) = (𝐹‘((𝑥𝑇) + 𝑇)))
58 simpl 486 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐵) → 𝜑)
5958, 37jca 515 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐵) → (𝜑 ∧ (𝑥𝑇) ∈ 𝐴))
60 eleq1 2839 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥𝑇) → (𝑦𝐴 ↔ (𝑥𝑇) ∈ 𝐴))
6160anbi2d 631 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥𝑇) → ((𝜑𝑦𝐴) ↔ (𝜑 ∧ (𝑥𝑇) ∈ 𝐴)))
62 fvoveq1 7178 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥𝑇) + 𝑇)))
63 fveq2 6662 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥𝑇) → (𝐹𝑦) = (𝐹‘(𝑥𝑇)))
6462, 63eqeq12d 2774 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
6561, 64imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥𝑇) → (((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥𝑇) ∈ 𝐴) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))))
66 eleq1 2839 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
6766anbi2d 631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝜑𝑥𝐴) ↔ (𝜑𝑦𝐴)))
68 fvoveq1 7178 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
69 fveq2 6662 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
7068, 69eqeq12d 2774 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
7167, 70imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
72 cncfperiod.fper . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
7371, 72chvarvv 2005 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
7465, 73vtoclg 3487 . . . . . . . . . . . . . . . 16 ((𝑥𝑇) ∈ 𝐴 → ((𝜑 ∧ (𝑥𝑇) ∈ 𝐴) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
7537, 59, 74sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐵) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))
7637fvresd 6682 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐵) → ((𝐹𝐴)‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
7775, 76eqtr4d 2796 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → (𝐹‘((𝑥𝑇) + 𝑇)) = ((𝐹𝐴)‘(𝑥𝑇)))
7850, 57, 773eqtrd 2797 . . . . . . . . . . . . 13 ((𝜑𝑥𝐵) → ((𝐹𝐵)‘𝑥) = ((𝐹𝐴)‘(𝑥𝑇)))
79783adant3 1129 . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑣𝐵) → ((𝐹𝐵)‘𝑥) = ((𝐹𝐴)‘(𝑥𝑇)))
80 eleq1 2839 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (𝑥𝐵𝑣𝐵))
8180anbi2d 631 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → ((𝜑𝑥𝐵) ↔ (𝜑𝑣𝐵)))
82 fveq2 6662 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → ((𝐹𝐵)‘𝑥) = ((𝐹𝐵)‘𝑣))
83 fvoveq1 7178 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → ((𝐹𝐴)‘(𝑥𝑇)) = ((𝐹𝐴)‘(𝑣𝑇)))
8482, 83eqeq12d 2774 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (((𝐹𝐵)‘𝑥) = ((𝐹𝐴)‘(𝑥𝑇)) ↔ ((𝐹𝐵)‘𝑣) = ((𝐹𝐴)‘(𝑣𝑇))))
8581, 84imbi12d 348 . . . . . . . . . . . . . 14 (𝑥 = 𝑣 → (((𝜑𝑥𝐵) → ((𝐹𝐵)‘𝑥) = ((𝐹𝐴)‘(𝑥𝑇))) ↔ ((𝜑𝑣𝐵) → ((𝐹𝐵)‘𝑣) = ((𝐹𝐴)‘(𝑣𝑇)))))
8685, 78chvarvv 2005 . . . . . . . . . . . . 13 ((𝜑𝑣𝐵) → ((𝐹𝐵)‘𝑣) = ((𝐹𝐴)‘(𝑣𝑇)))
87863adant2 1128 . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑣𝐵) → ((𝐹𝐵)‘𝑣) = ((𝐹𝐴)‘(𝑣𝑇)))
8879, 87oveq12d 7173 . . . . . . . . . . 11 ((𝜑𝑥𝐵𝑣𝐵) → (((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣)) = (((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇))))
8988fveq2d 6666 . . . . . . . . . 10 ((𝜑𝑥𝐵𝑣𝐵) → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) = (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))))
9044, 47, 48, 89syl3anc 1368 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) = (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))))
91 simpr 488 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(𝑥𝑣)) < 𝑧)
9222simpld 498 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐵) → 𝑥 ∈ ℂ)
9392adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → 𝑥 ∈ ℂ)
9451sseli 3890 . . . . . . . . . . . . . . . 16 (𝑣𝐵𝑣 ∈ ℂ)
9594adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → 𝑣 ∈ ℂ)
9654adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → 𝑇 ∈ ℂ)
9793, 95, 96nnncan2d 11075 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → ((𝑥𝑇) − (𝑣𝑇)) = (𝑥𝑣))
9897fveq2d 6666 . . . . . . . . . . . . 13 (((𝜑𝑥𝐵) ∧ 𝑣𝐵) → (abs‘((𝑥𝑇) − (𝑣𝑇))) = (abs‘(𝑥𝑣)))
9998adantr 484 . . . . . . . . . . . 12 ((((𝜑𝑥𝐵) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘((𝑥𝑇) − (𝑣𝑇))) = (abs‘(𝑥𝑣)))
100 simpr 488 . . . . . . . . . . . 12 ((((𝜑𝑥𝐵) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(𝑥𝑣)) < 𝑧)
10199, 100eqbrtrd 5057 . . . . . . . . . . 11 ((((𝜑𝑥𝐵) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧)
10244, 47, 48, 91, 101syl1111anc 838 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧)
103 oveq2 7163 . . . . . . . . . . . . . 14 (𝑏 = (𝑣𝑇) → ((𝑥𝑇) − 𝑏) = ((𝑥𝑇) − (𝑣𝑇)))
104103fveq2d 6666 . . . . . . . . . . . . 13 (𝑏 = (𝑣𝑇) → (abs‘((𝑥𝑇) − 𝑏)) = (abs‘((𝑥𝑇) − (𝑣𝑇))))
105104breq1d 5045 . . . . . . . . . . . 12 (𝑏 = (𝑣𝑇) → ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 ↔ (abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧))
106 fveq2 6662 . . . . . . . . . . . . . . 15 (𝑏 = (𝑣𝑇) → ((𝐹𝐴)‘𝑏) = ((𝐹𝐴)‘(𝑣𝑇)))
107106oveq2d 7171 . . . . . . . . . . . . . 14 (𝑏 = (𝑣𝑇) → (((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏)) = (((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇))))
108107fveq2d 6666 . . . . . . . . . . . . 13 (𝑏 = (𝑣𝑇) → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) = (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))))
109108breq1d 5045 . . . . . . . . . . . 12 (𝑏 = (𝑣𝑇) → ((abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤 ↔ (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))) < 𝑤))
110105, 109imbi12d 348 . . . . . . . . . . 11 (𝑏 = (𝑣𝑇) → (((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤) ↔ ((abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))) < 𝑤)))
111 simpll3 1211 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤))
112 oveq1 7162 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (𝑥𝑇) = (𝑣𝑇))
113112eleq1d 2836 . . . . . . . . . . . . . 14 (𝑥 = 𝑣 → ((𝑥𝑇) ∈ 𝐴 ↔ (𝑣𝑇) ∈ 𝐴))
11481, 113imbi12d 348 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (((𝜑𝑥𝐵) → (𝑥𝑇) ∈ 𝐴) ↔ ((𝜑𝑣𝐵) → (𝑣𝑇) ∈ 𝐴)))
115114, 37chvarvv 2005 . . . . . . . . . . . 12 ((𝜑𝑣𝐵) → (𝑣𝑇) ∈ 𝐴)
11644, 48, 115syl2anc 587 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (𝑣𝑇) ∈ 𝐴)
117110, 111, 116rspcdva 3545 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → ((abs‘((𝑥𝑇) − (𝑣𝑇))) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))) < 𝑤))
118102, 117mpd 15 . . . . . . . . 9 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘(𝑣𝑇)))) < 𝑤)
11990, 118eqbrtrd 5057 . . . . . . . 8 (((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) ∧ (abs‘(𝑥𝑣)) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤)
120119ex 416 . . . . . . 7 ((((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) ∧ 𝑣𝐵) → ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))
121120ralrimiva 3113 . . . . . 6 (((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤)) → ∀𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))
1221213exp 1116 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → (𝑧 ∈ ℝ+ → (∀𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤) → ∀𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))))
123122reximdvai 3196 . . . 4 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → (∃𝑧 ∈ ℝ+𝑏𝐴 ((abs‘((𝑥𝑇) − 𝑏)) < 𝑧 → (abs‘(((𝐹𝐴)‘(𝑥𝑇)) − ((𝐹𝐴)‘𝑏))) < 𝑤) → ∃𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤)))
12442, 123mpd 15 . . 3 ((𝜑 ∧ (𝑥𝐵𝑤 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))
125124ralrimivva 3120 . 2 (𝜑 → ∀𝑥𝐵𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))
12651a1i 11 . . 3 (𝜑𝐵 ⊆ ℂ)
127 ssidd 3917 . . 3 (𝜑 → ℂ ⊆ ℂ)
128 elcncf 23595 . . 3 ((𝐵 ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐹𝐵) ∈ (𝐵cn→ℂ) ↔ ((𝐹𝐵):𝐵⟶ℂ ∧ ∀𝑥𝐵𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))))
129126, 127, 128syl2anc 587 . 2 (𝜑 → ((𝐹𝐵) ∈ (𝐵cn→ℂ) ↔ ((𝐹𝐵):𝐵⟶ℂ ∧ ∀𝑥𝐵𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐵 ((abs‘(𝑥𝑣)) < 𝑧 → (abs‘(((𝐹𝐵)‘𝑥) − ((𝐹𝐵)‘𝑣))) < 𝑤))))
1303, 125, 129mpbir2and 712 1 (𝜑 → (𝐹𝐵) ∈ (𝐵cn→ℂ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  {crab 3074   ⊆ wss 3860   class class class wbr 5035  dom cdm 5527   ↾ cres 5529  ⟶wf 6335  ‘cfv 6339  (class class class)co 7155  ℂcc 10578  ℝcr 10579   + caddc 10583   < clt 10718   − cmin 10913  ℝ+crp 12435  abscabs 14646  –cn→ccncf 23582 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-po 5446  df-so 5447  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-er 8304  df-map 8423  df-en 8533  df-dom 8534  df-sdom 8535  df-pnf 10720  df-mnf 10721  df-ltxr 10723  df-sub 10915  df-cncf 23584 This theorem is referenced by:  itgperiod  43017  fourierdlem81  43223
 Copyright terms: Public domain W3C validator