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

Theorem ostth3 20783
Description: - Lemma for ostth 20784: 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
Dummy variables  k  b are mutually distinct and distinct from all other variables.
Allowed substitution groups:    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
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 12772 . . . . . . . . . . . . 13  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
53, 4syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  ( ZZ>= ` 
2 ) )
6 eluz2b2 10287 . . . . . . . . . . . 12  |-  ( P  e.  ( ZZ>= `  2
)  <->  ( P  e.  NN  /\  1  < 
P ) )
75, 6sylib 190 . . . . . . . . . . 11  |-  ( ph  ->  ( P  e.  NN  /\  1  <  P ) )
87simpld 447 . . . . . . . . . 10  |-  ( ph  ->  P  e.  NN )
9 nnq 10326 . . . . . . . . . 10  |-  ( P  e.  NN  ->  P  e.  QQ )
108, 9syl 17 . . . . . . . . 9  |-  ( ph  ->  P  e.  QQ )
11 qabsabv.a . . . . . . . . . 10  |-  A  =  (AbsVal `  Q )
12 qrng.q . . . . . . . . . . 11  |-  Q  =  (flds  QQ )
1312qrngbas 20764 . . . . . . . . . 10  |-  QQ  =  ( Base `  Q )
1411, 13abvcl 15585 . . . . . . . . 9  |-  ( ( F  e.  A  /\  P  e.  QQ )  ->  ( F `  P
)  e.  RR )
152, 10, 14syl2anc 644 . . . . . . . 8  |-  ( ph  ->  ( F `  P
)  e.  RR )
168nnne0d 9787 . . . . . . . . 9  |-  ( ph  ->  P  =/=  0 )
1712qrng0 20766 . . . . . . . . . 10  |-  0  =  ( 0g `  Q )
1811, 13, 17abvgt0 15589 . . . . . . . . 9  |-  ( ( F  e.  A  /\  P  e.  QQ  /\  P  =/=  0 )  ->  0  <  ( F `  P
) )
192, 10, 16, 18syl3anc 1184 . . . . . . . 8  |-  ( ph  ->  0  <  ( F `
 P ) )
2015, 19elrpd 10385 . . . . . . 7  |-  ( ph  ->  ( F `  P
)  e.  RR+ )
2120relogcld 19970 . . . . . 6  |-  ( ph  ->  ( log `  ( F `  P )
)  e.  RR )
228nnred 9758 . . . . . . 7  |-  ( ph  ->  P  e.  RR )
237simprd 451 . . . . . . 7  |-  ( ph  ->  1  <  P )
2422, 23rplogcld 19976 . . . . . 6  |-  ( ph  ->  ( log `  P
)  e.  RR+ )
2521, 24rerpdivcld 10414 . . . . 5  |-  ( ph  ->  ( ( log `  ( F `  P )
)  /  ( log `  P ) )  e.  RR )
2625renegcld 9207 . . . 4  |-  ( ph  -> 
-u ( ( log `  ( F `  P
) )  /  ( log `  P ) )  e.  RR )
271, 26syl5eqel 2370 . . 3  |-  ( ph  ->  R  e.  RR )
28 ostth3.4 . . . . . . . . 9  |-  ( ph  ->  ( F `  P
)  <  1 )
29 1rp 10355 . . . . . . . . . 10  |-  1  e.  RR+
30 logltb 19949 . . . . . . . . . 10  |-  ( ( ( F `  P
)  e.  RR+  /\  1  e.  RR+ )  ->  (
( F `  P
)  <  1  <->  ( log `  ( F `  P
) )  <  ( log `  1 ) ) )
3120, 29, 30sylancl 645 . . . . . . . . 9  |-  ( ph  ->  ( ( F `  P )  <  1  <->  ( log `  ( F `
 P ) )  <  ( log `  1
) ) )
3228, 31mpbid 203 . . . . . . . 8  |-  ( ph  ->  ( log `  ( F `  P )
)  <  ( log `  1 ) )
33 log1 19935 . . . . . . . 8  |-  ( log `  1 )  =  0
3432, 33syl6breq 4065 . . . . . . 7  |-  ( ph  ->  ( log `  ( F `  P )
)  <  0 )
3524rpred 10387 . . . . . . . . 9  |-  ( ph  ->  ( log `  P
)  e.  RR )
3635recnd 8858 . . . . . . . 8  |-  ( ph  ->  ( log `  P
)  e.  CC )
3736mul01d 9008 . . . . . . 7  |-  ( ph  ->  ( ( log `  P
)  x.  0 )  =  0 )
3834, 37breqtrrd 4052 . . . . . 6  |-  ( ph  ->  ( log `  ( F `  P )
)  <  ( ( log `  P )  x.  0 ) )
39 0re 8835 . . . . . . . 8  |-  0  e.  RR
4039a1i 12 . . . . . . 7  |-  ( ph  ->  0  e.  RR )
4121, 40, 24ltdivmuld 10434 . . . . . 6  |-  ( ph  ->  ( ( ( log `  ( F `  P
) )  /  ( log `  P ) )  <  0  <->  ( log `  ( F `  P
) )  <  (
( log `  P
)  x.  0 ) ) )
4238, 41mpbird 225 . . . . 5  |-  ( ph  ->  ( ( log `  ( F `  P )
)  /  ( log `  P ) )  <  0 )
4325lt0neg1d 9339 . . . . 5  |-  ( ph  ->  ( ( ( log `  ( F `  P
) )  /  ( log `  P ) )  <  0  <->  0  <  -u ( ( log `  ( F `  P )
)  /  ( log `  P ) ) ) )
4442, 43mpbid 203 . . . 4  |-  ( ph  ->  0  <  -u (
( log `  ( F `  P )
)  /  ( log `  P ) ) )
4544, 1syl6breqr 4066 . . 3  |-  ( ph  ->  0  <  R )
4627, 45elrpd 10385 . 2  |-  ( ph  ->  R  e.  RR+ )
47 padic.j . . . . 5  |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 ,  0 ,  ( q ^ -u (
q  pCnt  x )
) ) ) )
4812, 11, 47padicabvcxp 20777 . . . 4  |-  ( ( P  e.  Prime  /\  R  e.  RR+ )  ->  (
y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^ c  R
) )  e.  A
)
493, 46, 48syl2anc 644 . . 3  |-  ( ph  ->  ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) )  e.  A )
50 fveq2 5487 . . . . . . . . . 10  |-  ( y  =  P  ->  (
( J `  P
) `  y )  =  ( ( J `
 P ) `  P ) )
5150oveq1d 5836 . . . . . . . . 9  |-  ( y  =  P  ->  (
( ( J `  P ) `  y
)  ^ c  R
)  =  ( ( ( J `  P
) `  P )  ^ c  R )
)
52 eqid 2286 . . . . . . . . 9  |-  ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^ c  R )
)  =  ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^ c  R )
)
53 ovex 5846 . . . . . . . . 9  |-  ( ( ( J `  P
) `  P )  ^ c  R )  e.  _V
5451, 52, 53fvmpt 5565 . . . . . . . 8  |-  ( P  e.  QQ  ->  (
( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) ) `  P )  =  ( ( ( J `  P ) `  P
)  ^ c  R
) )
5510, 54syl 17 . . . . . . 7  |-  ( ph  ->  ( ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^ c  R ) ) `  P )  =  ( ( ( J `  P ) `  P
)  ^ c  R
) )
5647padicval 20762 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  P  e.  QQ )  ->  (
( J `  P
) `  P )  =  if ( P  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  P ) ) ) )
573, 10, 56syl2anc 644 . . . . . . . . 9  |-  ( ph  ->  ( ( J `  P ) `  P
)  =  if ( P  =  0 ,  0 ,  ( P ^ -u ( P 
pCnt  P ) ) ) )
5816neneqd 2465 . . . . . . . . . 10  |-  ( ph  ->  -.  P  =  0 )
59 iffalse 3575 . . . . . . . . . 10  |-  ( -.  P  =  0  ->  if ( P  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  P ) ) )  =  ( P ^ -u ( P 
pCnt  P ) ) )
6058, 59syl 17 . . . . . . . . 9  |-  ( ph  ->  if ( P  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  P ) ) )  =  ( P ^ -u ( P 
pCnt  P ) ) )
618nncnd 9759 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  CC )
6261exp1d 11236 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P ^ 1 )  =  P )
6362oveq2d 5837 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P  pCnt  ( P ^ 1 ) )  =  ( P  pCnt  P ) )
64 1z 10050 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
65 pcid 12921 . . . . . . . . . . . . . 14  |-  ( ( P  e.  Prime  /\  1  e.  ZZ )  ->  ( P  pCnt  ( P ^
1 ) )  =  1 )
663, 64, 65sylancl 645 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P  pCnt  ( P ^ 1 ) )  =  1 )
6763, 66eqtr3d 2320 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  pCnt  P
)  =  1 )
6867negeqd 9043 . . . . . . . . . . 11  |-  ( ph  -> 
-u ( P  pCnt  P )  =  -u 1
)
6968oveq2d 5837 . . . . . . . . . 10  |-  ( ph  ->  ( P ^ -u ( P  pCnt  P ) )  =  ( P ^ -u 1 ) )
70 znegcl 10052 . . . . . . . . . . . . 13  |-  ( 1  e.  ZZ  ->  -u 1  e.  ZZ )
7164, 70ax-mp 10 . . . . . . . . . . . 12  |-  -u 1  e.  ZZ
7271a1i 12 . . . . . . . . . . 11  |-  ( ph  -> 
-u 1  e.  ZZ )
7361, 16, 72cxpexpzd 20054 . . . . . . . . . 10  |-  ( ph  ->  ( P  ^ c  -u 1 )  =  ( P ^ -u 1
) )
7469, 73eqtr4d 2321 . . . . . . . . 9  |-  ( ph  ->  ( P ^ -u ( P  pCnt  P ) )  =  ( P  ^ c  -u 1 ) )
7557, 60, 743eqtrd 2322 . . . . . . . 8  |-  ( ph  ->  ( ( J `  P ) `  P
)  =  ( P  ^ c  -u 1
) )
7675oveq1d 5836 . . . . . . 7  |-  ( ph  ->  ( ( ( J `
 P ) `  P )  ^ c  R )  =  ( ( P  ^ c  -u 1 )  ^ c  R ) )
7727recnd 8858 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  CC )
7877mulm1d 9228 . . . . . . . . . 10  |-  ( ph  ->  ( -u 1  x.  R )  =  -u R )
791negeqi 9042 . . . . . . . . . . 11  |-  -u R  =  -u -u ( ( log `  ( F `  P
) )  /  ( log `  P ) )
8025recnd 8858 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  ( F `  P )
)  /  ( log `  P ) )  e.  CC )
8180negnegd 9145 . . . . . . . . . . 11  |-  ( ph  -> 
-u -u ( ( log `  ( F `  P
) )  /  ( log `  P ) )  =  ( ( log `  ( F `  P
) )  /  ( log `  P ) ) )
8279, 81syl5eq 2330 . . . . . . . . . 10  |-  ( ph  -> 
-u R  =  ( ( log `  ( F `  P )
)  /  ( log `  P ) ) )
8378, 82eqtrd 2318 . . . . . . . . 9  |-  ( ph  ->  ( -u 1  x.  R )  =  ( ( log `  ( F `  P )
)  /  ( log `  P ) ) )
8483oveq2d 5837 . . . . . . . 8  |-  ( ph  ->  ( P  ^ c 
( -u 1  x.  R
) )  =  ( P  ^ c  ( ( log `  ( F `  P )
)  /  ( log `  P ) ) ) )
858nnrpd 10386 . . . . . . . . 9  |-  ( ph  ->  P  e.  RR+ )
8671zrei 10027 . . . . . . . . . 10  |-  -u 1  e.  RR
8786a1i 12 . . . . . . . . 9  |-  ( ph  -> 
-u 1  e.  RR )
8885, 87, 77cxpmuld 20077 . . . . . . . 8  |-  ( ph  ->  ( P  ^ c 
( -u 1  x.  R
) )  =  ( ( P  ^ c  -u 1 )  ^ c  R ) )
8961, 16, 80cxpefd 20055 . . . . . . . . 9  |-  ( ph  ->  ( P  ^ c 
( ( log `  ( F `  P )
)  /  ( log `  P ) ) )  =  ( exp `  (
( ( log `  ( F `  P )
)  /  ( log `  P ) )  x.  ( log `  P
) ) ) )
9021recnd 8858 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  ( F `  P )
)  e.  CC )
9124rpne0d 10392 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  P
)  =/=  0 )
9290, 36, 91divcan1d 9534 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( log `  ( F `  P
) )  /  ( log `  P ) )  x.  ( log `  P
) )  =  ( log `  ( F `
 P ) ) )
