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

Theorem limcperiod 40378
 Description: If 𝐹 is a periodic function with period 𝑇, the limit doesn't change if we shift the limiting point by 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
limcperiod.f (𝜑𝐹:dom 𝐹⟶ℂ)
limcperiod.assc (𝜑𝐴 ⊆ ℂ)
limcperiod.3 (𝜑𝐴 ⊆ dom 𝐹)
limcperiod.t (𝜑𝑇 ∈ ℂ)
limcperiod.b 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)}
limcperiod.bss (𝜑𝐵 ⊆ dom 𝐹)
limcperiod.fper ((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
limcperiod.clim (𝜑𝐶 ∈ ((𝐹𝐴) lim 𝐷))
Assertion
Ref Expression
limcperiod (𝜑𝐶 ∈ ((𝐹𝐵) lim (𝐷 + 𝑇)))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐹,𝑦   𝑥,𝑇,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)

Proof of Theorem limcperiod
Dummy variables 𝑏 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 23859 . . 3 ((𝐹𝐴) lim 𝐷) ⊆ ℂ
2 limcperiod.clim . . 3 (𝜑𝐶 ∈ ((𝐹𝐴) lim 𝐷))
31, 2sseldi 3750 . 2 (𝜑𝐶 ∈ ℂ)
4 limcperiod.f . . . . . . . . 9 (𝜑𝐹:dom 𝐹⟶ℂ)
5 limcperiod.3 . . . . . . . . 9 (𝜑𝐴 ⊆ dom 𝐹)
64, 5fssresd 6211 . . . . . . . 8 (𝜑 → (𝐹𝐴):𝐴⟶ℂ)
7 limcperiod.assc . . . . . . . 8 (𝜑𝐴 ⊆ ℂ)
8 limcrcl 23858 . . . . . . . . . 10 (𝐶 ∈ ((𝐹𝐴) lim 𝐷) → ((𝐹𝐴):dom (𝐹𝐴)⟶ℂ ∧ dom (𝐹𝐴) ⊆ ℂ ∧ 𝐷 ∈ ℂ))
92, 8syl 17 . . . . . . . . 9 (𝜑 → ((𝐹𝐴):dom (𝐹𝐴)⟶ℂ ∧ dom (𝐹𝐴) ⊆ ℂ ∧ 𝐷 ∈ ℂ))
109simp3d 1138 . . . . . . . 8 (𝜑𝐷 ∈ ℂ)
116, 7, 10ellimc3 23863 . . . . . . 7 (𝜑 → (𝐶 ∈ ((𝐹𝐴) lim 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤))))
122, 11mpbid 222 . . . . . 6 (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)))
1312simprd 477 . . . . 5 (𝜑 → ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤))
1413r19.21bi 3081 . . . 4 ((𝜑𝑤 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤))
15 simpl1l 1278 . . . . . . . . . . 11 ((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) → 𝜑)
1615adantr 466 . . . . . . . . . 10 (((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → 𝜑)
17 simplr 744 . . . . . . . . . 10 (((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → 𝑏𝐵)
18 id 22 . . . . . . . . . . . . . . . 16 (𝑏𝐵𝑏𝐵)
19 limcperiod.b . . . . . . . . . . . . . . . . 17 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)}
20 oveq1 6800 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑧 → (𝑦 + 𝑇) = (𝑧 + 𝑇))
2120eqeq2d 2781 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (𝑥 = (𝑦 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
2221cbvrexv 3321 . . . . . . . . . . . . . . . . . . 19 (∃𝑦𝐴 𝑥 = (𝑦 + 𝑇) ↔ ∃𝑧𝐴 𝑥 = (𝑧 + 𝑇))
23 eqeq1 2775 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑤 = (𝑧 + 𝑇)))
2423rexbidv 3200 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (∃𝑧𝐴 𝑥 = (𝑧 + 𝑇) ↔ ∃𝑧𝐴 𝑤 = (𝑧 + 𝑇)))
2522, 24syl5bb 272 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (∃𝑦𝐴 𝑥 = (𝑦 + 𝑇) ↔ ∃𝑧𝐴 𝑤 = (𝑧 + 𝑇)))
2625cbvrabv 3349 . . . . . . . . . . . . . . . . 17 {𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧𝐴 𝑤 = (𝑧 + 𝑇)}
2719, 26eqtri 2793 . . . . . . . . . . . . . . . 16 𝐵 = {𝑤 ∈ ℂ ∣ ∃𝑧𝐴 𝑤 = (𝑧 + 𝑇)}
2818, 27syl6eleq 2860 . . . . . . . . . . . . . . 15 (𝑏𝐵𝑏 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧𝐴 𝑤 = (𝑧 + 𝑇)})
29 eqeq1 2775 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑏 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑏 = (𝑧 + 𝑇)))
3029rexbidv 3200 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑏 → (∃𝑧𝐴 𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧𝐴 𝑏 = (𝑧 + 𝑇)))
3130elrab 3515 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧𝐴 𝑤 = (𝑧 + 𝑇)} ↔ (𝑏 ∈ ℂ ∧ ∃𝑧𝐴 𝑏 = (𝑧 + 𝑇)))
3228, 31sylib 208 . . . . . . . . . . . . . 14 (𝑏𝐵 → (𝑏 ∈ ℂ ∧ ∃𝑧𝐴 𝑏 = (𝑧 + 𝑇)))
3332simprd 477 . . . . . . . . . . . . 13 (𝑏𝐵 → ∃𝑧𝐴 𝑏 = (𝑧 + 𝑇))
3433adantl 467 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ∃𝑧𝐴 𝑏 = (𝑧 + 𝑇))
35 oveq1 6800 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑧 + 𝑇) → (𝑏𝑇) = ((𝑧 + 𝑇) − 𝑇))
36353ad2ant3 1129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝐴𝑏 = (𝑧 + 𝑇)) → (𝑏𝑇) = ((𝑧 + 𝑇) − 𝑇))
377sselda 3752 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐴) → 𝑧 ∈ ℂ)
38 limcperiod.t . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑇 ∈ ℂ)
3938adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐴) → 𝑇 ∈ ℂ)
4037, 39pncand 10595 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐴) → ((𝑧 + 𝑇) − 𝑇) = 𝑧)
41403adant3 1126 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝐴𝑏 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) − 𝑇) = 𝑧)
4236, 41eqtrd 2805 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝐴𝑏 = (𝑧 + 𝑇)) → (𝑏𝑇) = 𝑧)
43 simp2 1131 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝐴𝑏 = (𝑧 + 𝑇)) → 𝑧𝐴)
4442, 43eqeltrd 2850 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐴𝑏 = (𝑧 + 𝑇)) → (𝑏𝑇) ∈ 𝐴)
45443exp 1112 . . . . . . . . . . . . . 14 (𝜑 → (𝑧𝐴 → (𝑏 = (𝑧 + 𝑇) → (𝑏𝑇) ∈ 𝐴)))
4645adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝑧𝐴 → (𝑏 = (𝑧 + 𝑇) → (𝑏𝑇) ∈ 𝐴)))
4746rexlimdv 3178 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → (∃𝑧𝐴 𝑏 = (𝑧 + 𝑇) → (𝑏𝑇) ∈ 𝐴))
4834, 47mpd 15 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → (𝑏𝑇) ∈ 𝐴)
49 ssrab2 3836 . . . . . . . . . . . . . . . 16 {𝑤 ∈ ℂ ∣ ∃𝑧𝐴 𝑤 = (𝑧 + 𝑇)} ⊆ ℂ
5027, 49eqsstri 3784 . . . . . . . . . . . . . . 15 𝐵 ⊆ ℂ
5150a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐵 ⊆ ℂ)
5251sselda 3752 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → 𝑏 ∈ ℂ)
5338adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → 𝑇 ∈ ℂ)
5452, 53npcand 10598 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ((𝑏𝑇) + 𝑇) = 𝑏)
5554eqcomd 2777 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → 𝑏 = ((𝑏𝑇) + 𝑇))
56 oveq1 6800 . . . . . . . . . . . . 13 (𝑥 = (𝑏𝑇) → (𝑥 + 𝑇) = ((𝑏𝑇) + 𝑇))
5756eqeq2d 2781 . . . . . . . . . . . 12 (𝑥 = (𝑏𝑇) → (𝑏 = (𝑥 + 𝑇) ↔ 𝑏 = ((𝑏𝑇) + 𝑇)))
5857rspcev 3460 . . . . . . . . . . 11 (((𝑏𝑇) ∈ 𝐴𝑏 = ((𝑏𝑇) + 𝑇)) → ∃𝑥𝐴 𝑏 = (𝑥 + 𝑇))
5948, 55, 58syl2anc 565 . . . . . . . . . 10 ((𝜑𝑏𝐵) → ∃𝑥𝐴 𝑏 = (𝑥 + 𝑇))
6016, 17, 59syl2anc 565 . . . . . . . . 9 (((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → ∃𝑥𝐴 𝑏 = (𝑥 + 𝑇))
61 nfv 1995 . . . . . . . . . . . 12 𝑥((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤))
62 nfrab1 3271 . . . . . . . . . . . . . 14 𝑥{𝑥 ∈ ℂ ∣ ∃𝑦𝐴 𝑥 = (𝑦 + 𝑇)}
6319, 62nfcxfr 2911 . . . . . . . . . . . . 13 𝑥𝐵
6463nfcri 2907 . . . . . . . . . . . 12 𝑥 𝑏𝐵
6561, 64nfan 1980 . . . . . . . . . . 11 𝑥(((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵)
66 nfv 1995 . . . . . . . . . . 11 𝑥(𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)
6765, 66nfan 1980 . . . . . . . . . 10 𝑥((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧))
68 nfcv 2913 . . . . . . . . . . . 12 𝑥abs
69 nfcv 2913 . . . . . . . . . . . . . . 15 𝑥𝐹
7069, 63nfres 5536 . . . . . . . . . . . . . 14 𝑥(𝐹𝐵)
71 nfcv 2913 . . . . . . . . . . . . . 14 𝑥𝑏
7270, 71nffv 6339 . . . . . . . . . . . . 13 𝑥((𝐹𝐵)‘𝑏)
73 nfcv 2913 . . . . . . . . . . . . 13 𝑥
74 nfcv 2913 . . . . . . . . . . . . 13 𝑥𝐶
7572, 73, 74nfov 6821 . . . . . . . . . . . 12 𝑥(((𝐹𝐵)‘𝑏) − 𝐶)
7668, 75nffv 6339 . . . . . . . . . . 11 𝑥(abs‘(((𝐹𝐵)‘𝑏) − 𝐶))
77 nfcv 2913 . . . . . . . . . . 11 𝑥 <
78 nfcv 2913 . . . . . . . . . . 11 𝑥𝑤
7976, 77, 78nfbr 4833 . . . . . . . . . 10 𝑥(abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤
80 simp3 1132 . . . . . . . . . . . . . . 15 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝑏 = (𝑥 + 𝑇))
8180fveq2d 6336 . . . . . . . . . . . . . 14 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → ((𝐹𝐵)‘𝑏) = ((𝐹𝐵)‘(𝑥 + 𝑇)))
82173ad2ant1 1127 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝑏𝐵)
8380, 82eqeltrrd 2851 . . . . . . . . . . . . . . 15 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (𝑥 + 𝑇) ∈ 𝐵)
84 fvres 6348 . . . . . . . . . . . . . . 15 ((𝑥 + 𝑇) ∈ 𝐵 → ((𝐹𝐵)‘(𝑥 + 𝑇)) = (𝐹‘(𝑥 + 𝑇)))
8583, 84syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → ((𝐹𝐵)‘(𝑥 + 𝑇)) = (𝐹‘(𝑥 + 𝑇)))
86163ad2ant1 1127 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝜑)
87 simp2 1131 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝑥𝐴)
88 eleq1w 2833 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
8988anbi2d 606 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑥 → ((𝜑𝑦𝐴) ↔ (𝜑𝑥𝐴)))
90 fvoveq1 6816 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘(𝑥 + 𝑇)))
91 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
9290, 91eqeq12d 2786 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑥 → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)))
9389, 92imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑𝑥𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))))
94 limcperiod.fper . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
9593, 94chvarv 2425 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
9686, 87, 95syl2anc 565 . . . . . . . . . . . . . . 15 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
97 fvres 6348 . . . . . . . . . . . . . . . 16 (𝑥𝐴 → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
9887, 97syl 17 . . . . . . . . . . . . . . 15 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
9996, 98eqtr4d 2808 . . . . . . . . . . . . . 14 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (𝐹‘(𝑥 + 𝑇)) = ((𝐹𝐴)‘𝑥))
10081, 85, 993eqtrd 2809 . . . . . . . . . . . . 13 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → ((𝐹𝐵)‘𝑏) = ((𝐹𝐴)‘𝑥))
101100fvoveq1d 6815 . . . . . . . . . . . 12 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) = (abs‘(((𝐹𝐴)‘𝑥) − 𝐶)))
102 simpll3 1258 . . . . . . . . . . . . . . 15 (((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤))
1031023ad2ant1 1127 . . . . . . . . . . . . . 14 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤))
104103, 87jca 495 . . . . . . . . . . . . 13 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤) ∧ 𝑥𝐴))
105 simp1rl 1304 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝑏 ≠ (𝐷 + 𝑇))
106105neneqd 2948 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → ¬ 𝑏 = (𝐷 + 𝑇))
107 oveq1 6800 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐷 → (𝑥 + 𝑇) = (𝐷 + 𝑇))
10880, 107sylan9eq 2825 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) ∧ 𝑥 = 𝐷) → 𝑏 = (𝐷 + 𝑇))
109106, 108mtand 799 . . . . . . . . . . . . . . 15 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → ¬ 𝑥 = 𝐷)
110109neqned 2950 . . . . . . . . . . . . . 14 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝑥𝐷)
11180oveq1d 6808 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (𝑏 − (𝐷 + 𝑇)) = ((𝑥 + 𝑇) − (𝐷 + 𝑇)))
1127sselda 3752 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝑥 ∈ ℂ)
11386, 87, 112syl2anc 565 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝑥 ∈ ℂ)
11486, 10syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝐷 ∈ ℂ)
11586, 38syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → 𝑇 ∈ ℂ)
116113, 114, 115pnpcan2d 10632 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → ((𝑥 + 𝑇) − (𝐷 + 𝑇)) = (𝑥𝐷))
117111, 116eqtr2d 2806 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (𝑥𝐷) = (𝑏 − (𝐷 + 𝑇)))
118117fveq2d 6336 . . . . . . . . . . . . . . 15 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (abs‘(𝑥𝐷)) = (abs‘(𝑏 − (𝐷 + 𝑇))))
119 simp1rr 1305 . . . . . . . . . . . . . . 15 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)
120118, 119eqbrtrd 4808 . . . . . . . . . . . . . 14 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (abs‘(𝑥𝐷)) < 𝑧)
121110, 120jca 495 . . . . . . . . . . . . 13 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (𝑥𝐷 ∧ (abs‘(𝑥𝐷)) < 𝑧))
122 neeq1 3005 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (𝑦𝐷𝑥𝐷))
123 fvoveq1 6816 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (abs‘(𝑦𝐷)) = (abs‘(𝑥𝐷)))
124123breq1d 4796 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → ((abs‘(𝑦𝐷)) < 𝑧 ↔ (abs‘(𝑥𝐷)) < 𝑧))
125122, 124anbi12d 608 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) ↔ (𝑥𝐷 ∧ (abs‘(𝑥𝐷)) < 𝑧)))
126 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → ((𝐹𝐴)‘𝑦) = ((𝐹𝐴)‘𝑥))
127126fvoveq1d 6815 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) = (abs‘(((𝐹𝐴)‘𝑥) − 𝐶)))
128127breq1d 4796 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → ((abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤 ↔ (abs‘(((𝐹𝐴)‘𝑥) − 𝐶)) < 𝑤))
129125, 128imbi12d 333 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤) ↔ ((𝑥𝐷 ∧ (abs‘(𝑥𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑥) − 𝐶)) < 𝑤)))
130129rspccva 3459 . . . . . . . . . . . . 13 ((∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤) ∧ 𝑥𝐴) → ((𝑥𝐷 ∧ (abs‘(𝑥𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑥) − 𝐶)) < 𝑤))
131104, 121, 130sylc 65 . . . . . . . . . . . 12 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (abs‘(((𝐹𝐴)‘𝑥) − 𝐶)) < 𝑤)
132101, 131eqbrtrd 4808 . . . . . . . . . . 11 ((((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥𝐴𝑏 = (𝑥 + 𝑇)) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤)
1331323exp 1112 . . . . . . . . . 10 (((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → (𝑥𝐴 → (𝑏 = (𝑥 + 𝑇) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤)))
13467, 79, 133rexlimd 3174 . . . . . . . . 9 (((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → (∃𝑥𝐴 𝑏 = (𝑥 + 𝑇) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤))
13560, 134mpd 15 . . . . . . . 8 (((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤)
136135ex 397 . . . . . . 7 ((((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏𝐵) → ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤))
137136ralrimiva 3115 . . . . . 6 (((𝜑𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤)) → ∀𝑏𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤))
1381373exp 1112 . . . . 5 ((𝜑𝑤 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤) → ∀𝑏𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤))))
139138reximdvai 3163 . . . 4 ((𝜑𝑤 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑦𝐴 ((𝑦𝐷 ∧ (abs‘(𝑦𝐷)) < 𝑧) → (abs‘(((𝐹𝐴)‘𝑦) − 𝐶)) < 𝑤) → ∃𝑧 ∈ ℝ+𝑏𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤)))
14014, 139mpd 15 . . 3 ((𝜑𝑤 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑏𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤))
141140ralrimiva 3115 . 2 (𝜑 → ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤))
142 limcperiod.bss . . . 4 (𝜑𝐵 ⊆ dom 𝐹)
1434, 142fssresd 6211 . . 3 (𝜑 → (𝐹𝐵):𝐵⟶ℂ)
14410, 38addcld 10261 . . 3 (𝜑 → (𝐷 + 𝑇) ∈ ℂ)
145143, 51, 144ellimc3 23863 . 2 (𝜑 → (𝐶 ∈ ((𝐹𝐵) lim (𝐷 + 𝑇)) ↔ (𝐶 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑧 ∈ ℝ+𝑏𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹𝐵)‘𝑏) − 𝐶)) < 𝑤))))
1463, 141, 145mpbir2and 684 1 (𝜑𝐶 ∈ ((𝐹𝐵) lim (𝐷 + 𝑇)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  ∃wrex 3062  {crab 3065   ⊆ wss 3723   class class class wbr 4786  dom cdm 5249   ↾ cres 5251  ⟶wf 6027  ‘cfv 6031  (class class class)co 6793  ℂcc 10136   + caddc 10141   < clt 10276   − cmin 10468  ℝ+crp 12035  abscabs 14182   limℂ climc 23846 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8473  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-plusg 16162  df-mulr 16163  df-starv 16164  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-rest 16291  df-topn 16292  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cnp 21253  df-xms 22345  df-ms 22346  df-limc 23850 This theorem is referenced by:  fourierdlem48  40888  fourierdlem49  40889  fourierdlem81  40921  fourierdlem89  40929  fourierdlem91  40931  fourierdlem92  40932
 Copyright terms: Public domain W3C validator