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

Theorem fourierswlem 41241
Description: The Fourier series for the square wave 𝐹 converges to 𝑌, a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierswlem.t 𝑇 = (2 · π)
fourierswlem.f 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
fourierswlem.x 𝑋 ∈ ℝ
fourierswlem.y 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹𝑋))
Assertion
Ref Expression
fourierswlem 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2)
Distinct variable groups:   𝑥,𝑇   𝑥,𝑋
Allowed substitution hints:   𝐹(𝑥)   𝑌(𝑥)

Proof of Theorem fourierswlem
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 simpr 479 . . . . . . . . . 10 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → 2 ∥ (𝑋 / π))
2 2z 11737 . . . . . . . . . . . 12 2 ∈ ℤ
32a1i 11 . . . . . . . . . . 11 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → 2 ∈ ℤ)
4 fourierswlem.x . . . . . . . . . . . . . 14 𝑋 ∈ ℝ
5 pirp 24613 . . . . . . . . . . . . . 14 π ∈ ℝ+
6 mod0 12970 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ ∧ π ∈ ℝ+) → ((𝑋 mod π) = 0 ↔ (𝑋 / π) ∈ ℤ))
74, 5, 6mp2an 685 . . . . . . . . . . . . 13 ((𝑋 mod π) = 0 ↔ (𝑋 / π) ∈ ℤ)
87biimpi 208 . . . . . . . . . . . 12 ((𝑋 mod π) = 0 → (𝑋 / π) ∈ ℤ)
98adantr 474 . . . . . . . . . . 11 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (𝑋 / π) ∈ ℤ)
10 divides 15359 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ (𝑋 / π) ∈ ℤ) → (2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π)))
113, 9, 10syl2anc 581 . . . . . . . . . 10 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π)))
121, 11mpbid 224 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π))
13 2cnd 11429 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → 2 ∈ ℂ)
14 picn 24611 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℂ
1514a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → π ∈ ℂ)
16 zcn 11709 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
1713, 15, 16mulassd 10380 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → ((2 · π) · 𝑘) = (2 · (π · 𝑘)))
1815, 16mulcld 10377 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (π · 𝑘) ∈ ℂ)
1913, 18mulcomd 10378 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → (2 · (π · 𝑘)) = ((π · 𝑘) · 2))
2017, 19eqtrd 2861 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → ((2 · π) · 𝑘) = ((π · 𝑘) · 2))
2120adantr 474 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((2 · π) · 𝑘) = ((π · 𝑘) · 2))
2215, 16, 13mulassd 10380 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → ((π · 𝑘) · 2) = (π · (𝑘 · 2)))
2322adantr 474 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((π · 𝑘) · 2) = (π · (𝑘 · 2)))
24 id 22 . . . . . . . . . . . . . . . . . . 19 ((𝑘 · 2) = (𝑋 / π) → (𝑘 · 2) = (𝑋 / π))
2524eqcomd 2831 . . . . . . . . . . . . . . . . . 18 ((𝑘 · 2) = (𝑋 / π) → (𝑋 / π) = (𝑘 · 2))
2625adantl 475 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / π) = (𝑘 · 2))
274recni 10371 . . . . . . . . . . . . . . . . . . 19 𝑋 ∈ ℂ
2827a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑋 ∈ ℂ)
2914a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → π ∈ ℂ)
3016adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑘 ∈ ℂ)
31 2cnd 11429 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 2 ∈ ℂ)
3230, 31mulcld 10377 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑘 · 2) ∈ ℂ)
33 pire 24610 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℝ
34 pipos 24612 . . . . . . . . . . . . . . . . . . . 20 0 < π
3533, 34gt0ne0ii 10888 . . . . . . . . . . . . . . . . . . 19 π ≠ 0
3635a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → π ≠ 0)
3728, 29, 32, 36divmuld 11149 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((𝑋 / π) = (𝑘 · 2) ↔ (π · (𝑘 · 2)) = 𝑋))
3826, 37mpbid 224 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (π · (𝑘 · 2)) = 𝑋)
3921, 23, 383eqtrrd 2866 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑋 = ((2 · π) · 𝑘))
40 fourierswlem.t . . . . . . . . . . . . . . . 16 𝑇 = (2 · π)
4140a1i 11 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑇 = (2 · π))
4239, 41oveq12d 6923 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) = (((2 · π) · 𝑘) / (2 · π)))
4313, 15mulcld 10377 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → (2 · π) ∈ ℂ)
44 2ne0 11462 . . . . . . . . . . . . . . . . . 18 2 ≠ 0
4544a1i 11 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → 2 ≠ 0)
4635a1i 11 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → π ≠ 0)
4713, 15, 45, 46mulne0d 11004 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → (2 · π) ≠ 0)
4816, 43, 47divcan3d 11132 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℤ → (((2 · π) · 𝑘) / (2 · π)) = 𝑘)
4948adantr 474 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (((2 · π) · 𝑘) / (2 · π)) = 𝑘)
5042, 49eqtrd 2861 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) = 𝑘)
51 simpl 476 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑘 ∈ ℤ)
5250, 51eqeltrd 2906 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) ∈ ℤ)
5352ex 403 . . . . . . . . . . 11 (𝑘 ∈ ℤ → ((𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ))
5453a1i 11 . . . . . . . . . 10 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (𝑘 ∈ ℤ → ((𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ)))
5554rexlimdv 3239 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ))
5612, 55mpd 15 . . . . . . . 8 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (𝑋 / 𝑇) ∈ ℤ)
57 2re 11425 . . . . . . . . . . . 12 2 ∈ ℝ
5857, 33remulcli 10373 . . . . . . . . . . 11 (2 · π) ∈ ℝ
5940, 58eqeltri 2902 . . . . . . . . . 10 𝑇 ∈ ℝ
60 2pos 11461 . . . . . . . . . . . 12 0 < 2
6157, 33, 60, 34mulgt0ii 10489 . . . . . . . . . . 11 0 < (2 · π)
6261, 40breqtrri 4900 . . . . . . . . . 10 0 < 𝑇
6359, 62elrpii 12115 . . . . . . . . 9 𝑇 ∈ ℝ+
64 mod0 12970 . . . . . . . . 9 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → ((𝑋 mod 𝑇) = 0 ↔ (𝑋 / 𝑇) ∈ ℤ))
654, 63, 64mp2an 685 . . . . . . . 8 ((𝑋 mod 𝑇) = 0 ↔ (𝑋 / 𝑇) ∈ ℤ)
6656, 65sylibr 226 . . . . . . 7 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (𝑋 mod 𝑇) = 0)
6766orcd 906 . . . . . 6 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → ((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π))
68 odd2np1 15439 . . . . . . . . . 10 ((𝑋 / π) ∈ ℤ → (¬ 2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = (𝑋 / π)))
697, 68sylbi 209 . . . . . . . . 9 ((𝑋 mod π) = 0 → (¬ 2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = (𝑋 / π)))
7069biimpa 470 . . . . . . . 8 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = (𝑋 / π))
7113, 16mulcld 10377 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → (2 · 𝑘) ∈ ℂ)
7271adantr 474 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (2 · 𝑘) ∈ ℂ)
73 1cnd 10351 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 1 ∈ ℂ)
7414a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → π ∈ ℂ)
7572, 73, 74adddird 10382 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (((2 · 𝑘) + 1) · π) = (((2 · 𝑘) · π) + (1 · π)))
7613, 16mulcomd 10378 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (2 · 𝑘) = (𝑘 · 2))
7776oveq1d 6920 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → ((2 · 𝑘) · π) = ((𝑘 · 2) · π))
7816, 13, 15mulassd 10380 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → ((𝑘 · 2) · π) = (𝑘 · (2 · π)))
7940eqcomi 2834 . . . . . . . . . . . . . . . . . . . 20 (2 · π) = 𝑇
8079a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (2 · π) = 𝑇)
8180oveq2d 6921 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → (𝑘 · (2 · π)) = (𝑘 · 𝑇))
8277, 78, 813eqtrd 2865 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → ((2 · 𝑘) · π) = (𝑘 · 𝑇))
8314mulid2i 10362 . . . . . . . . . . . . . . . . . 18 (1 · π) = π
8483a1i 11 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → (1 · π) = π)
8582, 84oveq12d 6923 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → (((2 · 𝑘) · π) + (1 · π)) = ((𝑘 · 𝑇) + π))
8685adantr 474 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (((2 · 𝑘) · π) + (1 · π)) = ((𝑘 · 𝑇) + π))
8740, 43syl5eqel 2910 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → 𝑇 ∈ ℂ)
8816, 87mulcld 10377 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → (𝑘 · 𝑇) ∈ ℂ)
8988, 15addcomd 10557 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → ((𝑘 · 𝑇) + π) = (π + (𝑘 · 𝑇)))
9089adantr 474 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → ((𝑘 · 𝑇) + π) = (π + (𝑘 · 𝑇)))
9175, 86, 903eqtrrd 2866 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (π + (𝑘 · 𝑇)) = (((2 · 𝑘) + 1) · π))
92 peano2cn 10527 . . . . . . . . . . . . . . . . 17 ((2 · 𝑘) ∈ ℂ → ((2 · 𝑘) + 1) ∈ ℂ)
9371, 92syl 17 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → ((2 · 𝑘) + 1) ∈ ℂ)
9493, 15mulcomd 10378 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℤ → (((2 · 𝑘) + 1) · π) = (π · ((2 · 𝑘) + 1)))
9594adantr 474 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (((2 · 𝑘) + 1) · π) = (π · ((2 · 𝑘) + 1)))
96 id 22 . . . . . . . . . . . . . . . . 17 (((2 · 𝑘) + 1) = (𝑋 / π) → ((2 · 𝑘) + 1) = (𝑋 / π))
9796eqcomd 2831 . . . . . . . . . . . . . . . 16 (((2 · 𝑘) + 1) = (𝑋 / π) → (𝑋 / π) = ((2 · 𝑘) + 1))
9897adantl 475 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (𝑋 / π) = ((2 · 𝑘) + 1))
9927a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 𝑋 ∈ ℂ)
10093adantr 474 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → ((2 · 𝑘) + 1) ∈ ℂ)
10135a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → π ≠ 0)
10299, 74, 100, 101divmuld 11149 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → ((𝑋 / π) = ((2 · 𝑘) + 1) ↔ (π · ((2 · 𝑘) + 1)) = 𝑋))
10398, 102mpbid 224 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (π · ((2 · 𝑘) + 1)) = 𝑋)
10491, 95, 1033eqtrrd 2866 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 𝑋 = (π + (𝑘 · 𝑇)))
105104oveq1d 6920 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (𝑋 mod 𝑇) = ((π + (𝑘 · 𝑇)) mod 𝑇))
106 modcyc 13000 . . . . . . . . . . . . . 14 ((π ∈ ℝ ∧ 𝑇 ∈ ℝ+𝑘 ∈ ℤ) → ((π + (𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇))
10733, 63, 106mp3an12 1581 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → ((π + (𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇))
108107adantr 474 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → ((π + (𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇))
10933a1i 11 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → π ∈ ℝ)
11063a1i 11 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 𝑇 ∈ ℝ+)
111 0re 10358 . . . . . . . . . . . . . . 15 0 ∈ ℝ
112111, 33, 34ltleii 10479 . . . . . . . . . . . . . 14 0 ≤ π
113112a1i 11 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 0 ≤ π)
114 2timesgt 40299 . . . . . . . . . . . . . . . 16 (π ∈ ℝ+ → π < (2 · π))
1155, 114ax-mp 5 . . . . . . . . . . . . . . 15 π < (2 · π)
116115, 40breqtrri 4900 . . . . . . . . . . . . . 14 π < 𝑇
117116a1i 11 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → π < 𝑇)
118 modid 12990 . . . . . . . . . . . . 13 (((π ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ π ∧ π < 𝑇)) → (π mod 𝑇) = π)
119109, 110, 113, 117, 118syl22anc 874 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (π mod 𝑇) = π)
120105, 108, 1193eqtrd 2865 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (𝑋 mod 𝑇) = π)
121120ex 403 . . . . . . . . . 10 (𝑘 ∈ ℤ → (((2 · 𝑘) + 1) = (𝑋 / π) → (𝑋 mod 𝑇) = π))
122121a1i 11 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → (𝑘 ∈ ℤ → (((2 · 𝑘) + 1) = (𝑋 / π) → (𝑋 mod 𝑇) = π)))
123122rexlimdv 3239 . . . . . . . 8 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → (∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = (𝑋 / π) → (𝑋 mod 𝑇) = π))
12470, 123mpd 15 . . . . . . 7 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → (𝑋 mod 𝑇) = π)
125124olcd 907 . . . . . 6 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → ((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π))
12667, 125pm2.61dan 849 . . . . 5 ((𝑋 mod π) = 0 → ((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π))
127 0xr 10403 . . . . . . . 8 0 ∈ ℝ*
12833rexri 10415 . . . . . . . 8 π ∈ ℝ*
129 iocgtlb 40523 . . . . . . . 8 ((0 ∈ ℝ* ∧ π ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (0(,]π)) → 0 < (𝑋 mod 𝑇))
130127, 128, 129mp3an12 1581 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (0(,]π) → 0 < (𝑋 mod 𝑇))
131130gt0ne0d 10916 . . . . . 6 ((𝑋 mod 𝑇) ∈ (0(,]π) → (𝑋 mod 𝑇) ≠ 0)
132131neneqd 3004 . . . . 5 ((𝑋 mod 𝑇) ∈ (0(,]π) → ¬ (𝑋 mod 𝑇) = 0)
133 pm2.53 884 . . . . . 6 (((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π) → (¬ (𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) = π))
134133imp 397 . . . . 5 ((((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) = π)
135126, 132, 134syl2anr 592 . . . 4 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) = π)
136127a1i 11 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → 0 ∈ ℝ*)
137128a1i 11 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → π ∈ ℝ*)
138 modcl 12967 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → (𝑋 mod 𝑇) ∈ ℝ)
1394, 63, 138mp2an 685 . . . . . . . . . . . . . 14 (𝑋 mod 𝑇) ∈ ℝ
140139rexri 10415 . . . . . . . . . . . . 13 (𝑋 mod 𝑇) ∈ ℝ*
141140a1i 11 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ∈ ℝ*)
142 id 22 . . . . . . . . . . . . 13 ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) = π)
14334, 142syl5breqr 4911 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → 0 < (𝑋 mod 𝑇))
14433eqlei2 10467 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ≤ π)
145136, 137, 141, 143, 144eliocd 40529 . . . . . . . . . . 11 ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ∈ (0(,]π))
146145iftrued 4314 . . . . . . . . . 10 ((𝑋 mod 𝑇) = π → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = 1)
147146adantl 475 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = 1)
148 oveq1 6912 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝑥 mod 𝑇) = (𝑋 mod 𝑇))
149148breq1d 4883 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → ((𝑥 mod 𝑇) < π ↔ (𝑋 mod 𝑇) < π))
150149ifbid 4328 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → if((𝑥 mod 𝑇) < π, 1, -1) = if((𝑋 mod 𝑇) < π, 1, -1))
151 fourierswlem.f . . . . . . . . . . . . 13 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
152 1ex 10352 . . . . . . . . . . . . . 14 1 ∈ V
153 negex 10599 . . . . . . . . . . . . . 14 -1 ∈ V
154152, 153ifex 4354 . . . . . . . . . . . . 13 if((𝑋 mod 𝑇) < π, 1, -1) ∈ V
155150, 151, 154fvmpt 6529 . . . . . . . . . . . 12 (𝑋 ∈ ℝ → (𝐹𝑋) = if((𝑋 mod 𝑇) < π, 1, -1))
1564, 155ax-mp 5 . . . . . . . . . . 11 (𝐹𝑋) = if((𝑋 mod 𝑇) < π, 1, -1)
157139a1i 11 . . . . . . . . . . . . . 14 ((𝑋 mod 𝑇) < π → (𝑋 mod 𝑇) ∈ ℝ)
158 id 22 . . . . . . . . . . . . . 14 ((𝑋 mod 𝑇) < π → (𝑋 mod 𝑇) < π)
159157, 158ltned 10492 . . . . . . . . . . . . 13 ((𝑋 mod 𝑇) < π → (𝑋 mod 𝑇) ≠ π)
160159necon2bi 3029 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → ¬ (𝑋 mod 𝑇) < π)
161160iffalsed 4317 . . . . . . . . . . 11 ((𝑋 mod 𝑇) = π → if((𝑋 mod 𝑇) < π, 1, -1) = -1)
162156, 161syl5eq 2873 . . . . . . . . . 10 ((𝑋 mod 𝑇) = π → (𝐹𝑋) = -1)
163162adantl 475 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (𝐹𝑋) = -1)
164147, 163oveq12d 6923 . . . . . . . 8 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = (1 + -1))
165 1pneg1e0 11477 . . . . . . . 8 (1 + -1) = 0
166164, 165syl6eq 2877 . . . . . . 7 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = 0)
167166oveq1d 6920 . . . . . 6 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = (0 / 2))
168167adantll 707 . . . . 5 ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = (0 / 2))
169 2cn 11426 . . . . . . 7 2 ∈ ℂ
170169, 44div0i 11085 . . . . . 6 (0 / 2) = 0
171170a1i 11 . . . . 5 ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → (0 / 2) = 0)
172 fourierswlem.y . . . . . . 7 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹𝑋))
173 iftrue 4312 . . . . . . 7 ((𝑋 mod π) = 0 → if((𝑋 mod π) = 0, 0, (𝐹𝑋)) = 0)
174172, 173syl5req 2874 . . . . . 6 ((𝑋 mod π) = 0 → 0 = 𝑌)
175174ad2antlr 720 . . . . 5 ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → 0 = 𝑌)
176168, 171, 1753eqtrrd 2866 . . . 4 ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
177135, 176mpdan 680 . . 3 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
178 iftrue 4312 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (0(,]π) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = 1)
179178adantr 474 . . . . . 6 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = 1)
180139a1i 11 . . . . . . . 8 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) ∈ ℝ)
18133a1i 11 . . . . . . . 8 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → π ∈ ℝ)
182 iocleub 40524 . . . . . . . . . 10 ((0 ∈ ℝ* ∧ π ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (0(,]π)) → (𝑋 mod 𝑇) ≤ π)
183127, 128, 182mp3an12 1581 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (0(,]π) → (𝑋 mod 𝑇) ≤ π)
184183adantr 474 . . . . . . . 8 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) ≤ π)
185 ax-1cn 10310 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℂ
186185, 14mulcomi 10365 . . . . . . . . . . . . . . . . . . 19 (1 · π) = (π · 1)
18783, 186eqtr3i 2851 . . . . . . . . . . . . . . . . . 18 π = (π · 1)
188187oveq1i 6915 . . . . . . . . . . . . . . . . 17 (π + (π · (2 · (⌊‘(𝑋 / 𝑇))))) = ((π · 1) + (π · (2 · (⌊‘(𝑋 / 𝑇)))))
189169, 14mulcomi 10365 . . . . . . . . . . . . . . . . . . . . 21 (2 · π) = (π · 2)
19040, 189eqtri 2849 . . . . . . . . . . . . . . . . . . . 20 𝑇 = (π · 2)
191190oveq1i 6915 . . . . . . . . . . . . . . . . . . 19 (𝑇 · (⌊‘(𝑋 / 𝑇))) = ((π · 2) · (⌊‘(𝑋 / 𝑇)))
192111, 62gtneii 10468 . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 ≠ 0
1934, 59, 192redivcli 11118 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 / 𝑇) ∈ ℝ
194 flcl 12891 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 / 𝑇) ∈ ℝ → (⌊‘(𝑋 / 𝑇)) ∈ ℤ)
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (⌊‘(𝑋 / 𝑇)) ∈ ℤ
196 zcn 11709 . . . . . . . . . . . . . . . . . . . . 21 ((⌊‘(𝑋 / 𝑇)) ∈ ℤ → (⌊‘(𝑋 / 𝑇)) ∈ ℂ)
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⌊‘(𝑋 / 𝑇)) ∈ ℂ
19814, 169, 197mulassi 10368 . . . . . . . . . . . . . . . . . . 19 ((π · 2) · (⌊‘(𝑋 / 𝑇))) = (π · (2 · (⌊‘(𝑋 / 𝑇))))
199191, 198eqtri 2849 . . . . . . . . . . . . . . . . . 18 (𝑇 · (⌊‘(𝑋 / 𝑇))) = (π · (2 · (⌊‘(𝑋 / 𝑇))))
200199oveq2i 6916 . . . . . . . . . . . . . . . . 17 (π + (𝑇 · (⌊‘(𝑋 / 𝑇)))) = (π + (π · (2 · (⌊‘(𝑋 / 𝑇)))))
201169, 197mulcli 10364 . . . . . . . . . . . . . . . . . 18 (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℂ
20214, 185, 201adddii 10369 . . . . . . . . . . . . . . . . 17 (π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) = ((π · 1) + (π · (2 · (⌊‘(𝑋 / 𝑇)))))
203188, 200, 2023eqtr4ri 2860 . . . . . . . . . . . . . . . 16 (π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) = (π + (𝑇 · (⌊‘(𝑋 / 𝑇))))
204203a1i 11 . . . . . . . . . . . . . . 15 (π = (𝑋 mod 𝑇) → (π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) = (π + (𝑇 · (⌊‘(𝑋 / 𝑇)))))
205 id 22 . . . . . . . . . . . . . . . . 17 (π = (𝑋 mod 𝑇) → π = (𝑋 mod 𝑇))
206 modval 12965 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → (𝑋 mod 𝑇) = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))))
2074, 63, 206mp2an 685 . . . . . . . . . . . . . . . . 17 (𝑋 mod 𝑇) = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇))))
208205, 207syl6eq 2877 . . . . . . . . . . . . . . . 16 (π = (𝑋 mod 𝑇) → π = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))))
209208oveq1d 6920 . . . . . . . . . . . . . . 15 (π = (𝑋 mod 𝑇) → (π + (𝑇 · (⌊‘(𝑋 / 𝑇)))) = ((𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))) + (𝑇 · (⌊‘(𝑋 / 𝑇)))))
21027a1i 11 . . . . . . . . . . . . . . . 16 (π = (𝑋 mod 𝑇) → 𝑋 ∈ ℂ)
21159recni 10371 . . . . . . . . . . . . . . . . . 18 𝑇 ∈ ℂ
212211, 197mulcli 10364 . . . . . . . . . . . . . . . . 17 (𝑇 · (⌊‘(𝑋 / 𝑇))) ∈ ℂ
213212a1i 11 . . . . . . . . . . . . . . . 16 (π = (𝑋 mod 𝑇) → (𝑇 · (⌊‘(𝑋 / 𝑇))) ∈ ℂ)
214210, 213npcand 10717 . . . . . . . . . . . . . . 15 (π = (𝑋 mod 𝑇) → ((𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))) + (𝑇 · (⌊‘(𝑋 / 𝑇)))) = 𝑋)
215204, 209, 2143eqtrrd 2866 . . . . . . . . . . . . . 14 (π = (𝑋 mod 𝑇) → 𝑋 = (π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))))
216215oveq1d 6920 . . . . . . . . . . . . 13 (π = (𝑋 mod 𝑇) → (𝑋 / π) = ((π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) / π))
217185, 201addcli 10363 . . . . . . . . . . . . . 14 (1 + (2 · (⌊‘(𝑋 / 𝑇)))) ∈ ℂ
218217, 14, 35divcan3i 11097 . . . . . . . . . . . . 13 ((π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) / π) = (1 + (2 · (⌊‘(𝑋 / 𝑇))))
219216, 218syl6eq 2877 . . . . . . . . . . . 12 (π = (𝑋 mod 𝑇) → (𝑋 / π) = (1 + (2 · (⌊‘(𝑋 / 𝑇)))))
220 1z 11735 . . . . . . . . . . . . . 14 1 ∈ ℤ
221 zmulcl 11754 . . . . . . . . . . . . . . 15 ((2 ∈ ℤ ∧ (⌊‘(𝑋 / 𝑇)) ∈ ℤ) → (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℤ)
2222, 195, 221mp2an 685 . . . . . . . . . . . . . 14 (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℤ
223 zaddcl 11745 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℤ) → (1 + (2 · (⌊‘(𝑋 / 𝑇)))) ∈ ℤ)
224220, 222, 223mp2an 685 . . . . . . . . . . . . 13 (1 + (2 · (⌊‘(𝑋 / 𝑇)))) ∈ ℤ
225224a1i 11 . . . . . . . . . . . 12 (π = (𝑋 mod 𝑇) → (1 + (2 · (⌊‘(𝑋 / 𝑇)))) ∈ ℤ)
226219, 225eqeltrd 2906 . . . . . . . . . . 11 (π = (𝑋 mod 𝑇) → (𝑋 / π) ∈ ℤ)
227226, 7sylibr 226 . . . . . . . . . 10 (π = (𝑋 mod 𝑇) → (𝑋 mod π) = 0)
228227necon3bi 3025 . . . . . . . . 9 (¬ (𝑋 mod π) = 0 → π ≠ (𝑋 mod 𝑇))
229228adantl 475 . . . . . . . 8 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → π ≠ (𝑋 mod 𝑇))
230180, 181, 184, 229leneltd 10510 . . . . . . 7 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) < π)
231 iftrue 4312 . . . . . . . 8 ((𝑋 mod 𝑇) < π → if((𝑋 mod 𝑇) < π, 1, -1) = 1)
232156, 231syl5eq 2873 . . . . . . 7 ((𝑋 mod 𝑇) < π → (𝐹𝑋) = 1)
233230, 232syl 17 . . . . . 6 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝐹𝑋) = 1)
234179, 233oveq12d 6923 . . . . 5 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = (1 + 1))
235234oveq1d 6920 . . . 4 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = ((1 + 1) / 2))
236 1p1e2 11483 . . . . . . 7 (1 + 1) = 2
237236oveq1i 6915 . . . . . 6 ((1 + 1) / 2) = (2 / 2)
238 2div2e1 11499 . . . . . 6 (2 / 2) = 1
239237, 238eqtr2i 2850 . . . . 5 1 = ((1 + 1) / 2)
240233, 239syl6req 2878 . . . 4 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → ((1 + 1) / 2) = (𝐹𝑋))
241 iffalse 4315 . . . . . 6 (¬ (𝑋 mod π) = 0 → if((𝑋 mod π) = 0, 0, (𝐹𝑋)) = (𝐹𝑋))
242172, 241syl5req 2874 . . . . 5 (¬ (𝑋 mod π) = 0 → (𝐹𝑋) = 𝑌)
243242adantl 475 . . . 4 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝐹𝑋) = 𝑌)
244235, 240, 2433eqtrrd 2866 . . 3 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
245177, 244pm2.61dan 849 . 2 ((𝑋 mod 𝑇) ∈ (0(,]π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
246131necon2bi 3029 . . . . . . . 8 ((𝑋 mod 𝑇) = 0 → ¬ (𝑋 mod 𝑇) ∈ (0(,]π))
247246iffalsed 4317 . . . . . . 7 ((𝑋 mod 𝑇) = 0 → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = -1)
248 id 22 . . . . . . . . . 10 ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) = 0)
249248, 34syl6eqbr 4912 . . . . . . . . 9 ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) < π)
250249iftrued 4314 . . . . . . . 8 ((𝑋 mod 𝑇) = 0 → if((𝑋 mod 𝑇) < π, 1, -1) = 1)
251156, 250syl5eq 2873 . . . . . . 7 ((𝑋 mod 𝑇) = 0 → (𝐹𝑋) = 1)
252247, 251oveq12d 6923 . . . . . 6 ((𝑋 mod 𝑇) = 0 → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = (-1 + 1))
253252oveq1d 6920 . . . . 5 ((𝑋 mod 𝑇) = 0 → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = ((-1 + 1) / 2))
254 neg1cn 11472 . . . . . . . . 9 -1 ∈ ℂ
255185, 254, 165addcomli 10547 . . . . . . . 8 (-1 + 1) = 0
256255oveq1i 6915 . . . . . . 7 ((-1 + 1) / 2) = (0 / 2)
257256, 170eqtri 2849 . . . . . 6 ((-1 + 1) / 2) = 0
258257a1i 11 . . . . 5 ((𝑋 mod 𝑇) = 0 → ((-1 + 1) / 2) = 0)
25940oveq2i 6916 . . . . . . . . . . . . 13 (𝑋 / 𝑇) = (𝑋 / (2 · π))
260 2cnne0 11568 . . . . . . . . . . . . . 14 (2 ∈ ℂ ∧ 2 ≠ 0)
26114, 35pm3.2i 464 . . . . . . . . . . . . . 14 (π ∈ ℂ ∧ π ≠ 0)
262 divdiv1 11062 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → ((𝑋 / 2) / π) = (𝑋 / (2 · π)))
26327, 260, 261, 262mp3an 1591 . . . . . . . . . . . . 13 ((𝑋 / 2) / π) = (𝑋 / (2 · π))
26427, 169, 14, 44, 35divdiv32i 11106 . . . . . . . . . . . . 13 ((𝑋 / 2) / π) = ((𝑋 / π) / 2)
265259, 263, 2643eqtr2i 2855 . . . . . . . . . . . 12 (𝑋 / 𝑇) = ((𝑋 / π) / 2)
266265oveq2i 6916 . . . . . . . . . . 11 (2 · (𝑋 / 𝑇)) = (2 · ((𝑋 / π) / 2))
26727, 14, 35divcli 11093 . . . . . . . . . . . 12 (𝑋 / π) ∈ ℂ
268267, 169, 44divcan2i 11094 . . . . . . . . . . 11 (2 · ((𝑋 / π) / 2)) = (𝑋 / π)
269266, 268eqtr2i 2850 . . . . . . . . . 10 (𝑋 / π) = (2 · (𝑋 / 𝑇))
2702a1i 11 . . . . . . . . . . 11 ((𝑋 / 𝑇) ∈ ℤ → 2 ∈ ℤ)
271 id 22 . . . . . . . . . . 11 ((𝑋 / 𝑇) ∈ ℤ → (𝑋 / 𝑇) ∈ ℤ)
272270, 271zmulcld 11816 . . . . . . . . . 10 ((𝑋 / 𝑇) ∈ ℤ → (2 · (𝑋 / 𝑇)) ∈ ℤ)
273269, 272syl5eqel 2910 . . . . . . . . 9 ((𝑋 / 𝑇) ∈ ℤ → (𝑋 / π) ∈ ℤ)
27465, 273sylbi 209 . . . . . . . 8 ((𝑋 mod 𝑇) = 0 → (𝑋 / π) ∈ ℤ)
275274, 7sylibr 226 . . . . . . 7 ((𝑋 mod 𝑇) = 0 → (𝑋 mod π) = 0)
276275iftrued 4314 . . . . . 6 ((𝑋 mod 𝑇) = 0 → if((𝑋 mod π) = 0, 0, (𝐹𝑋)) = 0)
277172, 276syl5req 2874 . . . . 5 ((𝑋 mod 𝑇) = 0 → 0 = 𝑌)
278253, 258, 2773eqtrrd 2866 . . . 4 ((𝑋 mod 𝑇) = 0 → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
279278adantl 475 . . 3 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod 𝑇) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
280128a1i 11 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π ∈ ℝ*)
28159rexri 10415 . . . . . 6 𝑇 ∈ ℝ*
282281a1i 11 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → 𝑇 ∈ ℝ*)
283139a1i 11 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ ℝ)
284 pm4.56 1018 . . . . . . . 8 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) ↔ ¬ ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
285284biimpi 208 . . . . . . 7 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → ¬ ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
286 olc 901 . . . . . . . . 9 ((𝑋 mod 𝑇) = 0 → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
287286adantl 475 . . . . . . . 8 (((𝑋 mod 𝑇) ≤ π ∧ (𝑋 mod 𝑇) = 0) → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
288127a1i 11 . . . . . . . . . 10 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → 0 ∈ ℝ*)
289128a1i 11 . . . . . . . . . 10 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → π ∈ ℝ*)
290140a1i 11 . . . . . . . . . 10 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ ℝ*)
291 0red 10360 . . . . . . . . . . . 12 (¬ (𝑋 mod 𝑇) = 0 → 0 ∈ ℝ)
292139a1i 11 . . . . . . . . . . . 12 (¬ (𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ∈ ℝ)
293 modge0 12973 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → 0 ≤ (𝑋 mod 𝑇))
2944, 63, 293mp2an 685 . . . . . . . . . . . . 13 0 ≤ (𝑋 mod 𝑇)
295294a1i 11 . . . . . . . . . . . 12 (¬ (𝑋 mod 𝑇) = 0 → 0 ≤ (𝑋 mod 𝑇))
296 neqne 3007 . . . . . . . . . . . 12 (¬ (𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ≠ 0)
297291, 292, 295, 296leneltd 10510 . . . . . . . . . . 11 (¬ (𝑋 mod 𝑇) = 0 → 0 < (𝑋 mod 𝑇))
298297adantl 475 . . . . . . . . . 10 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → 0 < (𝑋 mod 𝑇))
299 simpl 476 . . . . . . . . . 10 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π)
300288, 289, 290, 298, 299eliocd 40529 . . . . . . . . 9 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ (0(,]π))
301300orcd 906 . . . . . . . 8 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
302287, 301pm2.61dan 849 . . . . . . 7 ((𝑋 mod 𝑇) ≤ π → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
303285, 302nsyl 138 . . . . . 6 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → ¬ (𝑋 mod 𝑇) ≤ π)
30433a1i 11 . . . . . . 7 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π ∈ ℝ)
305304, 283ltnled 10503 . . . . . 6 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (π < (𝑋 mod 𝑇) ↔ ¬ (𝑋 mod 𝑇) ≤ π))
306303, 305mpbird 249 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π < (𝑋 mod 𝑇))
307 modlt 12974 . . . . . . 7 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → (𝑋 mod 𝑇) < 𝑇)
3084, 63, 307mp2an 685 . . . . . 6 (𝑋 mod 𝑇) < 𝑇
309308a1i 11 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) < 𝑇)
310280, 282, 283, 306, 309eliood 40519 . . . 4 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ (π(,)𝑇))
311127a1i 11 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → 0 ∈ ℝ*)
31233a1i 11 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → π ∈ ℝ)
313140a1i 11 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝑋 mod 𝑇) ∈ ℝ*)
314 ioogtlb 40516 . . . . . . . . . 10 ((π ∈ ℝ*𝑇 ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (π(,)𝑇)) → π < (𝑋 mod 𝑇))
315128, 281, 314mp3an12 1581 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → π < (𝑋 mod 𝑇))
316311, 312, 313, 315gtnelioc 40511 . . . . . . . 8 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) ∈ (0(,]π))
317316iffalsed 4317 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = -1)
318139a1i 11 . . . . . . . . . 10 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝑋 mod 𝑇) ∈ ℝ)
319312, 318, 315ltnsymd 10505 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) < π)
320319iffalsed 4317 . . . . . . . 8 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod 𝑇) < π, 1, -1) = -1)
321156, 320syl5eq 2873 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝐹𝑋) = -1)
322317, 321oveq12d 6923 . . . . . 6 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = (-1 + -1))
323322oveq1d 6920 . . . . 5 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = ((-1 + -1) / 2))
324 df-2 11414 . . . . . . . . . 10 2 = (1 + 1)
325324negeqi 10594 . . . . . . . . 9 -2 = -(1 + 1)
326185, 185negdii 10686 . . . . . . . . 9 -(1 + 1) = (-1 + -1)
327325, 326eqtr2i 2850 . . . . . . . 8 (-1 + -1) = -2
328327oveq1i 6915 . . . . . . 7 ((-1 + -1) / 2) = (-2 / 2)
329 divneg 11044 . . . . . . . 8 ((2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(2 / 2) = (-2 / 2))
330169, 169, 44, 329mp3an 1591 . . . . . . 7 -(2 / 2) = (-2 / 2)
331238negeqi 10594 . . . . . . 7 -(2 / 2) = -1
332328, 330, 3313eqtr2i 2855 . . . . . 6 ((-1 + -1) / 2) = -1
333332a1i 11 . . . . 5 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ((-1 + -1) / 2) = -1)
334172a1i 11 . . . . . 6 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹𝑋)))
335312, 318ltnled 10503 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (π < (𝑋 mod 𝑇) ↔ ¬ (𝑋 mod 𝑇) ≤ π))
336315, 335mpbid 224 . . . . . . . 8 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) ≤ π)
337248, 112syl6eqbr 4912 . . . . . . . . . 10 ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ≤ π)
338337adantl 475 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π)
339126orcanai 1032 . . . . . . . . . 10 (((𝑋 mod π) = 0 ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) = π)
340339, 144syl 17 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π)
341338, 340pm2.61dan 849 . . . . . . . 8 ((𝑋 mod π) = 0 → (𝑋 mod 𝑇) ≤ π)
342336, 341nsyl 138 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod π) = 0)
343342iffalsed 4317 . . . . . 6 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod π) = 0, 0, (𝐹𝑋)) = (𝐹𝑋))
344334, 343, 3213eqtrrd 2866 . . . . 5 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → -1 = 𝑌)
345323, 333, 3443eqtrrd 2866 . . . 4 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
346310, 345syl 17 . . 3 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
347279, 346pm2.61dan 849 . 2 (¬ (𝑋 mod 𝑇) ∈ (0(,]π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
348245, 347pm2.61i 177 1 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 880   = wceq 1658  wcel 2166  wne 2999  wrex 3118  ifcif 4306   class class class wbr 4873  cmpt 4952  cfv 6123  (class class class)co 6905  cc 10250  cr 10251  0cc0 10252  1c1 10253   + caddc 10255   · cmul 10257  *cxr 10390   < clt 10391  cle 10392  cmin 10585  -cneg 10586   / cdiv 11009  2c2 11406  cz 11704  +crp 12112  (,)cioo 12463  (,]cioc 12464  cfl 12886   mod cmo 12963  πcpi 15169  cdvds 15357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330  ax-addf 10331  ax-mulf 10332
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-iin 4743  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-of 7157  df-om 7327  df-1st 7428  df-2nd 7429  df-supp 7560  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-2o 7827  df-oadd 7830  df-er 8009  df-map 8124  df-pm 8125  df-ixp 8176  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-fsupp 8545  df-fi 8586  df-sup 8617  df-inf 8618  df-oi 8684  df-card 9078  df-cda 9305  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420  df-9 11421  df-n0 11619  df-z 11705  df-dec 11822  df-uz 11969  df-q 12072  df-rp 12113  df-xneg 12232  df-xadd 12233  df-xmul 12234  df-ioo 12467  df-ioc 12468  df-ico 12469  df-icc 12470  df-fz 12620  df-fzo 12761  df-fl 12888  df-mod 12964  df-seq 13096  df-exp 13155  df-fac 13354  df-bc 13383  df-hash 13411  df-shft 14184  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-limsup 14579  df-clim 14596  df-rlim 14597  df-sum 14794  df-ef 15170  df-sin 15172  df-cos 15173  df-pi 15175  df-dvds 15358  df-struct 16224  df-ndx 16225  df-slot 16226  df-base 16228  df-sets 16229  df-ress 16230  df-plusg 16318  df-mulr 16319  df-starv 16320  df-sca 16321  df-vsca 16322  df-ip 16323  df-tset 16324  df-ple 16325  df-ds 16327  df-unif 16328  df-hom 16329  df-cco 16330  df-rest 16436  df-topn 16437  df-0g 16455  df-gsum 16456  df-topgen 16457  df-pt 16458  df-prds 16461  df-xrs 16515  df-qtop 16520  df-imas 16521  df-xps 16523  df-mre 16599  df-mrc 16600  df-acs 16602  df-mgm 17595  df-sgrp 17637  df-mnd 17648  df-submnd 17689  df-mulg 17895  df-cntz 18100  df-cmn 18548  df-psmet 20098  df-xmet 20099  df-met 20100  df-bl 20101  df-mopn 20102  df-fbas 20103  df-fg 20104  df-cnfld 20107  df-top 21069  df-topon 21086  df-topsp 21108  df-bases 21121  df-cld 21194  df-ntr 21195  df-cls 21196  df-nei 21273  df-lp 21311  df-perf 21312  df-cn 21402  df-cnp 21403  df-haus 21490  df-tx 21736  df-hmeo 21929  df-fil 22020  df-fm 22112  df-flim 22113  df-flf 22114  df-xms 22495  df-ms 22496  df-tms 22497  df-cncf 23051  df-limc 24029  df-dv 24030
This theorem is referenced by:  fouriersw  41242
  Copyright terms: Public domain W3C validator