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 44545
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 486 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ 2 โˆฅ (๐‘‹ / ฯ€))
2 2z 12542 . . . . . . . . . . . 12 2 โˆˆ โ„ค
32a1i 11 . . . . . . . . . . 11 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ 2 โˆˆ โ„ค)
4 fourierswlem.x . . . . . . . . . . . . . 14 ๐‘‹ โˆˆ โ„
5 pirp 25834 . . . . . . . . . . . . . 14 ฯ€ โˆˆ โ„+
6 mod0 13788 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„ โˆง ฯ€ โˆˆ โ„+) โ†’ ((๐‘‹ mod ฯ€) = 0 โ†” (๐‘‹ / ฯ€) โˆˆ โ„ค))
74, 5, 6mp2an 691 . . . . . . . . . . . . 13 ((๐‘‹ mod ฯ€) = 0 โ†” (๐‘‹ / ฯ€) โˆˆ โ„ค)
87biimpi 215 . . . . . . . . . . . 12 ((๐‘‹ mod ฯ€) = 0 โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
98adantr 482 . . . . . . . . . . 11 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
10 divides 16145 . . . . . . . . . . 11 ((2 โˆˆ โ„ค โˆง (๐‘‹ / ฯ€) โˆˆ โ„ค) โ†’ (2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)))
113, 9, 10syl2anc 585 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)))
121, 11mpbid 231 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€))
13 2cnd 12238 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ 2 โˆˆ โ„‚)
14 picn 25832 . . . . . . . . . . . . . . . . . . . 20 ฯ€ โˆˆ โ„‚
1514a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ ฯ€ โˆˆ โ„‚)
16 zcn 12511 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ ๐‘˜ โˆˆ โ„‚)
1713, 15, 16mulassd 11185 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = (2 ยท (ฯ€ ยท ๐‘˜)))
1815, 16mulcld 11182 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (ฯ€ ยท ๐‘˜) โˆˆ โ„‚)
1913, 18mulcomd 11183 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท (ฯ€ ยท ๐‘˜)) = ((ฯ€ ยท ๐‘˜) ยท 2))
2017, 19eqtrd 2777 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = ((ฯ€ ยท ๐‘˜) ยท 2))
2120adantr 482 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = ((ฯ€ ยท ๐‘˜) ยท 2))
2215, 16, 13mulassd 11185 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((ฯ€ ยท ๐‘˜) ยท 2) = (ฯ€ ยท (๐‘˜ ยท 2)))
2322adantr 482 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((ฯ€ ยท ๐‘˜) ยท 2) = (ฯ€ ยท (๐‘˜ ยท 2)))
24 id 22 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘˜ ยท 2) = (๐‘‹ / ฯ€))
2524eqcomd 2743 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ฯ€) = (๐‘˜ ยท 2))
2625adantl 483 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ฯ€) = (๐‘˜ ยท 2))
274recni 11176 . . . . . . . . . . . . . . . . . . 19 ๐‘‹ โˆˆ โ„‚
2827a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ โˆˆ โ„‚)
2914a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„‚)
3016adantr 482 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘˜ โˆˆ โ„‚)
31 2cnd 12238 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ 2 โˆˆ โ„‚)
3230, 31mulcld 11182 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘˜ ยท 2) โˆˆ โ„‚)
33 pire 25831 . . . . . . . . . . . . . . . . . . . 20 ฯ€ โˆˆ โ„
34 pipos 25833 . . . . . . . . . . . . . . . . . . . 20 0 < ฯ€
3533, 34gt0ne0ii 11698 . . . . . . . . . . . . . . . . . . 19 ฯ€ โ‰  0
3635a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โ‰  0)
3728, 29, 32, 36divmuld 11960 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ / ฯ€) = (๐‘˜ ยท 2) โ†” (ฯ€ ยท (๐‘˜ ยท 2)) = ๐‘‹))
3826, 37mpbid 231 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ ยท (๐‘˜ ยท 2)) = ๐‘‹)
3921, 23, 383eqtrrd 2782 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ = ((2 ยท ฯ€) ยท ๐‘˜))
40 fourierswlem.t . . . . . . . . . . . . . . . 16 ๐‘‡ = (2 ยท ฯ€)
4140a1i 11 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‡ = (2 ยท ฯ€))
4239, 41oveq12d 7380 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) = (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)))
4313, 15mulcld 11182 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) โˆˆ โ„‚)
44 2ne0 12264 . . . . . . . . . . . . . . . . . 18 2 โ‰  0
4544a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ 2 โ‰  0)
4635a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ฯ€ โ‰  0)
4713, 15, 45, 46mulne0d 11814 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) โ‰  0)
4816, 43, 47divcan3d 11943 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)) = ๐‘˜)
4948adantr 482 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)) = ๐‘˜)
5042, 49eqtrd 2777 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) = ๐‘˜)
51 simpl 484 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘˜ โˆˆ โ„ค)
5250, 51eqeltrd 2838 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
5352ex 414 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค))
5453a1i 11 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)))
5554rexlimdv 3151 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค))
5612, 55mpd 15 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
57 2re 12234 . . . . . . . . . . . 12 2 โˆˆ โ„
5857, 33remulcli 11178 . . . . . . . . . . 11 (2 ยท ฯ€) โˆˆ โ„
5940, 58eqeltri 2834 . . . . . . . . . 10 ๐‘‡ โˆˆ โ„
60 2pos 12263 . . . . . . . . . . . 12 0 < 2
6157, 33, 60, 34mulgt0ii 11295 . . . . . . . . . . 11 0 < (2 ยท ฯ€)
6261, 40breqtrri 5137 . . . . . . . . . 10 0 < ๐‘‡
6359, 62elrpii 12925 . . . . . . . . 9 ๐‘‡ โˆˆ โ„+
64 mod0 13788 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ ((๐‘‹ mod ๐‘‡) = 0 โ†” (๐‘‹ / ๐‘‡) โˆˆ โ„ค))
654, 63, 64mp2an 691 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†” (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
6656, 65sylibr 233 . . . . . . 7 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = 0)
6766orcd 872 . . . . . 6 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€))
68 odd2np1 16230 . . . . . . . . . 10 ((๐‘‹ / ฯ€) โˆˆ โ„ค โ†’ (ยฌ 2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)))
697, 68sylbi 216 . . . . . . . . 9 ((๐‘‹ mod ฯ€) = 0 โ†’ (ยฌ 2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)))
7069biimpa 478 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€))
7113, 16mulcld 11182 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ๐‘˜) โˆˆ โ„‚)
7271adantr 482 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (2 ยท ๐‘˜) โˆˆ โ„‚)
73 1cnd 11157 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ 1 โˆˆ โ„‚)
7414a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„‚)
7572, 73, 74adddird 11187 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)))
7613, 16mulcomd 11183 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ๐‘˜) = (๐‘˜ ยท 2))
7776oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) ยท ฯ€) = ((๐‘˜ ยท 2) ยท ฯ€))
7816, 13, 15mulassd 11185 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) ยท ฯ€) = (๐‘˜ ยท (2 ยท ฯ€)))
7940eqcomi 2746 . . . . . . . . . . . . . . . . . . . 20 (2 ยท ฯ€) = ๐‘‡
8079a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) = ๐‘‡)
8180oveq2d 7378 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ ยท (2 ยท ฯ€)) = (๐‘˜ ยท ๐‘‡))
8277, 78, 813eqtrd 2781 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) ยท ฯ€) = (๐‘˜ ยท ๐‘‡))
8314mulid2i 11167 . . . . . . . . . . . . . . . . . 18 (1 ยท ฯ€) = ฯ€
8483a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (1 ยท ฯ€) = ฯ€)
8582, 84oveq12d 7380 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)) = ((๐‘˜ ยท ๐‘‡) + ฯ€))
8685adantr 482 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)) = ((๐‘˜ ยท ๐‘‡) + ฯ€))
8740, 43eqeltrid 2842 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ๐‘‡ โˆˆ โ„‚)
8816, 87mulcld 11182 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ ยท ๐‘‡) โˆˆ โ„‚)
8988, 15addcomd 11364 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท ๐‘‡) + ฯ€) = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
9089adantr 482 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((๐‘˜ ยท ๐‘‡) + ฯ€) = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
9175, 86, 903eqtrrd 2782 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ + (๐‘˜ ยท ๐‘‡)) = (((2 ยท ๐‘˜) + 1) ยท ฯ€))
92 peano2cn 11334 . . . . . . . . . . . . . . . . 17 ((2 ยท ๐‘˜) โˆˆ โ„‚ โ†’ ((2 ยท ๐‘˜) + 1) โˆˆ โ„‚)
9371, 92syl 17 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) + 1) โˆˆ โ„‚)
9493, 15mulcomd 11183 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (ฯ€ ยท ((2 ยท ๐‘˜) + 1)))
9594adantr 482 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (ฯ€ ยท ((2 ยท ๐‘˜) + 1)))
96 id 22 . . . . . . . . . . . . . . . . 17 (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€))
9796eqcomd 2743 . . . . . . . . . . . . . . . 16 (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ฯ€) = ((2 ยท ๐‘˜) + 1))
9897adantl 483 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ฯ€) = ((2 ยท ๐‘˜) + 1))
9927a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ โˆˆ โ„‚)
10093adantr 482 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((2 ยท ๐‘˜) + 1) โˆˆ โ„‚)
10135a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โ‰  0)
10299, 74, 100, 101divmuld 11960 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ / ฯ€) = ((2 ยท ๐‘˜) + 1) โ†” (ฯ€ ยท ((2 ยท ๐‘˜) + 1)) = ๐‘‹))
10398, 102mpbid 231 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ ยท ((2 ยท ๐‘˜) + 1)) = ๐‘‹)
10491, 95, 1033eqtrrd 2782 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
105104oveq1d 7377 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡))
106 modcyc 13818 . . . . . . . . . . . . . 14 ((ฯ€ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+ โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
10733, 63, 106mp3an12 1452 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„ค โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
108107adantr 482 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
10933a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„)
11063a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ๐‘‡ โˆˆ โ„+)
111 0re 11164 . . . . . . . . . . . . . . 15 0 โˆˆ โ„
112111, 33, 34ltleii 11285 . . . . . . . . . . . . . 14 0 โ‰ค ฯ€
113112a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ 0 โ‰ค ฯ€)
114 2timesgt 43596 . . . . . . . . . . . . . . . 16 (ฯ€ โˆˆ โ„+ โ†’ ฯ€ < (2 ยท ฯ€))
1155, 114ax-mp 5 . . . . . . . . . . . . . . 15 ฯ€ < (2 ยท ฯ€)
116115, 40breqtrri 5137 . . . . . . . . . . . . . 14 ฯ€ < ๐‘‡
117116a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ < ๐‘‡)
118 modid 13808 . . . . . . . . . . . . 13 (((ฯ€ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โˆง (0 โ‰ค ฯ€ โˆง ฯ€ < ๐‘‡)) โ†’ (ฯ€ mod ๐‘‡) = ฯ€)
119109, 110, 113, 117, 118syl22anc 838 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ mod ๐‘‡) = ฯ€)
120105, 108, 1193eqtrd 2781 . . . . . . . . . . 11 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
121120ex 414 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€))
122121a1i 11 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)))
123122rexlimdv 3151 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€))
12470, 123mpd 15 . . . . . . 7 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
125124olcd 873 . . . . . 6 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€))
12667, 125pm2.61dan 812 . . . . 5 ((๐‘‹ mod ฯ€) = 0 โ†’ ((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€))
127 0xr 11209 . . . . . . . 8 0 โˆˆ โ„*
12833rexri 11220 . . . . . . . 8 ฯ€ โˆˆ โ„*
129 iocgtlb 43814 . . . . . . . 8 ((0 โˆˆ โ„* โˆง ฯ€ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€)) โ†’ 0 < (๐‘‹ mod ๐‘‡))
130127, 128, 129mp3an12 1452 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ 0 < (๐‘‹ mod ๐‘‡))
131130gt0ne0d 11726 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ (๐‘‹ mod ๐‘‡) โ‰  0)
132131neneqd 2949 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ ยฌ (๐‘‹ mod ๐‘‡) = 0)
133 pm2.53 850 . . . . . 6 (((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) = ฯ€))
134133imp 408 . . . . 5 ((((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
135126, 132, 134syl2anr 598 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
136127a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ 0 โˆˆ โ„*)
137128a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ ฯ€ โˆˆ โ„*)
138 modcl 13785 . . . . . . . . . . . . . . 15 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
1394, 63, 138mp2an 691 . . . . . . . . . . . . . 14 (๐‘‹ mod ๐‘‡) โˆˆ โ„
140139rexri 11220 . . . . . . . . . . . . 13 (๐‘‹ mod ๐‘‡) โˆˆ โ„*
141140a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„*)
142 id 22 . . . . . . . . . . . . 13 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
14334, 142breqtrrid 5148 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ 0 < (๐‘‹ mod ๐‘‡))
14433eqlei2 11273 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
145136, 137, 141, 143, 144eliocd 43819 . . . . . . . . . . 11 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
146145iftrued 4499 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = 1)
147146adantl 483 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = 1)
148 oveq1 7369 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘‹ โ†’ (๐‘ฅ mod ๐‘‡) = (๐‘‹ mod ๐‘‡))
149148breq1d 5120 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘‹ โ†’ ((๐‘ฅ mod ๐‘‡) < ฯ€ โ†” (๐‘‹ mod ๐‘‡) < ฯ€))
150149ifbid 4514 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘‹ โ†’ if((๐‘ฅ mod ๐‘‡) < ฯ€, 1, -1) = if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1))
151 fourierswlem.f . . . . . . . . . . . . 13 ๐น = (๐‘ฅ โˆˆ โ„ โ†ฆ if((๐‘ฅ mod ๐‘‡) < ฯ€, 1, -1))
152 1ex 11158 . . . . . . . . . . . . . 14 1 โˆˆ V
153 negex 11406 . . . . . . . . . . . . . 14 -1 โˆˆ V
154152, 153ifex 4541 . . . . . . . . . . . . 13 if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) โˆˆ V
155150, 151, 154fvmpt 6953 . . . . . . . . . . . 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 11298 . . . . . . . . . . . . 13 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โ‰  ฯ€)
160159necon2bi 2975 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ ยฌ (๐‘‹ mod ๐‘‡) < ฯ€)
161160iffalsed 4502 . . . . . . . . . . 11 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = -1)
162156, 161eqtrid 2789 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐นโ€˜๐‘‹) = -1)
163162adantl 483 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (๐นโ€˜๐‘‹) = -1)
164147, 163oveq12d 7380 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (1 + -1))
165 1pneg1e0 12279 . . . . . . . 8 (1 + -1) = 0
166164, 165eqtrdi 2793 . . . . . . 7 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = 0)
167166oveq1d 7377 . . . . . 6 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = (0 / 2))
168167adantll 713 . . . . 5 ((((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = (0 / 2))
169 2cn 12235 . . . . . . 7 2 โˆˆ โ„‚
170169, 44div0i 11896 . . . . . 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 4497 . . . . . . 7 ((๐‘‹ mod ฯ€) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = 0)
174172, 173eqtr2id 2790 . . . . . 6 ((๐‘‹ mod ฯ€) = 0 โ†’ 0 = ๐‘Œ)
175174ad2antlr 726 . . . . 5 ((((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ 0 = ๐‘Œ)
176168, 171, 1753eqtrrd 2782 . . . 4 ((((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
177135, 176mpdan 686 . . 3 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
178 iftrue 4497 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = 1)
179178adantr 482 . . . . . 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 43815 . . . . . . . . . 10 ((0 โˆˆ โ„* โˆง ฯ€ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
183127, 128, 182mp3an12 1452 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
184183adantr 482 . . . . . . . 8 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
185 ax-1cn 11116 . . . . . . . . . . . . . . . . . . . 20 1 โˆˆ โ„‚
186185, 14mulcomi 11170 . . . . . . . . . . . . . . . . . . 19 (1 ยท ฯ€) = (ฯ€ ยท 1)
18783, 186eqtr3i 2767 . . . . . . . . . . . . . . . . . 18 ฯ€ = (ฯ€ ยท 1)
188187oveq1i 7372 . . . . . . . . . . . . . . . . 17 (ฯ€ + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = ((ฯ€ ยท 1) + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
189169, 14mulcomi 11170 . . . . . . . . . . . . . . . . . . . . 21 (2 ยท ฯ€) = (ฯ€ ยท 2)
19040, 189eqtri 2765 . . . . . . . . . . . . . . . . . . . 20 ๐‘‡ = (ฯ€ ยท 2)
191190oveq1i 7372 . . . . . . . . . . . . . . . . . . 19 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = ((ฯ€ ยท 2) ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))
192111, 62gtneii 11274 . . . . . . . . . . . . . . . . . . . . . . 23 ๐‘‡ โ‰  0
1934, 59, 192redivcli 11929 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘‹ / ๐‘‡) โˆˆ โ„
194 flcl 13707 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘‹ / ๐‘‡) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค)
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค
196 zcn 12511 . . . . . . . . . . . . . . . . . . . . 21 ((โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค โ†’ (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„‚)
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„‚
19814, 169, 197mulassi 11173 . . . . . . . . . . . . . . . . . . 19 ((ฯ€ ยท 2) ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
199191, 198eqtri 2765 . . . . . . . . . . . . . . . . . 18 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
200199oveq2i 7373 . . . . . . . . . . . . . . . . 17 (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = (ฯ€ + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
201169, 197mulcli 11169 . . . . . . . . . . . . . . . . . 18 (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚
20214, 185, 201adddii 11174 . . . . . . . . . . . . . . . . 17 (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = ((ฯ€ ยท 1) + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
203188, 200, 2023eqtr4ri 2776 . . . . . . . . . . . . . . . 16 (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
204203a1i 11 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
205 id 22 . . . . . . . . . . . . . . . . 17 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ฯ€ = (๐‘‹ mod ๐‘‡))
206 modval 13783 . . . . . . . . . . . . . . . . . 18 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
2074, 63, 206mp2an 691 . . . . . . . . . . . . . . . . 17 (๐‘‹ mod ๐‘‡) = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
208205, 207eqtrdi 2793 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ฯ€ = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
209208oveq1d 7377 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = ((๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
21027a1i 11 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ๐‘‹ โˆˆ โ„‚)
21159recni 11176 . . . . . . . . . . . . . . . . . 18 ๐‘‡ โˆˆ โ„‚
212211, 197mulcli 11169 . . . . . . . . . . . . . . . . 17 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚
213212a1i 11 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚)
214210, 213npcand 11523 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ((๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = ๐‘‹)
215204, 209, 2143eqtrrd 2782 . . . . . . . . . . . . . 14 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ๐‘‹ = (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))))
216215oveq1d 7377 . . . . . . . . . . . . 13 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) = ((ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) / ฯ€))
217185, 201addcli 11168 . . . . . . . . . . . . . 14 (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„‚
218217, 14, 35divcan3i 11908 . . . . . . . . . . . . 13 ((ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) / ฯ€) = (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
219216, 218eqtrdi 2793 . . . . . . . . . . . 12 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) = (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
220 1z 12540 . . . . . . . . . . . . . 14 1 โˆˆ โ„ค
221 zmulcl 12559 . . . . . . . . . . . . . . 15 ((2 โˆˆ โ„ค โˆง (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค) โ†’ (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค)
2222, 195, 221mp2an 691 . . . . . . . . . . . . . 14 (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค
223 zaddcl 12550 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค) โ†’ (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค)
224220, 222, 223mp2an 691 . . . . . . . . . . . . 13 (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค
225224a1i 11 . . . . . . . . . . . 12 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค)
226219, 225eqeltrd 2838 . . . . . . . . . . 11 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
227226, 7sylibr 233 . . . . . . . . . 10 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ mod ฯ€) = 0)
228227necon3bi 2971 . . . . . . . . 9 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ ฯ€ โ‰  (๐‘‹ mod ๐‘‡))
229228adantl 483 . . . . . . . 8 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ฯ€ โ‰  (๐‘‹ mod ๐‘‡))
230180, 181, 184, 229leneltd 11316 . . . . . . 7 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) < ฯ€)
231 iftrue 4497 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = 1)
232156, 231eqtrid 2789 . . . . . . 7 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ (๐นโ€˜๐‘‹) = 1)
233230, 232syl 17 . . . . . 6 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐นโ€˜๐‘‹) = 1)
234179, 233oveq12d 7380 . . . . 5 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (1 + 1))
235234oveq1d 7377 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((1 + 1) / 2))
236 1p1e2 12285 . . . . . . 7 (1 + 1) = 2
237236oveq1i 7372 . . . . . 6 ((1 + 1) / 2) = (2 / 2)
238 2div2e1 12301 . . . . . 6 (2 / 2) = 1
239237, 238eqtr2i 2766 . . . . 5 1 = ((1 + 1) / 2)
240233, 239eqtr2di 2794 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ((1 + 1) / 2) = (๐นโ€˜๐‘‹))
241 iffalse 4500 . . . . . 6 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = (๐นโ€˜๐‘‹))
242172, 241eqtr2id 2790 . . . . 5 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
243242adantl 483 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
244235, 240, 2433eqtrrd 2782 . . 3 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
245177, 244pm2.61dan 812 . 2 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
246131necon2bi 2975 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
247246iffalsed 4502 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = -1)
248 id 22 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) = 0)
249248, 34eqbrtrdi 5149 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) < ฯ€)
250249iftrued 4499 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = 1)
251156, 250eqtrid 2789 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐นโ€˜๐‘‹) = 1)
252247, 251oveq12d 7380 . . . . . 6 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (-1 + 1))
253252oveq1d 7377 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((-1 + 1) / 2))
254 neg1cn 12274 . . . . . . . . 9 -1 โˆˆ โ„‚
255185, 254, 165addcomli 11354 . . . . . . . 8 (-1 + 1) = 0
256255oveq1i 7372 . . . . . . 7 ((-1 + 1) / 2) = (0 / 2)
257256, 170eqtri 2765 . . . . . 6 ((-1 + 1) / 2) = 0
258257a1i 11 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ((-1 + 1) / 2) = 0)
25940oveq2i 7373 . . . . . . . . . . . . 13 (๐‘‹ / ๐‘‡) = (๐‘‹ / (2 ยท ฯ€))
260 2cnne0 12370 . . . . . . . . . . . . . 14 (2 โˆˆ โ„‚ โˆง 2 โ‰  0)
26114, 35pm3.2i 472 . . . . . . . . . . . . . 14 (ฯ€ โˆˆ โ„‚ โˆง ฯ€ โ‰  0)
262 divdiv1 11873 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0) โˆง (ฯ€ โˆˆ โ„‚ โˆง ฯ€ โ‰  0)) โ†’ ((๐‘‹ / 2) / ฯ€) = (๐‘‹ / (2 ยท ฯ€)))
26327, 260, 261, 262mp3an 1462 . . . . . . . . . . . . 13 ((๐‘‹ / 2) / ฯ€) = (๐‘‹ / (2 ยท ฯ€))
26427, 169, 14, 44, 35divdiv32i 11917 . . . . . . . . . . . . 13 ((๐‘‹ / 2) / ฯ€) = ((๐‘‹ / ฯ€) / 2)
265259, 263, 2643eqtr2i 2771 . . . . . . . . . . . 12 (๐‘‹ / ๐‘‡) = ((๐‘‹ / ฯ€) / 2)
266265oveq2i 7373 . . . . . . . . . . 11 (2 ยท (๐‘‹ / ๐‘‡)) = (2 ยท ((๐‘‹ / ฯ€) / 2))
26727, 14, 35divcli 11904 . . . . . . . . . . . 12 (๐‘‹ / ฯ€) โˆˆ โ„‚
268267, 169, 44divcan2i 11905 . . . . . . . . . . 11 (2 ยท ((๐‘‹ / ฯ€) / 2)) = (๐‘‹ / ฯ€)
269266, 268eqtr2i 2766 . . . . . . . . . 10 (๐‘‹ / ฯ€) = (2 ยท (๐‘‹ / ๐‘‡))
2702a1i 11 . . . . . . . . . . 11 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ 2 โˆˆ โ„ค)
271 id 22 . . . . . . . . . . 11 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
272270, 271zmulcld 12620 . . . . . . . . . 10 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (2 ยท (๐‘‹ / ๐‘‡)) โˆˆ โ„ค)
273269, 272eqeltrid 2842 . . . . . . . . 9 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
27465, 273sylbi 216 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
275274, 7sylibr 233 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ฯ€) = 0)
276275iftrued 4499 . . . . . 6 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = 0)
277172, 276eqtr2id 2790 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ 0 = ๐‘Œ)
278253, 258, 2773eqtrrd 2782 . . . 4 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
279278adantl 483 . . 3 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ๐‘‡) = 0) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
280128a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ฯ€ โˆˆ โ„*)
28159rexri 11220 . . . . . 6 ๐‘‡ โˆˆ โ„*
282281a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ๐‘‡ โˆˆ โ„*)
283139a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
284 pm4.56 988 . . . . . . . 8 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†” ยฌ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
285284biimpi 215 . . . . . . 7 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ยฌ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
286 olc 867 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
287286adantl 483 . . . . . . . 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 11165 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 โˆˆ โ„)
292139a1i 11 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
293 modge0 13791 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ 0 โ‰ค (๐‘‹ mod ๐‘‡))
2944, 63, 293mp2an 691 . . . . . . . . . . . . 13 0 โ‰ค (๐‘‹ mod ๐‘‡)
295294a1i 11 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 โ‰ค (๐‘‹ mod ๐‘‡))
296 neqne 2952 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โ‰  0)
297291, 292, 295, 296leneltd 11316 . . . . . . . . . . 11 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 < (๐‘‹ mod ๐‘‡))
298297adantl 483 . . . . . . . . . 10 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ 0 < (๐‘‹ mod ๐‘‡))
299 simpl 484 . . . . . . . . . 10 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
300288, 289, 290, 298, 299eliocd 43819 . . . . . . . . 9 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
301300orcd 872 . . . . . . . 8 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
302287, 301pm2.61dan 812 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โ†’ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
303285, 302nsyl 140 . . . . . 6 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
30433a1i 11 . . . . . . 7 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ฯ€ โˆˆ โ„)
305304, 283ltnled 11309 . . . . . 6 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (ฯ€ < (๐‘‹ mod ๐‘‡) โ†” ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€))
306303, 305mpbird 257 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
307 modlt 13792 . . . . . . 7 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) < ๐‘‡)
3084, 63, 307mp2an 691 . . . . . 6 (๐‘‹ mod ๐‘‡) < ๐‘‡
309308a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) < ๐‘‡)
310280, 282, 283, 306, 309eliood 43810 . . . 4 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡))
311127a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ 0 โˆˆ โ„*)
31233a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ฯ€ โˆˆ โ„)
313140a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„*)
314 ioogtlb 43807 . . . . . . . . . 10 ((ฯ€ โˆˆ โ„* โˆง ๐‘‡ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡)) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
315128, 281, 314mp3an12 1452 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
316311, 312, 313, 315gtnelioc 43803 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
317316iffalsed 4502 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = -1)
318139a1i 11 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
319312, 318, 315ltnsymd 11311 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) < ฯ€)
320319iffalsed 4502 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = -1)
321156, 320eqtrid 2789 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐นโ€˜๐‘‹) = -1)
322317, 321oveq12d 7380 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (-1 + -1))
323322oveq1d 7377 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((-1 + -1) / 2))
324 df-2 12223 . . . . . . . . . 10 2 = (1 + 1)
325324negeqi 11401 . . . . . . . . 9 -2 = -(1 + 1)
326185, 185negdii 11492 . . . . . . . . 9 -(1 + 1) = (-1 + -1)
327325, 326eqtr2i 2766 . . . . . . . 8 (-1 + -1) = -2
328327oveq1i 7372 . . . . . . 7 ((-1 + -1) / 2) = (-2 / 2)
329 divneg 11854 . . . . . . . 8 ((2 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง 2 โ‰  0) โ†’ -(2 / 2) = (-2 / 2))
330169, 169, 44, 329mp3an 1462 . . . . . . 7 -(2 / 2) = (-2 / 2)
331238negeqi 11401 . . . . . . 7 -(2 / 2) = -1
332328, 330, 3313eqtr2i 2771 . . . . . 6 ((-1 + -1) / 2) = -1
333332a1i 11 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ((-1 + -1) / 2) = -1)
334172a1i 11 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ๐‘Œ = if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)))
335312, 318ltnled 11309 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (ฯ€ < (๐‘‹ mod ๐‘‡) โ†” ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€))
336315, 335mpbid 231 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
337248, 112eqbrtrdi 5149 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
338337adantl 483 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
339126orcanai 1002 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
340339, 144syl 17 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
341338, 340pm2.61dan 812 . . . . . . . 8 ((๐‘‹ mod ฯ€) = 0 โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
342336, 341nsyl 140 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ฯ€) = 0)
343342iffalsed 4502 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = (๐นโ€˜๐‘‹))
344334, 343, 3213eqtrrd 2782 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ -1 = ๐‘Œ)
345323, 333, 3443eqtrrd 2782 . . . 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 812 . 2 (ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
348245, 347pm2.61i 182 1 ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆƒwrex 3074  ifcif 4491   class class class wbr 5110   โ†ฆ cmpt 5193  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063  โ„*cxr 11195   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392  -cneg 11393   / cdiv 11819  2c2 12215  โ„คcz 12506  โ„+crp 12922  (,)cioo 13271  (,]cioc 13272  โŒŠcfl 13702   mod cmo 13781  ฯ€cpi 15956   โˆฅ cdvds 16143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-pi 15962  df-dvds 16144  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247
This theorem is referenced by:  fouriersw  44546
  Copyright terms: Public domain W3C validator