9392fveq2d 5491 . . . . . . . . 9  |-  ( ph  ->  ( exp `  (
( ( log `  ( F `  P )
)  /  ( log `  P ) )  x.  ( log `  P
) ) )  =  ( exp `  ( log `  ( F `  P ) ) ) )
9420reeflogd 19971 . . . . . . . . 9  |-  ( ph  ->  ( exp `  ( log `  ( F `  P ) ) )  =  ( F `  P ) )
9589, 93, 943eqtrd 2322 . . . . . . . 8  |-  ( ph  ->  ( P  ^ c 
( ( log `  ( F `  P )
)  /  ( log `  P ) ) )  =  ( F `  P ) )
9684, 88, 953eqtr3d 2326 . . . . . . 7  |-  ( ph  ->  ( ( P  ^ c  -u 1 )  ^ c  R )  =  ( F `  P ) )
9755, 76, 963eqtrrd 2323 . . . . . 6  |-  ( ph  ->  ( F `  P
)  =  ( ( y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^ c  R
) ) `  P
) )
98 fveq2 5487 . . . . . . 7  |-  ( P  =  p  ->  ( F `  P )  =  ( F `  p ) )
99 fveq2 5487 . . . . . . 7  |-  ( P  =  p  ->  (
( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) ) `  P )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) ) `  p ) )
10098, 99eqeq12d 2300 . . . . . 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 ) ) )
10197, 100syl5ibcom 213 . . . . 5  |-  ( ph  ->  ( P  =  p  ->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) ) `  p ) ) )
102101adantr 453 . . . 4  |-  ( (
ph  /\  p  e.  Prime )  ->  ( P  =  p  ->  ( F `
 p )  =  ( ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^ c  R ) ) `  p ) ) )
