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

Theorem fourierswlem 37362
Description: The Fourier series for the square wave  F converges to  Y, a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierswlem.t  |-  T  =  ( 2  x.  pi )
fourierswlem.f  |-  F  =  ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
fourierswlem.x  |-  X  e.  RR
fourierswlem.y  |-  Y  =  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `  X
) )
Assertion
Ref Expression
fourierswlem  |-  Y  =  ( ( if ( ( X  mod  T
)  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 )
Distinct variable groups:    x, T    x, X
Allowed substitution hints:    F( x)    Y( x)

Proof of Theorem fourierswlem
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 simpr 459 . . . . . . . . . 10  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  2  ||  ( X  /  pi ) )
2 2z 10936 . . . . . . . . . . . 12  |-  2  e.  ZZ
32a1i 11 . . . . . . . . . . 11  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  2  e.  ZZ )
4 fourierswlem.x . . . . . . . . . . . . . 14  |-  X  e.  RR
5 pirp 23144 . . . . . . . . . . . . . 14  |-  pi  e.  RR+
6 mod0 12039 . . . . . . . . . . . . . 14  |-  ( ( X  e.  RR  /\  pi  e.  RR+ )  ->  (
( X  mod  pi )  =  0  <->  ( X  /  pi )  e.  ZZ ) )
74, 5, 6mp2an 670 . . . . . . . . . . . . 13  |-  ( ( X  mod  pi )  =  0  <->  ( X  /  pi )  e.  ZZ )
87biimpi 194 . . . . . . . . . . . 12  |-  ( ( X  mod  pi )  =  0  ->  ( X  /  pi )  e.  ZZ )
98adantr 463 . . . . . . . . . . 11  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  ( X  /  pi )  e.  ZZ )
10 divides 14195 . . . . . . . . . . 11  |-  ( ( 2  e.  ZZ  /\  ( X  /  pi )  e.  ZZ )  ->  ( 2  ||  ( X  /  pi )  <->  E. k  e.  ZZ  ( k  x.  2 )  =  ( X  /  pi ) ) )
113, 9, 10syl2anc 659 . . . . . . . . . 10  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  (
2  ||  ( X  /  pi )  <->  E. k  e.  ZZ  ( k  x.  2 )  =  ( X  /  pi ) ) )
121, 11mpbid 210 . . . . . . . . 9  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  E. k  e.  ZZ  ( k  x.  2 )  =  ( X  /  pi ) )
13 2cnd 10648 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ZZ  ->  2  e.  CC )
14 picn 23142 . . . . . . . . . . . . . . . . . . . 20  |-  pi  e.  CC
1514a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ZZ  ->  pi  e.  CC )
16 zcn 10909 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ZZ  ->  k  e.  CC )
1713, 15, 16mulassd 9648 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ZZ  ->  (
( 2  x.  pi )  x.  k )  =  ( 2  x.  ( pi  x.  k
) ) )
1815, 16mulcld 9645 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ZZ  ->  (
pi  x.  k )  e.  CC )
1913, 18mulcomd 9646 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ZZ  ->  (
2  x.  ( pi  x.  k ) )  =  ( ( pi  x.  k )  x.  2 ) )
2017, 19eqtrd 2443 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  (
( 2  x.  pi )  x.  k )  =  ( ( pi  x.  k )  x.  2 ) )
2120adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( ( 2  x.  pi )  x.  k )  =  ( ( pi  x.  k
)  x.  2 ) )
2215, 16, 13mulassd 9648 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  (
( pi  x.  k
)  x.  2 )  =  ( pi  x.  ( k  x.  2 ) ) )
2322adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( ( pi  x.  k )  x.  2 )  =  ( pi  x.  ( k  x.  2 ) ) )
24 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  x.  2 )  =  ( X  /  pi )  ->  ( k  x.  2 )  =  ( X  /  pi ) )
2524eqcomd 2410 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  x.  2 )  =  ( X  /  pi )  ->  ( X  /  pi )  =  ( k  x.  2 ) )
2625adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( X  /  pi )  =  (
k  x.  2 ) )
274recni 9637 . . . . . . . . . . . . . . . . . . 19  |-  X  e.  CC
2827a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  X  e.  CC )
2914a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  pi  e.  CC )
3016adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  k  e.  CC )
31 2cnd 10648 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  2  e.  CC )
3230, 31mulcld 9645 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( k  x.  2 )  e.  CC )
33 pire 23141 . . . . . . . . . . . . . . . . . . . 20  |-  pi  e.  RR
34 pipos 23143 . . . . . . . . . . . . . . . . . . . 20  |-  0  <  pi
3533, 34gt0ne0ii 10128 . . . . . . . . . . . . . . . . . . 19  |-  pi  =/=  0
3635a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  pi  =/=  0
)
3728, 29, 32, 36divmuld 10382 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( ( X  /  pi )  =  ( k  x.  2 )  <->  ( pi  x.  ( k  x.  2 ) )  =  X ) )
3826, 37mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( pi  x.  ( k  x.  2 ) )  =  X )
3921, 23, 383eqtrrd 2448 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  X  =  ( ( 2  x.  pi )  x.  k )
)
40 fourierswlem.t . . . . . . . . . . . . . . . 16  |-  T  =  ( 2  x.  pi )
4140a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  T  =  ( 2  x.  pi ) )
4239, 41oveq12d 6295 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( X  /  T )  =  ( ( ( 2  x.  pi )  x.  k
)  /  ( 2  x.  pi ) ) )
4313, 15mulcld 9645 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ZZ  ->  (
2  x.  pi )  e.  CC )
44 2ne0 10668 . . . . . . . . . . . . . . . . . 18  |-  2  =/=  0
4544a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  2  =/=  0 )
4635a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  pi  =/=  0 )
4713, 15, 45, 46mulne0d 10241 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ZZ  ->  (
2  x.  pi )  =/=  0 )
4816, 43, 47divcan3d 10365 . . . . . . . . . . . . . . 15  |-  ( k  e.  ZZ  ->  (
( ( 2  x.  pi )  x.  k
)  /  ( 2  x.  pi ) )  =  k )
4948adantr 463 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( ( ( 2  x.  pi )  x.  k )  / 
( 2  x.  pi ) )  =  k )
5042, 49eqtrd 2443 . . . . . . . . . . . . 13  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( X  /  T )  =  k )
51 simpl 455 . . . . . . . . . . . . 13  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  k  e.  ZZ )
5250, 51eqeltrd 2490 . . . . . . . . . . . 12  |-  ( ( k  e.  ZZ  /\  ( k  x.  2 )  =  ( X  /  pi ) )  ->  ( X  /  T )  e.  ZZ )
5352ex 432 . . . . . . . . . . 11  |-  ( k  e.  ZZ  ->  (
( k  x.  2 )  =  ( X  /  pi )  -> 
( X  /  T
)  e.  ZZ ) )
5453a1i 11 . . . . . . . . . 10  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  (
k  e.  ZZ  ->  ( ( k  x.  2 )  =  ( X  /  pi )  -> 
( X  /  T
)  e.  ZZ ) ) )
5554rexlimdv 2893 . . . . . . . . 9  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  ( E. k  e.  ZZ  ( k  x.  2 )  =  ( X  /  pi )  -> 
( X  /  T
)  e.  ZZ ) )
5612, 55mpd 15 . . . . . . . 8  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  ( X  /  T )  e.  ZZ )
57 2re 10645 . . . . . . . . . . . 12  |-  2  e.  RR
5857, 33remulcli 9639 . . . . . . . . . . 11  |-  ( 2  x.  pi )  e.  RR
5940, 58eqeltri 2486 . . . . . . . . . 10  |-  T  e.  RR
60 2pos 10667 . . . . . . . . . . . 12  |-  0  <  2
6157, 33, 60, 34mulgt0ii 9749 . . . . . . . . . . 11  |-  0  <  ( 2  x.  pi )
6261, 40breqtrri 4419 . . . . . . . . . 10  |-  0  <  T
6359, 62elrpii 11267 . . . . . . . . 9  |-  T  e.  RR+
64 mod0 12039 . . . . . . . . 9  |-  ( ( X  e.  RR  /\  T  e.  RR+ )  -> 
( ( X  mod  T )  =  0  <->  ( X  /  T )  e.  ZZ ) )
654, 63, 64mp2an 670 . . . . . . . 8  |-  ( ( X  mod  T )  =  0  <->  ( X  /  T )  e.  ZZ )
6656, 65sylibr 212 . . . . . . 7  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  ( X  mod  T )  =  0 )
6766orcd 390 . . . . . 6  |-  ( ( ( X  mod  pi )  =  0  /\  2  ||  ( X  /  pi ) )  ->  (
( X  mod  T
)  =  0  \/  ( X  mod  T
)  =  pi ) )
68 odd2np1 14253 . . . . . . . . . 10  |-  ( ( X  /  pi )  e.  ZZ  ->  ( -.  2  ||  ( X  /  pi )  <->  E. k  e.  ZZ  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) ) )
697, 68sylbi 195 . . . . . . . . 9  |-  ( ( X  mod  pi )  =  0  ->  ( -.  2  ||  ( X  /  pi )  <->  E. k  e.  ZZ  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) ) )
7069biimpa 482 . . . . . . . 8  |-  ( ( ( X  mod  pi )  =  0  /\  -.  2  ||  ( X  /  pi ) )  ->  E. k  e.  ZZ  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )
7113, 16mulcld 9645 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  (
2  x.  k )  e.  CC )
7271adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( 2  x.  k )  e.  CC )
73 1cnd 9641 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  1  e.  CC )
7414a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  pi  e.  CC )
7572, 73, 74adddird 9650 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( ( ( 2  x.  k )  +  1 )  x.  pi )  =  ( ( ( 2  x.  k )  x.  pi )  +  ( 1  x.  pi ) ) )
7613, 16mulcomd 9646 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ZZ  ->  (
2  x.  k )  =  ( k  x.  2 ) )
7776oveq1d 6292 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ZZ  ->  (
( 2  x.  k
)  x.  pi )  =  ( ( k  x.  2 )  x.  pi ) )
7816, 13, 15mulassd 9648 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ZZ  ->  (
( k  x.  2 )  x.  pi )  =  ( k  x.  ( 2  x.  pi ) ) )
7940eqcomi 2415 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2  x.  pi )  =  T
8079a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ZZ  ->  (
2  x.  pi )  =  T )
8180oveq2d 6293 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ZZ  ->  (
k  x.  ( 2  x.  pi ) )  =  ( k  x.  T ) )
8277, 78, 813eqtrd 2447 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  (
( 2  x.  k
)  x.  pi )  =  ( k  x.  T ) )
8314mulid2i 9628 . . . . . . . . . . . . . . . . . 18  |-  ( 1  x.  pi )  =  pi
8483a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  (
1  x.  pi )  =  pi )
8582, 84oveq12d 6295 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ZZ  ->  (
( ( 2  x.  k )  x.  pi )  +  ( 1  x.  pi ) )  =  ( ( k  x.  T )  +  pi ) )
8685adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( ( ( 2  x.  k )  x.  pi )  +  ( 1  x.  pi ) )  =  ( ( k  x.  T
)  +  pi ) )
8740, 43syl5eqel 2494 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ZZ  ->  T  e.  CC )
8816, 87mulcld 9645 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  (
k  x.  T )  e.  CC )
8988, 15addcomd 9815 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ZZ  ->  (
( k  x.  T
)  +  pi )  =  ( pi  +  ( k  x.  T
) ) )
9089adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( ( k  x.  T )  +  pi )  =  ( pi  +  ( k  x.  T ) ) )
9175, 86, 903eqtrrd 2448 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( pi  +  ( k  x.  T
) )  =  ( ( ( 2  x.  k )  +  1 )  x.  pi ) )
92 peano2cn 9785 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  x.  k )  e.  CC  ->  (
( 2  x.  k
)  +  1 )  e.  CC )
9371, 92syl 17 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ZZ  ->  (
( 2  x.  k
)  +  1 )  e.  CC )
9493, 15mulcomd 9646 . . . . . . . . . . . . . . 15  |-  ( k  e.  ZZ  ->  (
( ( 2  x.  k )  +  1 )  x.  pi )  =  ( pi  x.  ( ( 2  x.  k )  +  1 ) ) )
9594adantr 463 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( ( ( 2  x.  k )  +  1 )  x.  pi )  =  ( pi  x.  ( ( 2  x.  k )  +  1 ) ) )
96 id 22 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 2  x.  k
)  +  1 )  =  ( X  /  pi )  ->  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )
9796eqcomd 2410 . . . . . . . . . . . . . . . 16  |-  ( ( ( 2  x.  k
)  +  1 )  =  ( X  /  pi )  ->  ( X  /  pi )  =  ( ( 2  x.  k )  +  1 ) )
9897adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( X  /  pi )  =  (
( 2  x.  k
)  +  1 ) )
9927a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  X  e.  CC )
10093adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( ( 2  x.  k )  +  1 )  e.  CC )
10135a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  pi  =/=  0
)
10299, 74, 100, 101divmuld 10382 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( ( X  /  pi )  =  ( ( 2  x.  k )  +  1 )  <->  ( pi  x.  ( ( 2  x.  k )  +  1 ) )  =  X ) )
10398, 102mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( pi  x.  ( ( 2  x.  k )  +  1 ) )  =  X )
10491, 95, 1033eqtrrd 2448 . . . . . . . . . . . . 13  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  X  =  ( pi  +  ( k  x.  T ) ) )
105104oveq1d 6292 . . . . . . . . . . . 12  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( X  mod  T )  =  ( ( pi  +  ( k  x.  T ) )  mod  T ) )
106 modcyc 12068 . . . . . . . . . . . . . 14  |-  ( ( pi  e.  RR  /\  T  e.  RR+  /\  k  e.  ZZ )  ->  (
( pi  +  ( k  x.  T ) )  mod  T )  =  ( pi  mod  T ) )
10733, 63, 106mp3an12 1316 . . . . . . . . . . . . 13  |-  ( k  e.  ZZ  ->  (
( pi  +  ( k  x.  T ) )  mod  T )  =  ( pi  mod  T ) )
108107adantr 463 . . . . . . . . . . . 12  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( ( pi  +  ( k  x.  T ) )  mod 
T )  =  ( pi  mod  T ) )
10933a1i 11 . . . . . . . . . . . . 13  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  pi  e.  RR )
11063a1i 11 . . . . . . . . . . . . 13  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  T  e.  RR+ )
111 0re 9625 . . . . . . . . . . . . . . 15  |-  0  e.  RR
112111, 33, 34ltleii 9738 . . . . . . . . . . . . . 14  |-  0  <_  pi
113112a1i 11 . . . . . . . . . . . . 13  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  0  <_  pi )
114 2timesgt 36828 . . . . . . . . . . . . . . . 16  |-  ( pi  e.  RR+  ->  pi  <  ( 2  x.  pi ) )
1155, 114ax-mp 5 . . . . . . . . . . . . . . 15  |-  pi  <  ( 2  x.  pi )
116115, 40breqtrri 4419 . . . . . . . . . . . . . 14  |-  pi  <  T
117116a1i 11 . . . . . . . . . . . . 13  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  pi  <  T
)
118 modid 12057 . . . . . . . . . . . . 13  |-  ( ( ( pi  e.  RR  /\  T  e.  RR+ )  /\  ( 0  <_  pi  /\  pi  <  T ) )  ->  ( pi  mod  T )  =  pi )
119109, 110, 113, 117, 118syl22anc 1231 . . . . . . . . . . . 12  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( pi  mod  T )  =  pi )
120105, 108, 1193eqtrd 2447 . . . . . . . . . . 11  |-  ( ( k  e.  ZZ  /\  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi ) )  ->  ( X  mod  T )  =  pi )
121120ex 432 . . . . . . . . . 10  |-  ( k  e.  ZZ  ->  (
( ( 2  x.  k )  +  1 )  =  ( X  /  pi )  -> 
( X  mod  T
)  =  pi ) )
122121a1i 11 . . . . . . . . 9  |-  ( ( ( X  mod  pi )  =  0  /\  -.  2  ||  ( X  /  pi ) )  ->  ( k  e.  ZZ  ->  ( (
( 2  x.  k
)  +  1 )  =  ( X  /  pi )  ->  ( X  mod  T )  =  pi ) ) )
123122rexlimdv 2893 . . . . . . . 8  |-  ( ( ( X  mod  pi )  =  0  /\  -.  2  ||  ( X  /  pi ) )  ->  ( E. k  e.  ZZ  ( ( 2  x.  k )  +  1 )  =  ( X  /  pi )  ->  ( X  mod  T )  =  pi ) )
12470, 123mpd 15 . . . . . . 7  |-  ( ( ( X  mod  pi )  =  0  /\  -.  2  ||  ( X  /  pi ) )  ->  ( X  mod  T )  =  pi )
125124olcd 391 . . . . . 6  |-  ( ( ( X  mod  pi )  =  0  /\  -.  2  ||  ( X  /  pi ) )  ->  ( ( X  mod  T )  =  0  \/  ( X  mod  T )  =  pi ) )
12667, 125pm2.61dan 792 . . . . 5  |-  ( ( X  mod  pi )  =  0  ->  (
( X  mod  T
)  =  0  \/  ( X  mod  T
)  =  pi ) )
127 0xr 9669 . . . . . . . 8  |-  0  e.  RR*
12833rexri 9675 . . . . . . . 8  |-  pi  e.  RR*
129 iocgtlb 36884 . . . . . . . 8  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  ( X  mod  T )  e.  ( 0 (,] pi ) )  ->  0  <  ( X  mod  T
) )
130127, 128, 129mp3an12 1316 . . . . . . 7  |-  ( ( X  mod  T )  e.  ( 0 (,] pi )  ->  0  <  ( X  mod  T
) )
131130gt0ne0d 10156 . . . . . 6  |-  ( ( X  mod  T )  e.  ( 0 (,] pi )  ->  ( X  mod  T )  =/=  0 )
132131neneqd 2605 . . . . 5  |-  ( ( X  mod  T )  e.  ( 0 (,] pi )  ->  -.  ( X  mod  T )  =  0 )
133 pm2.53 371 . . . . . 6  |-  ( ( ( X  mod  T
)  =  0  \/  ( X  mod  T
)  =  pi )  ->  ( -.  ( X  mod  T )  =  0  ->  ( X  mod  T )  =  pi ) )
134133imp 427 . . . . 5  |-  ( ( ( ( X  mod  T )  =  0  \/  ( X  mod  T
)  =  pi )  /\  -.  ( X  mod  T )  =  0 )  ->  ( X  mod  T )  =  pi )
135126, 132, 134syl2anr 476 . . . 4  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  ( X  mod  pi )  =  0 )  -> 
( X  mod  T
)  =  pi )
136127a1i 11 . . . . . . . . . . . 12  |-  ( ( X  mod  T )  =  pi  ->  0  e.  RR* )
137128a1i 11 . . . . . . . . . . . 12  |-  ( ( X  mod  T )  =  pi  ->  pi  e.  RR* )
138 modcl 12036 . . . . . . . . . . . . . . 15  |-  ( ( X  e.  RR  /\  T  e.  RR+ )  -> 
( X  mod  T
)  e.  RR )
1394, 63, 138mp2an 670 . . . . . . . . . . . . . 14  |-  ( X  mod  T )  e.  RR
140139rexri 9675 . . . . . . . . . . . . 13  |-  ( X  mod  T )  e. 
RR*
141140a1i 11 . . . . . . . . . . . 12  |-  ( ( X  mod  T )  =  pi  ->  ( X  mod  T )  e. 
RR* )
142 id 22 . . . . . . . . . . . . 13  |-  ( ( X  mod  T )  =  pi  ->  ( X  mod  T )  =  pi )
14334, 142syl5breqr 4430 . . . . . . . . . . . 12  |-  ( ( X  mod  T )  =  pi  ->  0  <  ( X  mod  T
) )
14433eqlei2 9726 . . . . . . . . . . . 12  |-  ( ( X  mod  T )  =  pi  ->  ( X  mod  T )  <_  pi )
145136, 137, 141, 143, 144eliocd 36892 . . . . . . . . . . 11  |-  ( ( X  mod  T )  =  pi  ->  ( X  mod  T )  e.  ( 0 (,] pi ) )
146145iftrued 3892 . . . . . . . . . 10  |-  ( ( X  mod  T )  =  pi  ->  if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  =  1 )
147146adantl 464 . . . . . . . . 9  |-  ( ( ( X  mod  pi )  =  0  /\  ( X  mod  T )  =  pi )  ->  if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  =  1 )
148 oveq1 6284 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  mod  T )  =  ( X  mod  T ) )
149148breq1d 4404 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( x  mod  T
)  <  pi  <->  ( X  mod  T )  <  pi ) )
150149ifbid 3906 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
)  =  if ( ( X  mod  T
)  <  pi , 
1 ,  -u 1
) )
151 fourierswlem.f . . . . . . . . . . . . 13  |-  F  =  ( x  e.  RR  |->  if ( ( x  mod  T )  <  pi , 
1 ,  -u 1
) )
152 1ex 9620 . . . . . . . . . . . . . 14  |-  1  e.  _V
153 negex 9853 . . . . . . . . . . . . . 14  |-  -u 1  e.  _V
154152, 153ifex 3952 . . . . . . . . . . . . 13  |-  if ( ( X  mod  T
)  <  pi , 
1 ,  -u 1
)  e.  _V
155150, 151, 154fvmpt 5931 . . . . . . . . . . . 12  |-  ( X  e.  RR  ->  ( F `  X )  =  if ( ( X  mod  T )  < 
pi ,  1 , 
-u 1 ) )
1564, 155ax-mp 5 . . . . . . . . . . 11  |-  ( F `
 X )  =  if ( ( X  mod  T )  < 
pi ,  1 , 
-u 1 )
157139a1i 11 . . . . . . . . . . . . . 14  |-  ( ( X  mod  T )  <  pi  ->  ( X  mod  T )  e.  RR )
158 id 22 . . . . . . . . . . . . . 14  |-  ( ( X  mod  T )  <  pi  ->  ( X  mod  T )  < 
pi )
159157, 158ltned 9752 . . . . . . . . . . . . 13  |-  ( ( X  mod  T )  <  pi  ->  ( X  mod  T )  =/= 
pi )
160159necon2bi 2640 . . . . . . . . . . . 12  |-  ( ( X  mod  T )  =  pi  ->  -.  ( X  mod  T )  <  pi )
161160iffalsed 3895 . . . . . . . . . . 11  |-  ( ( X  mod  T )  =  pi  ->  if ( ( X  mod  T )  <  pi , 
1 ,  -u 1
)  =  -u 1
)
162156, 161syl5eq 2455 . . . . . . . . . 10  |-  ( ( X  mod  T )  =  pi  ->  ( F `  X )  =  -u 1 )
163162adantl 464 . . . . . . . . 9  |-  ( ( ( X  mod  pi )  =  0  /\  ( X  mod  T )  =  pi )  -> 
( F `  X
)  =  -u 1
)
164147, 163oveq12d 6295 . . . . . . . 8  |-  ( ( ( X  mod  pi )  =  0  /\  ( X  mod  T )  =  pi )  -> 
( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1 )  +  ( F `  X
) )  =  ( 1  +  -u 1
) )
165 1pneg1e0 10684 . . . . . . . 8  |-  ( 1  +  -u 1 )  =  0
166164, 165syl6eq 2459 . . . . . . 7  |-  ( ( ( X  mod  pi )  =  0  /\  ( X  mod  T )  =  pi )  -> 
( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1 )  +  ( F `  X
) )  =  0 )
167166oveq1d 6292 . . . . . 6  |-  ( ( ( X  mod  pi )  =  0  /\  ( X  mod  T )  =  pi )  -> 
( ( if ( ( X  mod  T
)  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 )  =  ( 0  /  2
) )
168167adantll 712 . . . . 5  |-  ( ( ( ( X  mod  T )  e.  ( 0 (,] pi )  /\  ( X  mod  pi )  =  0 )  /\  ( X  mod  T )  =  pi )  -> 
( ( if ( ( X  mod  T
)  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 )  =  ( 0  /  2
) )
169 2cn 10646 . . . . . . 7  |-  2  e.  CC
170169, 44div0i 10318 . . . . . 6  |-  ( 0  /  2 )  =  0
171170a1i 11 . . . . 5  |-  ( ( ( ( X  mod  T )  e.  ( 0 (,] pi )  /\  ( X  mod  pi )  =  0 )  /\  ( X  mod  T )  =  pi )  -> 
( 0  /  2
)  =  0 )
172 fourierswlem.y . . . . . . 7  |-  Y  =  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `  X
) )
173 iftrue 3890 . . . . . . 7  |-  ( ( X  mod  pi )  =  0  ->  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `  X ) )  =  0 )
174172, 173syl5req 2456 . . . . . 6  |-  ( ( X  mod  pi )  =  0  ->  0  =  Y )
175174ad2antlr 725 . . . . 5  |-  ( ( ( ( X  mod  T )  e.  ( 0 (,] pi )  /\  ( X  mod  pi )  =  0 )  /\  ( X  mod  T )  =  pi )  -> 
0  =  Y )
176168, 171, 1753eqtrrd 2448 . . . 4  |-  ( ( ( ( X  mod  T )  e.  ( 0 (,] pi )  /\  ( X  mod  pi )  =  0 )  /\  ( X  mod  T )  =  pi )  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 ) )
177135, 176mpdan 666 . . 3  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  ( X  mod  pi )  =  0 )  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 ) )
178 iftrue 3890 . . . . . . 7  |-  ( ( X  mod  T )  e.  ( 0 (,] pi )  ->  if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  =  1 )
179178adantr 463 . . . . . 6  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1 )  =  1 )
180139a1i 11 . . . . . . . 8  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  ( X  mod  T )  e.  RR )
18133a1i 11 . . . . . . . 8  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  pi  e.  RR )
182 iocleub 36885 . . . . . . . . . 10  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  ( X  mod  T )  e.  ( 0 (,] pi ) )  ->  ( X  mod  T )  <_  pi )
183127, 128, 182mp3an12 1316 . . . . . . . . 9  |-  ( ( X  mod  T )  e.  ( 0 (,] pi )  ->  ( X  mod  T )  <_  pi )
184183adantr 463 . . . . . . . 8  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  ( X  mod  T )  <_  pi )
185 ax-1cn 9579 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  CC
186185, 14mulcomi 9631 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  x.  pi )  =  ( pi  x.  1 )
18783, 186eqtr3i 2433 . . . . . . . . . . . . . . . . . 18  |-  pi  =  ( pi  x.  1
)
188187oveq1i 6287 . . . . . . . . . . . . . . . . 17  |-  ( pi  +  ( pi  x.  ( 2  x.  ( |_ `  ( X  /  T ) ) ) ) )  =  ( ( pi  x.  1 )  +  ( pi  x.  ( 2  x.  ( |_ `  ( X  /  T ) ) ) ) )
189169, 14mulcomi 9631 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  x.  pi )  =  ( pi  x.  2 )
19040, 189eqtri 2431 . . . . . . . . . . . . . . . . . . . 20  |-  T  =  ( pi  x.  2 )
191190oveq1i 6287 . . . . . . . . . . . . . . . . . . 19  |-  ( T  x.  ( |_ `  ( X  /  T
) ) )  =  ( ( pi  x.  2 )  x.  ( |_ `  ( X  /  T ) ) )
192111, 62gtneii 9727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  T  =/=  0
1934, 59, 192redivcli 10351 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( X  /  T )  e.  RR
194 flcl 11967 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  /  T )  e.  RR  ->  ( |_ `  ( X  /  T ) )  e.  ZZ )
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( |_
`  ( X  /  T ) )  e.  ZZ
196 zcn 10909 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( |_ `  ( X  /  T ) )  e.  ZZ  ->  ( |_ `  ( X  /  T ) )  e.  CC )
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( |_
`  ( X  /  T ) )  e.  CC
19814, 169, 197mulassi 9634 . . . . . . . . . . . . . . . . . . 19  |-  ( ( pi  x.  2 )  x.  ( |_ `  ( X  /  T
) ) )  =  ( pi  x.  (
2  x.  ( |_
`  ( X  /  T ) ) ) )
199191, 198eqtri 2431 . . . . . . . . . . . . . . . . . 18  |-  ( T  x.  ( |_ `  ( X  /  T
) ) )  =  ( pi  x.  (
2  x.  ( |_
`  ( X  /  T ) ) ) )
200199oveq2i 6288 . . . . . . . . . . . . . . . . 17  |-  ( pi  +  ( T  x.  ( |_ `  ( X  /  T ) ) ) )  =  ( pi  +  ( pi  x.  ( 2  x.  ( |_ `  ( X  /  T ) ) ) ) )
201169, 197mulcli 9630 . . . . . . . . . . . . . . . . . 18  |-  ( 2  x.  ( |_ `  ( X  /  T
) ) )  e.  CC
20214, 185, 201adddii 9635 . . . . . . . . . . . . . . . . 17  |-  ( pi  x.  ( 1  +  ( 2  x.  ( |_ `  ( X  /  T ) ) ) ) )  =  ( ( pi  x.  1 )  +  ( pi  x.  ( 2  x.  ( |_ `  ( X  /  T ) ) ) ) )
203188, 200, 2023eqtr4ri 2442 . . . . . . . . . . . . . . . 16  |-  ( pi  x.  ( 1  +  ( 2  x.  ( |_ `  ( X  /  T ) ) ) ) )  =  ( pi  +  ( T  x.  ( |_ `  ( X  /  T
) ) ) )
204203a1i 11 . . . . . . . . . . . . . . 15  |-  ( pi  =  ( X  mod  T )  ->  ( pi  x.  ( 1  +  ( 2  x.  ( |_
`  ( X  /  T ) ) ) ) )  =  ( pi  +  ( T  x.  ( |_ `  ( X  /  T
) ) ) ) )
205 id 22 . . . . . . . . . . . . . . . . 17  |-  ( pi  =  ( X  mod  T )  ->  pi  =  ( X  mod  T ) )
206 modval 12034 . . . . . . . . . . . . . . . . . 18  |-  ( ( X  e.  RR  /\  T  e.  RR+ )  -> 
( X  mod  T
)  =  ( X  -  ( T  x.  ( |_ `  ( X  /  T ) ) ) ) )
2074, 63, 206mp2an 670 . . . . . . . . . . . . . . . . 17  |-  ( X  mod  T )  =  ( X  -  ( T  x.  ( |_ `  ( X  /  T
) ) ) )
208205, 207syl6eq 2459 . . . . . . . . . . . . . . . 16  |-  ( pi  =  ( X  mod  T )  ->  pi  =  ( X  -  ( T  x.  ( |_ `  ( X  /  T
) ) ) ) )
209208oveq1d 6292 . . . . . . . . . . . . . . 15  |-  ( pi  =  ( X  mod  T )  ->  ( pi  +  ( T  x.  ( |_ `  ( X  /  T ) ) ) )  =  ( ( X  -  ( T  x.  ( |_ `  ( X  /  T
) ) ) )  +  ( T  x.  ( |_ `  ( X  /  T ) ) ) ) )
21027a1i 11 . . . . . . . . . . . . . . . 16  |-  ( pi  =  ( X  mod  T )  ->  X  e.  CC )
21159recni 9637 . . . . . . . . . . . . . . . . . 18  |-  T  e.  CC
212211, 197mulcli 9630 . . . . . . . . . . . . . . . . 17  |-  ( T  x.  ( |_ `  ( X  /  T
) ) )  e.  CC
213212a1i 11 . . . . . . . . . . . . . . . 16  |-  ( pi  =  ( X  mod  T )  ->  ( T  x.  ( |_ `  ( X  /  T ) ) )  e.  CC )
214210, 213npcand 9970 . . . . . . . . . . . . . . 15  |-  ( pi  =  ( X  mod  T )  ->  ( ( X  -  ( T  x.  ( |_ `  ( X  /  T ) ) ) )  +  ( T  x.  ( |_
`  ( X  /  T ) ) ) )  =  X )
215204, 209, 2143eqtrrd 2448 . . . . . . . . . . . . . 14  |-  ( pi  =  ( X  mod  T )  ->  X  =  ( pi  x.  (
1  +  ( 2  x.  ( |_ `  ( X  /  T
) ) ) ) ) )
216215oveq1d 6292 . . . . . . . . . . . . 13  |-  ( pi  =  ( X  mod  T )  ->  ( X  /  pi )  =  ( ( pi  x.  (
1  +  ( 2  x.  ( |_ `  ( X  /  T
) ) ) ) )  /  pi ) )
217185, 201addcli 9629 . . . . . . . . . . . . . 14  |-  ( 1  +  ( 2  x.  ( |_ `  ( X  /  T ) ) ) )  e.  CC
218217, 14, 35divcan3i 10330 . . . . . . . . . . . . 13  |-  ( ( pi  x.  ( 1  +  ( 2  x.  ( |_ `  ( X  /  T ) ) ) ) )  /  pi )  =  (
1  +  ( 2  x.  ( |_ `  ( X  /  T
) ) ) )
219216, 218syl6eq 2459 . . . . . . . . . . . 12  |-  ( pi  =  ( X  mod  T )  ->  ( X  /  pi )  =  ( 1  +  ( 2  x.  ( |_ `  ( X  /  T
) ) ) ) )
220 1z 10934 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
221 zmulcl 10952 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  ZZ  /\  ( |_ `  ( X  /  T ) )  e.  ZZ )  -> 
( 2  x.  ( |_ `  ( X  /  T ) ) )  e.  ZZ )
2222, 195, 221mp2an 670 . . . . . . . . . . . . . 14  |-  ( 2  x.  ( |_ `  ( X  /  T
) ) )  e.  ZZ
223 zaddcl 10944 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  ZZ  /\  ( 2  x.  ( |_ `  ( X  /  T ) ) )  e.  ZZ )  -> 
( 1  +  ( 2  x.  ( |_
`  ( X  /  T ) ) ) )  e.  ZZ )
224220, 222, 223mp2an 670 . . . . . . . . . . . . 13  |-  ( 1  +  ( 2  x.  ( |_ `  ( X  /  T ) ) ) )  e.  ZZ
225224a1i 11 . . . . . . . . . . . 12  |-  ( pi  =  ( X  mod  T )  ->  ( 1  +  ( 2  x.  ( |_ `  ( X  /  T ) ) ) )  e.  ZZ )
226219, 225eqeltrd 2490 . . . . . . . . . . 11  |-  ( pi  =  ( X  mod  T )  ->  ( X  /  pi )  e.  ZZ )
227226, 7sylibr 212 . . . . . . . . . 10  |-  ( pi  =  ( X  mod  T )  ->  ( X  mod  pi )  =  0 )
228227necon3bi 2632 . . . . . . . . 9  |-  ( -.  ( X  mod  pi )  =  0  ->  pi  =/=  ( X  mod  T ) )
229228adantl 464 . . . . . . . 8  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  pi  =/=  ( X  mod  T ) )
230180, 181, 184, 229leneltd 36844 . . . . . . 7  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  ( X  mod  T )  <  pi )
231 iftrue 3890 . . . . . . . 8  |-  ( ( X  mod  T )  <  pi  ->  if ( ( X  mod  T )  <  pi , 
1 ,  -u 1
)  =  1 )
232156, 231syl5eq 2455 . . . . . . 7  |-  ( ( X  mod  T )  <  pi  ->  ( F `  X )  =  1 )
233230, 232syl 17 . . . . . 6  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  ( F `  X )  =  1 )
234179, 233oveq12d 6295 . . . . 5  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  ( if ( ( X  mod  T
)  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  =  ( 1  +  1 ) )
235234oveq1d 6292 . . . 4  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 )  =  ( ( 1  +  1 )  /  2
) )
236 1p1e2 10689 . . . . . . 7  |-  ( 1  +  1 )  =  2
237236oveq1i 6287 . . . . . 6  |-  ( ( 1  +  1 )  /  2 )  =  ( 2  /  2
)
238 2div2e1 10698 . . . . . 6  |-  ( 2  /  2 )  =  1
239237, 238eqtr2i 2432 . . . . 5  |-  1  =  ( ( 1  +  1 )  / 
2 )
240233, 239syl6req 2460 . . . 4  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  ( ( 1  +  1 )  / 
2 )  =  ( F `  X ) )
241 iffalse 3893 . . . . . 6  |-  ( -.  ( X  mod  pi )  =  0  ->  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `  X ) )  =  ( F `
 X ) )
242172, 241syl5req 2456 . . . . 5  |-  ( -.  ( X  mod  pi )  =  0  ->  ( F `  X )  =  Y )
243242adantl 464 . . . 4  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  ( F `  X )  =  Y )
244235, 240, 2433eqtrrd 2448 . . 3  |-  ( ( ( X  mod  T
)  e.  ( 0 (,] pi )  /\  -.  ( X  mod  pi )  =  0 )  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1 )  +  ( F `  X
) )  /  2
) )
245177, 244pm2.61dan 792 . 2  |-  ( ( X  mod  T )  e.  ( 0 (,] pi )  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 ) )
246131necon2bi 2640 . . . . . . . 8  |-  ( ( X  mod  T )  =  0  ->  -.  ( X  mod  T )  e.  ( 0 (,] pi ) )
247246iffalsed 3895 . . . . . . 7  |-  ( ( X  mod  T )  =  0  ->  if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  =  -u 1
)
248 id 22 . . . . . . . . . 10  |-  ( ( X  mod  T )  =  0  ->  ( X  mod  T )  =  0 )
249248, 34syl6eqbr 4431 . . . . . . . . 9  |-  ( ( X  mod  T )  =  0  ->  ( X  mod  T )  < 
pi )
250249iftrued 3892 . . . . . . . 8  |-  ( ( X  mod  T )  =  0  ->  if ( ( X  mod  T )  <  pi , 
1 ,  -u 1
)  =  1 )
251156, 250syl5eq 2455 . . . . . . 7  |-  ( ( X  mod  T )  =  0  ->  ( F `  X )  =  1 )
252247, 251oveq12d 6295 . . . . . 6  |-  ( ( X  mod  T )  =  0  ->  ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  =  ( -u 1  +  1 ) )
253252oveq1d 6292 . . . . 5  |-  ( ( X  mod  T )  =  0  ->  (
( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1 )  +  ( F `  X
) )  /  2
)  =  ( (
-u 1  +  1 )  /  2 ) )
254 neg1cn 10679 . . . . . . . . 9  |-  -u 1  e.  CC
255185, 254, 165addcomli 9805 . . . . . . . 8  |-  ( -u
1  +  1 )  =  0
256255oveq1i 6287 . . . . . . 7  |-  ( (
-u 1  +  1 )  /  2 )  =  ( 0  / 
2 )
257256, 170eqtri 2431 . . . . . 6  |-  ( (
-u 1  +  1 )  /  2 )  =  0
258257a1i 11 . . . . 5  |-  ( ( X  mod  T )  =  0  ->  (
( -u 1  +  1 )  /  2 )  =  0 )
25940oveq2i 6288 . . . . . . . . . . . . 13  |-  ( X  /  T )  =  ( X  /  (
2  x.  pi ) )
260 2cnne0 10790 . . . . . . . . . . . . . 14  |-  ( 2  e.  CC  /\  2  =/=  0 )
26114, 35pm3.2i 453 . . . . . . . . . . . . . 14  |-  ( pi  e.  CC  /\  pi  =/=  0 )
262 divdiv1 10295 . . . . . . . . . . . . . 14  |-  ( ( X  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 )  /\  ( pi  e.  CC  /\  pi  =/=  0
) )  ->  (
( X  /  2
)  /  pi )  =  ( X  / 
( 2  x.  pi ) ) )
26327, 260, 261, 262mp3an 1326 . . . . . . . . . . . . 13  |-  ( ( X  /  2 )  /  pi )  =  ( X  /  (
2  x.  pi ) )
26427, 169, 14, 44, 35divdiv32i 10339 . . . . . . . . . . . . 13  |-  ( ( X  /  2 )  /  pi )  =  ( ( X  /  pi )  /  2
)
265259, 263, 2643eqtr2i 2437 . . . . . . . . . . . 12  |-  ( X  /  T )  =  ( ( X  /  pi )  /  2
)
266265oveq2i 6288 . . . . . . . . . . 11  |-  ( 2  x.  ( X  /  T ) )  =  ( 2  x.  (
( X  /  pi )  /  2 ) )
26727, 14, 35divcli 10326 . . . . . . . . . . . 12  |-  ( X  /  pi )  e.  CC
268267, 169, 44divcan2i 10327 . . . . . . . . . . 11  |-  ( 2  x.  ( ( X  /  pi )  / 
2 ) )  =  ( X  /  pi )
269266, 268eqtr2i 2432 . . . . . . . . . 10  |-  ( X  /  pi )  =  ( 2  x.  ( X  /  T ) )
2702a1i 11 . . . . . . . . . . 11  |-  ( ( X  /  T )  e.  ZZ  ->  2  e.  ZZ )
271 id 22 . . . . . . . . . . 11  |-  ( ( X  /  T )  e.  ZZ  ->  ( X  /  T )  e.  ZZ )
272270, 271zmulcld 11013 . . . . . . . . . 10  |-  ( ( X  /  T )  e.  ZZ  ->  (
2  x.  ( X  /  T ) )  e.  ZZ )
273269, 272syl5eqel 2494 . . . . . . . . 9  |-  ( ( X  /  T )  e.  ZZ  ->  ( X  /  pi )  e.  ZZ )
27465, 273sylbi 195 . . . . . . . 8  |-  ( ( X  mod  T )  =  0  ->  ( X  /  pi )  e.  ZZ )
275274, 7sylibr 212 . . . . . . 7  |-  ( ( X  mod  T )  =  0  ->  ( X  mod  pi )  =  0 )
276275iftrued 3892 . . . . . 6  |-  ( ( X  mod  T )  =  0  ->  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `  X ) )  =  0 )
277172, 276syl5req 2456 . . . . 5  |-  ( ( X  mod  T )  =  0  ->  0  =  Y )
278253, 258, 2773eqtrrd 2448 . . . 4  |-  ( ( X  mod  T )  =  0  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 ) )
279278adantl 464 . . 3  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  ( X  mod  T )  =  0 )  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 ) )
280128a1i 11 . . . . 5  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  pi  e.  RR* )
28159rexri 9675 . . . . . 6  |-  T  e. 
RR*
282281a1i 11 . . . . 5  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  T  e.  RR* )
283139a1i 11 . . . . 5  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  ( X  mod  T )  e.  RR )
284 pm4.56 493 . . . . . . . 8  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  <->  -.  ( ( X  mod  T )  e.  ( 0 (,] pi )  \/  ( X  mod  T
)  =  0 ) )
285284biimpi 194 . . . . . . 7  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  -.  ( ( X  mod  T )  e.  ( 0 (,] pi )  \/  ( X  mod  T )  =  0 ) )
286 olc 382 . . . . . . . . 9  |-  ( ( X  mod  T )  =  0  ->  (
( X  mod  T
)  e.  ( 0 (,] pi )  \/  ( X  mod  T
)  =  0 ) )
287286adantl 464 . . . . . . . 8  |-  ( ( ( X  mod  T
)  <_  pi  /\  ( X  mod  T )  =  0 )  -> 
( ( X  mod  T )  e.  ( 0 (,] pi )  \/  ( X  mod  T
)  =  0 ) )
288127a1i 11 . . . . . . . . . 10  |-  ( ( ( X  mod  T
)  <_  pi  /\  -.  ( X  mod  T
)  =  0 )  ->  0  e.  RR* )
289128a1i 11 . . . . . . . . . 10  |-  ( ( ( X  mod  T
)  <_  pi  /\  -.  ( X  mod  T
)  =  0 )  ->  pi  e.  RR* )
290140a1i 11 . . . . . . . . . 10  |-  ( ( ( X  mod  T
)  <_  pi  /\  -.  ( X  mod  T
)  =  0 )  ->  ( X  mod  T )  e.  RR* )
291 0red 9626 . . . . . . . . . . . 12  |-  ( -.  ( X  mod  T
)  =  0  -> 
0  e.  RR )
292139a1i 11 . . . . . . . . . . . 12  |-  ( -.  ( X  mod  T
)  =  0  -> 
( X  mod  T
)  e.  RR )
293 modge0 12042 . . . . . . . . . . . . . 14  |-  ( ( X  e.  RR  /\  T  e.  RR+ )  -> 
0  <_  ( X  mod  T ) )
2944, 63, 293mp2an 670 . . . . . . . . . . . . 13  |-  0  <_  ( X  mod  T
)
295294a1i 11 . . . . . . . . . . . 12  |-  ( -.  ( X  mod  T
)  =  0  -> 
0  <_  ( X  mod  T ) )
296 neqne 36790 . . . . . . . . . . . 12  |-  ( -.  ( X  mod  T
)  =  0  -> 
( X  mod  T
)  =/=  0 )
297291, 292, 295, 296leneltd 36844 . . . . . . . . . . 11  |-  ( -.  ( X  mod  T
)  =  0  -> 
0  <  ( X  mod  T ) )
298297adantl 464 . . . . . . . . . 10  |-  ( ( ( X  mod  T
)  <_  pi  /\  -.  ( X  mod  T
)  =  0 )  ->  0  <  ( X  mod  T ) )
299 simpl 455 . . . . . . . . . 10  |-  ( ( ( X  mod  T
)  <_  pi  /\  -.  ( X  mod  T
)  =  0 )  ->  ( X  mod  T )  <_  pi )
300288, 289, 290, 298, 299eliocd 36892 . . . . . . . . 9  |-  ( ( ( X  mod  T
)  <_  pi  /\  -.  ( X  mod  T
)  =  0 )  ->  ( X  mod  T )  e.  ( 0 (,] pi ) )
301300orcd 390 . . . . . . . 8  |-  ( ( ( X  mod  T
)  <_  pi  /\  -.  ( X  mod  T
)  =  0 )  ->  ( ( X  mod  T )  e.  ( 0 (,] pi )  \/  ( X  mod  T )  =  0 ) )
302287, 301pm2.61dan 792 . . . . . . 7  |-  ( ( X  mod  T )  <_  pi  ->  (
( X  mod  T
)  e.  ( 0 (,] pi )  \/  ( X  mod  T
)  =  0 ) )
303285, 302nsyl 121 . . . . . 6  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  -.  ( X  mod  T )  <_  pi )
30433a1i 11 . . . . . . 7  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  pi  e.  RR )
305304, 283ltnled 9763 . . . . . 6  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  ( pi  <  ( X  mod  T )  <->  -.  ( X  mod  T
)  <_  pi )
)
306303, 305mpbird 232 . . . . 5  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  pi  <  ( X  mod  T ) )
307 modlt 12043 . . . . . . 7  |-  ( ( X  e.  RR  /\  T  e.  RR+ )  -> 
( X  mod  T
)  <  T )
3084, 63, 307mp2an 670 . . . . . 6  |-  ( X  mod  T )  < 
T
309308a1i 11 . . . . 5  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  ( X  mod  T )  <  T )
310280, 282, 283, 306, 309eliood 36880 . . . 4  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  ( X  mod  T )  e.  ( pi
(,) T ) )
311127a1i 11 . . . . . . . . 9  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  0  e.  RR* )
31233a1i 11 . . . . . . . . 9  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  pi  e.  RR )
313140a1i 11 . . . . . . . . 9  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  ( X  mod  T )  e. 
RR* )
314 ioogtlb 36877 . . . . . . . . . 10  |-  ( ( pi  e.  RR*  /\  T  e.  RR*  /\  ( X  mod  T )  e.  ( pi (,) T
) )  ->  pi  <  ( X  mod  T
) )
315128, 281, 314mp3an12 1316 . . . . . . . . 9  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  pi  <  ( X  mod  T
) )
316311, 312, 313, 315gtnelioc 36872 . . . . . . . 8  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  -.  ( X  mod  T )  e.  ( 0 (,] pi ) )
317316iffalsed 3895 . . . . . . 7  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  =  -u 1
)
318139a1i 11 . . . . . . . . . 10  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  ( X  mod  T )  e.  RR )
319312, 318, 315ltnsymd 9765 . . . . . . . . 9  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  -.  ( X  mod  T )  <  pi )
320319iffalsed 3895 . . . . . . . 8  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  if ( ( X  mod  T )  <  pi , 
1 ,  -u 1
)  =  -u 1
)
321156, 320syl5eq 2455 . . . . . . 7  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  ( F `  X )  =  -u 1 )
322317, 321oveq12d 6295 . . . . . 6  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  =  ( -u 1  +  -u 1 ) )
323322oveq1d 6292 . . . . 5  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  (
( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1 )  +  ( F `  X
) )  /  2
)  =  ( (
-u 1  +  -u
1 )  /  2
) )
324 df-2 10634 . . . . . . . . . 10  |-  2  =  ( 1  +  1 )
325324negeqi 9848 . . . . . . . . 9  |-  -u 2  =  -u ( 1  +  1 )
326185, 185negdii 9938 . . . . . . . . 9  |-  -u (
1  +  1 )  =  ( -u 1  +  -u 1 )
327325, 326eqtr2i 2432 . . . . . . . 8  |-  ( -u
1  +  -u 1
)  =  -u 2
328327oveq1i 6287 . . . . . . 7  |-  ( (
-u 1  +  -u
1 )  /  2
)  =  ( -u
2  /  2 )
329 divneg 10279 . . . . . . . 8  |-  ( ( 2  e.  CC  /\  2  e.  CC  /\  2  =/=  0 )  ->  -u (
2  /  2 )  =  ( -u 2  /  2 ) )
330169, 169, 44, 329mp3an 1326 . . . . . . 7  |-  -u (
2  /  2 )  =  ( -u 2  /  2 )
331238negeqi 9848 . . . . . . 7  |-  -u (
2  /  2 )  =  -u 1
332328, 330, 3313eqtr2i 2437 . . . . . 6  |-  ( (
-u 1  +  -u
1 )  /  2
)  =  -u 1
333332a1i 11 . . . . 5  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  (
( -u 1  +  -u
1 )  /  2
)  =  -u 1
)
334172a1i 11 . . . . . 6  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  Y  =  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `  X
) ) )
335312, 318ltnled 9763 . . . . . . . . 9  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  (
pi  <  ( X  mod  T )  <->  -.  ( X  mod  T )  <_  pi ) )
336315, 335mpbid 210 . . . . . . . 8  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  -.  ( X  mod  T )  <_  pi )
337248, 112syl6eqbr 4431 . . . . . . . . . 10  |-  ( ( X  mod  T )  =  0  ->  ( X  mod  T )  <_  pi )
338337adantl 464 . . . . . . . . 9  |-  ( ( ( X  mod  pi )  =  0  /\  ( X  mod  T )  =  0 )  -> 
( X  mod  T
)  <_  pi )
339126orcanai 914 . . . . . . . . . 10  |-  ( ( ( X  mod  pi )  =  0  /\  -.  ( X  mod  T
)  =  0 )  ->  ( X  mod  T )  =  pi )
340339, 144syl 17 . . . . . . . . 9  |-  ( ( ( X  mod  pi )  =  0  /\  -.  ( X  mod  T
)  =  0 )  ->  ( X  mod  T )  <_  pi )
341338, 340pm2.61dan 792 . . . . . . . 8  |-  ( ( X  mod  pi )  =  0  ->  ( X  mod  T )  <_  pi )
342336, 341nsyl 121 . . . . . . 7  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  -.  ( X  mod  pi )  =  0 )
343342iffalsed 3895 . . . . . 6  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `  X ) )  =  ( F `
 X ) )
