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 45531
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 484 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ 2 โˆฅ (๐‘‹ / ฯ€))
2 2z 12610 . . . . . . . . . . . 12 2 โˆˆ โ„ค
32a1i 11 . . . . . . . . . . 11 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ 2 โˆˆ โ„ค)
4 fourierswlem.x . . . . . . . . . . . . . 14 ๐‘‹ โˆˆ โ„
5 pirp 26370 . . . . . . . . . . . . . 14 ฯ€ โˆˆ โ„+
6 mod0 13859 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„ โˆง ฯ€ โˆˆ โ„+) โ†’ ((๐‘‹ mod ฯ€) = 0 โ†” (๐‘‹ / ฯ€) โˆˆ โ„ค))
74, 5, 6mp2an 691 . . . . . . . . . . . . 13 ((๐‘‹ mod ฯ€) = 0 โ†” (๐‘‹ / ฯ€) โˆˆ โ„ค)
87biimpi 215 . . . . . . . . . . . 12 ((๐‘‹ mod ฯ€) = 0 โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
98adantr 480 . . . . . . . . . . 11 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
10 divides 16218 . . . . . . . . . . 11 ((2 โˆˆ โ„ค โˆง (๐‘‹ / ฯ€) โˆˆ โ„ค) โ†’ (2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)))
113, 9, 10syl2anc 583 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)))
121, 11mpbid 231 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€))
13 2cnd 12306 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ 2 โˆˆ โ„‚)
14 picn 26368 . . . . . . . . . . . . . . . . . . . 20 ฯ€ โˆˆ โ„‚
1514a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ ฯ€ โˆˆ โ„‚)
16 zcn 12579 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ ๐‘˜ โˆˆ โ„‚)
1713, 15, 16mulassd 11253 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = (2 ยท (ฯ€ ยท ๐‘˜)))
1815, 16mulcld 11250 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (ฯ€ ยท ๐‘˜) โˆˆ โ„‚)
1913, 18mulcomd 11251 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท (ฯ€ ยท ๐‘˜)) = ((ฯ€ ยท ๐‘˜) ยท 2))
2017, 19eqtrd 2767 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = ((ฯ€ ยท ๐‘˜) ยท 2))
2120adantr 480 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((2 ยท ฯ€) ยท ๐‘˜) = ((ฯ€ ยท ๐‘˜) ยท 2))
2215, 16, 13mulassd 11253 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((ฯ€ ยท ๐‘˜) ยท 2) = (ฯ€ ยท (๐‘˜ ยท 2)))
2322adantr 480 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((ฯ€ ยท ๐‘˜) ยท 2) = (ฯ€ ยท (๐‘˜ ยท 2)))
24 id 22 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘˜ ยท 2) = (๐‘‹ / ฯ€))
2524eqcomd 2733 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ฯ€) = (๐‘˜ ยท 2))
2625adantl 481 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ฯ€) = (๐‘˜ ยท 2))
274recni 11244 . . . . . . . . . . . . . . . . . . 19 ๐‘‹ โˆˆ โ„‚
2827a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ โˆˆ โ„‚)
2914a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„‚)
3016adantr 480 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘˜ โˆˆ โ„‚)
31 2cnd 12306 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ 2 โˆˆ โ„‚)
3230, 31mulcld 11250 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘˜ ยท 2) โˆˆ โ„‚)
33 pire 26367 . . . . . . . . . . . . . . . . . . . 20 ฯ€ โˆˆ โ„
34 pipos 26369 . . . . . . . . . . . . . . . . . . . 20 0 < ฯ€
3533, 34gt0ne0ii 11766 . . . . . . . . . . . . . . . . . . 19 ฯ€ โ‰  0
3635a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โ‰  0)
3728, 29, 32, 36divmuld 12028 . . . . . . . . . . . . . . . . 17 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ / ฯ€) = (๐‘˜ ยท 2) โ†” (ฯ€ ยท (๐‘˜ ยท 2)) = ๐‘‹))
3826, 37mpbid 231 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ ยท (๐‘˜ ยท 2)) = ๐‘‹)
3921, 23, 383eqtrrd 2772 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ = ((2 ยท ฯ€) ยท ๐‘˜))
40 fourierswlem.t . . . . . . . . . . . . . . . 16 ๐‘‡ = (2 ยท ฯ€)
4140a1i 11 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘‡ = (2 ยท ฯ€))
4239, 41oveq12d 7432 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) = (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)))
4313, 15mulcld 11250 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) โˆˆ โ„‚)
44 2ne0 12332 . . . . . . . . . . . . . . . . . 18 2 โ‰  0
4544a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ 2 โ‰  0)
4635a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ฯ€ โ‰  0)
4713, 15, 45, 46mulne0d 11882 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) โ‰  0)
4816, 43, 47divcan3d 12011 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)) = ๐‘˜)
4948adantr 480 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ฯ€) ยท ๐‘˜) / (2 ยท ฯ€)) = ๐‘˜)
5042, 49eqtrd 2767 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) = ๐‘˜)
51 simpl 482 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ ๐‘˜ โˆˆ โ„ค)
5250, 51eqeltrd 2828 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘˜ ยท 2) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
5352ex 412 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค))
5453a1i 11 . . . . . . . . . 10 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)))
5554rexlimdv 3148 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท 2) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค))
5612, 55mpd 15 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
57 2re 12302 . . . . . . . . . . . 12 2 โˆˆ โ„
5857, 33remulcli 11246 . . . . . . . . . . 11 (2 ยท ฯ€) โˆˆ โ„
5940, 58eqeltri 2824 . . . . . . . . . 10 ๐‘‡ โˆˆ โ„
60 2pos 12331 . . . . . . . . . . . 12 0 < 2
6157, 33, 60, 34mulgt0ii 11363 . . . . . . . . . . 11 0 < (2 ยท ฯ€)
6261, 40breqtrri 5169 . . . . . . . . . 10 0 < ๐‘‡
6359, 62elrpii 12995 . . . . . . . . 9 ๐‘‡ โˆˆ โ„+
64 mod0 13859 . . . . . . . . 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 16303 . . . . . . . . . 10 ((๐‘‹ / ฯ€) โˆˆ โ„ค โ†’ (ยฌ 2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)))
697, 68sylbi 216 . . . . . . . . 9 ((๐‘‹ mod ฯ€) = 0 โ†’ (ยฌ 2 โˆฅ (๐‘‹ / ฯ€) โ†” โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)))
7069biimpa 476 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€))
7113, 16mulcld 11250 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ๐‘˜) โˆˆ โ„‚)
7271adantr 480 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (2 ยท ๐‘˜) โˆˆ โ„‚)
73 1cnd 11225 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ 1 โˆˆ โ„‚)
7414a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„‚)
7572, 73, 74adddird 11255 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)))
7613, 16mulcomd 11251 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ๐‘˜) = (๐‘˜ ยท 2))
7776oveq1d 7429 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) ยท ฯ€) = ((๐‘˜ ยท 2) ยท ฯ€))
7816, 13, 15mulassd 11253 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท 2) ยท ฯ€) = (๐‘˜ ยท (2 ยท ฯ€)))
7940eqcomi 2736 . . . . . . . . . . . . . . . . . . . 20 (2 ยท ฯ€) = ๐‘‡
8079a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ โ„ค โ†’ (2 ยท ฯ€) = ๐‘‡)
8180oveq2d 7430 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ ยท (2 ยท ฯ€)) = (๐‘˜ ยท ๐‘‡))
8277, 78, 813eqtrd 2771 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) ยท ฯ€) = (๐‘˜ ยท ๐‘‡))
8314mullidi 11235 . . . . . . . . . . . . . . . . . 18 (1 ยท ฯ€) = ฯ€
8483a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (1 ยท ฯ€) = ฯ€)
8582, 84oveq12d 7432 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)) = ((๐‘˜ ยท ๐‘‡) + ฯ€))
8685adantr 480 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) ยท ฯ€) + (1 ยท ฯ€)) = ((๐‘˜ ยท ๐‘‡) + ฯ€))
8740, 43eqeltrid 2832 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ โ„ค โ†’ ๐‘‡ โˆˆ โ„‚)
8816, 87mulcld 11250 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ ยท ๐‘‡) โˆˆ โ„‚)
8988, 15addcomd 11432 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ ((๐‘˜ ยท ๐‘‡) + ฯ€) = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
9089adantr 480 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((๐‘˜ ยท ๐‘‡) + ฯ€) = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
9175, 86, 903eqtrrd 2772 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ + (๐‘˜ ยท ๐‘‡)) = (((2 ยท ๐‘˜) + 1) ยท ฯ€))
92 peano2cn 11402 . . . . . . . . . . . . . . . . 17 ((2 ยท ๐‘˜) โˆˆ โ„‚ โ†’ ((2 ยท ๐‘˜) + 1) โˆˆ โ„‚)
9371, 92syl 17 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ค โ†’ ((2 ยท ๐‘˜) + 1) โˆˆ โ„‚)
9493, 15mulcomd 11251 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (ฯ€ ยท ((2 ยท ๐‘˜) + 1)))
9594adantr 480 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (((2 ยท ๐‘˜) + 1) ยท ฯ€) = (ฯ€ ยท ((2 ยท ๐‘˜) + 1)))
96 id 22 . . . . . . . . . . . . . . . . 17 (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€))
9796eqcomd 2733 . . . . . . . . . . . . . . . 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 12028 . . . . . . . . . . . . . . 15 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((๐‘‹ / ฯ€) = ((2 ยท ๐‘˜) + 1) โ†” (ฯ€ ยท ((2 ยท ๐‘˜) + 1)) = ๐‘‹))
10398, 102mpbid 231 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ ยท ((2 ยท ๐‘˜) + 1)) = ๐‘‹)
10491, 95, 1033eqtrrd 2772 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ๐‘‹ = (ฯ€ + (๐‘˜ ยท ๐‘‡)))
105104oveq1d 7429 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡))
106 modcyc 13889 . . . . . . . . . . . . . 14 ((ฯ€ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+ โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
10733, 63, 106mp3an12 1448 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„ค โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
108107adantr 480 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ((ฯ€ + (๐‘˜ ยท ๐‘‡)) mod ๐‘‡) = (ฯ€ mod ๐‘‡))
10933a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ โˆˆ โ„)
11063a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ๐‘‡ โˆˆ โ„+)
111 0re 11232 . . . . . . . . . . . . . . 15 0 โˆˆ โ„
112111, 33, 34ltleii 11353 . . . . . . . . . . . . . 14 0 โ‰ค ฯ€
113112a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ 0 โ‰ค ฯ€)
114 2timesgt 44583 . . . . . . . . . . . . . . . 16 (ฯ€ โˆˆ โ„+ โ†’ ฯ€ < (2 ยท ฯ€))
1155, 114ax-mp 5 . . . . . . . . . . . . . . 15 ฯ€ < (2 ยท ฯ€)
116115, 40breqtrri 5169 . . . . . . . . . . . . . 14 ฯ€ < ๐‘‡
117116a1i 11 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ ฯ€ < ๐‘‡)
118 modid 13879 . . . . . . . . . . . . 13 (((ฯ€ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โˆง (0 โ‰ค ฯ€ โˆง ฯ€ < ๐‘‡)) โ†’ (ฯ€ mod ๐‘‡) = ฯ€)
119109, 110, 113, 117, 118syl22anc 838 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (ฯ€ mod ๐‘‡) = ฯ€)
120105, 108, 1193eqtrd 2771 . . . . . . . . . . 11 ((๐‘˜ โˆˆ โ„ค โˆง ((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
121120ex 412 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€))
122121a1i 11 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง ยฌ 2 โˆฅ (๐‘‹ / ฯ€)) โ†’ (๐‘˜ โˆˆ โ„ค โ†’ (((2 ยท ๐‘˜) + 1) = (๐‘‹ / ฯ€) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)))
123122rexlimdv 3148 . . . . . . . 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 11277 . . . . . . . 8 0 โˆˆ โ„*
12833rexri 11288 . . . . . . . 8 ฯ€ โˆˆ โ„*
129 iocgtlb 44800 . . . . . . . 8 ((0 โˆˆ โ„* โˆง ฯ€ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€)) โ†’ 0 < (๐‘‹ mod ๐‘‡))
130127, 128, 129mp3an12 1448 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ 0 < (๐‘‹ mod ๐‘‡))
131130gt0ne0d 11794 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ (๐‘‹ mod ๐‘‡) โ‰  0)
132131neneqd 2940 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ ยฌ (๐‘‹ mod ๐‘‡) = 0)
133 pm2.53 850 . . . . . 6 (((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) = ฯ€))
134133imp 406 . . . . 5 ((((๐‘‹ mod ๐‘‡) = 0 โˆจ (๐‘‹ mod ๐‘‡) = ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
135126, 132, 134syl2anr 596 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
136127a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ 0 โˆˆ โ„*)
137128a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ ฯ€ โˆˆ โ„*)
138 modcl 13856 . . . . . . . . . . . . . . 15 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
1394, 63, 138mp2an 691 . . . . . . . . . . . . . 14 (๐‘‹ mod ๐‘‡) โˆˆ โ„
140139rexri 11288 . . . . . . . . . . . . 13 (๐‘‹ mod ๐‘‡) โˆˆ โ„*
141140a1i 11 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„*)
142 id 22 . . . . . . . . . . . . 13 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) = ฯ€)
14334, 142breqtrrid 5180 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ 0 < (๐‘‹ mod ๐‘‡))
14433eqlei2 11341 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
145136, 137, 141, 143, 144eliocd 44805 . . . . . . . . . . 11 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
146145iftrued 4532 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = 1)
147146adantl 481 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = 1)
148 oveq1 7421 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘‹ โ†’ (๐‘ฅ mod ๐‘‡) = (๐‘‹ mod ๐‘‡))
149148breq1d 5152 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘‹ โ†’ ((๐‘ฅ mod ๐‘‡) < ฯ€ โ†” (๐‘‹ mod ๐‘‡) < ฯ€))
150149ifbid 4547 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘‹ โ†’ if((๐‘ฅ mod ๐‘‡) < ฯ€, 1, -1) = if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1))
151 fourierswlem.f . . . . . . . . . . . . 13 ๐น = (๐‘ฅ โˆˆ โ„ โ†ฆ if((๐‘ฅ mod ๐‘‡) < ฯ€, 1, -1))
152 1ex 11226 . . . . . . . . . . . . . 14 1 โˆˆ V
153 negex 11474 . . . . . . . . . . . . . 14 -1 โˆˆ V
154152, 153ifex 4574 . . . . . . . . . . . . 13 if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) โˆˆ V
155150, 151, 154fvmpt 6999 . . . . . . . . . . . 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 11366 . . . . . . . . . . . . 13 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ (๐‘‹ mod ๐‘‡) โ‰  ฯ€)
160159necon2bi 2966 . . . . . . . . . . . 12 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ ยฌ (๐‘‹ mod ๐‘‡) < ฯ€)
161160iffalsed 4535 . . . . . . . . . . 11 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = -1)
162156, 161eqtrid 2779 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = ฯ€ โ†’ (๐นโ€˜๐‘‹) = -1)
163162adantl 481 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (๐นโ€˜๐‘‹) = -1)
164147, 163oveq12d 7432 . . . . . . . 8 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (1 + -1))
165 1pneg1e0 12347 . . . . . . . 8 (1 + -1) = 0
166164, 165eqtrdi 2783 . . . . . . 7 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = 0)
167166oveq1d 7429 . . . . . 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 12303 . . . . . . 7 2 โˆˆ โ„‚
170169, 44div0i 11964 . . . . . 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 4530 . . . . . . 7 ((๐‘‹ mod ฯ€) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = 0)
174172, 173eqtr2id 2780 . . . . . 6 ((๐‘‹ mod ฯ€) = 0 โ†’ 0 = ๐‘Œ)
175174ad2antlr 726 . . . . 5 ((((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง (๐‘‹ mod ฯ€) = 0) โˆง (๐‘‹ mod ๐‘‡) = ฯ€) โ†’ 0 = ๐‘Œ)
176168, 171, 1753eqtrrd 2772 . . . 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 4530 . . . . . . 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 44801 . . . . . . . . . 10 ((0 โˆˆ โ„* โˆง ฯ€ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€)) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
183127, 128, 182mp3an12 1448 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
184183adantr 480 . . . . . . . 8 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
185 ax-1cn 11182 . . . . . . . . . . . . . . . . . . . 20 1 โˆˆ โ„‚
186185, 14mulcomi 11238 . . . . . . . . . . . . . . . . . . 19 (1 ยท ฯ€) = (ฯ€ ยท 1)
18783, 186eqtr3i 2757 . . . . . . . . . . . . . . . . . 18 ฯ€ = (ฯ€ ยท 1)
188187oveq1i 7424 . . . . . . . . . . . . . . . . 17 (ฯ€ + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = ((ฯ€ ยท 1) + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
189169, 14mulcomi 11238 . . . . . . . . . . . . . . . . . . . . 21 (2 ยท ฯ€) = (ฯ€ ยท 2)
19040, 189eqtri 2755 . . . . . . . . . . . . . . . . . . . 20 ๐‘‡ = (ฯ€ ยท 2)
191190oveq1i 7424 . . . . . . . . . . . . . . . . . . 19 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = ((ฯ€ ยท 2) ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))
192111, 62gtneii 11342 . . . . . . . . . . . . . . . . . . . . . . 23 ๐‘‡ โ‰  0
1934, 59, 192redivcli 11997 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘‹ / ๐‘‡) โˆˆ โ„
194 flcl 13778 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘‹ / ๐‘‡) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค)
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค
196 zcn 12579 . . . . . . . . . . . . . . . . . . . . 21 ((โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค โ†’ (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„‚)
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„‚
19814, 169, 197mulassi 11241 . . . . . . . . . . . . . . . . . . 19 ((ฯ€ ยท 2) ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
199191, 198eqtri 2755 . . . . . . . . . . . . . . . . . 18 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) = (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
200199oveq2i 7425 . . . . . . . . . . . . . . . . 17 (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = (ฯ€ + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
201169, 197mulcli 11237 . . . . . . . . . . . . . . . . . 18 (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚
20214, 185, 201adddii 11242 . . . . . . . . . . . . . . . . 17 (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = ((ฯ€ ยท 1) + (ฯ€ ยท (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
203188, 200, 2023eqtr4ri 2766 . . . . . . . . . . . . . . . 16 (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
204203a1i 11 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) = (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
205 id 22 . . . . . . . . . . . . . . . . 17 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ฯ€ = (๐‘‹ mod ๐‘‡))
206 modval 13854 . . . . . . . . . . . . . . . . . 18 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
2074, 63, 206mp2an 691 . . . . . . . . . . . . . . . . 17 (๐‘‹ mod ๐‘‡) = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
208205, 207eqtrdi 2783 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ฯ€ = (๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
209208oveq1d 7429 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (ฯ€ + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = ((๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
21027a1i 11 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ๐‘‹ โˆˆ โ„‚)
21159recni 11244 . . . . . . . . . . . . . . . . . 18 ๐‘‡ โˆˆ โ„‚
212211, 197mulcli 11237 . . . . . . . . . . . . . . . . 17 (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚
213212a1i 11 . . . . . . . . . . . . . . . 16 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„‚)
214210, 213npcand 11591 . . . . . . . . . . . . . . 15 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ((๐‘‹ โˆ’ (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) + (๐‘‡ ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) = ๐‘‹)
215204, 209, 2143eqtrrd 2772 . . . . . . . . . . . . . 14 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ ๐‘‹ = (ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))))
216215oveq1d 7429 . . . . . . . . . . . . 13 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) = ((ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) / ฯ€))
217185, 201addcli 11236 . . . . . . . . . . . . . 14 (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„‚
218217, 14, 35divcan3i 11976 . . . . . . . . . . . . 13 ((ฯ€ ยท (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))) / ฯ€) = (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))))
219216, 218eqtrdi 2783 . . . . . . . . . . . 12 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) = (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))))
220 1z 12608 . . . . . . . . . . . . . 14 1 โˆˆ โ„ค
221 zmulcl 12627 . . . . . . . . . . . . . . 15 ((2 โˆˆ โ„ค โˆง (โŒŠโ€˜(๐‘‹ / ๐‘‡)) โˆˆ โ„ค) โ†’ (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค)
2222, 195, 221mp2an 691 . . . . . . . . . . . . . 14 (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค
223 zaddcl 12618 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡))) โˆˆ โ„ค) โ†’ (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค)
224220, 222, 223mp2an 691 . . . . . . . . . . . . 13 (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค
225224a1i 11 . . . . . . . . . . . 12 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (1 + (2 ยท (โŒŠโ€˜(๐‘‹ / ๐‘‡)))) โˆˆ โ„ค)
226219, 225eqeltrd 2828 . . . . . . . . . . 11 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
227226, 7sylibr 233 . . . . . . . . . 10 (ฯ€ = (๐‘‹ mod ๐‘‡) โ†’ (๐‘‹ mod ฯ€) = 0)
228227necon3bi 2962 . . . . . . . . 9 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ ฯ€ โ‰  (๐‘‹ mod ๐‘‡))
229228adantl 481 . . . . . . . 8 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ฯ€ โ‰  (๐‘‹ mod ๐‘‡))
230180, 181, 184, 229leneltd 11384 . . . . . . 7 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐‘‹ mod ๐‘‡) < ฯ€)
231 iftrue 4530 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = 1)
232156, 231eqtrid 2779 . . . . . . 7 ((๐‘‹ mod ๐‘‡) < ฯ€ โ†’ (๐นโ€˜๐‘‹) = 1)
233230, 232syl 17 . . . . . 6 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐นโ€˜๐‘‹) = 1)
234179, 233oveq12d 7432 . . . . 5 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (1 + 1))
235234oveq1d 7429 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((1 + 1) / 2))
236 1p1e2 12353 . . . . . . 7 (1 + 1) = 2
237236oveq1i 7424 . . . . . 6 ((1 + 1) / 2) = (2 / 2)
238 2div2e1 12369 . . . . . 6 (2 / 2) = 1
239237, 238eqtr2i 2756 . . . . 5 1 = ((1 + 1) / 2)
240233, 239eqtr2di 2784 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ ((1 + 1) / 2) = (๐นโ€˜๐‘‹))
241 iffalse 4533 . . . . . 6 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = (๐นโ€˜๐‘‹))
242172, 241eqtr2id 2780 . . . . 5 (ยฌ (๐‘‹ mod ฯ€) = 0 โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
243242adantl 481 . . . 4 (((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ฯ€) = 0) โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
244235, 240, 2433eqtrrd 2772 . . 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 2966 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
247246iffalsed 4535 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = -1)
248 id 22 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) = 0)
249248, 34eqbrtrdi 5181 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) < ฯ€)
250249iftrued 4532 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = 1)
251156, 250eqtrid 2779 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐นโ€˜๐‘‹) = 1)
252247, 251oveq12d 7432 . . . . . 6 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (-1 + 1))
253252oveq1d 7429 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((-1 + 1) / 2))
254 neg1cn 12342 . . . . . . . . 9 -1 โˆˆ โ„‚
255185, 254, 165addcomli 11422 . . . . . . . 8 (-1 + 1) = 0
256255oveq1i 7424 . . . . . . 7 ((-1 + 1) / 2) = (0 / 2)
257256, 170eqtri 2755 . . . . . 6 ((-1 + 1) / 2) = 0
258257a1i 11 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ ((-1 + 1) / 2) = 0)
25940oveq2i 7425 . . . . . . . . . . . . 13 (๐‘‹ / ๐‘‡) = (๐‘‹ / (2 ยท ฯ€))
260 2cnne0 12438 . . . . . . . . . . . . . 14 (2 โˆˆ โ„‚ โˆง 2 โ‰  0)
26114, 35pm3.2i 470 . . . . . . . . . . . . . 14 (ฯ€ โˆˆ โ„‚ โˆง ฯ€ โ‰  0)
262 divdiv1 11941 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0) โˆง (ฯ€ โˆˆ โ„‚ โˆง ฯ€ โ‰  0)) โ†’ ((๐‘‹ / 2) / ฯ€) = (๐‘‹ / (2 ยท ฯ€)))
26327, 260, 261, 262mp3an 1458 . . . . . . . . . . . . 13 ((๐‘‹ / 2) / ฯ€) = (๐‘‹ / (2 ยท ฯ€))
26427, 169, 14, 44, 35divdiv32i 11985 . . . . . . . . . . . . 13 ((๐‘‹ / 2) / ฯ€) = ((๐‘‹ / ฯ€) / 2)
265259, 263, 2643eqtr2i 2761 . . . . . . . . . . . 12 (๐‘‹ / ๐‘‡) = ((๐‘‹ / ฯ€) / 2)
266265oveq2i 7425 . . . . . . . . . . 11 (2 ยท (๐‘‹ / ๐‘‡)) = (2 ยท ((๐‘‹ / ฯ€) / 2))
26727, 14, 35divcli 11972 . . . . . . . . . . . 12 (๐‘‹ / ฯ€) โˆˆ โ„‚
268267, 169, 44divcan2i 11973 . . . . . . . . . . 11 (2 ยท ((๐‘‹ / ฯ€) / 2)) = (๐‘‹ / ฯ€)
269266, 268eqtr2i 2756 . . . . . . . . . 10 (๐‘‹ / ฯ€) = (2 ยท (๐‘‹ / ๐‘‡))
2702a1i 11 . . . . . . . . . . 11 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ 2 โˆˆ โ„ค)
271 id 22 . . . . . . . . . . 11 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (๐‘‹ / ๐‘‡) โˆˆ โ„ค)
272270, 271zmulcld 12688 . . . . . . . . . 10 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (2 ยท (๐‘‹ / ๐‘‡)) โˆˆ โ„ค)
273269, 272eqeltrid 2832 . . . . . . . . 9 ((๐‘‹ / ๐‘‡) โˆˆ โ„ค โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
27465, 273sylbi 216 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ / ฯ€) โˆˆ โ„ค)
275274, 7sylibr 233 . . . . . . 7 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ฯ€) = 0)
276275iftrued 4532 . . . . . 6 ((๐‘‹ mod ๐‘‡) = 0 โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = 0)
277172, 276eqtr2id 2780 . . . . 5 ((๐‘‹ mod ๐‘‡) = 0 โ†’ 0 = ๐‘Œ)
278253, 258, 2773eqtrrd 2772 . . . 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 11288 . . . . . 6 ๐‘‡ โˆˆ โ„*
282281a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ๐‘‡ โˆˆ โ„*)
283139a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
284 pm4.56 987 . . . . . . . 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 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 11233 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 โˆˆ โ„)
292139a1i 11 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
293 modge0 13862 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ 0 โ‰ค (๐‘‹ mod ๐‘‡))
2944, 63, 293mp2an 691 . . . . . . . . . . . . 13 0 โ‰ค (๐‘‹ mod ๐‘‡)
295294a1i 11 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 โ‰ค (๐‘‹ mod ๐‘‡))
296 neqne 2943 . . . . . . . . . . . 12 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โ‰  0)
297291, 292, 295, 296leneltd 11384 . . . . . . . . . . 11 (ยฌ (๐‘‹ mod ๐‘‡) = 0 โ†’ 0 < (๐‘‹ mod ๐‘‡))
298297adantl 481 . . . . . . . . . 10 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ 0 < (๐‘‹ mod ๐‘‡))
299 simpl 482 . . . . . . . . . 10 (((๐‘‹ mod ๐‘‡) โ‰ค ฯ€ โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
300288, 289, 290, 298, 299eliocd 44805 . . . . . . . . 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 11377 . . . . . 6 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (ฯ€ < (๐‘‹ mod ๐‘‡) โ†” ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€))
306303, 305mpbird 257 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
307 modlt 13863 . . . . . . 7 ((๐‘‹ โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„+) โ†’ (๐‘‹ mod ๐‘‡) < ๐‘‡)
3084, 63, 307mp2an 691 . . . . . 6 (๐‘‹ mod ๐‘‡) < ๐‘‡
309308a1i 11 . . . . 5 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) < ๐‘‡)
310280, 282, 283, 306, 309eliood 44796 . . . 4 ((ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€) โˆง ยฌ (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡))
311127a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ 0 โˆˆ โ„*)
31233a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ฯ€ โˆˆ โ„)
313140a1i 11 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„*)
314 ioogtlb 44793 . . . . . . . . . 10 ((ฯ€ โˆˆ โ„* โˆง ๐‘‡ โˆˆ โ„* โˆง (๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡)) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
315128, 281, 314mp3an12 1448 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ฯ€ < (๐‘‹ mod ๐‘‡))
316311, 312, 313, 315gtnelioc 44789 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€))
317316iffalsed 4535 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) = -1)
318139a1i 11 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐‘‹ mod ๐‘‡) โˆˆ โ„)
319312, 318, 315ltnsymd 11379 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) < ฯ€)
320319iffalsed 4535 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ๐‘‡) < ฯ€, 1, -1) = -1)
321156, 320eqtrid 2779 . . . . . . 7 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (๐นโ€˜๐‘‹) = -1)
322317, 321oveq12d 7432 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) = (-1 + -1))
323322oveq1d 7429 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ((if((๐‘‹ mod ๐‘‡) โˆˆ (0(,]ฯ€), 1, -1) + (๐นโ€˜๐‘‹)) / 2) = ((-1 + -1) / 2))
324 df-2 12291 . . . . . . . . . 10 2 = (1 + 1)
325324negeqi 11469 . . . . . . . . 9 -2 = -(1 + 1)
326185, 185negdii 11560 . . . . . . . . 9 -(1 + 1) = (-1 + -1)
327325, 326eqtr2i 2756 . . . . . . . 8 (-1 + -1) = -2
328327oveq1i 7424 . . . . . . 7 ((-1 + -1) / 2) = (-2 / 2)
329 divneg 11922 . . . . . . . 8 ((2 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง 2 โ‰  0) โ†’ -(2 / 2) = (-2 / 2))
330169, 169, 44, 329mp3an 1458 . . . . . . 7 -(2 / 2) = (-2 / 2)
331238negeqi 11469 . . . . . . 7 -(2 / 2) = -1
332328, 330, 3313eqtr2i 2761 . . . . . 6 ((-1 + -1) / 2) = -1
333332a1i 11 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ((-1 + -1) / 2) = -1)
334172a1i 11 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ๐‘Œ = if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)))
335312, 318ltnled 11377 . . . . . . . . 9 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ (ฯ€ < (๐‘‹ mod ๐‘‡) โ†” ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€))
336315, 335mpbid 231 . . . . . . . 8 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ ยฌ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
337248, 112eqbrtrdi 5181 . . . . . . . . . 10 ((๐‘‹ mod ๐‘‡) = 0 โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
338337adantl 481 . . . . . . . . 9 (((๐‘‹ mod ฯ€) = 0 โˆง (๐‘‹ mod ๐‘‡) = 0) โ†’ (๐‘‹ mod ๐‘‡) โ‰ค ฯ€)
339126orcanai 1001 . . . . . . . . . 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 4535 . . . . . 6 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ if((๐‘‹ mod ฯ€) = 0, 0, (๐นโ€˜๐‘‹)) = (๐นโ€˜๐‘‹))
344334, 343, 3213eqtrrd 2772 . . . . 5 ((๐‘‹ mod ๐‘‡) โˆˆ (ฯ€(,)๐‘‡) โ†’ -1 = ๐‘Œ)
345323, 333, 3443eqtrrd 2772 . . . 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 395   โˆจ wo 846   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2935  โˆƒwrex 3065  ifcif 4524   class class class wbr 5142   โ†ฆ cmpt 5225  โ€˜cfv 6542  (class class class)co 7414  โ„‚cc 11122  โ„cr 11123  0cc0 11124  1c1 11125   + caddc 11127   ยท cmul 11129  โ„*cxr 11263   < clt 11264   โ‰ค cle 11265   โˆ’ cmin 11460  -cneg 11461   / cdiv 11887  2c2 12283  โ„คcz 12574  โ„+crp 12992  (,)cioo 13342  (,]cioc 13343  โŒŠcfl 13773   mod cmo 13852  ฯ€cpi 16028   โˆฅ cdvds 16216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-inf2 9650  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202  ax-addf 11203
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7677  df-om 7863  df-1st 7985  df-2nd 7986  df-supp 8158  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-er 8716  df-map 8836  df-pm 8837  df-ixp 8906  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-fsupp 9376  df-fi 9420  df-sup 9451  df-inf 9452  df-oi 9519  df-card 9948  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-div 11888  df-nn 12229  df-2 12291  df-3 12292  df-4 12293  df-5 12294  df-6 12295  df-7 12296  df-8 12297  df-9 12298  df-n0 12489  df-z 12575  df-dec 12694  df-uz 12839  df-q 12949  df-rp 12993  df-xneg 13110  df-xadd 13111  df-xmul 13112  df-ioo 13346  df-ioc 13347  df-ico 13348  df-icc 13349  df-fz 13503  df-fzo 13646  df-fl 13775  df-mod 13853  df-seq 13985  df-exp 14045  df-fac 14251  df-bc 14280  df-hash 14308  df-shft 15032  df-cj 15064  df-re 15065  df-im 15066  df-sqrt 15200  df-abs 15201  df-limsup 15433  df-clim 15450  df-rlim 15451  df-sum 15651  df-ef 16029  df-sin 16031  df-cos 16032  df-pi 16034  df-dvds 16217  df-struct 17101  df-sets 17118  df-slot 17136  df-ndx 17148  df-base 17166  df-ress 17195  df-plusg 17231  df-mulr 17232  df-starv 17233  df-sca 17234  df-vsca 17235  df-ip 17236  df-tset 17237  df-ple 17238  df-ds 17240  df-unif 17241  df-hom 17242  df-cco 17243  df-rest 17389  df-topn 17390  df-0g 17408  df-gsum 17409  df-topgen 17410  df-pt 17411  df-prds 17414  df-xrs 17469  df-qtop 17474  df-imas 17475  df-xps 17477  df-mre 17551  df-mrc 17552  df-acs 17554  df-mgm 18585  df-sgrp 18664  df-mnd 18680  df-submnd 18726  df-mulg 19008  df-cntz 19252  df-cmn 19721  df-psmet 21251  df-xmet 21252  df-met 21253  df-bl 21254  df-mopn 21255  df-fbas 21256  df-fg 21257  df-cnfld 21260  df-top 22770  df-topon 22787  df-topsp 22809  df-bases 22823  df-cld 22897  df-ntr 22898  df-cls 22899  df-nei 22976  df-lp 23014  df-perf 23015  df-cn 23105  df-cnp 23106  df-haus 23193  df-tx 23440  df-hmeo 23633  df-fil 23724  df-fm 23816  df-flim 23817  df-flf 23818  df-xms 24200  df-ms 24201  df-tms 24202  df-cncf 24772  df-limc 25769  df-dv 25770
This theorem is referenced by:  fouriersw  45532
  Copyright terms: Public domain W3C validator