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

Theorem fourierswlem 39123
 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 476 . . . . . . . . . 10 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → 2 ∥ (𝑋 / π))
2 2z 11286 . . . . . . . . . . . 12 2 ∈ ℤ
32a1i 11 . . . . . . . . . . 11 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → 2 ∈ ℤ)
4 fourierswlem.x . . . . . . . . . . . . . 14 𝑋 ∈ ℝ
5 pirp 24017 . . . . . . . . . . . . . 14 π ∈ ℝ+
6 mod0 12537 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ ∧ π ∈ ℝ+) → ((𝑋 mod π) = 0 ↔ (𝑋 / π) ∈ ℤ))
74, 5, 6mp2an 704 . . . . . . . . . . . . 13 ((𝑋 mod π) = 0 ↔ (𝑋 / π) ∈ ℤ)
87biimpi 205 . . . . . . . . . . . 12 ((𝑋 mod π) = 0 → (𝑋 / π) ∈ ℤ)
98adantr 480 . . . . . . . . . . 11 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (𝑋 / π) ∈ ℤ)
10 divides 14823 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ (𝑋 / π) ∈ ℤ) → (2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π)))
113, 9, 10syl2anc 691 . . . . . . . . . 10 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π)))
121, 11mpbid 221 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π))
13 2cnd 10970 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → 2 ∈ ℂ)
14 picn 24015 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℂ
1514a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → π ∈ ℂ)
16 zcn 11259 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
1713, 15, 16mulassd 9942 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → ((2 · π) · 𝑘) = (2 · (π · 𝑘)))
1815, 16mulcld 9939 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (π · 𝑘) ∈ ℂ)
1913, 18mulcomd 9940 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → (2 · (π · 𝑘)) = ((π · 𝑘) · 2))
2017, 19eqtrd 2644 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → ((2 · π) · 𝑘) = ((π · 𝑘) · 2))
2120adantr 480 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((2 · π) · 𝑘) = ((π · 𝑘) · 2))
2215, 16, 13mulassd 9942 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → ((π · 𝑘) · 2) = (π · (𝑘 · 2)))
2322adantr 480 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((π · 𝑘) · 2) = (π · (𝑘 · 2)))
24 id 22 . . . . . . . . . . . . . . . . . . 19 ((𝑘 · 2) = (𝑋 / π) → (𝑘 · 2) = (𝑋 / π))
2524eqcomd 2616 . . . . . . . . . . . . . . . . . 18 ((𝑘 · 2) = (𝑋 / π) → (𝑋 / π) = (𝑘 · 2))
2625adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / π) = (𝑘 · 2))
274recni 9931 . . . . . . . . . . . . . . . . . . 19 𝑋 ∈ ℂ
2827a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑋 ∈ ℂ)
2914a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → π ∈ ℂ)
3016adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑘 ∈ ℂ)
31 2cnd 10970 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 2 ∈ ℂ)
3230, 31mulcld 9939 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑘 · 2) ∈ ℂ)
33 pire 24014 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℝ
34 pipos 24016 . . . . . . . . . . . . . . . . . . . 20 0 < π
3533, 34gt0ne0ii 10443 . . . . . . . . . . . . . . . . . . 19 π ≠ 0
3635a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → π ≠ 0)
3728, 29, 32, 36divmuld 10702 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((𝑋 / π) = (𝑘 · 2) ↔ (π · (𝑘 · 2)) = 𝑋))
3826, 37mpbid 221 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (π · (𝑘 · 2)) = 𝑋)
3921, 23, 383eqtrrd 2649 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑋 = ((2 · π) · 𝑘))
40 fourierswlem.t . . . . . . . . . . . . . . . 16 𝑇 = (2 · π)
4140a1i 11 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑇 = (2 · π))
4239, 41oveq12d 6567 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) = (((2 · π) · 𝑘) / (2 · π)))
4313, 15mulcld 9939 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → (2 · π) ∈ ℂ)
44 2ne0 10990 . . . . . . . . . . . . . . . . . 18 2 ≠ 0
4544a1i 11 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → 2 ≠ 0)
4635a1i 11 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → π ≠ 0)
4713, 15, 45, 46mulne0d 10558 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → (2 · π) ≠ 0)
4816, 43, 47divcan3d 10685 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℤ → (((2 · π) · 𝑘) / (2 · π)) = 𝑘)
4948adantr 480 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (((2 · π) · 𝑘) / (2 · π)) = 𝑘)
5042, 49eqtrd 2644 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) = 𝑘)
51 simpl 472 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑘 ∈ ℤ)
5250, 51eqeltrd 2688 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) ∈ ℤ)
5352ex 449 . . . . . . . . . . 11 (𝑘 ∈ ℤ → ((𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ))
5453a1i 11 . . . . . . . . . 10 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (𝑘 ∈ ℤ → ((𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ)))
5554rexlimdv 3012 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ))
5612, 55mpd 15 . . . . . . . 8 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (𝑋 / 𝑇) ∈ ℤ)
57 2re 10967 . . . . . . . . . . . 12 2 ∈ ℝ
5857, 33remulcli 9933 . . . . . . . . . . 11 (2 · π) ∈ ℝ
5940, 58eqeltri 2684 . . . . . . . . . 10 𝑇 ∈ ℝ
60 2pos 10989 . . . . . . . . . . . 12 0 < 2
6157, 33, 60, 34mulgt0ii 10049 . . . . . . . . . . 11 0 < (2 · π)
6261, 40breqtrri 4610 . . . . . . . . . 10 0 < 𝑇
6359, 62elrpii 11711 . . . . . . . . 9 𝑇 ∈ ℝ+
64 mod0 12537 . . . . . . . . 9 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → ((𝑋 mod 𝑇) = 0 ↔ (𝑋 / 𝑇) ∈ ℤ))
654, 63, 64mp2an 704 . . . . . . . 8 ((𝑋 mod 𝑇) = 0 ↔ (𝑋 / 𝑇) ∈ ℤ)
6656, 65sylibr 223 . . . . . . 7 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → (𝑋 mod 𝑇) = 0)
6766orcd 406 . . . . . 6 (((𝑋 mod π) = 0 ∧ 2 ∥ (𝑋 / π)) → ((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π))
68 odd2np1 14903 . . . . . . . . . 10 ((𝑋 / π) ∈ ℤ → (¬ 2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = (𝑋 / π)))
697, 68sylbi 206 . . . . . . . . 9 ((𝑋 mod π) = 0 → (¬ 2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = (𝑋 / π)))
7069biimpa 500 . . . . . . . 8 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → ∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = (𝑋 / π))
7113, 16mulcld 9939 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → (2 · 𝑘) ∈ ℂ)
7271adantr 480 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (2 · 𝑘) ∈ ℂ)
73 1cnd 9935 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 1 ∈ ℂ)
7414a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → π ∈ ℂ)
7572, 73, 74adddird 9944 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (((2 · 𝑘) + 1) · π) = (((2 · 𝑘) · π) + (1 · π)))
7613, 16mulcomd 9940 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (2 · 𝑘) = (𝑘 · 2))
7776oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → ((2 · 𝑘) · π) = ((𝑘 · 2) · π))
7816, 13, 15mulassd 9942 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → ((𝑘 · 2) · π) = (𝑘 · (2 · π)))
7940eqcomi 2619 . . . . . . . . . . . . . . . . . . . 20 (2 · π) = 𝑇
8079a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (2 · π) = 𝑇)
8180oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → (𝑘 · (2 · π)) = (𝑘 · 𝑇))
8277, 78, 813eqtrd 2648 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → ((2 · 𝑘) · π) = (𝑘 · 𝑇))
8314mulid2i 9922 . . . . . . . . . . . . . . . . . 18 (1 · π) = π
8483a1i 11 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → (1 · π) = π)
8582, 84oveq12d 6567 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → (((2 · 𝑘) · π) + (1 · π)) = ((𝑘 · 𝑇) + π))
8685adantr 480 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (((2 · 𝑘) · π) + (1 · π)) = ((𝑘 · 𝑇) + π))
8740, 43syl5eqel 2692 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → 𝑇 ∈ ℂ)
8816, 87mulcld 9939 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → (𝑘 · 𝑇) ∈ ℂ)
8988, 15addcomd 10117 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → ((𝑘 · 𝑇) + π) = (π + (𝑘 · 𝑇)))
9089adantr 480 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → ((𝑘 · 𝑇) + π) = (π + (𝑘 · 𝑇)))
9175, 86, 903eqtrrd 2649 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (π + (𝑘 · 𝑇)) = (((2 · 𝑘) + 1) · π))
92 peano2cn 10087 . . . . . . . . . . . . . . . . 17 ((2 · 𝑘) ∈ ℂ → ((2 · 𝑘) + 1) ∈ ℂ)
9371, 92syl 17 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℤ → ((2 · 𝑘) + 1) ∈ ℂ)
9493, 15mulcomd 9940 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℤ → (((2 · 𝑘) + 1) · π) = (π · ((2 · 𝑘) + 1)))
9594adantr 480 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (((2 · 𝑘) + 1) · π) = (π · ((2 · 𝑘) + 1)))
96 id 22 . . . . . . . . . . . . . . . . 17 (((2 · 𝑘) + 1) = (𝑋 / π) → ((2 · 𝑘) + 1) = (𝑋 / π))
9796eqcomd 2616 . . . . . . . . . . . . . . . 16 (((2 · 𝑘) + 1) = (𝑋 / π) → (𝑋 / π) = ((2 · 𝑘) + 1))
9897adantl 481 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (𝑋 / π) = ((2 · 𝑘) + 1))
9927a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 𝑋 ∈ ℂ)
10093adantr 480 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → ((2 · 𝑘) + 1) ∈ ℂ)
10135a1i 11 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → π ≠ 0)
10299, 74, 100, 101divmuld 10702 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → ((𝑋 / π) = ((2 · 𝑘) + 1) ↔ (π · ((2 · 𝑘) + 1)) = 𝑋))
10398, 102mpbid 221 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (π · ((2 · 𝑘) + 1)) = 𝑋)
10491, 95, 1033eqtrrd 2649 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 𝑋 = (π + (𝑘 · 𝑇)))
105104oveq1d 6564 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (𝑋 mod 𝑇) = ((π + (𝑘 · 𝑇)) mod 𝑇))
106 modcyc 12567 . . . . . . . . . . . . . 14 ((π ∈ ℝ ∧ 𝑇 ∈ ℝ+𝑘 ∈ ℤ) → ((π + (𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇))
10733, 63, 106mp3an12 1406 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → ((π + (𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇))
108107adantr 480 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → ((π + (𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇))
10933a1i 11 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → π ∈ ℝ)
11063a1i 11 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 𝑇 ∈ ℝ+)
111 0re 9919 . . . . . . . . . . . . . . 15 0 ∈ ℝ
112111, 33, 34ltleii 10039 . . . . . . . . . . . . . 14 0 ≤ π
113112a1i 11 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → 0 ≤ π)
114 2timesgt 38441 . . . . . . . . . . . . . . . 16 (π ∈ ℝ+ → π < (2 · π))
1155, 114ax-mp 5 . . . . . . . . . . . . . . 15 π < (2 · π)
116115, 40breqtrri 4610 . . . . . . . . . . . . . 14 π < 𝑇
117116a1i 11 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → π < 𝑇)
118 modid 12557 . . . . . . . . . . . . 13 (((π ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ π ∧ π < 𝑇)) → (π mod 𝑇) = π)
119109, 110, 113, 117, 118syl22anc 1319 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (π mod 𝑇) = π)
120105, 108, 1193eqtrd 2648 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ ((2 · 𝑘) + 1) = (𝑋 / π)) → (𝑋 mod 𝑇) = π)
121120ex 449 . . . . . . . . . 10 (𝑘 ∈ ℤ → (((2 · 𝑘) + 1) = (𝑋 / π) → (𝑋 mod 𝑇) = π))
122121a1i 11 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → (𝑘 ∈ ℤ → (((2 · 𝑘) + 1) = (𝑋 / π) → (𝑋 mod 𝑇) = π)))
123122rexlimdv 3012 . . . . . . . 8 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → (∃𝑘 ∈ ℤ ((2 · 𝑘) + 1) = (𝑋 / π) → (𝑋 mod 𝑇) = π))
12470, 123mpd 15 . . . . . . 7 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → (𝑋 mod 𝑇) = π)
125124olcd 407 . . . . . 6 (((𝑋 mod π) = 0 ∧ ¬ 2 ∥ (𝑋 / π)) → ((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π))
12667, 125pm2.61dan 828 . . . . 5 ((𝑋 mod π) = 0 → ((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π))
127 0xr 9965 . . . . . . . 8 0 ∈ ℝ*
12833rexri 9976 . . . . . . . 8 π ∈ ℝ*
129 iocgtlb 38571 . . . . . . . 8 ((0 ∈ ℝ* ∧ π ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (0(,]π)) → 0 < (𝑋 mod 𝑇))
130127, 128, 129mp3an12 1406 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (0(,]π) → 0 < (𝑋 mod 𝑇))
131130gt0ne0d 10471 . . . . . 6 ((𝑋 mod 𝑇) ∈ (0(,]π) → (𝑋 mod 𝑇) ≠ 0)
132131neneqd 2787 . . . . 5 ((𝑋 mod 𝑇) ∈ (0(,]π) → ¬ (𝑋 mod 𝑇) = 0)
133 pm2.53 387 . . . . . 6 (((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π) → (¬ (𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) = π))
134133imp 444 . . . . 5 ((((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) = π)
135126, 132, 134syl2anr 494 . . . 4 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) = π)
136127a1i 11 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → 0 ∈ ℝ*)
137128a1i 11 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → π ∈ ℝ*)
138 modcl 12534 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → (𝑋 mod 𝑇) ∈ ℝ)
1394, 63, 138mp2an 704 . . . . . . . . . . . . . 14 (𝑋 mod 𝑇) ∈ ℝ
140139rexri 9976 . . . . . . . . . . . . 13 (𝑋 mod 𝑇) ∈ ℝ*
141140a1i 11 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ∈ ℝ*)
142 id 22 . . . . . . . . . . . . 13 ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) = π)
14334, 142syl5breqr 4621 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → 0 < (𝑋 mod 𝑇))
14433eqlei2 10027 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ≤ π)
145136, 137, 141, 143, 144eliocd 38577 . . . . . . . . . . 11 ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ∈ (0(,]π))
146145iftrued 4044 . . . . . . . . . 10 ((𝑋 mod 𝑇) = π → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = 1)
147146adantl 481 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = 1)
148 oveq1 6556 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝑥 mod 𝑇) = (𝑋 mod 𝑇))
149148breq1d 4593 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → ((𝑥 mod 𝑇) < π ↔ (𝑋 mod 𝑇) < π))
150149ifbid 4058 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → if((𝑥 mod 𝑇) < π, 1, -1) = if((𝑋 mod 𝑇) < π, 1, -1))
151 fourierswlem.f . . . . . . . . . . . . 13 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
152 1ex 9914 . . . . . . . . . . . . . 14 1 ∈ V
153 negex 10158 . . . . . . . . . . . . . 14 -1 ∈ V
154152, 153ifex 4106 . . . . . . . . . . . . 13 if((𝑋 mod 𝑇) < π, 1, -1) ∈ V
155150, 151, 154fvmpt 6191 . . . . . . . . . . . 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 10052 . . . . . . . . . . . . 13 ((𝑋 mod 𝑇) < π → (𝑋 mod 𝑇) ≠ π)
160159necon2bi 2812 . . . . . . . . . . . 12 ((𝑋 mod 𝑇) = π → ¬ (𝑋 mod 𝑇) < π)
161160iffalsed 4047 . . . . . . . . . . 11 ((𝑋 mod 𝑇) = π → if((𝑋 mod 𝑇) < π, 1, -1) = -1)
162156, 161syl5eq 2656 . . . . . . . . . 10 ((𝑋 mod 𝑇) = π → (𝐹𝑋) = -1)
163162adantl 481 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (𝐹𝑋) = -1)
164147, 163oveq12d 6567 . . . . . . . 8 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = (1 + -1))
165 1pneg1e0 11006 . . . . . . . 8 (1 + -1) = 0
166164, 165syl6eq 2660 . . . . . . 7 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = 0)
167166oveq1d 6564 . . . . . 6 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = (0 / 2))
168167adantll 746 . . . . 5 ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = (0 / 2))
169 2cn 10968 . . . . . . 7 2 ∈ ℂ
170169, 44div0i 10638 . . . . . 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 4042 . . . . . . 7 ((𝑋 mod π) = 0 → if((𝑋 mod π) = 0, 0, (𝐹𝑋)) = 0)
174172, 173syl5req 2657 . . . . . 6 ((𝑋 mod π) = 0 → 0 = 𝑌)
175174ad2antlr 759 . . . . 5 ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → 0 = 𝑌)
176168, 171, 1753eqtrrd 2649 . . . 4 ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
177135, 176mpdan 699 . . 3 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
178 iftrue 4042 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (0(,]π) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = 1)
179178adantr 480 . . . . . 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 38572 . . . . . . . . . 10 ((0 ∈ ℝ* ∧ π ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (0(,]π)) → (𝑋 mod 𝑇) ≤ π)
183127, 128, 182mp3an12 1406 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (0(,]π) → (𝑋 mod 𝑇) ≤ π)
184183adantr 480 . . . . . . . 8 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) ≤ π)
185 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℂ
186185, 14mulcomi 9925 . . . . . . . . . . . . . . . . . . 19 (1 · π) = (π · 1)
18783, 186eqtr3i 2634 . . . . . . . . . . . . . . . . . 18 π = (π · 1)
188187oveq1i 6559 . . . . . . . . . . . . . . . . 17 (π + (π · (2 · (⌊‘(𝑋 / 𝑇))))) = ((π · 1) + (π · (2 · (⌊‘(𝑋 / 𝑇)))))
189169, 14mulcomi 9925 . . . . . . . . . . . . . . . . . . . . 21 (2 · π) = (π · 2)
19040, 189eqtri 2632 . . . . . . . . . . . . . . . . . . . 20 𝑇 = (π · 2)
191190oveq1i 6559 . . . . . . . . . . . . . . . . . . 19 (𝑇 · (⌊‘(𝑋 / 𝑇))) = ((π · 2) · (⌊‘(𝑋 / 𝑇)))
192111, 62gtneii 10028 . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 ≠ 0
1934, 59, 192redivcli 10671 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 / 𝑇) ∈ ℝ
194 flcl 12458 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 / 𝑇) ∈ ℝ → (⌊‘(𝑋 / 𝑇)) ∈ ℤ)
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (⌊‘(𝑋 / 𝑇)) ∈ ℤ
196 zcn 11259 . . . . . . . . . . . . . . . . . . . . 21 ((⌊‘(𝑋 / 𝑇)) ∈ ℤ → (⌊‘(𝑋 / 𝑇)) ∈ ℂ)
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⌊‘(𝑋 / 𝑇)) ∈ ℂ
19814, 169, 197mulassi 9928 . . . . . . . . . . . . . . . . . . 19 ((π · 2) · (⌊‘(𝑋 / 𝑇))) = (π · (2 · (⌊‘(𝑋 / 𝑇))))
199191, 198eqtri 2632 . . . . . . . . . . . . . . . . . 18 (𝑇 · (⌊‘(𝑋 / 𝑇))) = (π · (2 · (⌊‘(𝑋 / 𝑇))))
200199oveq2i 6560 . . . . . . . . . . . . . . . . 17 (π + (𝑇 · (⌊‘(𝑋 / 𝑇)))) = (π + (π · (2 · (⌊‘(𝑋 / 𝑇)))))
201169, 197mulcli 9924 . . . . . . . . . . . . . . . . . 18 (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℂ
20214, 185, 201adddii 9929 . . . . . . . . . . . . . . . . 17 (π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) = ((π · 1) + (π · (2 · (⌊‘(𝑋 / 𝑇)))))
203188, 200, 2023eqtr4ri 2643 . . . . . . . . . . . . . . . 16 (π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) = (π + (𝑇 · (⌊‘(𝑋 / 𝑇))))
204203a1i 11 . . . . . . . . . . . . . . 15 (π = (𝑋 mod 𝑇) → (π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) = (π + (𝑇 · (⌊‘(𝑋 / 𝑇)))))
205 id 22 . . . . . . . . . . . . . . . . 17 (π = (𝑋 mod 𝑇) → π = (𝑋 mod 𝑇))
206 modval 12532 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → (𝑋 mod 𝑇) = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))))
2074, 63, 206mp2an 704 . . . . . . . . . . . . . . . . 17 (𝑋 mod 𝑇) = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇))))
208205, 207syl6eq 2660 . . . . . . . . . . . . . . . 16 (π = (𝑋 mod 𝑇) → π = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))))
209208oveq1d 6564 . . . . . . . . . . . . . . 15 (π = (𝑋 mod 𝑇) → (π + (𝑇 · (⌊‘(𝑋 / 𝑇)))) = ((𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))) + (𝑇 · (⌊‘(𝑋 / 𝑇)))))
21027a1i 11 . . . . . . . . . . . . . . . 16 (π = (𝑋 mod 𝑇) → 𝑋 ∈ ℂ)
21159recni 9931 . . . . . . . . . . . . . . . . . 18 𝑇 ∈ ℂ
212211, 197mulcli 9924 . . . . . . . . . . . . . . . . 17 (𝑇 · (⌊‘(𝑋 / 𝑇))) ∈ ℂ
213212a1i 11 . . . . . . . . . . . . . . . 16 (π = (𝑋 mod 𝑇) → (𝑇 · (⌊‘(𝑋 / 𝑇))) ∈ ℂ)
214210, 213npcand 10275 . . . . . . . . . . . . . . 15 (π = (𝑋 mod 𝑇) → ((𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))) + (𝑇 · (⌊‘(𝑋 / 𝑇)))) = 𝑋)
215204, 209, 2143eqtrrd 2649 . . . . . . . . . . . . . 14 (π = (𝑋 mod 𝑇) → 𝑋 = (π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))))
216215oveq1d 6564 . . . . . . . . . . . . 13 (π = (𝑋 mod 𝑇) → (𝑋 / π) = ((π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) / π))
217185, 201addcli 9923 . . . . . . . . . . . . . 14 (1 + (2 · (⌊‘(𝑋 / 𝑇)))) ∈ ℂ
218217, 14, 35divcan3i 10650 . . . . . . . . . . . . 13 ((π · (1 + (2 · (⌊‘(𝑋 / 𝑇))))) / π) = (1 + (2 · (⌊‘(𝑋 / 𝑇))))
219216, 218syl6eq 2660 . . . . . . . . . . . 12 (π = (𝑋 mod 𝑇) → (𝑋 / π) = (1 + (2 · (⌊‘(𝑋 / 𝑇)))))
220 1z 11284 . . . . . . . . . . . . . 14 1 ∈ ℤ
221 zmulcl 11303 . . . . . . . . . . . . . . 15 ((2 ∈ ℤ ∧ (⌊‘(𝑋 / 𝑇)) ∈ ℤ) → (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℤ)
2222, 195, 221mp2an 704 . . . . . . . . . . . . . 14 (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℤ
223 zaddcl 11294 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℤ) → (1 + (2 · (⌊‘(𝑋 / 𝑇)))) ∈ ℤ)
224220, 222, 223mp2an 704 . . . . . . . . . . . . 13 (1 + (2 · (⌊‘(𝑋 / 𝑇)))) ∈ ℤ
225224a1i 11 . . . . . . . . . . . 12 (π = (𝑋 mod 𝑇) → (1 + (2 · (⌊‘(𝑋 / 𝑇)))) ∈ ℤ)
226219, 225eqeltrd 2688 . . . . . . . . . . 11 (π = (𝑋 mod 𝑇) → (𝑋 / π) ∈ ℤ)
227226, 7sylibr 223 . . . . . . . . . 10 (π = (𝑋 mod 𝑇) → (𝑋 mod π) = 0)
228227necon3bi 2808 . . . . . . . . 9 (¬ (𝑋 mod π) = 0 → π ≠ (𝑋 mod 𝑇))
229228adantl 481 . . . . . . . 8 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → π ≠ (𝑋 mod 𝑇))
230180, 181, 184, 229leneltd 10070 . . . . . . 7 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) < π)
231 iftrue 4042 . . . . . . . 8 ((𝑋 mod 𝑇) < π → if((𝑋 mod 𝑇) < π, 1, -1) = 1)
232156, 231syl5eq 2656 . . . . . . 7 ((𝑋 mod 𝑇) < π → (𝐹𝑋) = 1)
233230, 232syl 17 . . . . . 6 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝐹𝑋) = 1)
234179, 233oveq12d 6567 . . . . 5 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = (1 + 1))
235234oveq1d 6564 . . . 4 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = ((1 + 1) / 2))
236 1p1e2 11011 . . . . . . 7 (1 + 1) = 2
237236oveq1i 6559 . . . . . 6 ((1 + 1) / 2) = (2 / 2)
238 2div2e1 11027 . . . . . 6 (2 / 2) = 1
239237, 238eqtr2i 2633 . . . . 5 1 = ((1 + 1) / 2)
240233, 239syl6req 2661 . . . 4 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → ((1 + 1) / 2) = (𝐹𝑋))
241 iffalse 4045 . . . . . 6 (¬ (𝑋 mod π) = 0 → if((𝑋 mod π) = 0, 0, (𝐹𝑋)) = (𝐹𝑋))
242172, 241syl5req 2657 . . . . 5 (¬ (𝑋 mod π) = 0 → (𝐹𝑋) = 𝑌)
243242adantl 481 . . . 4 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝐹𝑋) = 𝑌)
244235, 240, 2433eqtrrd 2649 . . 3 (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
245177, 244pm2.61dan 828 . 2 ((𝑋 mod 𝑇) ∈ (0(,]π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
246131necon2bi 2812 . . . . . . . 8 ((𝑋 mod 𝑇) = 0 → ¬ (𝑋 mod 𝑇) ∈ (0(,]π))
247246iffalsed 4047 . . . . . . 7 ((𝑋 mod 𝑇) = 0 → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = -1)
248 id 22 . . . . . . . . . 10 ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) = 0)
249248, 34syl6eqbr 4622 . . . . . . . . 9 ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) < π)
250249iftrued 4044 . . . . . . . 8 ((𝑋 mod 𝑇) = 0 → if((𝑋 mod 𝑇) < π, 1, -1) = 1)
251156, 250syl5eq 2656 . . . . . . 7 ((𝑋 mod 𝑇) = 0 → (𝐹𝑋) = 1)
252247, 251oveq12d 6567 . . . . . 6 ((𝑋 mod 𝑇) = 0 → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = (-1 + 1))
253252oveq1d 6564 . . . . 5 ((𝑋 mod 𝑇) = 0 → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = ((-1 + 1) / 2))
254 neg1cn 11001 . . . . . . . . 9 -1 ∈ ℂ
255185, 254, 165addcomli 10107 . . . . . . . 8 (-1 + 1) = 0
256255oveq1i 6559 . . . . . . 7 ((-1 + 1) / 2) = (0 / 2)
257256, 170eqtri 2632 . . . . . 6 ((-1 + 1) / 2) = 0
258257a1i 11 . . . . 5 ((𝑋 mod 𝑇) = 0 → ((-1 + 1) / 2) = 0)
25940oveq2i 6560 . . . . . . . . . . . . 13 (𝑋 / 𝑇) = (𝑋 / (2 · π))
260 2cnne0 11119 . . . . . . . . . . . . . 14 (2 ∈ ℂ ∧ 2 ≠ 0)
26114, 35pm3.2i 470 . . . . . . . . . . . . . 14 (π ∈ ℂ ∧ π ≠ 0)
262 divdiv1 10615 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → ((𝑋 / 2) / π) = (𝑋 / (2 · π)))
26327, 260, 261, 262mp3an 1416 . . . . . . . . . . . . 13 ((𝑋 / 2) / π) = (𝑋 / (2 · π))
26427, 169, 14, 44, 35divdiv32i 10659 . . . . . . . . . . . . 13 ((𝑋 / 2) / π) = ((𝑋 / π) / 2)
265259, 263, 2643eqtr2i 2638 . . . . . . . . . . . 12 (𝑋 / 𝑇) = ((𝑋 / π) / 2)
266265oveq2i 6560 . . . . . . . . . . 11 (2 · (𝑋 / 𝑇)) = (2 · ((𝑋 / π) / 2))
26727, 14, 35divcli 10646 . . . . . . . . . . . 12 (𝑋 / π) ∈ ℂ
268267, 169, 44divcan2i 10647 . . . . . . . . . . 11 (2 · ((𝑋 / π) / 2)) = (𝑋 / π)
269266, 268eqtr2i 2633 . . . . . . . . . 10 (𝑋 / π) = (2 · (𝑋 / 𝑇))
2702a1i 11 . . . . . . . . . . 11 ((𝑋 / 𝑇) ∈ ℤ → 2 ∈ ℤ)
271 id 22 . . . . . . . . . . 11 ((𝑋 / 𝑇) ∈ ℤ → (𝑋 / 𝑇) ∈ ℤ)
272270, 271zmulcld 11364 . . . . . . . . . 10 ((𝑋 / 𝑇) ∈ ℤ → (2 · (𝑋 / 𝑇)) ∈ ℤ)
273269, 272syl5eqel 2692 . . . . . . . . 9 ((𝑋 / 𝑇) ∈ ℤ → (𝑋 / π) ∈ ℤ)
27465, 273sylbi 206 . . . . . . . 8 ((𝑋 mod 𝑇) = 0 → (𝑋 / π) ∈ ℤ)
275274, 7sylibr 223 . . . . . . 7 ((𝑋 mod 𝑇) = 0 → (𝑋 mod π) = 0)
276275iftrued 4044 . . . . . 6 ((𝑋 mod 𝑇) = 0 → if((𝑋 mod π) = 0, 0, (𝐹𝑋)) = 0)
277172, 276syl5req 2657 . . . . 5 ((𝑋 mod 𝑇) = 0 → 0 = 𝑌)
278253, 258, 2773eqtrrd 2649 . . . 4 ((𝑋 mod 𝑇) = 0 → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
279278adantl 481 . . 3 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod 𝑇) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
280128a1i 11 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π ∈ ℝ*)
28159rexri 9976 . . . . . 6 𝑇 ∈ ℝ*
282281a1i 11 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → 𝑇 ∈ ℝ*)
283139a1i 11 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ ℝ)
284 pm4.56 515 . . . . . . . 8 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) ↔ ¬ ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
285284biimpi 205 . . . . . . 7 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → ¬ ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
286 olc 398 . . . . . . . . 9 ((𝑋 mod 𝑇) = 0 → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
287286adantl 481 . . . . . . . 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 9920 . . . . . . . . . . . 12 (¬ (𝑋 mod 𝑇) = 0 → 0 ∈ ℝ)
292139a1i 11 . . . . . . . . . . . 12 (¬ (𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ∈ ℝ)
293 modge0 12540 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → 0 ≤ (𝑋 mod 𝑇))
2944, 63, 293mp2an 704 . . . . . . . . . . . . 13 0 ≤ (𝑋 mod 𝑇)
295294a1i 11 . . . . . . . . . . . 12 (¬ (𝑋 mod 𝑇) = 0 → 0 ≤ (𝑋 mod 𝑇))
296 neqne 2790 . . . . . . . . . . . 12 (¬ (𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ≠ 0)
297291, 292, 295, 296leneltd 10070 . . . . . . . . . . 11 (¬ (𝑋 mod 𝑇) = 0 → 0 < (𝑋 mod 𝑇))
298297adantl 481 . . . . . . . . . 10 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → 0 < (𝑋 mod 𝑇))
299 simpl 472 . . . . . . . . . 10 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π)
300288, 289, 290, 298, 299eliocd 38577 . . . . . . . . 9 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ (0(,]π))
301300orcd 406 . . . . . . . 8 (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
302287, 301pm2.61dan 828 . . . . . . 7 ((𝑋 mod 𝑇) ≤ π → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0))
303285, 302nsyl 134 . . . . . 6 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → ¬ (𝑋 mod 𝑇) ≤ π)
30433a1i 11 . . . . . . 7 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π ∈ ℝ)
305304, 283ltnled 10063 . . . . . 6 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (π < (𝑋 mod 𝑇) ↔ ¬ (𝑋 mod 𝑇) ≤ π))
306303, 305mpbird 246 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π < (𝑋 mod 𝑇))
307 modlt 12541 . . . . . . 7 ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+) → (𝑋 mod 𝑇) < 𝑇)
3084, 63, 307mp2an 704 . . . . . 6 (𝑋 mod 𝑇) < 𝑇
309308a1i 11 . . . . 5 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) < 𝑇)
310280, 282, 283, 306, 309eliood 38567 . . . 4 ((¬ (𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ (π(,)𝑇))
311127a1i 11 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → 0 ∈ ℝ*)
31233a1i 11 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → π ∈ ℝ)
313140a1i 11 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝑋 mod 𝑇) ∈ ℝ*)
314 ioogtlb 38564 . . . . . . . . . 10 ((π ∈ ℝ*𝑇 ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (π(,)𝑇)) → π < (𝑋 mod 𝑇))
315128, 281, 314mp3an12 1406 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → π < (𝑋 mod 𝑇))
316311, 312, 313, 315gtnelioc 38559 . . . . . . . 8 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) ∈ (0(,]π))
317316iffalsed 4047 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) = -1)
318139a1i 11 . . . . . . . . . 10 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝑋 mod 𝑇) ∈ ℝ)
319312, 318, 315ltnsymd 10065 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) < π)
320319iffalsed 4047 . . . . . . . 8 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod 𝑇) < π, 1, -1) = -1)
321156, 320syl5eq 2656 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝐹𝑋) = -1)
322317, 321oveq12d 6567 . . . . . 6 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) = (-1 + -1))
323322oveq1d 6564 . . . . 5 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2) = ((-1 + -1) / 2))
324 df-2 10956 . . . . . . . . . 10 2 = (1 + 1)
325324negeqi 10153 . . . . . . . . 9 -2 = -(1 + 1)
326185, 185negdii 10244 . . . . . . . . 9 -(1 + 1) = (-1 + -1)
327325, 326eqtr2i 2633 . . . . . . . 8 (-1 + -1) = -2
328327oveq1i 6559 . . . . . . 7 ((-1 + -1) / 2) = (-2 / 2)
329 divneg 10598 . . . . . . . 8 ((2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(2 / 2) = (-2 / 2))
330169, 169, 44, 329mp3an 1416 . . . . . . 7 -(2 / 2) = (-2 / 2)
331238negeqi 10153 . . . . . . 7 -(2 / 2) = -1
332328, 330, 3313eqtr2i 2638 . . . . . 6 ((-1 + -1) / 2) = -1
333332a1i 11 . . . . 5 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ((-1 + -1) / 2) = -1)
334172a1i 11 . . . . . 6 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹𝑋)))
335312, 318ltnled 10063 . . . . . . . . 9 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (π < (𝑋 mod 𝑇) ↔ ¬ (𝑋 mod 𝑇) ≤ π))
336315, 335mpbid 221 . . . . . . . 8 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) ≤ π)
337248, 112syl6eqbr 4622 . . . . . . . . . 10 ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ≤ π)
338337adantl 481 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π)
339126orcanai 950 . . . . . . . . . 10 (((𝑋 mod π) = 0 ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) = π)
340339, 144syl 17 . . . . . . . . 9 (((𝑋 mod π) = 0 ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π)
341338, 340pm2.61dan 828 . . . . . . . 8 ((𝑋 mod π) = 0 → (𝑋 mod 𝑇) ≤ π)
342336, 341nsyl 134 . . . . . . 7 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod π) = 0)
343342iffalsed 4047 . . . . . 6 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod π) = 0, 0, (𝐹𝑋)) = (𝐹𝑋))
344334, 343, 3213eqtrrd 2649 . . . . 5 ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → -1 = 𝑌)
345323, 333, 3443eqtrrd 2649 . . . 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 828 . 2 (¬ (𝑋 mod 𝑇) ∈ (0(,]π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2))
348245, 347pm2.61i 175 1 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹𝑋)) / 2)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146   / cdiv 10563  2c2 10947  ℤcz 11254  ℝ+crp 11708  (,)cioo 12046  (,]cioc 12047  ⌊cfl 12453   mod cmo 12530  πcpi 14636   ∥ cdvds 14821 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-dvds 14822  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437 This theorem is referenced by:  fouriersw  39124
 Copyright terms: Public domain W3C validator