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

Theorem ostth3 22771
Description: - Lemma for ostth 22772: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.)
Hypotheses
Ref Expression
qrng.q  |-  Q  =  (flds  QQ )
qabsabv.a  |-  A  =  (AbsVal `  Q )
padic.j  |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 ,  0 ,  ( q ^ -u (
q  pCnt  x )
) ) ) )
ostth.k  |-  K  =  ( x  e.  QQ  |->  if ( x  =  0 ,  0 ,  1 ) )
ostth.1  |-  ( ph  ->  F  e.  A )
ostth3.2  |-  ( ph  ->  A. n  e.  NN  -.  1  <  ( F `
 n ) )
ostth3.3  |-  ( ph  ->  P  e.  Prime )
ostth3.4  |-  ( ph  ->  ( F `  P
)  <  1 )
ostth3.5  |-  R  = 
-u ( ( log `  ( F `  P
) )  /  ( log `  P ) )
ostth3.6  |-  S  =  if ( ( F `
 P )  <_ 
( F `  p
) ,  ( F `
 p ) ,  ( F `  P
) )
Assertion
Ref Expression
ostth3  |-  ( ph  ->  E. a  e.  RR+  F  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^c  a ) ) )
Distinct variable groups:    n, p, y    n, K    x, n, a, p, q, y, ph    J, a, p, y    S, a    A, a, n, p, q, x, y    Q, n, x, y    F, a, n, p, q, y    P, a, p, q, x, y    R, a, p, q, y    x, F
Allowed substitution hints:    P( n)    Q( q, p, a)    R( x, n)    S( x, y, n, q, p)    J( x, n, q)    K( x, y, q, p, a)

