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 45677
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 483 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ 2 โˆฅ (๐‘‹ / ฯ€))
2 2z 12619 . . . . . . . . . . . 12 2 โˆˆ โ„ค
32a1i 11 . . . . . . . . . . 11 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ 2 โˆˆ โ„ค)
4 fourierswlem.x . . . . . . . . . . . . . 14 ๐‘‹ โˆˆ โ„
5 pirp 26409 . . . . . . . . . . . . . 14 ฯ€ โˆˆ โ„+
6 mod0 13868 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„ โˆง ฯ€ โˆˆ โ„+) โ†’ ((๐‘‹ mod ฯ€) = 0 โ†” (๐‘‹ / ฯ€) โˆˆ โ„ค))
74, 5, 6mp2an 690 . . . . . . . . . . . . 13 ((๐‘‹ mod ฯ€) = 0 โ†” (๐‘‹ / ฯ€) โˆˆ โ„ค)
87biimpi 215 . . . . . . . . . . . 12 ((๐‘‹ mod ฯ€) = 0 โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
98adantr 479 . . . . . . . . . . 11 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
10 divides 16227 . . . . . . . . . . 11 ((2 โˆˆ โ„ค โˆง (๐‘‹ / ฯ€) โˆˆ โ„ค) โ†’ (2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)))
113, 9, 10syl2anc 582 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)))
121, 11mpbid 231 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€))
13 2cnd 12315 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ 2 โˆˆ โ„‚)
14 picn 26407 . . . . . . . . . . . . . . . . . . . 20 ฯ€ โˆˆ โ„‚
1514a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ ฯ€ โˆˆ โ„‚)
16 zcn 12588 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ ๐‘˜ โˆˆ โ„‚)
1713, 15, 16mulassd 11262 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = (2 ยท (ฯ€ ยท ๐‘˜)))
1815, 16mulcld 11259 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (ฯ€ ยท ๐‘˜) โˆˆ โ„‚)
1913, 18mulcomd 11260 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท (ฯ€ ยท ๐‘˜)) = ((ฯ€ ยท ๐‘˜) ยท 2))
2017, 19eqtrd 2765 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = ((ฯ€ ยท ๐‘˜) ยท 2))
2120adantr 479 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = ((ฯ€ ยท ๐‘˜) ยท 2))
2215, 16, 13mulassd 11262 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((ฯ€ ยท ๐‘˜) ยท 2) = (ฯ€ ยท (๐‘˜ ยท 2)))
2322adantr 479 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((ฯ€ ยท ๐‘˜) ยท 2) = (ฯ€ ยท (๐‘˜ ยท 2)))
24 id 22 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘˜ ยท 2) = (๐‘‹ / ฯ€))
2524eqcomd 2731 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ฯ€) = (๐‘˜ ยท 2))
2625adantl 480 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ฯ€) = (๐‘˜ ยท 2))
274recni 11253 . . . . . . . . . . . . . . . . . . 19 ๐‘‹ โˆˆ โ„‚
2827a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ โˆˆ โ„‚)
2914a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„‚)
3016adantr 479 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘˜ โˆˆ โ„‚)
31 2cnd 12315 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ 2 โˆˆ โ„‚)
3230, 31mulcld 11259 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘˜ ยท 2) โˆˆ โ„‚)
33 pire 26406 . . . . . . . . . . . . . . . . . . . 20 ฯ€ โˆˆ โ„
34 pipos 26408 . . . . . . . . . . . . . . . . . . . 20 0 < ฯ€
3533, 34gt0ne0ii 11775 . . . . . . . . . . . . . . . . . . 19 ฯ€ โ‰  0
3635a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โ‰  0)
3728, 29, 32, 36divmuld 12037 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ / ฯ€) = (๐‘˜ ยท 2) โ†” (ฯ€ ยท (๐‘˜ ยท 2)) = ๐‘‹))
3826, 37mpbid 231 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ ยท (๐‘˜ ยท 2)) = ๐‘‹)
3921, 23, 383eqtrrd 2770 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ = ((2 ยท ฯ€) ยท ๐‘˜))
40 fourierswlem.t . . . . . . . . . . . . . . . 16 ๐‘‡ = (2 ยท ฯ€)
4140a1i 11 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‡ = (2 ยท ฯ€))
4239, 41oveq12d 7431 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) = (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)))
4313, 15mulcld 11259 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) โˆˆ โ„‚)
44 2ne0 12341 . . . . . . . . . . . . . . . . . 18 2 โ‰  0
4544a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ 2 โ‰  0)
4635a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ฯ€ โ‰  0)
4713, 15, 45, 46mulne0d 11891 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) โ‰  0)
4816, 43, 47divcan3d 12020 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)) = ๐‘˜)
4948adantr 479 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)) = ๐‘˜)
5042, 49eqtrd 2765 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) = ๐‘˜)
51 simpl 481 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘˜ โˆˆ โ„ค)
5250, 51eqeltrd 2825 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
5352ex 411 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค))
5453a1i 11 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)))
5554rexlimdv 3143 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค))
5612, 55mpd 15 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
57 2re 12311 . . . . . . . . . . . 12 2 โˆˆ โ„
5857, 33remulcli 11255 . . . . . . . . . . 11 (2 ยท ฯ€) โˆˆ โ„
5940, 58eqeltri 2821 . . . . . . . . . 10 ๐‘‡ โˆˆ โ„
60 2pos 12340 . . . . . . . . . . . 12 0 < 2
6157, 33, 60, 34mulgt0ii 11372 . . . . . . . . . . 11 0 < (2 ยท ฯ€)
6261, 40breqtrri 5171 . . . . . . . . . 10 0 < ๐‘‡
6359, 62elrpii 13004 . . . . . . . . 9 ๐‘‡ โˆˆ โ„+
64 mod0 13868 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ ((๐‘‹ mod ๐‘‡) = 0 โ†” (๐‘‹ / ๐‘‡) โˆˆ โ„ค))
654, 63, 64mp2an 690 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†” (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
6656, 65sylibr 233 . . . . . . 7 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = 0)
6766orcd 871 . . . . . 6 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€))
68 odd2np1 16312 . . . . . . . . . 10 ((๐‘‹ / ฯ€) โˆˆ โ„ค โ†’ (ยฌ 2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)))
697, 68sylbi 216 . . . . . . . . 9 ((๐‘‹ mod ฯ€) = 0 โ†’ (ยฌ 2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)))
7069biimpa 475 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€))
7113, 16mulcld 11259 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ๐‘˜) โˆˆ โ„‚)
7271adantr 479 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (2 ยท ๐‘˜) โˆˆ โ„‚)
73 1cnd 11234 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ 1 โˆˆ โ„‚)
7414a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„‚)
7572, 73, 74adddird 11264 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)))
7613, 16mulcomd 11260 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ๐‘˜) = (๐‘˜ ยท 2))
7776oveq1d 7428 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) ยท ฯ€) = ((๐‘˜ ยท 2) ยท ฯ€))
7816, 13, 15mulassd 11262 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) ยท ฯ€) = (๐‘˜ ยท (2 ยท ฯ€)))
7940eqcomi 2734 . . . . . . . . . . . . . . . . . . . 20 (2 ยท ฯ€) = ๐‘‡
8079a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) = ๐‘‡)
8180oveq2d 7429 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ ยท (2 ยท ฯ€)) = (๐‘˜ ยท ๐‘‡))
8277, 78, 813eqtrd 2769 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) ยท ฯ€) = (๐‘˜ ยท ๐‘‡))
8314mullidi 11244 . . . . . . . . . . . . . . . . . 18 (1 ยท ฯ€) = ฯ€
8483a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (1 ยท ฯ€) = ฯ€)
8582, 84oveq12d 7431 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)) = ((๐‘˜ ยท ๐‘‡) + ฯ€))
8685adantr 479 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)) = ((๐‘˜ ยท ๐‘‡) + ฯ€))
8740, 43eqeltrid 2829 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ๐‘‡ โˆˆ โ„‚)
8816, 87mulcld 11259 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ ยท ๐‘‡) โˆˆ โ„‚)
8988, 15addcomd 11441 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท ๐‘‡) + ฯ€) = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
9089adantr 479 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((๐‘˜ ยท ๐‘‡) + ฯ€) = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
9175, 86, 903eqtrrd 2770 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ + (๐‘˜ ยท ๐‘‡)) = (((2 ยท ๐‘˜) + 1) ยท ฯ€))
92 peano2cn 11411 . . . . . . . . . . . . . . . . 17 ((2 ยท ๐‘˜) โˆˆ โ„‚ โ†’ ((2 ยท ๐‘˜) + 1) โˆˆ โ„‚)
9371, 92syl 17 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) + 1) โˆˆ โ„‚)
9493, 15mulcomd 11260 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (ฯ€ ยท ((2 ยท ๐‘˜) + 1)))
9594adantr 479 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (ฯ€ ยท ((2 ยท ๐‘˜) + 1)))
96 id 22 . . . . . . . . . . . . . . . . 17 (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€))
9796eqcomd 2731 . . . . . . . . . . . . . . . 16 (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ฯ€) = ((2 ยท ๐‘˜) + 1))
9897adantl 480 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ฯ€) = ((2 ยท ๐‘˜) + 1))
9927a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ โˆˆ โ„‚)
10093adantr 479 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((2 ยท ๐‘˜) + 1) โˆˆ โ„‚)
10135a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โ‰  0)
10299, 74, 100, 101divmuld 12037 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ / ฯ€) = ((2 ยท ๐‘˜) + 1) โ†” (ฯ€ ยท ((2 ยท ๐‘˜) + 1)) = ๐‘‹))
10398, 102mpbid 231 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ ยท ((2 ยท ๐‘˜) + 1)) = ๐‘‹)
10491, 95, 1033eqtrrd 2770 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
105104oveq1d 7428 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡))
106 modcyc 13898 . . . . . . . . . . . . . 14 ((ฯ€ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+ โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
10733, 63, 106mp3an12 1447 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„ค โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
108107adantr 479 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
10933a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„)
11063a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ๐‘‡ โˆˆ โ„+)
111 0re 11241 . . . . . . . . . . . . . . 15 0 โˆˆ โ„
112111, 33, 34ltleii 11362 . . . . . . . . . . . . . 14 0 โ‰ค ฯ€
113112a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ 0 โ‰ค ฯ€)
114 2timesgt 44729 . . . . . . . . . . . . . . . 16 (ฯ€ โˆˆ โ„+ โ†’ ฯ€ < (2 ยท ฯ€))
1155, 114ax-mp 5 . . . . . . . . . . . . . . 15 ฯ€ < (2 ยท ฯ€)
116115, 40breqtrri 5171 . . . . . . . . . . . . . 14 ฯ€ < ๐‘‡
117116a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ < ๐‘‡)
118 modid 13888 . . . . . . . . . . . . 13 (((ฯ€ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โˆง (0 โ‰ค ฯ€ โˆง ฯ€ < ๐‘‡)) โ†’ (ฯ€ mod ๐‘‡) = ฯ€)
119109, 110, 113, 117, 118syl22anc 837 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ mod ๐‘‡) = ฯ€)
120105, 108, 1193eqtrd 2769 . . . . . . . . . . 11 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
121120ex 411 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€))
122121a1i 11 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)))
123122rexlimdv 3143 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€))
12470, 123mpd 15 . . . . . . 7 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
125124olcd 872 . . . . . 6 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€))
12667, 125pm2.61dan 811 . . . . 5 ((๐‘‹ mod ฯ€) = 0 โ†’ ((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€))
127 0xr 11286 . . . . . . . 8 0 โˆˆ โ„*
12833rexri 11297 . . . . . . . 8 ฯ€ โˆˆ โ„*
129 iocgtlb 44946 . . . . . . . 8 ((0 โˆˆ โ„* โˆง ฯ€ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€)) โ†’ 0 < (๐‘‹ mod ๐‘‡))
130127, 128, 129mp3an12 1447 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ 0 < (๐‘‹ mod ๐‘‡))
131130gt0ne0d 11803 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ (๐‘‹ mod ๐‘‡) โ‰  0)
132131neneqd 2935 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ ยฌ (๐‘‹ mod ๐‘‡) = 0)
133 pm2.53 849 . . . . . 6 (((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) = ฯ€))
134133imp 405 . . . . 5 ((((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
135126, 132, 134syl2anr 595 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
136127a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ 0 โˆˆ โ„*)
137128a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ ฯ€ โˆˆ โ„*)
138 modcl 13865 . . . . . . . . . . . . . . 15 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
1394, 63, 138mp2an 690 . . . . . . . . . . . . . 14 (๐‘‹ mod ๐‘‡) โˆˆ โ„
140139rexri 11297 . . . . . . . . . . . . 13 (๐‘‹ mod ๐‘‡) โˆˆ โ„*
141140a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„*)
142 id 22 . . . . . . . . . . . . 13 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
14334, 142breqtrrid 5182 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ 0 < (๐‘‹ mod ๐‘‡))
14433eqlei2 11350 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
145136, 137, 141, 143, 144eliocd 44951 . . . . . . . . . . 11 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
146145iftrued 4533 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = 1)
147146adantl 480 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = 1)
148 oveq1 7420 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘‹ โ†’ (๐‘ฅ mod ๐‘‡) = (๐‘‹ mod ๐‘‡))
149148breq1d 5154 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘‹ โ†’ ((๐‘ฅ mod ๐‘‡) < ฯ€ โ†” (๐‘‹ mod ๐‘‡) < ฯ€))
150149ifbid 4548 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘‹ โ†’ if((๐‘ฅ mod ๐‘‡) < ฯ€, 1, -1) = if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1))
151 fourierswlem.f . . . . . . . . . . . . 13 ๐น = (๐‘ฅ โˆˆ โ„ โ†ฆ if((๐‘ฅ mod ๐‘‡) < ฯ€, 1, -1))
152 1ex 11235 . . . . . . . . . . . . . 14 1 โˆˆ V
153 negex 11483 . . . . . . . . . . . . . 14 -1 โˆˆ V
154152, 153ifex 4575 . . . . . . . . . . . . 13 if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) โˆˆ V
155150, 151, 154fvmpt 6998 . . . . . . . . . . . 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 11375 . . . . . . . . . . . . 13 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โ‰  ฯ€)
160159necon2bi 2961 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ ยฌ (๐‘‹ mod ๐‘‡) < ฯ€)
161160iffalsed 4536 . . . . . . . . . . 11 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = -1)
162156, 161eqtrid 2777 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐นโ€˜๐‘‹) = -1)
163162adantl 480 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (๐นโ€˜๐‘‹) = -1)
164147, 163oveq12d 7431 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (1 + -1))
165 1pneg1e0 12356 . . . . . . . 8 (1 + -1) = 0
166164, 165eqtrdi 2781 . . . . . . 7 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = 0)
167166oveq1d 7428 . . . . . 6 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = (0 / 2))
168167adantll 712 . . . . 5 ((((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = (0 / 2))
169 2cn 12312 . . . . . . 7 2 โˆˆ โ„‚
170169, 44div0i 11973 . . . . . 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 4531 . . . . . . 7 ((๐‘‹ mod ฯ€) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = 0)
174172, 173eqtr2id 2778 . . . . . 6 ((๐‘‹ mod ฯ€) = 0 โ†’ 0 = ๐‘Œ)
175174ad2antlr 725 . . . . 5 ((((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ 0 = ๐‘Œ)
176168, 171, 1753eqtrrd 2770 . . . 4 ((((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
177135, 176mpdan 685 . . 3 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
178 iftrue 4531 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = 1)
179178adantr 479 . . . . . 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 44947 . . . . . . . . . 10 ((0 โˆˆ โ„* โˆง ฯ€ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
183127, 128, 182mp3an12 1447 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
184183adantr 479 . . . . . . . 8 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
185 ax-1cn 11191 . . . . . . . . . . . . . . . . . . . 20 1 โˆˆ โ„‚
186185, 14mulcomi 11247 . . . . . . . . . . . . . . . . . . 19 (1 ยท ฯ€) = (ฯ€ ยท 1)
18783, 186eqtr3i 2755 . . . . . . . . . . . . . . . . . 18 ฯ€ = (ฯ€ ยท 1)
188187oveq1i 7423 . . . . . . . . . . . . . . . . 17 (ฯ€ + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = ((ฯ€ ยท 1) + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
189169, 14mulcomi 11247 . . . . . . . . . . . . . . . . . . . . 21 (2 ยท ฯ€) = (ฯ€ ยท 2)
19040, 189eqtri 2753 . . . . . . . . . . . . . . . . . . . 20 ๐‘‡ = (ฯ€ ยท 2)
191190oveq1i 7423 . . . . . . . . . . . . . . . . . . 19 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = ((ฯ€ ยท 2) ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))
192111, 62gtneii 11351 . . . . . . . . . . . . . . . . . . . . . . 23 ๐‘‡ โ‰  0
1934, 59, 192redivcli 12006 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘‹ / ๐‘‡) โˆˆ โ„
194 flcl 13787 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘‹ / ๐‘‡) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค)
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค
196 zcn 12588 . . . . . . . . . . . . . . . . . . . . 21 ((โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค โ†’ (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„‚)
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„‚
19814, 169, 197mulassi 11250 . . . . . . . . . . . . . . . . . . 19 ((ฯ€ ยท 2) ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
199191, 198eqtri 2753 . . . . . . . . . . . . . . . . . 18 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
200199oveq2i 7424 . . . . . . . . . . . . . . . . 17 (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = (ฯ€ + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
201169, 197mulcli 11246 . . . . . . . . . . . . . . . . . 18 (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚
20214, 185, 201adddii 11251 . . . . . . . . . . . . . . . . 17 (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = ((ฯ€ ยท 1) + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
203188, 200, 2023eqtr4ri 2764 . . . . . . . . . . . . . . . 16 (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
204203a1i 11 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
205 id 22 . . . . . . . . . . . . . . . . 17 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ฯ€ = (๐‘‹ mod ๐‘‡))
206 modval 13863 . . . . . . . . . . . . . . . . . 18 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
2074, 63, 206mp2an 690 . . . . . . . . . . . . . . . . 17 (๐‘‹ mod ๐‘‡) = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
208205, 207eqtrdi 2781 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ฯ€ = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
209208oveq1d 7428 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = ((๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
21027a1i 11 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ๐‘‹ โˆˆ โ„‚)
21159recni 11253 . . . . . . . . . . . . . . . . . 18 ๐‘‡ โˆˆ โ„‚
212211, 197mulcli 11246 . . . . . . . . . . . . . . . . 17 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚
213212a1i 11 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚)
214210, 213npcand 11600 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ((๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = ๐‘‹)
215204, 209, 2143eqtrrd 2770 . . . . . . . . . . . . . 14 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ๐‘‹ = (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))))
216215oveq1d 7428 . . . . . . . . . . . . 13 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) = ((ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) / ฯ€))
217185, 201addcli 11245 . . . . . . . . . . . . . 14 (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„‚
218217, 14, 35divcan3i 11985 . . . . . . . . . . . . 13 ((ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) / ฯ€) = (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
219216, 218eqtrdi 2781 . . . . . . . . . . . 12 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) = (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
220 1z 12617 . . . . . . . . . . . . . 14 1 โˆˆ โ„ค
221 zmulcl 12636 . . . . . . . . . . . . . . 15 ((2 โˆˆ โ„ค โˆง (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค) โ†’ (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค)
2222, 195, 221mp2an 690 . . . . . . . . . . . . . 14 (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค
223 zaddcl 12627 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค) โ†’ (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค)
224220, 222, 223mp2an 690 . . . . . . . . . . . . 13 (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค
225224a1i 11 . . . . . . . . . . . 12 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค)
226219, 225eqeltrd 2825 . . . . . . . . . . 11 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
227226, 7sylibr 233 . . . . . . . . . 10 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ mod ฯ€) = 0)
228227necon3bi 2957 . . . . . . . . 9 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ ฯ€ โ‰  (๐‘‹ mod ๐‘‡))
229228adantl 480 . . . . . . . 8 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ฯ€ โ‰  (๐‘‹ mod ๐‘‡))
230180, 181, 184, 229leneltd 11393 . . . . . . 7 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) < ฯ€)
231 iftrue 4531 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = 1)
232156, 231eqtrid 2777 . . . . . . 7 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ (๐นโ€˜๐‘‹) = 1)
233230, 232syl 17 . . . . . 6 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐นโ€˜๐‘‹) = 1)
234179, 233oveq12d 7431 . . . . 5 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (1 + 1))
235234oveq1d 7428 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((1 + 1) / 2))
236 1p1e2 12362 . . . . . . 7 (1 + 1) = 2
237236oveq1i 7423 . . . . . 6 ((1 + 1) / 2) = (2 / 2)
238 2div2e1 12378 . . . . . 6 (2 / 2) = 1
239237, 238eqtr2i 2754 . . . . 5 1 = ((1 + 1) / 2)
240233, 239eqtr2di 2782 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ((1 + 1) / 2) = (๐นโ€˜๐‘‹))
241 iffalse 4534 . . . . . 6 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = (๐นโ€˜๐‘‹))
242172, 241eqtr2id 2778 . . . . 5 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
243242adantl 480 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
244235, 240, 2433eqtrrd 2770 . . 3 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
245177, 244pm2.61dan 811 . 2 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
246131necon2bi 2961 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
247246iffalsed 4536 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = -1)
248 id 22 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) = 0)
249248, 34eqbrtrdi 5183 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) < ฯ€)
250249iftrued 4533 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = 1)
251156, 250eqtrid 2777 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐นโ€˜๐‘‹) = 1)
252247, 251oveq12d 7431 . . . . . 6 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (-1 + 1))
253252oveq1d 7428 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((-1 + 1) / 2))
254 neg1cn 12351 . . . . . . . . 9 -1 โˆˆ โ„‚
255185, 254, 165addcomli 11431 . . . . . . . 8 (-1 + 1) = 0
256255oveq1i 7423 . . . . . . 7 ((-1 + 1) / 2) = (0 / 2)
257256, 170eqtri 2753 . . . . . 6 ((-1 + 1) / 2) = 0
258257a1i 11 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ((-1 + 1) / 2) = 0)
25940oveq2i 7424 . . . . . . . . . . . . 13 (๐‘‹ / ๐‘‡) = (๐‘‹ / (2 ยท ฯ€))
260 2cnne0 12447 . . . . . . . . . . . . . 14 (2 โˆˆ โ„‚ โˆง 2 โ‰  0)
26114, 35pm3.2i 469 . . . . . . . . . . . . . 14 (ฯ€ โˆˆ โ„‚ โˆง ฯ€ โ‰  0)
262 divdiv1 11950 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0) โˆง (ฯ€ โˆˆ โ„‚ โˆง ฯ€ โ‰  0)) โ†’ ((๐‘‹ / 2) / ฯ€) = (๐‘‹ / (2 ยท ฯ€)))
26327, 260, 261, 262mp3an 1457 . . . . . . . . . . . . 13 ((๐‘‹ / 2) / ฯ€) = (๐‘‹ / (2 ยท ฯ€))
26427, 169, 14, 44, 35divdiv32i 11994 . . . . . . . . . . . . 13 ((๐‘‹ / 2) / ฯ€) = ((๐‘‹ / ฯ€) / 2)
265259, 263, 2643eqtr2i 2759 . . . . . . . . . . . 12 (๐‘‹ / ๐‘‡) = ((๐‘‹ / ฯ€) / 2)
266265oveq2i 7424 . . . . . . . . . . 11 (2 ยท (๐‘‹ / ๐‘‡)) = (2 ยท ((๐‘‹ / ฯ€) / 2))
26727, 14, 35divcli 11981 . . . . . . . . . . . 12 (๐‘‹ / ฯ€) โˆˆ โ„‚
268267, 169, 44divcan2i 11982 . . . . . . . . . . 11 (2 ยท ((๐‘‹ / ฯ€) / 2)) = (๐‘‹ / ฯ€)
269266, 268eqtr2i 2754 . . . . . . . . . 10 (๐‘‹ / ฯ€) = (2 ยท (๐‘‹ / ๐‘‡))
2702a1i 11 . . . . . . . . . . 11 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ 2 โˆˆ โ„ค)
271 id 22 . . . . . . . . . . 11 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
272270, 271zmulcld 12697 . . . . . . . . . 10 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (2 ยท (๐‘‹ / ๐‘‡)) โˆˆ โ„ค)
273269, 272eqeltrid 2829 . . . . . . . . 9 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
27465, 273sylbi 216 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
275274, 7sylibr 233 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ฯ€) = 0)
276275iftrued 4533 . . . . . 6 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = 0)
277172, 276eqtr2id 2778 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ 0 = ๐‘Œ)
278253, 258, 2773eqtrrd 2770 . . . 4 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
279278adantl 480 . . 3 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ๐‘‡) = 0) โ†’ ๐‘Œ = ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2))
280128a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ฯ€ โˆˆ โ„*)
28159rexri 11297 . . . . . 6 ๐‘‡ โˆˆ โ„*
282281a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ๐‘‡ โˆˆ โ„*)
283139a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
284 pm4.56 986 . . . . . . . 8 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†” ยฌ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
285284biimpi 215 . . . . . . 7 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ยฌ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
286 olc 866 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
287286adantl 480 . . . . . . . 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 11242 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 โˆˆ โ„)
292139a1i 11 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
293 modge0 13871 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ 0 โ‰ค (๐‘‹ mod ๐‘‡))
2944, 63, 293mp2an 690 . . . . . . . . . . . . 13 0 โ‰ค (๐‘‹ mod ๐‘‡)
295294a1i 11 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 โ‰ค (๐‘‹ mod ๐‘‡))
296 neqne 2938 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โ‰  0)
297291, 292, 295, 296leneltd 11393 . . . . . . . . . . 11 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 < (๐‘‹ mod ๐‘‡))
298297adantl 480 . . . . . . . . . 10 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ 0 < (๐‘‹ mod ๐‘‡))
299 simpl 481 . . . . . . . . . 10 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
300288, 289, 290, 298, 299eliocd 44951 . . . . . . . . 9 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
301300orcd 871 . . . . . . . 8 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
302287, 301pm2.61dan 811 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โ†’ ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆจ (๐‘‹ mod ๐‘‡) = 0))
303285, 302nsyl 140 . . . . . 6 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
30433a1i 11 . . . . . . 7 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ฯ€ โˆˆ โ„)
305304, 283ltnled 11386 . . . . . 6 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (ฯ€ < (๐‘‹ mod ๐‘‡) โ†” ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€))
306303, 305mpbird 256 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
307 modlt 13872 . . . . . . 7 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) < ๐‘‡)
3084, 63, 307mp2an 690 . . . . . 6 (๐‘‹ mod ๐‘‡) < ๐‘‡
309308a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) < ๐‘‡)
310280, 282, 283, 306, 309eliood 44942 . . . 4 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡))
311127a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ 0 โˆˆ โ„*)
31233a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ฯ€ โˆˆ โ„)
313140a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„*)
314 ioogtlb 44939 . . . . . . . . . 10 ((ฯ€ โˆˆ โ„* โˆง ๐‘‡ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡)) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
315128, 281, 314mp3an12 1447 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
316311, 312, 313, 315gtnelioc 44935 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
317316iffalsed 4536 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = -1)
318139a1i 11 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
319312, 318, 315ltnsymd 11388 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) < ฯ€)
320319iffalsed 4536 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = -1)
321156, 320eqtrid 2777 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐นโ€˜๐‘‹) = -1)
322317, 321oveq12d 7431 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (-1 + -1))
323322oveq1d 7428 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((-1 + -1) / 2))
324 df-2 12300 . . . . . . . . . 10 2 = (1 + 1)
325324negeqi 11478 . . . . . . . . 9 -2 = -(1 + 1)
326185, 185negdii 11569 . . . . . . . . 9 -(1 + 1) = (-1 + -1)
327325, 326eqtr2i 2754 . . . . . . . 8 (-1 + -1) = -2
328327oveq1i 7423 . . . . . . 7 ((-1 + -1) / 2) = (-2 / 2)
329 divneg 11931 . . . . . . . 8 ((2 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง 2 โ‰  0) โ†’ -(2 / 2) = (-2 / 2))
330169, 169, 44, 329mp3an 1457 . . . . . . 7 -(2 / 2) = (-2 / 2)
331238negeqi 11478 . . . . . . 7 -(2 / 2) = -1
332328, 330, 3313eqtr2i 2759 . . . . . 6 ((-1 + -1) / 2) = -1
333332a1i 11 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ((-1 + -1) / 2) = -1)
334172a1i 11 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ๐‘Œ = if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)))
335312, 318ltnled 11386 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (ฯ€ < (๐‘‹ mod ๐‘‡) โ†” ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€))
336315, 335mpbid 231 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
337248, 112eqbrtrdi 5183 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
338337adantl 480 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
339126orcanai 1000 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
340339, 144syl 17 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
341338, 340pm2.61dan 811 . . . . . . . 8 ((๐‘‹ mod ฯ€) = 0 โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
342336, 341nsyl 140 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ฯ€) = 0)
343342iffalsed 4536 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = (๐นโ€˜๐‘‹))
344334, 343, 3213eqtrrd 2770 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ -1 = ๐‘Œ)
345323, 333, 3443eqtrrd 2770 . . . 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 811 . 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 394   โˆจ wo 845   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2930  โˆƒwrex 3060  ifcif 4525   class class class wbr 5144   โ†ฆ cmpt 5227  โ€˜cfv 6543  (class class class)co 7413  โ„‚cc 11131  โ„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   ยท cmul 11138  โ„*cxr 11272   < clt 11273   โ‰ค cle 11274   โˆ’ cmin 11469  -cneg 11470   / cdiv 11896  2c2 12292  โ„คcz 12583  โ„+crp 13001  (,)cioo 13351  (,]cioc 13352  โŒŠcfl 13782   mod cmo 13861  ฯ€cpi 16037   โˆฅ cdvds 16225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211  ax-addf 11212
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-iin 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7866  df-1st 7987  df-2nd 7988  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9381  df-fi 9429  df-sup 9460  df-inf 9461  df-oi 9528  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-4 12302  df-5 12303  df-6 12304  df-7 12305  df-8 12306  df-9 12307  df-n0 12498  df-z 12584  df-dec 12703  df-uz 12848  df-q 12958  df-rp 13002  df-xneg 13119  df-xadd 13120  df-xmul 13121  df-ioo 13355  df-ioc 13356  df-ico 13357  df-icc 13358  df-fz 13512  df-fzo 13655  df-fl 13784  df-mod 13862  df-seq 13994  df-exp 14054  df-fac 14260  df-bc 14289  df-hash 14317  df-shft 15041  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-limsup 15442  df-clim 15459  df-rlim 15460  df-sum 15660  df-ef 16038  df-sin 16040  df-cos 16041  df-pi 16043  df-dvds 16226  df-struct 17110  df-sets 17127  df-slot 17145  df-ndx 17157  df-base 17175  df-ress 17204  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-hom 17251  df-cco 17252  df-rest 17398  df-topn 17399  df-0g 17417  df-gsum 17418  df-topgen 17419  df-pt 17420  df-prds 17423  df-xrs 17478  df-qtop 17483  df-imas 17484  df-xps 17486  df-mre 17560  df-mrc 17561  df-acs 17563  df-mgm 18594  df-sgrp 18673  df-mnd 18689  df-submnd 18735  df-mulg 19023  df-cntz 19267  df-cmn 19736  df-psmet 21270  df-xmet 21271  df-met 21272  df-bl 21273  df-mopn 21274  df-fbas 21275  df-fg 21276  df-cnfld 21279  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-nei 23015  df-lp 23053  df-perf 23054  df-cn 23144  df-cnp 23145  df-haus 23232  df-tx 23479  df-hmeo 23672  df-fil 23763  df-fm 23855  df-flim 23856  df-flf 23857  df-xms 24239  df-ms 24240  df-tms 24241  df-cncf 24811  df-limc 25808  df-dv 25809
This theorem is referenced by:  fouriersw  45678
  Copyright terms: Public domain W3C validator