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

Theorem fourierdlem4 43360
Description: 𝐸 is a function that maps any point to a periodic corresponding point in (𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem4.a (𝜑𝐴 ∈ ℝ)
fourierdlem4.b (𝜑𝐵 ∈ ℝ)
fourierdlem4.altb (𝜑𝐴 < 𝐵)
fourierdlem4.t 𝑇 = (𝐵𝐴)
fourierdlem4.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
Assertion
Ref Expression
fourierdlem4 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑇   𝜑,𝑥
Allowed substitution hint:   𝐸(𝑥)

Proof of Theorem fourierdlem4
StepHypRef Expression
1 simpr 488 . . . 4 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
2 fourierdlem4.b . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
32adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
43, 1resubcld 11287 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) ∈ ℝ)
5 fourierdlem4.t . . . . . . . . . 10 𝑇 = (𝐵𝐴)
6 fourierdlem4.a . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
72, 6resubcld 11287 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
85, 7eqeltrid 2844 . . . . . . . . 9 (𝜑𝑇 ∈ ℝ)
98adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
105a1i 11 . . . . . . . . . 10 (𝜑𝑇 = (𝐵𝐴))
112recnd 10888 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
126recnd 10888 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
13 fourierdlem4.altb . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
146, 13gtned 10994 . . . . . . . . . . 11 (𝜑𝐵𝐴)
1511, 12, 14subne0d 11225 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ≠ 0)
1610, 15eqnetrd 3010 . . . . . . . . 9 (𝜑𝑇 ≠ 0)
1716adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑇 ≠ 0)
184, 9, 17redivcld 11687 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → ((𝐵𝑥) / 𝑇) ∈ ℝ)
1918flcld 13400 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)
2019zred 12309 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℝ)
2120, 9remulcld 10890 . . . 4 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
221, 21readdcld 10889 . . 3 ((𝜑𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
236adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
2423, 1resubcld 11287 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝐴𝑥) ∈ ℝ)
2524, 9, 17redivcld 11687 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → ((𝐴𝑥) / 𝑇) ∈ ℝ)
2625, 9remulcld 10890 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (((𝐴𝑥) / 𝑇) · 𝑇) ∈ ℝ)
2711addid1d 11059 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 + 0) = 𝐵)
2827eqcomd 2745 . . . . . . . . . . . . . 14 (𝜑𝐵 = (𝐵 + 0))
2911, 12subcld 11216 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝐴) ∈ ℂ)
3029subidd 11204 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴) − (𝐵𝐴)) = 0)
3130eqcomd 2745 . . . . . . . . . . . . . . 15 (𝜑 → 0 = ((𝐵𝐴) − (𝐵𝐴)))
3231oveq2d 7250 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 + 0) = (𝐵 + ((𝐵𝐴) − (𝐵𝐴))))
3311, 29, 29addsub12d 11239 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 + ((𝐵𝐴) − (𝐵𝐴))) = ((𝐵𝐴) + (𝐵 − (𝐵𝐴))))
3411, 12nncand 11221 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 − (𝐵𝐴)) = 𝐴)
3534oveq2d 7250 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵𝐴) + (𝐵 − (𝐵𝐴))) = ((𝐵𝐴) + 𝐴))
3629, 12addcomd 11061 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴) + 𝐴) = (𝐴 + (𝐵𝐴)))
3710eqcomd 2745 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝐴) = 𝑇)
3837oveq2d 7250 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 + (𝐵𝐴)) = (𝐴 + 𝑇))
3936, 38eqtrd 2779 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵𝐴) + 𝐴) = (𝐴 + 𝑇))
4033, 35, 393eqtrd 2783 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 + ((𝐵𝐴) − (𝐵𝐴))) = (𝐴 + 𝑇))
4128, 32, 403eqtrd 2783 . . . . . . . . . . . . 13 (𝜑𝐵 = (𝐴 + 𝑇))
4241adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → 𝐵 = (𝐴 + 𝑇))
4342oveq1d 7249 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) = ((𝐴 + 𝑇) − 𝑥))
4412adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℂ)
459recnd 10888 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
461recnd 10888 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
4744, 45, 46addsubd 11237 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → ((𝐴 + 𝑇) − 𝑥) = ((𝐴𝑥) + 𝑇))
4843, 47eqtrd 2779 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) = ((𝐴𝑥) + 𝑇))
4948oveq1d 7249 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → ((𝐵𝑥) / 𝑇) = (((𝐴𝑥) + 𝑇) / 𝑇))
5044, 46subcld 11216 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → (𝐴𝑥) ∈ ℂ)
5150, 45, 45, 17divdird 11673 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (((𝐴𝑥) + 𝑇) / 𝑇) = (((𝐴𝑥) / 𝑇) + (𝑇 / 𝑇)))
525, 29eqeltrid 2844 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℂ)
5352, 16dividd 11633 . . . . . . . . . . 11 (𝜑 → (𝑇 / 𝑇) = 1)
5453adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → (𝑇 / 𝑇) = 1)
5554oveq2d 7250 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (((𝐴𝑥) / 𝑇) + (𝑇 / 𝑇)) = (((𝐴𝑥) / 𝑇) + 1))
5649, 51, 553eqtrd 2783 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ((𝐵𝑥) / 𝑇) = (((𝐴𝑥) / 𝑇) + 1))
5756fveq2d 6742 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘(((𝐴𝑥) / 𝑇) + 1)))
5857oveq1d 7249 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘(((𝐴𝑥) / 𝑇) + 1)) · 𝑇))
5958, 21eqeltrrd 2841 . . . . 5 ((𝜑𝑥 ∈ ℝ) → ((⌊‘(((𝐴𝑥) / 𝑇) + 1)) · 𝑇) ∈ ℝ)
60 peano2re 11032 . . . . . . . 8 (((𝐴𝑥) / 𝑇) ∈ ℝ → (((𝐴𝑥) / 𝑇) + 1) ∈ ℝ)
6125, 60syl 17 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (((𝐴𝑥) / 𝑇) + 1) ∈ ℝ)
62 reflcl 13398 . . . . . . 7 ((((𝐴𝑥) / 𝑇) + 1) ∈ ℝ → (⌊‘(((𝐴𝑥) / 𝑇) + 1)) ∈ ℝ)
6361, 62syl 17 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (⌊‘(((𝐴𝑥) / 𝑇) + 1)) ∈ ℝ)
646, 2posdifd 11446 . . . . . . . . . 10 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
6513, 64mpbid 235 . . . . . . . . 9 (𝜑 → 0 < (𝐵𝐴))
6665, 10breqtrrd 5097 . . . . . . . 8 (𝜑 → 0 < 𝑇)
678, 66elrpd 12652 . . . . . . 7 (𝜑𝑇 ∈ ℝ+)
6867adantr 484 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ+)
69 flltp1 13402 . . . . . . . 8 (((𝐴𝑥) / 𝑇) ∈ ℝ → ((𝐴𝑥) / 𝑇) < ((⌊‘((𝐴𝑥) / 𝑇)) + 1))
7025, 69syl 17 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → ((𝐴𝑥) / 𝑇) < ((⌊‘((𝐴𝑥) / 𝑇)) + 1))
71 1zzd 12235 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 1 ∈ ℤ)
72 fladdz 13427 . . . . . . . 8 ((((𝐴𝑥) / 𝑇) ∈ ℝ ∧ 1 ∈ ℤ) → (⌊‘(((𝐴𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴𝑥) / 𝑇)) + 1))
7325, 71, 72syl2anc 587 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (⌊‘(((𝐴𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴𝑥) / 𝑇)) + 1))
7470, 73breqtrrd 5097 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → ((𝐴𝑥) / 𝑇) < (⌊‘(((𝐴𝑥) / 𝑇) + 1)))
7525, 63, 68, 74ltmul1dd 12710 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (((𝐴𝑥) / 𝑇) · 𝑇) < ((⌊‘(((𝐴𝑥) / 𝑇) + 1)) · 𝑇))
7626, 59, 1, 75ltadd2dd 11018 . . . 4 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (((𝐴𝑥) / 𝑇) · 𝑇)) < (𝑥 + ((⌊‘(((𝐴𝑥) / 𝑇) + 1)) · 𝑇)))
7750, 45, 17divcan1d 11636 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (((𝐴𝑥) / 𝑇) · 𝑇) = (𝐴𝑥))
7877oveq2d 7250 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (((𝐴𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐴𝑥)))
7946, 44pncan3d 11219 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (𝐴𝑥)) = 𝐴)
8078, 79eqtrd 2779 . . . 4 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (((𝐴𝑥) / 𝑇) · 𝑇)) = 𝐴)
8158oveq2d 7250 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘(((𝐴𝑥) / 𝑇) + 1)) · 𝑇)))
8281eqcomd 2745 . . . 4 ((𝜑𝑥 ∈ ℝ) → (𝑥 + ((⌊‘(((𝐴𝑥) / 𝑇) + 1)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
8376, 80, 823brtr3d 5100 . . 3 ((𝜑𝑥 ∈ ℝ) → 𝐴 < (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
8418, 9remulcld 10890 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (((𝐵𝑥) / 𝑇) · 𝑇) ∈ ℝ)
85 flle 13401 . . . . . . 7 (((𝐵𝑥) / 𝑇) ∈ ℝ → (⌊‘((𝐵𝑥) / 𝑇)) ≤ ((𝐵𝑥) / 𝑇))
8618, 85syl 17 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ≤ ((𝐵𝑥) / 𝑇))
8720, 18, 68lemul1d 12698 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) ≤ ((𝐵𝑥) / 𝑇) ↔ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵𝑥) / 𝑇) · 𝑇)))
8886, 87mpbid 235 . . . . 5 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵𝑥) / 𝑇) · 𝑇))
8921, 84, 1, 88leadd2dd 11474 . . . 4 ((𝜑𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ≤ (𝑥 + (((𝐵𝑥) / 𝑇) · 𝑇)))
904recnd 10888 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) ∈ ℂ)
9190, 45, 17divcan1d 11636 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (((𝐵𝑥) / 𝑇) · 𝑇) = (𝐵𝑥))
9291oveq2d 7250 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (((𝐵𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐵𝑥)))
9311adantr 484 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℂ)
9446, 93pncan3d 11219 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (𝐵𝑥)) = 𝐵)
9592, 94eqtrd 2779 . . . 4 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (((𝐵𝑥) / 𝑇) · 𝑇)) = 𝐵)
9689, 95breqtrd 5095 . . 3 ((𝜑𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)
9723rexrd 10910 . . . 4 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℝ*)
98 elioc2 13025 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)))
9997, 3, 98syl2anc 587 . . 3 ((𝜑𝑥 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)))
10022, 83, 96, 99mpbir3and 1344 . 2 ((𝜑𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
101 fourierdlem4.e . 2 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
102100, 101fmptd 6952 1 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2112  wne 2942   class class class wbr 5069  cmpt 5151  wf 6396  cfv 6400  (class class class)co 7234  cc 10754  cr 10755  0cc0 10756  1c1 10757   + caddc 10759   · cmul 10761  *cxr 10893   < clt 10894  cle 10895  cmin 11089   / cdiv 11516  cz 12203  +crp 12613  (,]cioc 12963  cfl 13392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-cnex 10812  ax-resscn 10813  ax-1cn 10814  ax-icn 10815  ax-addcl 10816  ax-addrcl 10817  ax-mulcl 10818  ax-mulrcl 10819  ax-mulcom 10820  ax-addass 10821  ax-mulass 10822  ax-distr 10823  ax-i2m1 10824  ax-1ne0 10825  ax-1rid 10826  ax-rnegex 10827  ax-rrecex 10828  ax-cnre 10829  ax-pre-lttri 10830  ax-pre-lttrn 10831  ax-pre-ltadd 10832  ax-pre-mulgt0 10833  ax-pre-sup 10834
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3711  df-csb 3828  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-om 7666  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-sup 9085  df-inf 9086  df-pnf 10896  df-mnf 10897  df-xr 10898  df-ltxr 10899  df-le 10900  df-sub 11091  df-neg 11092  df-div 11517  df-nn 11858  df-n0 12118  df-z 12204  df-uz 12466  df-rp 12614  df-ioc 12967  df-fl 13394
This theorem is referenced by:  fourierdlem19  43375  fourierdlem37  43393  fourierdlem41  43397  fourierdlem48  43403  fourierdlem49  43404  fourierdlem51  43406  fourierdlem63  43418  fourierdlem65  43420  fourierdlem71  43426  fourierdlem79  43434  fourierdlem89  43444  fourierdlem90  43445  fourierdlem91  43446  fourierdlem102  43457  fourierdlem114  43469
  Copyright terms: Public domain W3C validator