MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisum0flblem2 Structured version   Unicode version

Theorem dchrisum0flblem2 21205
Description: Lemma for dchrisum0flb 21206. Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z  |-  Z  =  (ℤ/n `  N )
rpvmasum.l  |-  L  =  ( ZRHom `  Z
)
rpvmasum.a  |-  ( ph  ->  N  e.  NN )
rpvmasum2.g  |-  G  =  (DChr `  N )
rpvmasum2.d  |-  D  =  ( Base `  G
)
rpvmasum2.1  |-  .1.  =  ( 0g `  G )
dchrisum0f.f  |-  F  =  ( b  e.  NN  |->  sum_ v  e.  { q  e.  NN  |  q 
||  b }  ( X `  ( L `  v ) ) )
dchrisum0f.x  |-  ( ph  ->  X  e.  D )
dchrisum0flb.r  |-  ( ph  ->  X : ( Base `  Z ) --> RR )
dchrisum0flb.1  |-  ( ph  ->  A  e.  ( ZZ>= ` 
2 ) )
dchrisum0flb.2  |-  ( ph  ->  P  e.  Prime )
dchrisum0flb.3  |-  ( ph  ->  P  ||  A )
dchrisum0flb.4  |-  ( ph  ->  A. y  e.  ( 1..^ A ) if ( ( sqr `  y
)  e.  NN , 
1 ,  0 )  <_  ( F `  y ) )
Assertion
Ref Expression
dchrisum0flblem2  |-  ( ph  ->  if ( ( sqr `  A )  e.  NN ,  1 ,  0 )  <_  ( F `  A ) )
Distinct variable groups:    y,  .1.    y, F    q, b, v, y, A    N, q,
y    P, b, q, v, y    y, Z    y, D    L, b, v, y    X, b, v, y
Allowed substitution hints:    ph( y, v, q, b)    D( v, q, b)    .1. ( v,
q, b)    F( v,
q, b)    G( y,
v, q, b)    L( q)    N( v, b)    X( q)    Z( v, q, b)

Proof of Theorem dchrisum0flblem2
StepHypRef Expression
1 breq1 4217 . . 3  |-  ( 1  =  if ( ( sqr `  A )  e.  NN ,  1 ,  0 )  -> 
( 1  <_  (
( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )  <->  if ( ( sqr `  A )  e.  NN ,  1 ,  0 )  <_  ( ( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) ) )
2 breq1 4217 . . 3  |-  ( 0  =  if ( ( sqr `  A )  e.  NN ,  1 ,  0 )  -> 
( 0  <_  (
( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )  <->  if ( ( sqr `  A )  e.  NN ,  1 ,  0 )  <_  ( ( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) ) )
3 1t1e1 10128 . . . 4  |-  ( 1  x.  1 )  =  1
4 dchrisum0flb.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  Prime )
54adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  P  e.  Prime )
6 nnq 10589 . . . . . . . . . . . . . . 15  |-  ( ( sqr `  A )  e.  NN  ->  ( sqr `  A )  e.  QQ )
76adantl 454 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  A
)  e.  QQ )
8 nnne0 10034 . . . . . . . . . . . . . . 15  |-  ( ( sqr `  A )  e.  NN  ->  ( sqr `  A )  =/=  0 )
98adantl 454 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  A
)  =/=  0 )
10 2z 10314 . . . . . . . . . . . . . . 15  |-  2  e.  ZZ
1110a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  2  e.  ZZ )
12 pcexp 13235 . . . . . . . . . . . . . 14  |-  ( ( P  e.  Prime  /\  (
( sqr `  A
)  e.  QQ  /\  ( sqr `  A )  =/=  0 )  /\  2  e.  ZZ )  ->  ( P  pCnt  (
( sqr `  A
) ^ 2 ) )  =  ( 2  x.  ( P  pCnt  ( sqr `  A ) ) ) )
135, 7, 9, 11, 12syl121anc 1190 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P  pCnt  ( ( sqr `  A
) ^ 2 ) )  =  ( 2  x.  ( P  pCnt  ( sqr `  A ) ) ) )
14 dchrisum0flb.1 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  ( ZZ>= ` 
2 ) )
15 eluz2b2 10550 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  ( ZZ>= `  2
)  <->  ( A  e.  NN  /\  1  < 
A ) )
1615simplbi 448 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  ( ZZ>= `  2
)  ->  A  e.  NN )
1714, 16syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  e.  NN )
1817nncnd 10018 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  CC )
1918adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  A  e.  CC )
2019sqsqrd 12243 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( ( sqr `  A ) ^ 2 )  =  A )
2120oveq2d 6099 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P  pCnt  ( ( sqr `  A
) ^ 2 ) )  =  ( P 
pCnt  A ) )
22 2cn 10072 . . . . . . . . . . . . . . 15  |-  2  e.  CC
2322a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  2  e.  CC )
24 simpr 449 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  A
)  e.  NN )
255, 24pccld 13226 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P  pCnt  ( sqr `  A ) )  e.  NN0 )
2625nn0cnd 10278 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P  pCnt  ( sqr `  A ) )  e.  CC )
2723, 26mulcomd 9111 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( 2  x.  ( P  pCnt  ( sqr `  A ) ) )  =  ( ( P  pCnt  ( sqr `  A ) )  x.  2 ) )
2813, 21, 273eqtr3rd 2479 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( ( P 
pCnt  ( sqr `  A
) )  x.  2 )  =  ( P 
pCnt  A ) )
2928oveq2d 6099 . . . . . . . . . . 11  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P ^
( ( P  pCnt  ( sqr `  A ) )  x.  2 ) )  =  ( P ^ ( P  pCnt  A ) ) )
30 prmnn 13084 . . . . . . . . . . . . . 14  |-  ( P  e.  Prime  ->  P  e.  NN )
315, 30syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  P  e.  NN )
3231nncnd 10018 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  P  e.  CC )
33 2nn0 10240 . . . . . . . . . . . . 13  |-  2  e.  NN0
3433a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  2  e.  NN0 )
3532, 34, 25expmuld 11528 . . . . . . . . . . 11  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P ^
( ( P  pCnt  ( sqr `  A ) )  x.  2 ) )  =  ( ( P ^ ( P 
pCnt  ( sqr `  A
) ) ) ^
2 ) )
3629, 35eqtr3d 2472 . . . . . . . . . 10  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P ^
( P  pCnt  A
) )  =  ( ( P ^ ( P  pCnt  ( sqr `  A
) ) ) ^
2 ) )
3736fveq2d 5734 . . . . . . . . 9  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  ( P ^ ( P  pCnt  A ) ) )  =  ( sqr `  (
( P ^ ( P  pCnt  ( sqr `  A
) ) ) ^
2 ) ) )
3831, 25nnexpcld 11546 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P ^
( P  pCnt  ( sqr `  A ) ) )  e.  NN )
3938nnrpd 10649 . . . . . . . . . . 11  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P ^
( P  pCnt  ( sqr `  A ) ) )  e.  RR+ )
4039rprege0d 10657 . . . . . . . . . 10  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( ( P ^ ( P  pCnt  ( sqr `  A ) ) )  e.  RR  /\  0  <_  ( P ^ ( P  pCnt  ( sqr `  A ) ) ) ) )
41 sqrsq 12077 . . . . . . . . . 10  |-  ( ( ( P ^ ( P  pCnt  ( sqr `  A
) ) )  e.  RR  /\  0  <_ 
( P ^ ( P  pCnt  ( sqr `  A
) ) ) )  ->  ( sqr `  (
( P ^ ( P  pCnt  ( sqr `  A
) ) ) ^
2 ) )  =  ( P ^ ( P  pCnt  ( sqr `  A
) ) ) )
4240, 41syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  (
( P ^ ( P  pCnt  ( sqr `  A
) ) ) ^
2 ) )  =  ( P ^ ( P  pCnt  ( sqr `  A
) ) ) )
4337, 42eqtrd 2470 . . . . . . . 8  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  ( P ^ ( P  pCnt  A ) ) )  =  ( P ^ ( P  pCnt  ( sqr `  A
) ) ) )
4443, 38eqeltrd 2512 . . . . . . 7  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN )
45 iftrue 3747 . . . . . . 7  |-  ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN  ->  if (
( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 )  =  1 )
4644, 45syl 16 . . . . . 6  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 )  =  1 )
47 rpvmasum.z . . . . . . . 8  |-  Z  =  (ℤ/n `  N )
48 rpvmasum.l . . . . . . . 8  |-  L  =  ( ZRHom `  Z
)
49 rpvmasum.a . . . . . . . 8  |-  ( ph  ->  N  e.  NN )
50 rpvmasum2.g . . . . . . . 8  |-  G  =  (DChr `  N )
51 rpvmasum2.d . . . . . . . 8  |-  D  =  ( Base `  G
)
52 rpvmasum2.1 . . . . . . . 8  |-  .1.  =  ( 0g `  G )
53 dchrisum0f.f . . . . . . . 8  |-  F  =  ( b  e.  NN  |->  sum_ v  e.  { q  e.  NN  |  q 
||  b }  ( X `  ( L `  v ) ) )
54 dchrisum0f.x . . . . . . . 8  |-  ( ph  ->  X  e.  D )
55 dchrisum0flb.r . . . . . . . 8  |-  ( ph  ->  X : ( Base `  Z ) --> RR )
564, 17pccld 13226 . . . . . . . 8  |-  ( ph  ->  ( P  pCnt  A
)  e.  NN0 )
5747, 48, 49, 50, 51, 52, 53, 54, 55, 4, 56dchrisum0flblem1 21204 . . . . . . 7  |-  ( ph  ->  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN , 
1 ,  0 )  <_  ( F `  ( P ^ ( P 
pCnt  A ) ) ) )
5857adantr 453 . . . . . 6  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 )  <_  ( F `  ( P ^ ( P  pCnt  A ) ) ) )
5946, 58eqbrtrrd 4236 . . . . 5  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  1  <_  ( F `  ( P ^ ( P  pCnt  A ) ) ) )
60 pcdvds 13239 . . . . . . . . . . . . 13  |-  ( ( P  e.  Prime  /\  A  e.  NN )  ->  ( P ^ ( P  pCnt  A ) )  ||  A
)
614, 17, 60syl2anc 644 . . . . . . . . . . . 12  |-  ( ph  ->  ( P ^ ( P  pCnt  A ) ) 
||  A )
624, 30syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  e.  NN )
6362, 56nnexpcld 11546 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P ^ ( P  pCnt  A ) )  e.  NN )
64 nndivdvds 12860 . . . . . . . . . . . . 13  |-  ( ( A  e.  NN  /\  ( P ^ ( P 
pCnt  A ) )  e.  NN )  ->  (
( P ^ ( P  pCnt  A ) ) 
||  A  <->  ( A  /  ( P ^
( P  pCnt  A
) ) )  e.  NN ) )
6517, 63, 64syl2anc 644 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( P ^
( P  pCnt  A
) )  ||  A  <->  ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  NN ) )
6661, 65mpbid 203 . . . . . . . . . . 11  |-  ( ph  ->  ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  NN )
6766nnzd 10376 . . . . . . . . . 10  |-  ( ph  ->  ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  ZZ )
6867adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( A  / 
( P ^ ( P  pCnt  A ) ) )  e.  ZZ )
6917adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  A  e.  NN )
7069nnrpd 10649 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  A  e.  RR+ )
7170rprege0d 10657 . . . . . . . . . . 11  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( A  e.  RR  /\  0  <_  A ) )
7263adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P ^
( P  pCnt  A
) )  e.  NN )
7372nnrpd 10649 . . . . . . . . . . 11  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( P ^
( P  pCnt  A
) )  e.  RR+ )
74 sqrdiv 12073 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( P ^ ( P  pCnt  A ) )  e.  RR+ )  ->  ( sqr `  ( A  / 
( P ^ ( P  pCnt  A ) ) ) )  =  ( ( sqr `  A
)  /  ( sqr `  ( P ^ ( P  pCnt  A ) ) ) ) )
7571, 73, 74syl2anc 644 . . . . . . . . . 10  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  =  ( ( sqr `  A )  /  ( sqr `  ( P ^
( P  pCnt  A
) ) ) ) )
76 nnz 10305 . . . . . . . . . . . 12  |-  ( ( sqr `  A )  e.  NN  ->  ( sqr `  A )  e.  ZZ )
7776adantl 454 . . . . . . . . . . 11  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  A
)  e.  ZZ )
78 znq 10580 . . . . . . . . . . 11  |-  ( ( ( sqr `  A
)  e.  ZZ  /\  ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN )  ->  (
( sqr `  A
)  /  ( sqr `  ( P ^ ( P  pCnt  A ) ) ) )  e.  QQ )
7977, 44, 78syl2anc 644 . . . . . . . . . 10  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( ( sqr `  A )  /  ( sqr `  ( P ^
( P  pCnt  A
) ) ) )  e.  QQ )
8075, 79eqeltrd 2512 . . . . . . . . 9  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  QQ )
81 zsqrelqelz 13152 . . . . . . . . 9  |-  ( ( ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  ZZ  /\  ( sqr `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  e.  QQ )  -> 
( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  ZZ )
8268, 80, 81syl2anc 644 . . . . . . . 8  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  ZZ )
8366adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( A  / 
( P ^ ( P  pCnt  A ) ) )  e.  NN )
8483nnrpd 10649 . . . . . . . . 9  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( A  / 
( P ^ ( P  pCnt  A ) ) )  e.  RR+ )
8584sqrgt0d 12217 . . . . . . . 8  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  0  <  ( sqr `  ( A  / 
( P ^ ( P  pCnt  A ) ) ) ) )
86 elnnz 10294 . . . . . . . 8  |-  ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN  <->  ( ( sqr `  ( A  / 
( P ^ ( P  pCnt  A ) ) ) )  e.  ZZ  /\  0  <  ( sqr `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) ) ) )
8782, 85, 86sylanbrc 647 . . . . . . 7  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN )
88 iftrue 3747 . . . . . . 7  |-  ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN  ->  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 )  =  1 )
8987, 88syl 16 . . . . . 6  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 )  =  1 )
90 nnuz 10523 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
9166, 90syl6eleq 2528 . . . . . . . . 9  |-  ( ph  ->  ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  ( ZZ>= `  1 )
)
9217nnzd 10376 . . . . . . . . 9  |-  ( ph  ->  A  e.  ZZ )
9362nnred 10017 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  RR )
94 dchrisum0flb.3 . . . . . . . . . . . . 13  |-  ( ph  ->  P  ||  A )
95 pcelnn 13245 . . . . . . . . . . . . . 14  |-  ( ( P  e.  Prime  /\  A  e.  NN )  ->  (
( P  pCnt  A
)  e.  NN  <->  P  ||  A
) )
964, 17, 95syl2anc 644 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( P  pCnt  A )  e.  NN  <->  P  ||  A
) )
9794, 96mpbird 225 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  pCnt  A
)  e.  NN )
98 prmuz2 13099 . . . . . . . . . . . . 13  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
99 eluz2b2 10550 . . . . . . . . . . . . . 14  |-  ( P  e.  ( ZZ>= `  2
)  <->  ( P  e.  NN  /\  1  < 
P ) )
10099simprbi 452 . . . . . . . . . . . . 13  |-  ( P  e.  ( ZZ>= `  2
)  ->  1  <  P )
1014, 98, 1003syl 19 . . . . . . . . . . . 12  |-  ( ph  ->  1  <  P )
102 expgt1 11420 . . . . . . . . . . . 12  |-  ( ( P  e.  RR  /\  ( P  pCnt  A )  e.  NN  /\  1  <  P )  ->  1  <  ( P ^ ( P  pCnt  A ) ) )
10393, 97, 101, 102syl3anc 1185 . . . . . . . . . . 11  |-  ( ph  ->  1  <  ( P ^ ( P  pCnt  A ) ) )
104 1re 9092 . . . . . . . . . . . . 13  |-  1  e.  RR
105104a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  1  e.  RR )
10663nnred 10017 . . . . . . . . . . . 12  |-  ( ph  ->  ( P ^ ( P  pCnt  A ) )  e.  RR )
10717nnred 10017 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  RR )
108 0lt1 9552 . . . . . . . . . . . . 13  |-  0  <  1
109108a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  1 )
11063nngt0d 10045 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  ( P ^ ( P  pCnt  A ) ) )
11117nngt0d 10045 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  A )
112 ltdiv2OLD 9898 . . . . . . . . . . . 12  |-  ( ( ( 1  e.  RR  /\  ( P ^ ( P  pCnt  A ) )  e.  RR  /\  A  e.  RR )  /\  (
0  <  1  /\  0  <  ( P ^
( P  pCnt  A
) )  /\  0  <  A ) )  -> 
( 1  <  ( P ^ ( P  pCnt  A ) )  <->  ( A  /  ( P ^
( P  pCnt  A
) ) )  < 
( A  /  1
) ) )
113105, 106, 107, 109, 110, 111, 112syl33anc 1200 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  <  ( P ^ ( P  pCnt  A ) )  <->  ( A  /  ( P ^
( P  pCnt  A
) ) )  < 
( A  /  1
) ) )
114103, 113mpbid 203 . . . . . . . . . 10  |-  ( ph  ->  ( A  /  ( P ^ ( P  pCnt  A ) ) )  < 
( A  /  1
) )
11518div1d 9784 . . . . . . . . . 10  |-  ( ph  ->  ( A  /  1
)  =  A )
116114, 115breqtrd 4238 . . . . . . . . 9  |-  ( ph  ->  ( A  /  ( P ^ ( P  pCnt  A ) ) )  < 
A )
117 elfzo2 11145 . . . . . . . . 9  |-  ( ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  ( 1..^ A )  <-> 
( ( A  / 
( P ^ ( P  pCnt  A ) ) )  e.  ( ZZ>= ` 
1 )  /\  A  e.  ZZ  /\  ( A  /  ( P ^
( P  pCnt  A
) ) )  < 
A ) )
11891, 92, 116, 117syl3anbrc 1139 . . . . . . . 8  |-  ( ph  ->  ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  ( 1..^ A ) )
119 dchrisum0flb.4 . . . . . . . 8  |-  ( ph  ->  A. y  e.  ( 1..^ A ) if ( ( sqr `  y
)  e.  NN , 
1 ,  0 )  <_  ( F `  y ) )
120 fveq2 5730 . . . . . . . . . . . 12  |-  ( y  =  ( A  / 
( P ^ ( P  pCnt  A ) ) )  ->  ( sqr `  y )  =  ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )
121120eleq1d 2504 . . . . . . . . . . 11  |-  ( y  =  ( A  / 
( P ^ ( P  pCnt  A ) ) )  ->  ( ( sqr `  y )  e.  NN  <->  ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ) )
122121ifbid 3759 . . . . . . . . . 10  |-  ( y  =  ( A  / 
( P ^ ( P  pCnt  A ) ) )  ->  if (
( sqr `  y
)  e.  NN , 
1 ,  0 )  =  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 ) )
123 fveq2 5730 . . . . . . . . . 10  |-  ( y  =  ( A  / 
( P ^ ( P  pCnt  A ) ) )  ->  ( F `  y )  =  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )
124122, 123breq12d 4227 . . . . . . . . 9  |-  ( y  =  ( A  / 
( P ^ ( P  pCnt  A ) ) )  ->  ( if ( ( sqr `  y
)  e.  NN , 
1 ,  0 )  <_  ( F `  y )  <->  if (
( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 )  <_ 
( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) )
125124rspcv 3050 . . . . . . . 8  |-  ( ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  ( 1..^ A )  ->  ( A. y  e.  ( 1..^ A ) if ( ( sqr `  y )  e.  NN ,  1 ,  0 )  <_  ( F `  y )  ->  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 )  <_ 
( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) )
126118, 119, 125sylc 59 . . . . . . 7  |-  ( ph  ->  if ( ( sqr `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  e.  NN ,  1 ,  0 )  <_ 
( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )
127126adantr 453 . . . . . 6  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 )  <_ 
( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )
12889, 127eqbrtrrd 4236 . . . . 5  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  1  <_  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )
129 0le1 9553 . . . . . . . 8  |-  0  <_  1
130104, 129pm3.2i 443 . . . . . . 7  |-  ( 1  e.  RR  /\  0  <_  1 )
131130a1i 11 . . . . . 6  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( 1  e.  RR  /\  0  <_ 
1 ) )
13247, 48, 49, 50, 51, 52, 53, 54, 55dchrisum0ff 21203 . . . . . . . 8  |-  ( ph  ->  F : NN --> RR )
133132, 63ffvelrnd 5873 . . . . . . 7  |-  ( ph  ->  ( F `  ( P ^ ( P  pCnt  A ) ) )  e.  RR )
134133adantr 453 . . . . . 6  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( F `  ( P ^ ( P 
pCnt  A ) ) )  e.  RR )
135132, 66ffvelrnd 5873 . . . . . . 7  |-  ( ph  ->  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  RR )
136135adantr 453 . . . . . 6  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( F `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  e.  RR )
137 lemul12a 9870 . . . . . 6  |-  ( ( ( ( 1  e.  RR  /\  0  <_ 
1 )  /\  ( F `  ( P ^ ( P  pCnt  A ) ) )  e.  RR )  /\  (
( 1  e.  RR  /\  0  <_  1 )  /\  ( F `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  e.  RR ) )  ->  ( ( 1  <_  ( F `  ( P ^ ( P 
pCnt  A ) ) )  /\  1  <_  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )  ->  ( 1  x.  1 )  <_ 
( ( F `  ( P ^ ( P 
pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) ) ) ) )
138131, 134, 131, 136, 137syl22anc 1186 . . . . 5  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( ( 1  <_  ( F `  ( P ^ ( P 
pCnt  A ) ) )  /\  1  <_  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) )  ->  ( 1  x.  1 )  <_ 
( ( F `  ( P ^ ( P 
pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) ) ) ) )
13959, 128, 138mp2and 662 . . . 4  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  ( 1  x.  1 )  <_  (
( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) )
1403, 139syl5eqbrr 4248 . . 3  |-  ( (
ph  /\  ( sqr `  A )  e.  NN )  ->  1  <_  (
( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) )
141 0re 9093 . . . . . . 7  |-  0  e.  RR
142141a1i 11 . . . . . 6  |-  ( ph  ->  0  e.  RR )
143104, 141keepel 3798 . . . . . . 7  |-  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 )  e.  RR
144143a1i 11 . . . . . 6  |-  ( ph  ->  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN , 
1 ,  0 )  e.  RR )
145 breq2 4218 . . . . . . . 8  |-  ( 1  =  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 )  ->  (
0  <_  1  <->  0  <_  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 ) ) )
146 breq2 4218 . . . . . . . 8  |-  ( 0  =  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 )  ->  (
0  <_  0  <->  0  <_  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 ) ) )
147 0le0 10083 . . . . . . . 8  |-  0  <_  0
148145, 146, 129, 147keephyp 3795 . . . . . . 7  |-  0  <_  if ( ( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN , 
1 ,  0 )
149148a1i 11 . . . . . 6  |-  ( ph  ->  0  <_  if (
( sqr `  ( P ^ ( P  pCnt  A ) ) )  e.  NN ,  1 ,  0 ) )
150142, 144, 133, 149, 57letrd 9229 . . . . 5  |-  ( ph  ->  0  <_  ( F `  ( P ^ ( P  pCnt  A ) ) ) )
151104, 141keepel 3798 . . . . . . 7  |-  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 )  e.  RR
152151a1i 11 . . . . . 6  |-  ( ph  ->  if ( ( sqr `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  e.  NN ,  1 ,  0 )  e.  RR )
153 breq2 4218 . . . . . . . 8  |-  ( 1  =  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 )  -> 
( 0  <_  1  <->  0  <_  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 ) ) )
154 breq2 4218 . . . . . . . 8  |-  ( 0  =  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 )  -> 
( 0  <_  0  <->  0  <_  if ( ( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 ) ) )
155153, 154, 129, 147keephyp 3795 . . . . . . 7  |-  0  <_  if ( ( sqr `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  e.  NN ,  1 ,  0 )
156155a1i 11 . . . . . 6  |-  ( ph  ->  0  <_  if (
( sqr `  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  e.  NN ,  1 ,  0 ) )
157142, 152, 135, 156, 126letrd 9229 . . . . 5  |-  ( ph  ->  0  <_  ( F `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) ) )
158133, 135, 150, 157mulge0d 9605 . . . 4  |-  ( ph  ->  0  <_  ( ( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) )
159158adantr 453 . . 3  |-  ( (
ph  /\  -.  ( sqr `  A )  e.  NN )  ->  0  <_  ( ( F `  ( P ^ ( P 
pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) ) ) )
1601, 2, 140, 159ifbothda 3771 . 2  |-  ( ph  ->  if ( ( sqr `  A )  e.  NN ,  1 ,  0 )  <_  ( ( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) )
16163nncnd 10018 . . . . 5  |-  ( ph  ->  ( P ^ ( P  pCnt  A ) )  e.  CC )
16263nnne0d 10046 . . . . 5  |-  ( ph  ->  ( P ^ ( P  pCnt  A ) )  =/=  0 )
16318, 161, 162divcan2d 9794 . . . 4  |-  ( ph  ->  ( ( P ^
( P  pCnt  A
) )  x.  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  =  A )
164163fveq2d 5734 . . 3  |-  ( ph  ->  ( F `  (
( P ^ ( P  pCnt  A ) )  x.  ( A  / 
( P ^ ( P  pCnt  A ) ) ) ) )  =  ( F `  A
) )
165 pcndvds2 13243 . . . . . . 7  |-  ( ( P  e.  Prime  /\  A  e.  NN )  ->  -.  P  ||  ( A  / 
( P ^ ( P  pCnt  A ) ) ) )
1664, 17, 165syl2anc 644 . . . . . 6  |-  ( ph  ->  -.  P  ||  ( A  /  ( P ^
( P  pCnt  A
) ) ) )
167 coprm 13102 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( A  /  ( P ^
( P  pCnt  A
) ) )  e.  ZZ )  ->  ( -.  P  ||  ( A  /  ( P ^
( P  pCnt  A
) ) )  <->  ( P  gcd  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  =  1 ) )
1684, 67, 167syl2anc 644 . . . . . 6  |-  ( ph  ->  ( -.  P  ||  ( A  /  ( P ^ ( P  pCnt  A ) ) )  <->  ( P  gcd  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  =  1 ) )
169166, 168mpbid 203 . . . . 5  |-  ( ph  ->  ( P  gcd  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  =  1 )
170 prmz 13085 . . . . . . 7  |-  ( P  e.  Prime  ->  P  e.  ZZ )
1714, 170syl 16 . . . . . 6  |-  ( ph  ->  P  e.  ZZ )
172 rpexp1i 13123 . . . . . 6  |-  ( ( P  e.  ZZ  /\  ( A  /  ( P ^ ( P  pCnt  A ) ) )  e.  ZZ  /\  ( P 
pCnt  A )  e.  NN0 )  ->  ( ( P  gcd  ( A  / 
( P ^ ( P  pCnt  A ) ) ) )  =  1  ->  ( ( P ^ ( P  pCnt  A ) )  gcd  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  =  1 ) )
173171, 67, 56, 172syl3anc 1185 . . . . 5  |-  ( ph  ->  ( ( P  gcd  ( A  /  ( P ^ ( P  pCnt  A ) ) ) )  =  1  ->  (
( P ^ ( P  pCnt  A ) )  gcd  ( A  / 
( P ^ ( P  pCnt  A ) ) ) )  =  1 ) )
174169, 173mpd 15 . . . 4  |-  ( ph  ->  ( ( P ^
( P  pCnt  A
) )  gcd  ( A  /  ( P ^
( P  pCnt  A
) ) ) )  =  1 )
17547, 48, 49, 50, 51, 52, 53, 54, 63, 66, 174dchrisum0fmul 21202 . . 3  |-  ( ph  ->  ( F `  (
( P ^ ( P  pCnt  A ) )  x.  ( A  / 
( P ^ ( P  pCnt  A ) ) ) ) )  =  ( ( F `  ( P ^ ( P 
pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^ ( P  pCnt  A ) ) ) ) ) )
176164, 175eqtr3d 2472 . 2  |-  ( ph  ->  ( F `  A
)  =  ( ( F `  ( P ^ ( P  pCnt  A ) ) )  x.  ( F `  ( A  /  ( P ^
( P  pCnt  A
) ) ) ) ) )
177160, 176breqtrrd 4240 1  |-  ( ph  ->  if ( ( sqr `  A )  e.  NN ,  1 ,  0 )  <_  ( F `  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726    =/= wne 2601   A.wral 2707   {crab 2711   ifcif 3741   class class class wbr 4214    e. cmpt 4268   -->wf 5452   ` cfv 5456  (class class class)co 6083   CCcc 8990   RRcr 8991   0cc0 8992   1c1 8993    x. cmul 8997    < clt 9122    <_ cle 9123    / cdiv 9679   NNcn 10002   2c2 10051   NN0cn0 10223   ZZcz 10284   ZZ>=cuz 10490   QQcq 10576   RR+crp 10614  ..^cfzo 11137   ^cexp 11384   sqrcsqr 12040   sum_csu 12481    || cdivides 12854    gcd cgcd 13008   Primecprime 13081    pCnt cpc 13212   Basecbs 13471   0gc0g 13725   ZRHomczrh 16780  ℤ/nczn 16783  DChrcdchr 21018
This theorem is referenced by:  dchrisum0flb  21206
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-inf2 7598  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069  ax-pre-sup 9070  ax-addf 9071  ax-mulf 9072
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-disj 4185  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-se 4544  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-isom 5465  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-of 6307  df-1st 6351  df-2nd 6352  df-tpos 6481  df-riota 6551  df-recs 6635  df-rdg 6670  df-1o 6726  df-2o 6727  df-oadd 6730  df-omul 6731  df-er 6907  df-ec 6909  df-qs 6913  df-map 7022  df-pm 7023  df-ixp 7066  df-en 7112  df-dom 7113  df-sdom 7114  df-fin 7115  df-fi 7418  df-sup 7448  df-oi 7481  df-card 7828  df-acn 7831  df-cda 8050  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-div 9680  df-nn 10003  df-2 10060  df-3 10061  df-4 10062  df-5 10063  df-6 10064  df-7 10065  df-8 10066  df-9 10067  df-10 10068  df-n0 10224  df-z 10285  df-dec 10385  df-uz 10491  df-q 10577  df-rp 10615  df-xneg 10712  df-xadd 10713  df-xmul 10714  df-ioo 10922  df-ioc 10923  df-ico 10924  df-icc 10925  df-fz 11046  df-fzo 11138  df-fl 11204  df-mod 11253  df-seq 11326  df-exp 11385  df-fac 11569  df-bc 11596  df-hash 11621  df-shft 11884  df-cj 11906  df-re 11907  df-im 11908  df-sqr 12042  df-abs 12043  df-limsup 12267  df-clim 12284  df-rlim 12285  df-sum 12482  df-ef 12672  df-sin 12674  df-cos 12675  df-pi 12677  df-dvds 12855  df-gcd 13009  df-prm 13082  df-numer 13129  df-denom 13130  df-pc 13213  df-struct 13473  df-ndx 13474  df-slot 13475  df-base 13476  df-sets 13477  df-ress 13478  df-plusg 13544  df-mulr 13545  df-starv 13546  df-sca 13547  df-vsca 13548  df-tset 13550  df-ple 13551  df-ds 13553  df-unif 13554  df-hom 13555  df-cco 13556  df-rest 13652  df-topn 13653  df-topgen 13669  df-pt 13670  df-prds 13673  df-xrs 13728  df-0g 13729  df-gsum 13730  df-qtop 13735  df-imas 13736  df-divs 13737  df-xps 13738  df-mre 13813  df-mrc 13814  df-acs 13816  df-mnd 14692  df-mhm 14740  df-submnd 14741  df-grp 14814  df-minusg 14815  df-sbg 14816  df-mulg 14817  df-subg 14943  df-nsg 14944  df-eqg 14945  df-ghm 15006  df-cntz 15118  df-od 15169  df-cmn 15416  df-abl 15417  df-mgp 15651  df-rng 15665  df-cring 15666  df-ur 15667  df-oppr 15730  df-dvdsr 15748  df-unit 15749  df-invr 15779  df-dvr 15790  df-rnghom 15821  df-drng 15839  df-subrg 15868  df-lmod 15954  df-lss 16011  df-lsp 16050  df-sra 16246  df-rgmod 16247  df-lidl 16248  df-rsp 16249  df-2idl 16305  df-psmet 16696  df-xmet 16697  df-met 16698  df-bl 16699  df-mopn 16700  df-fbas 16701  df-fg 16702  df-cnfld 16706  df-zrh 16784  df-zn 16787  df-top 16965  df-bases 16967  df-topon 16968  df-topsp 16969  df-cld 17085  df-ntr 17086  df-cls 17087  df-nei 17164  df-lp 17202  df-perf 17203  df-cn 17293  df-cnp 17294  df-haus 17381  df-tx 17596  df-hmeo 17789  df-fil 17880  df-fm 17972  df-flim 17973  df-flf 17974  df-xms 18352  df-ms 18353  df-tms 18354  df-cncf 18910  df-limc 19755  df-dv 19756  df-log 20456  df-cxp 20457  df-dchr 21019
  Copyright terms: Public domain W3C validator