103 prmnn 12757 . . . . . . . . 9  |-  ( p  e.  Prime  ->  p  e.  NN )
104103ad2antlr 709 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  p  e.  NN )
105 nnq 10326 . . . . . . . 8  |-  ( p  e.  NN  ->  p  e.  QQ )
106104, 105syl 17 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  p  e.  QQ )
107 fveq2 5487 . . . . . . . . 9  |-  ( y  =  p  ->  (
( J `  P
) `  y )  =  ( ( J `
 P ) `  p ) )
108107oveq1d 5836 . . . . . . . 8  |-  ( y  =  p  ->  (
( ( J `  P ) `  y
)  ^ c  R
)  =  ( ( ( J `  P
) `  p )  ^ c  R )
)
109 ovex 5846 . . . . . . . 8  |-  ( ( ( J `  P
) `  p )  ^ c  R )  e.  _V
110108, 52, 109fvmpt 5565 . . . . . . 7  |-  ( p  e.  QQ  ->  (
( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) ) `  p )  =  ( ( ( J `  P ) `  p
)  ^ c  R
) )
111106, 110syl 17 . . . . . 6  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) ) `  p )  =  ( ( ( J `  P ) `  p
)  ^ c  R
) )
11277ad2antrr 708 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  R  e.  CC )
1131121cxpd 20050 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
1  ^ c  R
)  =  1 )
1143ad2antrr 708 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  P  e.  Prime )
11547padicval 20762 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  p  e.  QQ )  ->  (
( J `  P
) `  p )  =  if ( p  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  p ) ) ) )
116114, 106, 115syl2anc 644 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( J `  P
) `  p )  =  if ( p  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  p ) ) ) )
117104nnne0d 9787 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  p  =/=  0 )
118117neneqd 2465 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -.  p  =  0 )
119 iffalse 3575 . . . . . . . . . 10  |-  ( -.  p  =  0  ->  if ( p  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  p ) ) )  =  ( P ^ -u ( P 
pCnt  p ) ) )
120118, 119syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  if ( p  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  p ) ) )  =  ( P ^ -u ( P 
pCnt  p ) ) )
121 pceq0 12919 . . . . . . . . . . . . . . . 16  |-  ( ( P  e.  Prime  /\  p  e.  NN )  ->  (
( P  pCnt  p
)  =  0  <->  -.  P  ||  p ) )
1223, 103, 121syl2an 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  Prime )  ->  ( ( P  pCnt  p )  =  0  <->  -.  P  ||  p
) )
123 dvdsprm 12774 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  p  e.  Prime )  ->  ( P  ||  p  <->  P  =  p ) )
1245, 123sylan 459 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  p  e.  Prime )  ->  ( P  ||  p  <->  P  =  p
) )
125124necon3bbid 2483 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  p  e.  Prime )  ->  ( -.  P  ||  p  <->  P  =/=  p ) )
126122, 125bitrd 246 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  p  e.  Prime )  ->  ( ( P  pCnt  p )  =  0  <->  P  =/=  p
) )
127126biimpar 473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( P  pCnt  p )  =  0 )
128127negeqd 9043 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -u ( P  pCnt  p )  = 
-u 0 )
129 neg0 9090 . . . . . . . . . . . 12  |-  -u 0  =  0
130128, 129syl6eq 2334 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -u ( P  pCnt  p )  =  0 )
131130oveq2d 5837 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( P ^ -u ( P 
pCnt  p ) )  =  ( P ^ 0 ) )
13261ad2antrr 708 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  P  e.  CC )
133132exp0d 11235 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( P ^ 0 )  =  1 )
134131, 133eqtrd 2318 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( P ^ -u ( P 
pCnt  p ) )  =  1 )
135116, 120, 1343eqtrd 2322 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( J `  P
) `  p )  =  1 )
136135oveq1d 5836 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( ( J `  P ) `  p
)  ^ c  R
)  =  ( 1  ^ c  R ) )
137 2re 9812 . . . . . . . . . . . . 13  |-  2  e.  RR
138137a1i 12 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
2  e.  RR )
139 ostth3.6 . . . . . . . . . . . . . 14  |-  S  =  if ( ( F `
 P )  <_ 
( F `  p
) ,  ( F `
 p ) ,  ( F `  P
) )
1402ad2antrr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  F  e.  A )
14111, 13abvcl 15585 . . . . . . . . . . . . . . . . . 18  |-  ( ( F  e.  A  /\  p  e.  QQ )  ->  ( F `  p
)  e.  RR )
142140, 106, 141syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( F `  p )  e.  RR )
14311, 13, 17abvgt0 15589 . . . . . . . . . . . . . . . . . 18  |-  ( ( F  e.  A  /\  p  e.  QQ  /\  p  =/=  0 )  ->  0  <  ( F `  p
) )
144140, 106, 117, 143syl3anc 1184 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  0  <  ( F `  p
) )
145142, 144elrpd 10385 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( F `  p )  e.  RR+ )
146145adantrr 699 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( F `  p
)  e.  RR+ )
14720ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( F `  P
)  e.  RR+ )
148 ifcl 3604 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  p
)  e.  RR+  /\  ( F `  P )  e.  RR+ )  ->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  e.  RR+ )
149146, 147, 148syl2anc 644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  e.  RR+ )
150139, 149syl5eqel 2370 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  e.  RR+ )
151150rprecred 10398 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( 1  /  S
)  e.  RR )
152 simprr 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( F `  p
)  <  1 )
15328ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( F `  P
)  <  1 )
154 breq1 4029 . . . . . . . . . . . . . . . 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 ) )
155 breq1 4029 . . . . . . . . . . . . . . . 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 ) )
156154, 155ifboth 3599 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  p
)  <  1  /\  ( F `  P )  <  1 )  ->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  <  1 )
157152, 153, 156syl2anc 644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  if ( ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )  <  1 )
158139, 157syl5eqbr 4059 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  <  1 )
159150reclt1d 10400 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( S  <  1  <->  1  <  ( 1  /  S ) ) )
160158, 159mpbid 203 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
1  <  ( 1  /  S ) )
161 expnbnd 11226 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR  /\  ( 1  /  S
)  e.  RR  /\  1  <  ( 1  /  S ) )  ->  E. k  e.  NN  2  <  ( ( 1  /  S ) ^
k ) )
162138, 151, 160, 161syl3anc 1184 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  E. k  e.  NN  2  <  ( ( 1  /  S ) ^
k ) )
163150rpred 10387 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  e.  RR )
164163recnd 8858 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  e.  CC )
165164adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  S  e.  CC )
166150rpne0d 10392 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  S  =/=  0 )
167166adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  S  =/=  0 )
168 nnz 10042 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  NN  ->  k  e.  ZZ )
169168adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  k  e.  ZZ )
170165, 167, 169exprecd 11249 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( 1  /  S
) ^ k )  =  ( 1  / 
( S ^ k
) ) )
1712ad3antrrr 712 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  F  e.  A )
172 ax-1ne0 8803 . . . . . . . . . . . . . . . . . 18  |-  1  =/=  0
17312qrng1 20767 . . . . . . . . . . . . . . . . . . 19  |-  1  =  ( 1r `  Q )
17411, 173, 17abv1z 15593 . . . . . . . . . . . . . . . . . 18  |-  ( ( F  e.  A  /\  1  =/=  0 )  -> 
( F `  1
)  =  1 )
175171, 172, 174sylancl 645 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( F `  1 )  =  1 )
1768ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  P  e.  NN )
177 nnnn0 9969 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN  ->  k  e.  NN0 )
178 nnexpcl 11112 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  e.  NN  /\  k  e.  NN0 )  -> 
( P ^ k
)  e.  NN )
179176, 177, 178syl2an 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( P ^ k )  e.  NN )
180179nnzd 10113 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( P ^ k )  e.  ZZ )
181103ad2antlr 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  p  e.  NN )
182 nnexpcl 11112 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( p  e.  NN  /\  k  e.  NN0 )  -> 
( p ^ k
)  e.  NN )
183181, 177, 182syl2an 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
p ^ k )  e.  NN )
184183nnzd 10113 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
p ^ k )  e.  ZZ )
185 bezout 12717 . . . . . . . . . . . . . . . . . . 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
) ) )
186180, 184, 185syl2anc 644 . . . . . . . . . . . . . . . . . 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 ) ) )
187 simprl 734 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  P  =/=  p )
1883ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  P  e.  Prime )
189 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  p  e.  Prime )
190 prmrp 12776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( P  e.  Prime  /\  p  e.  Prime )  ->  (
( P  gcd  p
)  =  1  <->  P  =/=  p ) )
191188, 189, 190syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( ( P  gcd  p )  =  1  <-> 
P  =/=  p ) )
192187, 191mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( P  gcd  p
)  =  1 )
193192adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( P  gcd  p )  =  1 )
194176adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  P  e.  NN )
195181adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  p  e.  NN )
196 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  k  e.  NN )
197 rppwr 12732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( P  e.  NN  /\  p  e.  NN  /\  k  e.  NN )  ->  (
( P  gcd  p
)  =  1  -> 
( ( P ^
k )  gcd  (
p ^ k ) )  =  1 ) )
198194, 195, 196, 197syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( P  gcd  p
)  =  1  -> 
( ( P ^
k )  gcd  (
p ^ k ) )  =  1 ) )
199193, 198mpd 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( P ^ k
)  gcd  ( p ^ k ) )  =  1 )
200199adantrr 699 . . . . . . . . . . . . . . . . . . . . . 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 )
201200eqeq1d 2294 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
2022ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  F  e.  A )
203179adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( P ^ k )  e.  NN )
204 nnq 10326 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( P ^ k )  e.  NN  ->  ( P ^ k )  e.  QQ )
205203, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( P ^ k )  e.  QQ )
206 simprrl 742 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  a  e.  ZZ )
207 zq 10319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  e.  ZZ  ->  a  e.  QQ )
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  a  e.  QQ )
209 qmulcl 10331 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( P ^ k
)  e.  QQ  /\  a  e.  QQ )  ->  ( ( P ^
k )  x.  a
)  e.  QQ )
210205, 208, 209syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
211183adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
p ^ k )  e.  NN )
212 nnq 10326 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( p ^ k )  e.  NN  ->  (
p ^ k )  e.  QQ )
213211, 212syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
p ^ k )  e.  QQ )
214 simprrr 743 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  b  e.  ZZ )
215 zq 10319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  e.  ZZ  ->  b  e.  QQ )
216214, 215syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  b  e.  QQ )
217 qmulcl 10331 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( p ^ k
)  e.  QQ  /\  b  e.  QQ )  ->  ( ( p ^
k )  x.  b
)  e.  QQ )
218213, 216, 217syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
219 qaddcl 10329 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( P ^
k )  x.  a
)  e.  QQ  /\  ( ( p ^
k )  x.  b
)  e.  QQ )  ->  ( ( ( P ^ k )  x.  a )  +  ( ( p ^
k )  x.  b
) )  e.  QQ )
220210, 218, 219syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 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 )
22111, 13abvcl 15585 . . . . . . . . . . . . . . . . . . . . . . . 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 )
222202, 220, 221syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . 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 )
22311, 13abvcl 15585 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F  e.  A  /\  ( ( P ^
k )  x.  a
)  e.  QQ )  ->  ( F `  ( ( P ^
k )  x.  a
) )  e.  RR )
224202, 210, 223syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 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 )
22511, 13abvcl 15585 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F  e.  A  /\  ( ( p ^
k )  x.  b
)  e.  QQ )  ->  ( F `  ( ( p ^
k )  x.  b
) )  e.  RR )
226202, 218, 225syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 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 )
227224, 226readdcld 8859 . . . . . . . . . . . . . . . . . . . . . . 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 )
228 rpexpcl 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( S  e.  RR+  /\  k  e.  ZZ )  ->  ( S ^ k )  e.  RR+ )
229150, 168, 228syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( S ^ k )  e.  RR+ )
230229rpred 10387 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( S ^ k )  e.  RR )
231230adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( S ^ k )  e.  RR )
232 remulcl 8819 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2  e.  RR  /\  ( S ^ k )  e.  RR )  -> 
( 2  x.  ( S ^ k ) )  e.  RR )
233137, 231, 232sylancr 646 . . . . . . . . . . . . . . . . . . . . . . 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 )
234 qex 10325 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  QQ  e.  _V
235 cnfldadd 16380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  +  =  ( +g  ` fld )
23612, 235ressplusg 13246 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( QQ  e.  _V  ->  +  =  ( +g  `  Q
) )
237234, 236ax-mp 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  +  =  ( +g  `  Q )
23811, 13, 237abvtri 15591 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
239202, 210, 218, 238syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
240 cnfldmul 16381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  x.  =  ( .r ` fld )
24112, 240ressmulr 13257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( QQ  e.  _V  ->  x.  =  ( .r `  Q ) )
242234, 241ax-mp 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  x.  =  ( .r `  Q )
24311, 13, 242abvmul 15590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F  e.  A  /\  ( P ^ k )  e.  QQ  /\  a  e.  QQ )  ->  ( F `  ( ( P ^ k )  x.  a ) )  =  ( ( F `  ( P ^ k ) )  x.  ( F `
 a ) ) )
244202, 205, 208, 243syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
24510ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  P  e.  QQ )
246177ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  k  e.  NN0 )
24712, 11qabvexp 20771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  A  /\  P  e.  QQ  /\  k  e.  NN0 )  ->  ( F `  ( P ^ k ) )  =  ( ( F `
 P ) ^
k ) )
248202, 245, 246, 247syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
249248oveq1d 5836 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
250244, 249eqtrd 2318 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
251202, 245, 14syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  P )  e.  RR )
252251, 246reexpcld 11258 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  P
) ^ k )  e.  RR )
25311, 13abvcl 15585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  A  /\  a  e.  QQ )  ->  ( F `  a
)  e.  RR )
254202, 208, 253syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  a )  e.  RR )
255252, 254remulcld 8860 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
256 elz 10023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( a  e.  ZZ  <->  ( a  e.  RR  /\  ( a  =  0  \/  a  e.  NN  \/  -u a  e.  NN ) ) )
257256simprbi 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( a  e.  ZZ  ->  (
a  =  0  \/  a  e.  NN  \/  -u a  e.  NN ) )
258257adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( a  =  0  \/  a  e.  NN  \/  -u a  e.  NN ) )
25911, 17abv0 15592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( F  e.  A  ->  ( F `  0 )  =  0 )
2602, 259syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( F `  0
)  =  0 )
261 0le1 9294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  0  <_  1
262260, 261syl6eqbr 4063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( F `  0
)  <_  1 )
263262adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( F `
 0 )  <_ 