Proof of Theorem ostth3
Dummy variables  k 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ostth3.5 . . . 4  |-  R  = 
-u ( ( log `  ( F `  P
) )  /  ( log `  P ) )
2 ostth.1 . . . . . . . . 9  |-  ( ph  ->  F  e.  A )
3 ostth3.3 . . . . . . . . . . . . 13  |-  ( ph  ->  P  e.  Prime )
4 prmuz2 13763 . . . . . . . . . . . . 13  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
53, 4syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  ( ZZ>= ` 
2 ) )
6 eluz2b2 10914 . . . . . . . . . . . 12  |-  ( P  e.  ( ZZ>= `  2
)  <->  ( P  e.  NN  /\  1  < 
P ) )
75, 6sylib 196 . . . . . . . . . . 11  |-  ( ph  ->  ( P  e.  NN  /\  1  <  P ) )
87simpld 456 . . . . . . . . . 10  |-  ( ph  ->  P  e.  NN )
9 nnq 10953 . . . . . . . . . 10  |-  ( P  e.  NN  ->  P  e.  QQ )
108, 9syl 16 . . . . . . . . 9  |-  ( ph  ->  P  e.  QQ )
11 qabsabv.a . . . . . . . . . 10  |-  A  =  (AbsVal `  Q )
12 qrng.q . . . . . . . . . . 11  |-  Q  =  (flds  QQ )
1312qrngbas 22752 . . . . . . . . . 10  |-  QQ  =  ( Base `  Q )
1411, 13abvcl 16832 . . . . . . . . 9  |-  ( ( F  e.  A  /\  P  e.  QQ )  ->  ( F `  P
)  e.  RR )
152, 10, 14syl2anc 654 . . . . . . . 8  |-  ( ph  ->  ( F `  P
)  e.  RR )
168nnne0d 10353 . . . . . . . . 9  |-  ( ph  ->  P  =/=  0 )
1712qrng0 22754 . . . . . . . . . 10  |-  0  =  ( 0g `  Q )
1811, 13, 17abvgt0 16836 . . . . . . . . 9  |-  ( ( F  e.  A  /\  P  e.  QQ  /\  P  =/=  0 )  ->  0  <  ( F `  P
) )
192, 10, 16, 18syl3anc 1211 . . . . . . . 8  |-  ( ph  ->  0  <  ( F `
 P ) )
2015, 19elrpd 11012 . . . . . . 7  |-  ( ph  ->  ( F `  P
)  e.  RR+ )
2120relogcld 21956 . . . . . 6  |-  ( ph  ->  ( log `  ( F `  P )
)  e.  RR )
228nnred 10324 . . . . . . 7  |-  ( ph  ->  P  e.  RR )
237simprd 460 . . . . . . 7  |-  ( ph  ->  1  <  P )
2422, 23rplogcld 21962 . . . . . 6  |-  ( ph  ->  ( log `  P
)  e.  RR+ )
2521, 24rerpdivcld 11041 . . . . 5  |-  ( ph  ->  ( ( log `  ( F `  P )
)  /  ( log `  P ) )  e.  RR )
2625renegcld 9762 . . . 4  |-  ( ph  -> 
-u ( ( log `  ( F `  P
) )  /  ( log `  P ) )  e.  RR )
271, 26syl5eqel 2517 . . 3  |-  ( ph  ->  R  e.  RR )
28 ostth3.4 . . . . . . . . 9  |-  ( ph  ->  ( F `  P
)  <  1 )
29 1rp 10982 . . . . . . . . . 10  |-  1  e.  RR+
30 logltb 21932 . . . . . . . . . 10  |-  ( ( ( F `  P
)  e.  RR+  /\  1  e.  RR+ )  ->  (
( F `  P
)  <  1  <->  ( log `  ( F `  P
) )  <  ( log `  1 ) ) )
3120, 29, 30sylancl 655 . . . . . . . . 9  |-  ( ph  ->  ( ( F `  P )  <  1  <->  ( log `  ( F `
 P ) )  <  ( log `  1
) ) )
3228, 31mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( log `  ( F `  P )
)  <  ( log `  1 ) )
33 log1 21918 . . . . . . . 8  |-  ( log `  1 )  =  0
3432, 33syl6breq 4319 . . . . . . 7  |-  ( ph  ->  ( log `  ( F `  P )
)  <  0 )
3524rpcnd 11016 . . . . . . . 8  |-  ( ph  ->  ( log `  P
)  e.  CC )
3635mul01d 9555 . . . . . . 7  |-  ( ph  ->  ( ( log `  P
)  x.  0 )  =  0 )
3734, 36breqtrrd 4306 . . . . . 6  |-  ( ph  ->  ( log `  ( F `  P )
)  <  ( ( log `  P )  x.  0 ) )
38 0red 9374 . . . . . . 7  |-  ( ph  ->  0  e.  RR )
3921, 38, 24ltdivmuld 11061 . . . . . 6  |-  ( ph  ->  ( ( ( log `  ( F `  P
) )  /  ( log `  P ) )  <  0  <->  ( log `  ( F `  P
) )  <  (
( log `  P
)  x.  0 ) ) )
4037, 39mpbird 232 . . . . 5  |-  ( ph  ->  ( ( log `  ( F `  P )
)  /  ( log `  P ) )  <  0 )
4125lt0neg1d 9896 . . . . 5  |-  ( ph  ->  ( ( ( log `  ( F `  P
) )  /  ( log `  P ) )  <  0  <->  0  <  -u ( ( log `  ( F `  P )
)  /  ( log `  P ) ) ) )
4240, 41mpbid 210 . . . 4  |-  ( ph  ->  0  <  -u (
( log `  ( F `  P )
)  /  ( log `  P ) ) )
4342, 1syl6breqr 4320 . . 3  |-  ( ph  ->  0  <  R )
4427, 43elrpd 11012 . 2  |-  ( ph  ->  R  e.  RR+ )
45 padic.j . . . . 5  |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 ,  0 ,  ( q ^ -u (
q  pCnt  x )
) ) ) )
4612, 11, 45padicabvcxp 22765 . . . 4  |-  ( ( P  e.  Prime  /\  R  e.  RR+ )  ->  (
y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^c  R ) )  e.  A
)
473, 44, 46syl2anc 654 . . 3  |-  ( ph  ->  ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) )  e.  A )
48 fveq2 5679 . . . . . . . . . 10  |-  ( y  =  P  ->  (
( J `  P
) `  y )  =  ( ( J `
 P ) `  P ) )
4948oveq1d 6095 . . . . . . . . 9  |-  ( y  =  P  ->  (
( ( J `  P ) `  y
)  ^c  R )  =  ( ( ( J `  P
) `  P )  ^c  R )
)
50 eqid 2433 . . . . . . . . 9  |-  ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^c  R )
)  =  ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^c  R )
)
51 ovex 6105 . . . . . . . . 9  |-  ( ( ( J `  P
) `  P )  ^c  R )  e.  _V
5249, 50, 51fvmpt 5762 . . . . . . . 8  |-  ( P  e.  QQ  ->  (
( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  P )  =  ( ( ( J `  P ) `  P
)  ^c  R ) )
5310, 52syl 16 . . . . . . 7  |-  ( ph  ->  ( ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^c  R ) ) `  P )  =  ( ( ( J `  P ) `  P
)  ^c  R ) )
5445padicval 22750 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  P  e.  QQ )  ->  (
( J `  P
) `  P )  =  if ( P  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  P ) ) ) )
553, 10, 54syl2anc 654 . . . . . . . . 9  |-  ( ph  ->  ( ( J `  P ) `  P
)  =  if ( P  =  0 ,  0 ,  ( P ^ -u ( P 
pCnt  P ) ) ) )
5616neneqd 2614 . . . . . . . . . 10  |-  ( ph  ->  -.  P  =  0 )
57 iffalse 3787 . . . . . . . . . 10  |-  ( -.  P  =  0  ->  if ( P  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  P ) ) )  =  ( P ^ -u ( P 
pCnt  P ) ) )
5856, 57syl 16 . . . . . . . . 9  |-  ( ph  ->  if ( P  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  P ) ) )  =  ( P ^ -u ( P 
pCnt  P ) ) )
598nncnd 10325 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  CC )
6059exp1d 11986 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P ^ 1 )  =  P )
6160oveq2d 6096 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P  pCnt  ( P ^ 1 ) )  =  ( P  pCnt  P ) )
62 1z 10663 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
63 pcid 13921 . . . . . . . . . . . . . 14  |-  ( ( P  e.  Prime  /\  1  e.  ZZ )  ->  ( P  pCnt  ( P ^
1 ) )  =  1 )
643, 62, 63sylancl 655 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P  pCnt  ( P ^ 1 ) )  =  1 )
6561, 64eqtr3d 2467 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  pCnt  P
)  =  1 )
6665negeqd 9591 . . . . . . . . . . 11  |-  ( ph  -> 
-u ( P  pCnt  P )  =  -u 1
)
6766oveq2d 6096 . . . . . . . . . 10  |-  ( ph  ->  ( P ^ -u ( P  pCnt  P ) )  =  ( P ^ -u 1 ) )
68 neg1z 10668 . . . . . . . . . . . 12  |-  -u 1  e.  ZZ
6968a1i 11 . . . . . . . . . . 11  |-  ( ph  -> 
-u 1  e.  ZZ )
7059, 16, 69cxpexpzd 22040 . . . . . . . . . 10  |-  ( ph  ->  ( P  ^c  -u 1 )  =  ( P ^ -u 1
) )
7167, 70eqtr4d 2468 . . . . . . . . 9  |-  ( ph  ->  ( P ^ -u ( P  pCnt  P ) )  =  ( P  ^c  -u 1 ) )
7255, 58, 713eqtrd 2469 . . . . . . . 8  |-  ( ph  ->  ( ( J `  P ) `  P
)  =  ( P  ^c  -u 1
) )
7372oveq1d 6095 . . . . . . 7  |-  ( ph  ->  ( ( ( J `
 P ) `  P )  ^c  R )  =  ( ( P  ^c  -u 1 )  ^c  R ) )
7427recnd 9399 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  CC )
7574mulm1d 9783 . . . . . . . . . 10  |-  ( ph  ->  ( -u 1  x.  R )  =  -u R )
761negeqi 9590 . . . . . . . . . . 11  |-  -u R  =  -u -u ( ( log `  ( F `  P
) )  /  ( log `  P ) )
7725recnd 9399 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  ( F `  P )
)  /  ( log `  P ) )  e.  CC )
7877negnegd 9697 . . . . . . . . . . 11  |-  ( ph  -> 
-u -u ( ( log `  ( F `  P
) )  /  ( log `  P ) )  =  ( ( log `  ( F `  P
) )  /  ( log `  P ) ) )
7976, 78syl5eq 2477 . . . . . . . . . 10  |-  ( ph  -> 
-u R  =  ( ( log `  ( F `  P )
)  /  ( log `  P ) ) )
8075, 79eqtrd 2465 . . . . . . . . 9  |-  ( ph  ->  ( -u 1  x.  R )  =  ( ( log `  ( F `  P )
)  /  ( log `  P ) ) )
8180oveq2d 6096 . . . . . . . 8  |-  ( ph  ->  ( P  ^c 
( -u 1  x.  R
) )  =  ( P  ^c  ( ( log `  ( F `  P )
)  /  ( log `  P ) ) ) )
828nnrpd 11013 . . . . . . . . 9  |-  ( ph  ->  P  e.  RR+ )
83 neg1rr 10413 . . . . . . . . . 10  |-  -u 1  e.  RR
8483a1i 11 . . . . . . . . 9  |-  ( ph  -> 
-u 1  e.  RR )
8582, 84, 74cxpmuld 22063 . . . . . . . 8  |-  ( ph  ->  ( P  ^c 
( -u 1  x.  R
) )  =  ( ( P  ^c  -u 1 )  ^c  R ) )
8659, 16, 77cxpefd 22041 . . . . . . . . 9  |-  ( ph  ->  ( P  ^c 
( ( log `  ( F `  P )
)  /  ( log `  P ) ) )  =  ( exp `  (
( ( log `  ( F `  P )
)  /  ( log `  P ) )  x.  ( log `  P
) ) ) )
8721recnd 9399 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  ( F `  P )
)  e.  CC )
8824rpne0d 11019 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  P
)  =/=  0 )
8987, 35, 88divcan1d 10095 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( log `  ( F `  P
) )  /  ( log `  P ) )  x.  ( log `  P
) )  =  ( log `  ( F `
 P ) ) )
9089fveq2d 5683 . . . . . . . . 9  |-  ( ph  ->  ( exp `  (
( ( log `  ( F `  P )
)  /  ( log `  P ) )  x.  ( log `  P
) ) )  =  ( exp `  ( log `  ( F `  P ) ) ) )
9120reeflogd 21957 . . . . . . . . 9  |-  ( ph  ->  ( exp `  ( log `  ( F `  P ) ) )  =  ( F `  P ) )
9286, 90, 913eqtrd 2469 . . . . . . . 8  |-  ( ph  ->  ( P  ^c 
( ( log `  ( F `  P )
)  /  ( log `  P ) ) )  =  ( F `  P ) )
9381, 85, 923eqtr3d 2473 . . . . . . 7  |-  ( ph  ->  ( ( P  ^c  -u 1 )  ^c  R )  =  ( F `  P ) )
9453, 73, 933eqtrrd 2470 . . . . . 6  |-  ( ph  ->  ( F `  P
)  =  ( ( y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^c  R ) ) `  P
) )
95 fveq2 5679 . . . . . . 7  |-  ( P  =  p  ->  ( F `  P )  =  ( F `  p ) )
96 fveq2 5679 . . . . . . 7  |-  ( P  =  p  ->  (
( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  P )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  p ) )
9795, 96eqeq12d 2447 . . . . . 6  |-  ( P  =  p  ->  (
( F `  P
)  =  ( ( y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^c  R ) ) `  P
)  <->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  p ) ) )
9894, 97syl5ibcom 220 . . . . 5  |-  ( ph  ->  ( P  =  p  ->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  p ) ) )
9998adantr 462 . . . 4  |-  ( (
ph  /\  p  e.  Prime )  ->  ( P  =  p  ->  ( F `
 p )  =  ( ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^c  R ) ) `  p ) ) )