344334, 343, 3213eqtrrd 2448 . . . . 5  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  -u 1  =  Y )
345323, 333, 3443eqtrrd 2448 . . . 4  |-  ( ( X  mod  T )  e.  ( pi (,) T )  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 ) )
346310, 345syl 17 . . 3  |-  ( ( -.  ( X  mod  T )  e.  ( 0 (,] pi )  /\  -.  ( X  mod  T
)  =  0 )  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1 )  +  ( F `  X
) )  /  2
) )
347279, 346pm2.61dan 792 . 2  |-  ( -.  ( X  mod  T
)  e.  ( 0 (,] pi )  ->  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 ) )
348245, 347pm2.61i 164 1  |-  Y  =  ( ( if ( ( X  mod  T
)  e.  ( 0 (,] pi ) ,  1 ,  -u 1
)  +  ( F `
 X ) )  /  2 )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    = wceq 1405    e. wcel 1842    =/= wne 2598   E.wrex 2754   ifcif 3884   class class class wbr 4394    |-> cmpt 4452   ` cfv 5568  (class class class)co 6277   CCcc 9519   RRcr 9520   0cc0 9521   1c1 9522    + caddc 9524    x. cmul 9526   RR*cxr 9656    < clt 9657    <_ cle 9658    - cmin 9840   -ucneg 9841    / cdiv 10246   2c2 10625   ZZcz 10904   RR+crp 11264   (,)cioo 11581   (,]cioc 11582   |_cfl 11962    mod cmo 12032   picpi 14009    || cdvds 14193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-inf2 8090  ax-cnex 9577  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-mulcom 9585  ax-addass 9586  ax-mulass 9587  ax-distr 9588  ax-i2m1 9589  ax-1ne0 9590  ax-1rid 9591  ax-rnegex 9592  ax-rrecex 9593  ax-cnre 9594  ax-pre-lttri 9595  ax-pre-lttrn 9596  ax-pre-ltadd 9597  ax-pre-mulgt0 9598  ax-pre-sup 9599  ax-addf 9600  ax-mulf 9601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-iin 4273  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-isom 5577  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6520  df-om 6683  df-1st 6783  df-2nd 6784  df-supp 6902  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-1o 7166  df-2o 7167  df-oadd 7170  df-er 7347  df-map 7458  df-pm 7459  df-ixp 7507  df-en 7554  df-dom 7555  df-sdom 7556  df-fin 7557  df-fsupp 7863  df-fi 7904  df-sup 7934  df-oi 7968  df-card 8351  df-cda 8579  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-sub 9842  df-neg 9843  df-div 10247  df-nn 10576  df-2 10634  df-3 10635  df-4 10636  df-5 10637  df-6 10638  df-7 10639  df-8 10640  df-9 10641  df-10 10642  df-n0 10836  df-z 10905  df-dec 11019  df-uz 11127  df-q 11227  df-rp 11265  df-xneg 11370  df-xadd 11371  df-xmul 11372  df-ioo 11585  df-ioc 11586  df-ico 11587  df-icc 11588  df-fz 11725  df-fzo 11853  df-fl 11964  df-mod 12033  df-seq 12150  df-exp 12209  df-fac 12396  df-bc 12423  df-hash 12451  df-shft 13047  df-cj 13079  df-re 13080  df-im 13081  df-sqrt 13215  df-abs 13216  df-limsup 13441  df-clim 13458  df-rlim 13459  df-sum 13656  df-ef 14010  df-sin 14012  df-cos 14013  df-pi 14015  df-dvds 14194  df-struct 14841  df-ndx 14842  df-slot 14843  df-base 14844  df-sets 14845  df-ress 14846  df-plusg 14920  df-mulr 14921  df-starv 14922  df-sca 14923  df-vsca 14924  df-ip 14925  df-tset 14926  df-ple 14927  df-ds 14929  df-unif 14930  df-hom 14931  df-cco 14932  df-rest 15035  df-topn 15036  df-0g 15054  df-gsum 15055  df-topgen 15056  df-pt 15057  df-prds 15060  df-xrs 15114  df-qtop 15119  df-imas 15120  df-xps 15122  df-mre 15198  df-mrc 15199  df-acs 15201  df-mgm 16194  df-sgrp 16233  df-mnd 16243  df-submnd 16289  df-mulg 16382  df-cntz 16677  df-cmn 17122  df-psmet 18729  df-xmet 18730  df-met 18731  df-bl 18732  df-mopn 18733  df-fbas 18734  df-fg 18735  df-cnfld 18739  df-top 19689  df-bases 19691  df-topon 19692  df-topsp 19693  df-cld 19810  df-ntr 19811  df-cls 19812  df-nei 19890  df-lp 19928  df-perf 19929  df-cn 20019  df-cnp 20020  df-haus 20107  df-tx 20353  df-hmeo 20546  df-fil 20637  df-fm 20729  df-flim 20730  df-flf 20731  df-xms 21113  df-ms 21114  df-tms 21115  df-cncf 21672  df-limc 22560  df-dv 22561
This theorem is referenced by:  fouriersw  37363
  Copyright terms: Public domain W3C validator