1 )
264 fveq2 5487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( a  =  0  ->  ( F `  a )  =  ( F ` 
0 ) )
265264breq1d 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( a  =  0  ->  (
( F `  a
)  <_  1  <->  ( F `  0 )  <_ 
1 ) )
266263, 265syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( a  =  0  ->  ( F `  a )  <_  1 ) )
267 ostth3.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  A. n  e.  NN  -.  1  <  ( F `
 n ) )
268 nnq 10326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( n  e.  NN  ->  n  e.  QQ )
26911, 13abvcl 15585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( F  e.  A  /\  n  e.  QQ )  ->  ( F `  n
)  e.  RR )
2702, 268, 269syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  e.  RR )
271 1re 8834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  1  e.  RR
272 lenlt 8898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( F `  n
)  e.  RR  /\  1  e.  RR )  ->  ( ( F `  n )  <_  1  <->  -.  1  <  ( F `
 n ) ) )
273270, 271, 272sylancl 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( F `  n )  <_  1  <->  -.  1  <  ( F `  n
) ) )
274273ralbidva 2562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( A. n  e.  NN  ( F `  n )  <_  1  <->  A. n  e.  NN  -.  1  <  ( F `  n ) ) )
275267, 274mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  A. n  e.  NN  ( F `  n )  <_  1 )
276 fveq2 5487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  a  ->  ( F `  n )  =  ( F `  a ) )
277276breq1d 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  =  a  ->  (
( F `  n
)  <_  1  <->  ( F `  a )  <_  1
) )
278277rspccv 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( A. n  e.  NN  ( F `  n )  <_  1  ->  ( a  e.  NN  ->  ( F `  a )  <_  1
) )
279275, 278syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( a  e.  NN  ->  ( F `  a
)  <_  1 ) )
280279adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( a  e.  NN  ->  ( F `  a )  <_  1 ) )
2812adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  ->  F  e.  A )
282207ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
a  e.  QQ )
283 eqid 2286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( inv g `  Q )  =  ( inv g `  Q )
28411, 13, 283abvneg 15595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( F  e.  A  /\  a  e.  QQ )  ->  ( F `  (
( inv g `  Q ) `  a
) )  =  ( F `  a ) )
285281, 282, 284syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( F `  (
( inv g `  Q ) `  a
) )  =  ( F `  a ) )
28612qrngneg 20768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( a  e.  QQ  ->  (
( inv g `  Q ) `  a
)  =  -u a
)
287282, 286syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( ( inv g `  Q ) `  a
)  =  -u a
)
288 simprr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  ->  -u a  e.  NN )
289287, 288eqeltrd 2360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( ( inv g `  Q ) `  a
)  e.  NN )
290275adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  ->  A. n  e.  NN  ( F `  n )  <_  1 )
291 fveq2 5487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( n  =  ( ( inv g `  Q ) `
 a )  -> 
( F `  n
)  =  ( F `
 ( ( inv g `  Q ) `
 a ) ) )
292291breq1d 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  ( ( inv g `  Q ) `
 a )  -> 
( ( F `  n )  <_  1  <->  ( F `  ( ( inv g `  Q
) `  a )
)  <_  1 ) )
293292rspcv 2883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( inv g `  Q ) `  a
)  e.  NN  ->  ( A. n  e.  NN  ( F `  n )  <_  1  ->  ( F `  ( ( inv g `  Q ) `
 a ) )  <_  1 ) )
294289, 290, 293sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( F `  (
( inv g `  Q ) `  a
) )  <_  1
)
295285, 294eqbrtrrd 4048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  ( a  e.  ZZ  /\  -u a  e.  NN ) )  -> 
( F `  a
)  <_  1 )
296295expr 600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( -u a  e.  NN  ->  ( F `  a )  <_  1 ) )
297266, 280, 2963jaod 1248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( ( a  =  0  \/  a  e.  NN  \/  -u a  e.  NN )  ->  ( F `  a )  <_  1
) )
298258, 297mpd 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  a  e.  ZZ )  ->  ( F `
 a )  <_ 
1 )
299298ralrimiva 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  A. a  e.  ZZ  ( F `  a )  <_  1 )
300299ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
301 rsp 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. a  e.  ZZ  ( F `  a )  <_  1  ->  ( a  e.  ZZ  ->  ( F `  a )  <_  1
) )
302300, 206, 301sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  a )  <_  1 )
303271a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  1  e.  RR )
304168ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  k  e.  ZZ )
30519ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <  ( F `  P
) )
306 expgt0 11131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( F `  P
)  e.  RR  /\  k  e.  ZZ  /\  0  <  ( F `  P
) )  ->  0  <  ( ( F `  P ) ^ k
) )
307251, 304, 305, 306syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <  ( ( F `  P ) ^ k
) )
308 lemul2 9606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
309254, 303, 252, 307, 308syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
310302, 309mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
311252recnd 8858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  P
) ^ k )  e.  CC )
312311mulid1d 8849 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
313310, 312breqtrd 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
314163adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  S  e.  RR )
315147adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  P )  e.  RR+ )
316315rpge0d 10391 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <_  ( F `  P
) )
317181adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  p  e.  NN )
318317, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  p  e.  QQ )
319202, 318, 141syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  p )  e.  RR )
320 max1 10510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( F `  P
)  e.  RR  /\  ( F `  p )  e.  RR )  -> 
( F `  P
)  <_  if (
( F `  P
)  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) ) )
321251, 319, 320syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
322321, 139syl6breqr 4066 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  P )  <_  S )
323 leexp1a 11156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  P )  e.  RR  /\  S  e.  RR  /\  k  e.  NN0 )  /\  ( 0  <_  ( F `  P )  /\  ( F `  P
)  <_  S )
)  ->  ( ( F `  P ) ^ k )  <_ 
( S ^ k
) )
324251, 314, 246, 316, 322, 323syl32anc 1192 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  P
) ^ k )  <_  ( S ^
k ) )
325255, 252, 231, 313, 324letrd 8970 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
326250, 325eqbrtrd 4046 . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
32711, 13, 242abvmul 15590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F  e.  A  /\  ( p ^ k
)  e.  QQ  /\  b  e.  QQ )  ->  ( F `  (
( p ^ k
)  x.  b ) )  =  ( ( F `  ( p ^ k ) )  x.  ( F `  b ) ) )
328202, 213, 216, 327syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
32912, 11qabvexp 20771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  A  /\  p  e.  QQ  /\  k  e.  NN0 )  ->  ( F `  ( p ^ k ) )  =  ( ( F `
 p ) ^