100 prmnn 13748 . . . . . . . . 9  |-  ( p  e.  Prime  ->  p  e.  NN )
101100ad2antlr 719 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  p  e.  NN )
102 nnq 10953 . . . . . . . 8  |-  ( p  e.  NN  ->  p  e.  QQ )
103101, 102syl 16 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  p  e.  QQ )
104 fveq2 5679 . . . . . . . . 9  |-  ( y  =  p  ->  (
( J `  P
) `  y )  =  ( ( J `
 P ) `  p ) )
105104oveq1d 6095 . . . . . . . 8  |-  ( y  =  p  ->  (
( ( J `  P ) `  y
)  ^c  R )  =  ( ( ( J `  P
) `  p )  ^c  R )
)
106 ovex 6105 . . . . . . . 8  |-  ( ( ( J `  P
) `  p )  ^c  R )  e.  _V
107105, 50, 106fvmpt 5762 . . . . . . 7  |-  ( p  e.  QQ  ->  (
( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  p )  =  ( ( ( J `  P ) `  p
)  ^c  R ) )
108103, 107syl 16 . . . . . 6  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  p )  =  ( ( ( J `  P ) `  p
)  ^c  R ) )
10974ad2antrr 718 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  R  e.  CC )
1101091cxpd 22036 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
1  ^c  R )  =  1 )
1113ad2antrr 718 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  P  e.  Prime )
11245padicval 22750 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  p  e.  QQ )  ->  (
( J `  P
) `  p )  =  if ( p  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  p ) ) ) )
113111, 103, 112syl2anc 654 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( J `  P
) `  p )  =  if ( p  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  p ) ) ) )
114101nnne0d 10353 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  p  =/=  0 )
115114neneqd 2614 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -.  p  =  0 )
116 iffalse 3787 . . . . . . . . . 10  |-  ( -.  p  =  0  ->  if ( p  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  p ) ) )  =  ( P ^ -u ( P 
pCnt  p ) ) )
117115, 116syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  if ( p  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  p ) ) )  =  ( P ^ -u ( P 
pCnt  p ) ) )
118 pceq0 13919 . . . . . . . . . . . . . . . 16  |-  ( ( P  e.  Prime  /\  p  e.  NN )  ->  (
( P  pCnt  p
)  =  0  <->  -.  P  ||  p ) )
1193, 100, 118syl2an 474 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  Prime )  ->  ( ( P  pCnt  p )  =  0  <->  -.  P  ||  p
) )
120 dvdsprm 13767 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  p  e.  Prime )  ->  ( P  ||  p  <->  P  =  p ) )
1215, 120sylan 468 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  p  e.  Prime )  ->  ( P  ||  p  <->  P  =  p
) )
122121necon3bbid 2632 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  Prime )  ->  ( -.  P  ||  p  <->  P  =/=  p ) )
123119, 122bitrd 253 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  p  e.  Prime )  ->  ( ( P  pCnt  p )  =  0  <->  P  =/=  p
) )
124123biimpar 482 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( P  pCnt  p )  =  0 )
125124negeqd 9591 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -u ( P  pCnt  p )  = 
-u 0 )
126 neg0 9642 . . . . . . . . . . . 12  |-  -u 0  =  0
127125, 126syl6eq 2481 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -u ( P  pCnt  p )  =  0 )
128127oveq2d 6096 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( P ^ -u ( P 
pCnt  p ) )  =  ( P ^ 0 ) )
12959ad2antrr 718 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  P  e.  CC )
130129exp0d 11985 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( P ^ 0 )  =  1 )
131128, 130eqtrd 2465 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( P ^ -u ( P 
pCnt  p ) )  =  1 )
132113, 117, 1313eqtrd 2469 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( J `  P
) `  p )  =  1 )
133132oveq1d 6095 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( ( J `  P ) `  p
)  ^c  R )  =  ( 1  ^c  R ) )
134 2re 10378 . . . . . . . . . . . . 13  |-  2  e.  RR
135134a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
2  e.  RR )
136 ostth3.6 . . . . . . . . . . . . . 14  |-  S  =  if ( ( F `
 P )  <_ 
( F `  p
) ,  ( F `
 p ) ,  ( F `  P
) )
1372ad2antrr 718 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  F  e.  A )
13811, 13abvcl 16832 . . . . . . . . . . . . . . . . . 18  |-  ( ( F  e.  A  /\  p  e.  QQ )  ->  ( F `  p
)  e.  RR )
139137, 103, 138syl2anc 654 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( F `  p )  e.  RR )
14011, 13, 17abvgt0 16836 . . . . . . . . . . . . . . . . . 18  |-  ( ( F  e.  A  /\  p  e.  QQ  /\  p  =/=  0 )  ->  0  <  ( F `  p
) )
141137, 103, 114, 140syl3anc 1211 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  0  <  ( F `  p
) )
142139, 141elrpd 11012 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( F `  p )  e.  RR+ )
143142adantrr 709 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( F `  p
)  e.  RR+ )
14420ad2antrr 718 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( F `  P
)  e.  RR+ )
145 ifcl 3819 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  p
)  e.  RR+  /\  ( F `  P )  e.  RR+ )  ->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  e.  RR+ )
146143, 144, 145syl2anc 654 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  e.  RR+ )
147136, 146syl5eqel 2517 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  e.  RR+ )
148147rprecred 11025 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( 1  /  S
)  e.  RR )
149 simprr 749 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( F `  p
)  <  1 )
15028ad2antrr 718 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( F `  P
)  <  1 )
151 breq1 4283 . . . . . . . . . . . . . . . 16  |-  ( ( F `  p )  =  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  -> 
( ( F `  p )  <  1  <->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  <  1 ) )
152 breq1 4283 . . . . . . . . . . . . . . . 16  |-  ( ( F `  P )  =  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  -> 
( ( F `  P )  <  1  <->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  <  1 ) )
153151, 152ifboth 3813 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  p
)  <  1  /\  ( F `  P )  <  1 )  ->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  <  1 )
154149, 150, 153syl2anc 654 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  <  1 )
155136, 154syl5eqbr 4313 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  <  1 )
156147reclt1d 11027 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( S  <  1  <->  1  <  ( 1  /  S ) ) )
157155, 156mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
1  <  ( 1  /  S ) )
158 expnbnd 11976 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR  /\  ( 1  /  S
)  e.  RR  /\  1  <  ( 1  /  S ) )  ->  E. k  e.  NN  2  <  ( ( 1  /  S ) ^
k ) )
159135, 148, 157, 158syl3anc 1211 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  E. k  e.  NN  2  <  ( ( 1  /  S ) ^
k ) )
160147rpcnd 11016 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  e.  CC )
161160adantr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  S  e.  CC )
162147rpne0d 11019 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  =/=  0 )
163162adantr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  S  =/=  0 )
164 nnz 10655 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  NN  ->  k  e.  ZZ )
165164adantl 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  k  e.  ZZ )
166161, 163, 165exprecd 11999 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( 1  /  S
) ^ k )  =  ( 1  / 
( S ^ k
) ) )
1672ad3antrrr 722 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  F  e.  A )
168 ax-1ne0 9338 . . . . . . . . . . . . . . . . . 18  |-  1  =/=  0
16912qrng1 22755 . . . . . . . . . . . . . . . . . . 19  |-  1  =  ( 1r `  Q )
17011, 169, 17abv1z 16840 . . . . . . . . . . . . . . . . . 18  |-  ( ( F  e.  A  /\  1  =/=  0 )  -> 
( F `  1
)  =  1 )
171167, 168, 170sylancl 655 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( F `  1 )  =  1 )
1728ad2antrr 718 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  P  e.  NN )
173 nnnn0 10573 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN  ->  k  e.  NN0 )
174 nnexpcl 11861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  e.  NN  /\  k  e.  NN0 )  -> 
( P ^ k
)  e.  NN )
175172, 173, 174syl2an 474 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( P ^ k )  e.  NN )
176175nnzd 10733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( P ^ k )  e.  ZZ )
177100ad2antlr 719 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  p  e.  NN )
178 nnexpcl 11861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( p  e.  NN  /\  k  e.  NN0 )  -> 
( p ^ k
)  e.  NN )
179177, 173, 178syl2an 474 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
p ^ k )  e.  NN )
180179nnzd 10733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
p ^ k )  e.  ZZ )
181 bezout 13708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( P ^ k
)  e.  ZZ  /\  ( p ^ k
)  e.  ZZ )  ->  E. a  e.  ZZ  E. b  e.  ZZ  (
( P ^ k
)  gcd  ( p ^ k ) )  =  ( ( ( P ^ k )  x.  a )  +  ( ( p ^
k )  x.  b
) ) )
182176, 180, 181syl2anc 654 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  E. a  e.  ZZ  E. b  e.  ZZ  ( ( P ^ k )  gcd  ( p ^ k
) )  =  ( ( ( P ^
k )  x.  a
)  +  ( ( p ^ k )  x.  b ) ) )
183 simprl 748 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  P  =/=  p )
1843ad2antrr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  P  e.  Prime )
185 simplr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  p  e.  Prime )
186 prmrp 13769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( P  e.  Prime  /\  p  e.  Prime )  ->  (
( P  gcd  p
)  =  1  <->  P  =/=  p ) )
187184, 185, 186syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( ( P  gcd  p )  =  1  <-> 
P  =/=  p ) )
188183, 187mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( P  gcd  p
)  =  1 )
189188adantr 462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( P  gcd  p )  =  1 )
190172adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  P  e.  NN )
191177adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  p  e.  NN )
192 simpr 458 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  k  e.  NN )
193 rppwr 13723 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( P  e.  NN  /\  p  e.  NN  /\  k  e.  NN )  ->  (
( P  gcd  p
)  =  1  -> 
( ( P ^
k )  gcd  (
p ^ k ) )  =  1 ) )
194190, 191, 192, 193syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( P  gcd  p
)  =  1  -> 
( ( P ^
k )  gcd  (
p ^ k ) )  =  1 ) )
195189, 194mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( P ^ k
)  gcd  ( p ^ k ) )  =  1 )
196195adantrr 709 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( P ^ k
)  gcd  ( p ^ k ) )  =  1 )
197196eqeq1d 2441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( P ^
k )  gcd  (
p ^ k ) )  =  ( ( ( P ^ k
)  x.  a )  +  ( ( p ^ k )  x.  b ) )  <->  1  =  ( ( ( P ^ k )  x.  a )  +  ( ( p ^ k
)  x.  b ) ) ) )
1982ad3antrrr 722 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  F  e.  A )
199175adantrr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( P ^ k )  e.  NN )
200 nnq 10953 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( P ^ k )  e.  NN  ->  ( P ^ k )  e.  QQ )
201199, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( P ^ k )  e.  QQ )
202 simprrl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  a  e.  ZZ )
203 zq 10946 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  e.  ZZ  ->  a  e.  QQ )
204202, 203syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  a  e.  QQ )
205 qmulcl 10958 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( P ^ k
)  e.  QQ  /\  a  e.  QQ )  ->  ( ( P ^
k )  x.  a
)  e.  QQ )
206201, 204, 205syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( P ^ k
)  x.  a )  e.  QQ )
207179adantrr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
p ^ k )  e.  NN )
208 nnq 10953 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( p ^ k )  e.  NN  ->  (
p ^ k )  e.  QQ )
209207, 208syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
p ^ k )  e.  QQ )
210 simprrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  b  e.  ZZ )
211 zq 10946 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  e.  ZZ  ->  b  e.  QQ )
212210, 211syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  b  e.  QQ )
213 qmulcl 10958 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( p ^ k
)  e.  QQ  /\  b  e.  QQ )  ->  ( ( p ^
k )  x.  b
)  e.  QQ )
214209, 212, 213syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( p ^ k
)  x.  b )  e.  QQ )
215 qaddcl 10956 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( P ^
k )  x.  a
)  e.  QQ  /\  ( ( p ^
k )  x.  b
)  e.  QQ )  ->  ( ( ( P ^ k )  x.  a )  +  ( ( p ^
k )  x.  b
) )  e.  QQ )
216206, 214, 215syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( P ^
k )  x.  a
)  +  ( ( p ^ k )  x.  b ) )  e.  QQ )
21711, 13abvcl 16832 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F  e.  A  /\  ( ( ( P ^ k )  x.  a )  +  ( ( p ^ k
)  x.  b ) )  e.  QQ )  ->  ( F `  ( ( ( P ^ k )  x.  a )  +  ( ( p ^ k
)  x.  b ) ) )  e.  RR )
218198, 216, 217syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( (
( P ^ k
)  x.  a )  +  ( ( p ^ k )  x.  b ) ) )  e.  RR )
21911, 13abvcl 16832 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F  e.  A  /\  ( ( P ^
k )  x.  a
)  e.  QQ )  ->  ( F `  ( ( P ^
k )  x.  a
) )  e.  RR )
220198, 206, 219syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( ( P ^ k )  x.  a ) )  e.  RR )
22111, 13abvcl 16832 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F  e.  A  /\  ( ( p ^
k )  x.  b
)  e.  QQ )  ->  ( F `  ( ( p ^
k )  x.  b
) )  e.  RR )
222198, 214, 221syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( (
p ^ k )  x.  b ) )  e.  RR )
223220, 222readdcld 9400 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  (
( P ^ k
)  x.  a ) )  +  ( F `
 ( ( p ^ k )  x.  b ) ) )  e.  RR )