k ) )
330202, 318, 246, 329syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
331330oveq1d 5836 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
332328, 331eqtrd 2318 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
333319, 246reexpcld 11258 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  p
) ^ k )  e.  RR )
33411, 13abvcl 15585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  A  /\  b  e.  QQ )  ->  ( F `  b
)  e.  RR )
335202, 216, 334syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  b )  e.  RR )
336333, 335remulcld 8860 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
337 fveq2 5487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  b  ->  ( F `  a )  =  ( F `  b ) )
338337breq1d 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a  =  b  ->  (
( F `  a
)  <_  1  <->  ( F `  b )  <_  1
) )
339338rspcv 2883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  e.  ZZ  ->  ( A. a  e.  ZZ  ( F `  a )  <_  1  ->  ( F `  b )  <_  1 ) )
340214, 300, 339sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  b )  <_  1 )
341317nnne0d 9787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  p  =/=  0 )
342202, 318, 341, 143syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <  ( F `  p
) )
343 expgt0 11131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( F `  p
)  e.  RR  /\  k  e.  ZZ  /\  0  <  ( F `  p
) )  ->  0  <  ( ( F `  p ) ^ k
) )
344319, 304, 342, 343syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <  ( ( F `  p ) ^ k
) )
345 lemul2 9606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
346335, 303, 333, 344, 345syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
347340, 346mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
348333recnd 8858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  p
) ^ k )  e.  CC )
349348mulid1d 8849 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
350347, 349breqtrd 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
351146adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  p )  e.  RR+ )
352351rpge0d 10391 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  0  <_  ( F `  p
) )
353 max2 10512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( F `  P
)  e.  RR  /\  ( F `  p )  e.  RR )  -> 
( F `  p
)  <_  if (
( F `  P
)  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) ) )
354251, 319, 353syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
355354, 139syl6breqr 4066 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  ( F `  p )  <_  S )
356 leexp1a 11156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F `  p )  e.  RR  /\  S  e.  RR  /\  k  e.  NN0 )  /\  ( 0  <_  ( F `  p )  /\  ( F `  p
)  <_  S )
)  ->  ( ( F `  p ) ^ k )  <_ 
( S ^ k
) )
357319, 314, 246, 352, 355, 356syl32anc 1192 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  ( k  e.  NN  /\  (
a  e.  ZZ  /\  b  e.  ZZ )
) )  ->  (
( F `  p
) ^ k )  <_  ( S ^
k ) )
358336, 333, 231, 350, 357letrd 8970 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
359332, 358eqbrtrd 4046 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
360224, 226, 231, 231, 326, 359le2addd 9387 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
361230recnd 8858 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( S ^ k )  e.  CC )
3623612timesd 9951 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
2  x.  ( S ^ k ) )  =  ( ( S ^ k )  +  ( S ^ k
) ) )
363362adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
364360, 363breqtrrd 4052 . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
365222, 227, 233, 239, 364letrd 8970 . . . . . . . . . . . . . . . . . . . . . 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
) ) )
366 fveq2 5487 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1  =  ( ( ( P ^ k )  x.  a )  +  ( ( p ^
k )  x.  b
) )  ->  ( F `  1 )  =  ( F `  ( ( ( P ^ k )  x.  a )  +  ( ( p ^ k
)  x.  b ) ) ) )
367366breq1d 4036 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
368365, 367syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
369201, 368sylbid 208 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
370369anassrs 631 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
371370rexlimdvva 2677 . . . . . . . . . . . . . . . . . 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 ) ) ) )
372186, 371mpd 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  ( F `  1 )  <_  ( 2  x.  ( S ^ k ) ) )
373175, 372eqbrtrrd 4048 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  1  <_  ( 2  x.  ( S ^ k ) ) )
374229rpregt0d 10393 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( S ^ k
)  e.  RR  /\  0  <  ( S ^
k ) ) )
375 ledivmul2 9630 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  RR  /\  2  e.  RR  /\  (
( S ^ k
)  e.  RR  /\  0  <  ( S ^
k ) ) )  ->  ( ( 1  /  ( S ^
k ) )  <_ 
2  <->  1  <_  (
2  x.  ( S ^ k ) ) ) )
376271, 137, 375mp3an12 1269 . . . . . . . . . . . . . . . . 17  |-  ( ( ( S ^ k
)  e.  RR  /\  0  <  ( S ^
k ) )  -> 
( ( 1  / 
( S ^ k
) )  <_  2  <->  1  <_  ( 2  x.  ( S ^ k
) ) ) )
377374, 376syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( 1  /  ( S ^ k ) )  <_  2  <->  1  <_  ( 2  x.  ( S ^ k ) ) ) )
378373, 377mpbird 225 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
1  /  ( S ^ k ) )  <_  2 )
379170, 378eqbrtrd 4046 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( 1  /  S
) ^ k )  <_  2 )
380 reexpcl 11116 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  /  S
)  e.  RR  /\  k  e.  NN0 )  -> 
( ( 1  /  S ) ^ k
)  e.  RR )
381151, 177, 380syl2an 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( 1  /  S
) ^ k )  e.  RR )
382 lenlt 8898 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 1  /  S ) ^ k
)  e.  RR  /\  2  e.  RR )  ->  ( ( ( 1  /  S ) ^
k )  <_  2  <->  -.  2  <  ( ( 1  /  S ) ^ k ) ) )
383381, 137, 382sylancl 645 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
( ( 1  /  S ) ^ k
)  <_  2  <->  -.  2  <  ( ( 1  /  S ) ^ k
) ) )
384379, 383mpbid 203 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  -.  2  <  ( ( 1  /  S ) ^
k ) )
385384pm2.21d 100 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p
)  <  1 ) )  /\  k  e.  NN )  ->  (
2  <  ( (
1  /  S ) ^ k )  ->  -.  ( F `  p
)  <  1 ) )
386385rexlimdva 2670 . . . . . . . . . . 11  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  -> 
( E. k  e.  NN  2  <  (
( 1  /  S
) ^ k )  ->  -.  ( F `  p )  <  1
) )
387162, 386mpd 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  p  e.  Prime )  /\  ( P  =/=  p  /\  ( F `  p )  <  1 ) )  ->  -.  ( F `  p
)  <  1 )
388387expr 600 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( F `  p
)  <  1  ->  -.  ( F `  p
)  <  1 ) )
389388pm2.01d 163 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -.  ( F `  p )  <  1 )
390267ad2antrr 708 . . . . . . . . 9  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  A. n  e.  NN  -.  1  < 
( F `  n
) )
391 fveq2 5487 . . . . . . . . . . . 12  |-  ( n  =  p  ->  ( F `  n )  =  ( F `  p ) )
392391breq2d 4038 . . . . . . . . . . 11  |-  ( n  =  p  ->  (
1  <  ( F `  n )  <->  1  <  ( F `  p ) ) )
393392notbid 287 . . . . . . . . . 10  |-  ( n  =  p  ->  ( -.  1  <  ( F `
 n )  <->  -.  1  <  ( F `  p
) ) )
394393rspcv 2883 . . . . . . . . 9  |-  ( p  e.  NN  ->  ( A. n  e.  NN  -.  1  <  ( F `
 n )  ->  -.  1  <  ( F `
 p ) ) )