224 rpexpcl 11867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( S  e.  RR+  /\  k  e.  ZZ )  ->  ( S ^ k )  e.  RR+ )
225147, 164, 224syl2an 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( S ^ k )  e.  RR+ )
226225rpred 11014 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( S ^ k )  e.  RR )
227226adantrr 709 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( S ^ k )  e.  RR )
228 remulcl 9354 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2  e.  RR  /\  ( S ^ k )  e.  RR )  -> 
( 2  x.  ( S ^ k ) )  e.  RR )
229134, 227, 228sylancr 656 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
2  x.  ( S ^ k ) )  e.  RR )
230 qex 10952 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  QQ  e.  _V
231 cnfldadd 17666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  +  =  ( +g  ` fld )
23212, 231ressplusg 14262 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( QQ  e.  _V  ->  +  =  ( +g  `  Q
) )
233230, 232ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  +  =  ( +g  `  Q )
23411, 13, 233abvtri 16838 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F  e.  A  /\  ( ( P ^
k )  x.  a
)  e.  QQ  /\  ( ( p ^
k )  x.  b
)  e.  QQ )  ->  ( F `  ( ( ( P ^ k )  x.  a )  +  ( ( p ^ k
)  x.  b ) ) )  <_  (
( F `  (
( P ^ k
)  x.  a ) )  +  ( F `
 ( ( p ^ k )  x.  b ) ) ) )
235198, 206, 214, 234syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( (
( P ^ k
)  x.  a )  +  ( ( p ^ k )  x.  b ) ) )  <_  ( ( F `
 ( ( P ^ k )  x.  a ) )  +  ( F `  (
( p ^ k
)  x.  b ) ) ) )
236 cnfldmul 17667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  x.  =  ( .r ` fld )
23712, 236ressmulr 14273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( QQ  e.  _V  ->  x.  =  ( .r `  Q ) )
238230, 237ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  x.  =  ( .r `  Q )
23911, 13, 238abvmul 16837 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F  e.  A  /\  ( P ^ k )  e.  QQ  /\  a  e.  QQ )  ->  ( F `  ( ( P ^ k )  x.  a ) )  =  ( ( F `  ( P ^ k ) )  x.  ( F `
 a ) ) )
240198, 201, 204, 239syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( ( P ^ k )  x.  a ) )  =  ( ( F `  ( P ^ k ) )  x.  ( F `
 a ) ) )
24110ad3antrrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  P  e.  QQ )
242173ad2antrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  k  e.  NN0 )
24312, 11qabvexp 22759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  A  /\  P  e.  QQ  /\  k  e.  NN0 )  ->  ( F `  ( P ^ k ) )  =  ( ( F `
 P ) ^
k ) )
244198, 241, 242, 243syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( P ^ k ) )  =  ( ( F `
 P ) ^
k ) )
245244oveq1d 6095 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  ( P ^ k ) )  x.  ( F `  a ) )  =  ( ( ( F `
 P ) ^
k )  x.  ( F `  a )
) )
246240, 245eqtrd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( ( P ^ k )  x.  a ) )  =  ( ( ( F `
 P ) ^
k )  x.  ( F `  a )
) )
247198, 241, 14syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  P )  e.  RR )
248247, 242reexpcld 12008 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  P
) ^ k )  e.  RR )
24911, 13abvcl 16832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  A  /\  a  e.  QQ )  ->  ( F `  a
)  e.  RR )
250198, 204, 249syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  a )  e.  RR )
251248, 250remulcld 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  P ) ^ k
)  x.  ( F `
 a ) )  e.  RR )
252 elz 10635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( a  e.  ZZ  <->  ( a  e.  RR  /\  ( a  =  0  \/  a  e.  NN  \/  -u a  e.  NN ) ) )
253252simprbi 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( a  e.  ZZ  ->  (
a  =  0  \/  a  e.  NN  \/  -u a  e.  NN ) )
254253adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( a  =  0  \/  a  e.  NN  \/  -u a  e.  NN ) )
25511, 17abv0 16839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( F  e.  A  ->  ( F `  0 )  =  0 )
2562, 255syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( F `  0
)  =  0 )
257 0le1 9850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  0  <_  1
258256, 257syl6eqbr 4317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( F `  0
)  <_  1 )
259258adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( F `
 0 )  <_ 
1 )
260 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( a  =  0  ->  ( F `  a )  =  ( F ` 
0 ) )
261260breq1d 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( a  =  0  ->  (
( F `  a
)  <_  1  <->  ( F `  0 )  <_ 
1 ) )
262259, 261syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( a  =  0  ->  ( F `  a )  <_  1 ) )
263 ostth3.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  A. n  e.  NN  -.  1  <  ( F `
 n ) )
264 nnq 10953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( n  e.  NN  ->  n  e.  QQ )
26511, 13abvcl 16832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( F  e.  A  /\  n  e.  QQ )  ->  ( F `  n
)  e.  RR )
2662, 264, 265syl2an 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  e.  RR )
267 1re 9372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  1  e.  RR
268 lenlt 9440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( F `  n
)  e.  RR  /\  1  e.  RR )  ->  ( ( F `  n )  <_  1  <->  -.  1  <  ( F `
 n ) ) )