395104, 390, 394sylc 58 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  -.  1  <  ( F `  p ) )
396 lttri3 8902 . . . . . . . . 9  |-  ( ( ( F `  p
)  e.  RR  /\  1  e.  RR )  ->  ( ( F `  p )  =  1  <-> 
( -.  ( F `
 p )  <  1  /\  -.  1  <  ( F `  p
) ) ) )
397142, 271, 396sylancl 645 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( F `  p
)  =  1  <->  ( -.  ( F `  p
)  <  1  /\  -.  1  <  ( F `
 p ) ) ) )
398389, 395, 397mpbir2and 890 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( F `  p )  =  1 )
399113, 136, 3983eqtr4d 2328 . . . . . 6  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  (
( ( J `  P ) `  p
)  ^ c  R
)  =  ( F `
 p ) )
400111, 399eqtr2d 2319 . . . . 5  |-  ( ( ( ph  /\  p  e.  Prime )  /\  P  =/=  p )  ->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^ c  R )
) `  p )
)
401400ex 425 . . . 4  |-  ( (
ph  /\  p  e.  Prime )  ->  ( P  =/=  p  ->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) ) `  p ) ) )
402102, 401pm2.61dne 2526 . . 3  |-  ( (
ph  /\  p  e.  Prime )  ->  ( F `  p )  =  ( ( y  e.  QQ  |->  ( ( ( J `
 P ) `  y )  ^ c  R ) ) `  p ) )