269266, 267, 268sylancl 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( F `  n )  <_  1  <->  -.  1  <  ( F `  n
) ) )
270269ralbidva 2721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( A. n  e.  NN  ( F `  n )  <_  1  <->  A. n  e.  NN  -.  1  <  ( F `  n ) ) )
271263, 270mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  A. n  e.  NN  ( F `  n )  <_  1 )
272 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  a  ->  ( F `  n )  =  ( F `  a ) )
273272breq1d 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  =  a  ->  (
( F `  n
)  <_  1  <->  ( F `  a )  <_  1
) )
274273rspccv 3059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( A. n  e.  NN  ( F `  n )  <_  1  ->  ( a  e.  NN  ->  ( F `  a )  <_  1
) )
275271, 274syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( a  e.  NN  ->  ( F `  a
)  <_  1 ) )
276275adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( a  e.  NN  ->  ( F `  a )  <_  1 ) )
2772adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  ->  F  e.  A )
278203ad2antrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
a  e.  QQ )
279 eqid 2433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( invg `  Q )  =  ( invg `  Q )
28011, 13, 279abvneg 16842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( F  e.  A  /\  a  e.  QQ )  ->  ( F `  (
( invg `  Q ) `  a
) )  =  ( F `  a ) )
281277, 278, 280syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( F `  (
( invg `  Q ) `  a
) )  =  ( F `  a ) )
28212qrngneg 22756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( a  e.  QQ  ->  (
( invg `  Q ) `  a
)  =  -u a
)
283278, 282syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( ( invg `  Q ) `  a
)  =  -u a
)
284 simprr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  ->  -u a  e.  NN )
285283, 284eqeltrd 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( ( invg `  Q ) `  a
)  e.  NN )
286271adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  ->  A. n  e.  NN  ( F `  n )  <_  1 )
287 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( n  =  ( ( invg `  Q ) `
 a )  -> 
( F `  n
)  =  ( F `
 ( ( invg `  Q ) `
 a ) ) )
288287breq1d 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  ( ( invg `  Q ) `
 a )  -> 
( ( F `  n )  <_  1  <->  ( F `  ( ( invg `  Q
) `  a )
)  <_  1 ) )
289288rspcv 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( invg `  Q ) `  a
)  e.  NN  ->  ( A. n  e.  NN  ( F `  n )  <_  1  ->  ( F `  ( ( invg `  Q ) `
 a ) )  <_  1 ) )
290285, 286, 289sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( F `  (
( invg `  Q ) `  a
) )  <_  1
)
291281, 290eqbrtrrd 4302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( F `  a
)  <_  1 )
292291expr 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( -u a  e.  NN  ->  ( F `  a )  <_  1 ) )
293262, 276, 2923jaod 1275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( ( a  =  0  \/  a  e.  NN  \/  -u a  e.  NN )  ->  ( F `  a )  <_  1
) )
294254, 293mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( F `
 a )  <_ 
1 )
295294ralrimiva 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  A. a  e.  ZZ  ( F `  a )  <_  1 )
296295ad3antrrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  A. a  e.  ZZ  ( F `  a )  <_  1
)
297 rsp 2766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. a  e.  ZZ  ( F `  a )  <_  1  ->  ( a  e.  ZZ  ->  ( F `  a )  <_  1
) )
298296, 202, 297sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  a )  <_  1 )
299267a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  1  e.  RR )
300164ad2antrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  k  e.  ZZ )
30119ad3antrrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <  ( F `  P
) )
302 expgt0 11880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( F `  P
)  e.  RR  /\  k  e.  ZZ  /\  0  <  ( F `  P
) )  ->  0  <  ( ( F `  P ) ^ k
) )
303247, 300, 301, 302syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <  ( ( F `  P ) ^ k
) )
304 lemul2 10169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( F `  a
)  e.  RR  /\  1  e.  RR  /\  (
( ( F `  P ) ^ k
)  e.  RR  /\  0  <  ( ( F `
 P ) ^
k ) ) )  ->  ( ( F `
 a )  <_ 
1  <->  ( ( ( F `  P ) ^ k )  x.  ( F `  a
) )  <_  (
( ( F `  P ) ^ k
)  x.  1 ) ) )
305250, 299, 248, 303, 304syl112anc 1215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  a
)  <_  1  <->  ( (
( F `  P
) ^ k )  x.  ( F `  a ) )  <_ 
( ( ( F `
 P ) ^
k )  x.  1 ) ) )
306298, 305mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  P ) ^ k
)  x.  ( F `
 a ) )  <_  ( ( ( F `  P ) ^ k )  x.  1 ) )
307248recnd 9399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  P
) ^ k )  e.  CC )
308307mulid1d 9390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  P ) ^ k
)  x.  1 )  =  ( ( F `
 P ) ^
k ) )
309306, 308breqtrd 4304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  P ) ^ k
)  x.  ( F `
 a ) )  <_  ( ( F `
 P ) ^
k ) )
310147rpred 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  e.  RR )
311310adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  S  e.  RR )
312144adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  P )  e.  RR+ )
313312rpge0d 11018 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <_  ( F `  P
) )
314177adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  p  e.  NN )
315314, 102syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  p  e.  QQ )
316198, 315, 138syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  p )  e.  RR )
317 max1 11144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( F `  P
)  e.  RR  /\  ( F `  p )  e.  RR )  -> 
( F `  P
)  <_  if (
( F `  P
)  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) ) )
318247, 316, 317syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  P )  <_  if ( ( F `
 P )  <_ 
( F `  p
) ,  ( F `
 p ) ,  ( F `  P
) ) )
319318, 136syl6breqr 4320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  P )  <_  S )
320 leexp1a 11905 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  P )  e.  RR  /\  S  e.  RR  /\  k  e.  NN0 )  /\  ( 0  <_  ( F `  P )  /\  ( F `  P
)  <_  S )
)  ->  ( ( F `  P ) ^ k )  <_ 
( S ^ k
) )
321247, 311, 242, 313, 319, 320syl32anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  P
) ^ k )  <_  ( S ^
k ) )
322251, 248, 227, 309, 321letrd 9515 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  P ) ^ k
)  x.  ( F `
 a ) )  <_  ( S ^
k ) )
323246, 322eqbrtrd 4300 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( ( P ^ k )  x.  a ) )  <_ 
( S ^ k
) )
32411, 13, 238abvmul 16837 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F  e.  A  /\  ( p ^ k
)  e.  QQ  /\  b  e.  QQ )  ->  ( F `  (
( p ^ k
)  x.  b ) )  =  ( ( F `  ( p ^ k ) )  x.  ( F `  b ) ) )
325198, 209, 212, 324syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( (
p ^ k )  x.  b ) )  =  ( ( F `
 ( p ^
k ) )  x.  ( F `  b
) ) )
32612, 11qabvexp 22759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  A  /\  p  e.  QQ  /\  k  e.  NN0 )  ->  ( F `  ( p ^ k ) )  =  ( ( F `
 p ) ^
k ) )
327198, 315, 242, 326syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( p ^ k ) )  =  ( ( F `
 p ) ^
k ) )
328327oveq1d 6095 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  (
p ^ k ) )  x.  ( F `
 b ) )  =  ( ( ( F `  p ) ^ k )  x.  ( F `  b
) ) )
329325, 328eqtrd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( (
p ^ k )  x.  b ) )  =  ( ( ( F `  p ) ^ k )  x.  ( F `  b
) ) )
330316, 242reexpcld 12008 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  p
) ^ k )  e.  RR )
33111, 13abvcl 16832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  A  /\  b  e.  QQ )  ->  ( F `  b
)  e.  RR )
332198, 212, 331syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  b )  e.  RR )
333330, 332remulcld 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  p ) ^ k
)  x.  ( F `
 b ) )  e.  RR )
334 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  b  ->  ( F `  a )  =  ( F `  b ) )
335334breq1d 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a  =  b  ->  (
( F `  a
)  <_  1  <->  ( F `  b )  <_  1
) )
336335rspcv 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  e.  ZZ  ->  ( A. a  e.  ZZ  ( F `  a )  <_  1  ->  ( F `  b )  <_  1 ) )
337210, 296, 336sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  b )  <_  1 )
338314nnne0d 10353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  p  =/=  0 )
339198, 315, 338, 140syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <  ( F `  p
) )
340 expgt0 11880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( F `  p
)  e.  RR  /\  k  e.  ZZ  /\  0  <  ( F `  p
) )  ->  0  <  ( ( F `  p ) ^ k
) )
341316, 300, 339, 340syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <  ( ( F `  p ) ^ k
) )
342 lemul2 10169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( F `  b
)  e.  RR  /\  1  e.  RR  /\  (
( ( F `  p ) ^ k
)  e.  RR  /\  0  <  ( ( F `
 p ) ^
k ) ) )  ->  ( ( F `
 b )  <_ 
1  <->  ( ( ( F `  p ) ^ k )  x.  ( F `  b
) )  <_  (
( ( F `  p ) ^ k
)  x.  1 ) ) )
343332, 299, 330, 341, 342syl112anc 1215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  b
)  <_  1  <->  ( (
( F `  p
) ^ k )  x.  ( F `  b ) )  <_ 
( ( ( F `
 p ) ^
k )  x.  1 ) ) )
344337, 343mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  p ) ^ k
)  x.  ( F `
 b ) )  <_  ( ( ( F `  p ) ^ k )  x.  1 ) )
345330recnd 9399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  p
) ^ k )  e.  CC )
346345mulid1d 9390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  p ) ^ k
)  x.  1 )  =  ( ( F `
 p ) ^
k ) )
347344, 346breqtrd 4304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  p ) ^ k
)  x.  ( F `
 b ) )  <_  ( ( F `
 p ) ^
k ) )
348143adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  p )  e.  RR+ )
349348rpge0d 11018 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <_  ( F `  p
) )
350 max2 11146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( F `  P
)  e.  RR  /\  ( F `  p )  e.  RR )  -> 
( F `  p
)  <_  if (
( F `  P
)  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) ) )
351247, 316, 350syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  p )  <_  if ( ( F `
 P )  <_ 
( F `  p
) ,  ( F `
 p ) ,  ( F `  P
) ) )
352351, 136syl6breqr 4320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  p )  <_  S )
353 leexp1a 11905 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  p )  e.  RR  /\  S  e.  RR  /\  k  e.  NN0 )  /\  ( 0  <_  ( F `  p )  /\  ( F `  p
)  <_  S )
)  ->  ( ( F `  p ) ^ k )  <_ 
( S ^ k
) )
354316, 311, 242, 349, 352, 353syl32anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  p
) ^ k )  <_  ( S ^
k ) )
355333, 330, 227, 347, 354letrd 9515 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( F `  p ) ^ k
)  x.  ( F `
 b ) )  <_  ( S ^
k ) )
356329, 355eqbrtrd 4300 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( (
p ^ k )  x.  b ) )  <_  ( S ^
k ) )
357220, 222, 227, 227, 323, 356le2addd 9944 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  (
( P ^ k
)  x.  a ) )  +  ( F `
 ( ( p ^ k )  x.  b ) ) )  <_  ( ( S ^ k )  +  ( S ^ k
) ) )
358225rpcnd 11016 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( S ^ k )  e.  CC )
3593582timesd 10554 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
2  x.  ( S ^ k ) )  =  ( ( S ^ k )  +  ( S ^ k
) ) )
360359adantrr 709 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
2  x.  ( S ^ k ) )  =  ( ( S ^ k )  +  ( S ^ k
) ) )
361357, 360breqtrrd 4306 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  (
( P ^ k
)  x.  a ) )  +  ( F `
 ( ( p ^ k )  x.  b ) ) )  <_  ( 2  x.  ( S ^ k
) ) )
362218, 223, 229, 235, 361letrd 9515 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  ( (
( P ^ k
)  x.  a )  +  ( ( p ^ k )  x.  b ) ) )  <_  ( 2  x.  ( S ^ k
) ) )
363 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1  =  ( ( ( P ^ k )  x.  a )  +  ( ( p ^
k )  x.  b
) )  ->  ( F `  1 )  =  ( F `  ( ( ( P ^ k )  x.  a )  +  ( ( p ^ k
)  x.  b ) ) ) )
364363breq1d 4290 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  =  ( ( ( P ^ k )  x.  a )  +  ( ( p ^
k )  x.  b
) )  ->  (
( F `  1
)  <_  ( 2  x.  ( S ^
k ) )  <->  ( F `  ( ( ( P ^ k )  x.  a )  +  ( ( p ^ k
)  x.  b ) ) )  <_  (
2  x.  ( S ^ k ) ) ) )
365362, 364syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
1  =  ( ( ( P ^ k
)  x.  a )  +  ( ( p ^ k )  x.  b ) )  -> 
( F `  1
)  <_  ( 2  x.  ( S ^
k ) ) ) )
366197, 365sylbid 215 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( ( P ^
k )  gcd  (
p ^ k ) )  =  ( ( ( P ^ k
)  x.  a )  +  ( ( p ^ k )  x.  b ) )  -> 
( F `  1
)  <_  ( 2  x.  ( S ^
k ) ) ) )
367366anassrs 641 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
)  ->  ( (
( P ^ k
)  gcd  ( p ^ k ) )  =  ( ( ( P ^ k )  x.  a )  +  ( ( p ^
k )  x.  b
) )  ->  ( F `  1 )  <_  ( 2  x.  ( S ^ k ) ) ) )
368367rexlimdvva 2838 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( E. a  e.  ZZ  E. b  e.  ZZ  (
( P ^ k
)  gcd  ( p ^ k ) )  =  ( ( ( P ^ k )  x.  a )  +  ( ( p ^
k )  x.  b
) )  ->  ( F `  1 )  <_  ( 2  x.  ( S ^ k ) ) ) )
369182, 368mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( F `  1 )  <_  ( 2  x.  ( S ^ k ) ) )
370171, 369eqbrtrrd 4302 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  1  <_  ( 2  x.  ( S ^ k ) ) )
371225rpregt0d 11020 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( S ^ k
)  e.  RR  /\  0  <  ( S ^
k ) ) )
372 ledivmul2 10196 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  RR  /\  2  e.  RR  /\  (
( S ^ k
)  e.  RR  /\  0  <  ( S ^
k ) ) )  ->  ( ( 1  /  ( S ^
k ) )  <_ 
2  <->  1  <_  (
2  x.  ( S ^ k ) ) ) )
373267, 134, 372mp3an12 1297 . . . . . . . . . . . . . . . . 17  |-  ( ( ( S ^ k
)  e.  RR  /\  0  <  ( S ^
k ) )  -> 
( ( 1  / 
( S ^ k
) )  <_  2  <->  1  <_  ( 2  x.  ( S ^ k
) ) ) )
374371, 373syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( 1  /  ( S ^ k ) )  <_  2  <->  1  <_  ( 2  x.  ( S ^ k ) ) ) )
375370, 374mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
1  /  ( S ^ k ) )  <_  2 )
376166, 375eqbrtrd 4300 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( 1  /  S
) ^ k )  <_  2 )
377 reexpcl 11865 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  /  S
)  e.  RR  /\  k  e.  NN0 )  -> 
( ( 1  /  S ) ^ k
)  e.  RR )
378148, 173, 377syl2an 474 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( 1  /  S
) ^ k )  e.  RR )
379 lenlt 9440 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 1  /  S ) ^ k
)  e.  RR  /\  2  e.  RR )  ->  ( ( ( 1  /  S ) ^
k )  <_  2  <->  -.  2  <  ( ( 1  /  S ) ^ k ) ) )
380378, 134, 379sylancl 655 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( ( 1  /  S ) ^ k
)  <_  2  <->  -.  2  <  ( ( 1  /  S ) ^ k
) ) )
381376, 380mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  -.  2  <  ( ( 1  /  S ) ^
k ) )
382381pm2.21d 106 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
2  <  ( (
1  /  S ) ^ k )  ->  -.  ( F `  p
)  <  1 ) )
383382rexlimdva 2831 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( E. k  e.  NN  2  <  (
( 1  /  S
) ^ k )  ->  -.  ( F `  p )  <  1
) )
384159, 383mpd 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  -.  ( F `  p
)  <  1 )
385384expr 610 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( F `  p
)  <  1  ->  -.  ( F `  p
)  <  1 ) )
386385pm2.01d 169 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -.  ( F `  p )  <  1 )
387263ad2antrr 718 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  A. n  e.  NN  -.  1  < 
( F `  n
) )
388 fveq2 5679 . . . . . . . . . . . 12  |-  ( n  =  p  ->  ( F `  n )  =  ( F `  p ) )
389388breq2d 4292 . . . . . . . . . . 11  |-  ( n  =  p  ->  (
1  <  ( F `  n )  <->  1  <  ( F `  p ) ) )
390389notbid 294 . . . . . . . . . 10  |-  ( n  =  p  ->  ( -.  1  <  ( F `
 n )  <->  -.  1  <  ( F `  p
) ) )
391390rspcv 3058 . . . . . . . . 9  |-  ( p  e.  NN  ->  ( A. n  e.  NN  -.  1  <  ( F `
 n )  ->  -.  1  <  ( F `
 p ) ) )
392101, 387, 391sylc 60 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -.  1  <  ( F `  p ) )
393 lttri3 9445 . . . . . . . . 9  |-  ( ( ( F `  p
)  e.  RR  /\  1  e.  RR )  ->  ( ( F `  p )  =  1  <-> 
( -.  ( F `
 p )  <  1  /\  -.  1  <  ( F `  p
) ) ) )
394139, 267, 393sylancl 655 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( F `  p
)  =  1  <->  ( -.  ( F `  p
)  <  1  /\  -.  1  <  ( F `
 p ) ) ) )
395386, 392, 394mpbir2and 906 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( F `  p )  =  1 )
396110, 133, 3953eqtr4d 2475 . . . . . 6  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( ( J `  P ) `  p
)  ^c  R )  =  ( F `
 p ) )
397108, 396eqtr2d 2466 . . . . 5  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^c  R )
) `  p )
)
398397ex 434 . . . 4  |-  ( (
ph  /\  p  e.  Prime )  ->  ( P  =/=  p  ->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  p ) ) )
39999, 398pm2.61dne 2678 . . 3  |-  ( (
ph  /\  p  e.  Prime )  ->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^c  R ) ) `  p ) )
40012, 11, 2, 47, 399ostthlem2 22761 . 2  |-  ( ph  ->  F  =  ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^c  R )
) )
401 oveq2 6088 . . . . 5  |-  ( a  =  R  ->  (
( ( J `  P ) `  y
)  ^c  a )  =  ( ( ( J `  P
) `  y )  ^c  R )
)
402401mpteq2dv 4367 . . . 4  |-  ( a  =  R  ->  (
y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^c  a ) )  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^c  R ) ) )
403402eqeq2d 2444 . . 3  |-  ( a  =  R  ->  ( F  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^c  a ) )  <-> 
F  =  ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^c  R )
) ) )
404403rspcev 3062 . 2  |-  ( ( R  e.  RR+  /\  F  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^c  R ) ) )  ->  E. a  e.  RR+  F  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^c  a ) ) )
40544, 400, 404syl2anc 654 1  |-  ( ph  ->  E. a  e.  RR+  F  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^c  a ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    \/ w3o 957    = wceq 1362    e. wcel 1755    =/= wne 2596   A.wral 2705   E.wrex 2706   _Vcvv 2962   ifcif 3779   class class class wbr 4280    e. cmpt 4338   ` cfv 5406  (class class class)co 6080   CCcc 9267   RRcr 9268   0cc0 9269   1c1 9270    + caddc 9272    x. cmul 9274    < clt 9405    <_ cle 9406   -ucneg 9583    / cdiv 9980   NNcn 10309   2c2 10358   NN0cn0 10566   ZZcz 10633   ZZ>=cuz 10848   QQcq 10940   RR+crp 10978   ^cexp 11848   expce 13329    || cdivides 13517    gcd cgcd 13672   Primecprime 13745    pCnt cpc 13885   ↾s cress 14157   +g cplusg 14220   .rcmulr 14221   invgcminusg 15393  AbsValcabv 16824  ℂfldccnfld 17661   logclog 21890    ^c ccxp 21891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9325  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-mulcom 9333  ax-addass 9334  ax-mulass 9335  ax-distr 9336  ax-i2m1 9337  ax-1ne0 9338  ax-1rid 9339  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342  ax-pre-lttri 9343  ax-pre-lttrn 9344  ax-pre-ltadd 9345  ax-pre-mulgt0 9346  ax-pre-sup 9347  ax-addf 9348  ax-mulf 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-iin 4162  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-om 6466  df-1st 6566  df-2nd 6567  df-supp 6680  df-tpos 6734  df-recs 6818  df-rdg 6852  df-1o 6908  df-2o 6909  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-ixp 7252  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fsupp 7609  df-fi 7649  df-sup 7679  df-oi 7712  df-card 8097  df-cda 8325  df-pnf 9407  df-mnf 9408  df-xr 9409  df-ltxr 9410  df-le 9411  df-sub 9584  df-neg 9585  df-div 9981  df-nn 10310  df-2 10367  df-3 10368  df-4 10369  df-5 10370  df-6 10371  df-7 10372  df-8 10373  df-9 10374  df-10 10375  df-n0 10567  df-z 10634  df-dec 10743  df-uz 10849  df-q 10941  df-rp 10979  df-xneg 11076  df-xadd 11077  df-xmul 11078  df-ioo 11291  df-ioc 11292  df-ico 11293  df-icc 11294  df-fz 11424  df-fzo 11532  df-fl 11625  df-mod 11692  df-seq 11790  df-exp 11849  df-fac 12035  df-bc 12062  df-hash 12087  df-shft 12539  df-cj 12571  df-re 12572  df-im 12573  df-sqr 12707  df-abs 12708  df-limsup 12932  df-clim 12949  df-rlim 12950  df-sum 13147  df-ef 13335  df-sin 13337  df-cos 13338  df-pi 13340  df-dvds 13518  df-gcd 13673  df-prm 13746  df-pc 13886  df-struct 14158  df-ndx 14159  df-slot 14160  df-base 14161  df-sets 14162  df-ress 14163  df-plusg 14233  df-mulr 14234  df-starv 14235  df-sca 14236  df-vsca 14237  df-ip 14238  df-tset 14239  df-ple 14240  df-ds 14242  df-unif 14243  df-hom 14244  df-cco 14245  df-rest 14343  df-topn 14344  df-0g 14362  df-gsum 14363  df-topgen 14364  df-pt 14365  df-prds 14368  df-xrs 14422  df-qtop 14427  df-imas 14428  df-xps 14430  df-mre 14506  df-mrc 14507  df-acs 14509  df-mnd 15397  df-submnd 15447  df-grp 15524  df-minusg 15525  df-mulg 15527  df-subg 15657  df-cntz 15814  df-cmn 16258  df-mgp 16565  df-rng 16579  df-cring 16580  df-ur 16581  df-oppr 16648  df-dvdsr 16666  df-unit 16667  df-invr 16697  df-dvr 16708  df-drng 16757  df-subrg 16786  df-abv 16825  df-psmet 17652  df-xmet 17653  df-met 17654  df-bl 17655  df-mopn 17656  df-fbas 17657  df-fg