40312, 11, 2, 49, 402ostthlem2 20773 . 2  |-  ( ph  ->  F  =  ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^ c  R )
) )
404 oveq2 5829 . . . . 5  |-  ( a  =  R  ->  (
( ( J `  P ) `  y
)  ^ c  a )  =  ( ( ( J `  P
) `  y )  ^ c  R )
)
405404mpteq2dv 4110 . . . 4  |-  ( a  =  R  ->  (
y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^ c  a ) )  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `  y
)  ^ c  R
) ) )
406405eqeq2d 2297 . . 3  |-  ( a  =  R  ->  ( F  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^ c  a ) )  <-> 
F  =  ( y  e.  QQ  |->  ( ( ( J `  P
) `  y )  ^ c  R )
) ) )
407406rspcev 2887 . 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 ) ) )
40846, 403, 407syl2anc 644 1  |-  ( ph  ->  E. a  e.  RR+  F  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `
 y )  ^ c  a ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360    \/ w3o 935    = wceq 1625    e. wcel 1687    =/= wne 2449   A.wral 2546   E.wrex 2547   _Vcvv 2791   ifcif 3568   class class class wbr 4026    e. cmpt 4080   ` cfv 5223  (class class class)co 5821   CCcc 8732   RRcr 8733   0cc0 8734   1c1 8735    + caddc 8737    x. cmul 8739    < clt 8864    <_ cle 8865   -ucneg 9035    / cdiv 9420   NNcn 9743   2c2 9792   NN0cn0 9962   ZZcz 10021   ZZ>=cuz 10227   QQcq 10313   RR+crp 10351   ^cexp 11100   expce 12339    || cdivides 12527    gcd cgcd 12681   Primecprime 12754    pCnt cpc 12885   ↾s cress 13145   +g cplusg 13204   .rcmulr 13205   inv gcminusg 14359  AbsValcabv 15577  ℂfldccnfld 16373   logclog 19908    ^ c ccxp 19909
This theorem is referenced by:  ostth  20784
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-rep 4134  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513  ax-inf2 7339  ax-cnex 8790  ax-resscn 8791  ax-1cn 8792  ax-icn 8793  ax-addcl 8794  ax-addrcl 8795  ax-mulcl 8796  ax-mulrcl 8797  ax-mulcom 8798  ax-addass 8799  ax-mulass 8800  ax-distr 8801  ax-i2m1 8802  ax-1ne0 8803  ax-1rid 8804  ax-rnegex 8805  ax-rrecex 8806  ax-cnre 8807  ax-pre-lttri 8808  ax-pre-lttrn 8809  ax-pre-ltadd 8810  ax-pre-mulgt0 8811  ax-pre-sup 8812  ax-addf 8813  ax-mulf 8814
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-nel 2452  df-ral 2551  df-rex 2552  df-reu 2553  df-rmo 2554  df-rab 2555  df-v 2793  df-sbc 2995  df-csb 3085  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-pss 3171  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-tp 3651  df-op 3652  df-uni 3831  df-int 3866  df-iun 3910  df-iin 3911  df-br 4027  df-opab 4081  df-mpt 4082  df-tr 4117  df-eprel 4306  df-id 4310  df-po 4315  df-so 4316  df-fr 4353  df-se 4354  df-we 4355  df-ord 4396  df-on 4397  df-lim 4398  df-suc 4399  df-om 4658  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-f1 5228  df-fo 5229  df-f1o 5230  df-fv 5231  df-isom 5232  df-ov 5824  df-oprab 5825  df-mpt2 5826  df-of 6041  df-1st 6085  df-2nd 6086  df-tpos 6197  df-iota 6254  df-riota 6301  df-recs 6385  df-rdg 6420  df-1o 6476  df-2o 6477  df-oadd 6480  df-er 6657  df-map 6771  df-pm 6772  df-ixp 6815  df-en 6861  df-dom 6862  df-sdom 6863  df-fin 6864  df-fi 7162  df-sup 7191  df-oi 7222  df-card 7569  df-cda 7791  df-pnf 8866  df-mnf 8867  df-xr 8868  df-ltxr 8869  df-le 8870  df-sub 9036  df-neg 9037  df-div 9421  df-nn 9744  df-2 9801  df-3 9802  df-4 9803  df-5 9804  df-6 9805  df-7 9806  df-8 9807  df-9 9808  df-10 9809  df-n0 9963  df-z 10022  df-dec 10122  df-uz 10228  df-q 10314  df-rp 10352  df-xneg 10449  df-xadd 10450  df-xmul 10451  df-ioo 10656  df-ioc 10657  df-ico