Metamath Proof Explorer

Theorem ostth3

Description: - Lemma for ostth : p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q 
|- Q = ( CCfld |`s 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 ostth3 
|- ( ph -> E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c a ) ) )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qabsabv.a 
 |-  A = ( AbsVal ` Q )
3 padic.j 
 |-  J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
4 ostth.k 
 |-  K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )
5 ostth.1 
 |-  ( ph -> F e. A )
6 ostth3.2 
 |-  ( ph -> A. n e. NN -. 1 < ( F ` n ) )
7 ostth3.3 
 |-  ( ph -> P e. Prime )
8 ostth3.4 
 |-  ( ph -> ( F ` P ) < 1 )
9 ostth3.5 
 |-  R = -u ( ( log ` ( F ` P ) ) / ( log ` P ) )
10 ostth3.6 
 |-  S = if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) )
11 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
12 7 11 syl 
 |-  ( ph -> P e. ( ZZ>= ` 2 ) )
13 eluz2b2 
 |-  ( P e. ( ZZ>= ` 2 ) <-> ( P e. NN /\ 1 < P ) )
14 12 13 sylib 
 |-  ( ph -> ( P e. NN /\ 1 < P ) )
15 14 simpld 
 |-  ( ph -> P e. NN )
16 nnq 
 |-  ( P e. NN -> P e. QQ )
17 15 16 syl 
 |-  ( ph -> P e. QQ )
18 1 qrngbas 
 |-  QQ = ( Base ` Q )
19 2 18 abvcl 
 |-  ( ( F e. A /\ P e. QQ ) -> ( F ` P ) e. RR )
20 5 17 19 syl2anc 
 |-  ( ph -> ( F ` P ) e. RR )
21 15 nnne0d 
 |-  ( ph -> P =/= 0 )
22 1 qrng0 
 |-  0 = ( 0g ` Q )
23 2 18 22 abvgt0 
 |-  ( ( F e. A /\ P e. QQ /\ P =/= 0 ) -> 0 < ( F ` P ) )
24 5 17 21 23 syl3anc 
 |-  ( ph -> 0 < ( F ` P ) )
25 20 24 elrpd 
 |-  ( ph -> ( F ` P ) e. RR+ )
26 25 relogcld 
 |-  ( ph -> ( log ` ( F ` P ) ) e. RR )
27 15 nnred 
 |-  ( ph -> P e. RR )
28 14 simprd 
 |-  ( ph -> 1 < P )
29 27 28 rplogcld 
 |-  ( ph -> ( log ` P ) e. RR+ )
30 26 29 rerpdivcld 
 |-  ( ph -> ( ( log ` ( F ` P ) ) / ( log ` P ) ) e. RR )
31 30 renegcld 
 |-  ( ph -> -u ( ( log ` ( F ` P ) ) / ( log ` P ) ) e. RR )
32 9 31 eqeltrid 
 |-  ( ph -> R e. RR )
33 1rp 
 |-  1 e. RR+
34 logltb 
 |-  ( ( ( F ` P ) e. RR+ /\ 1 e. RR+ ) -> ( ( F ` P ) < 1 <-> ( log ` ( F ` P ) ) < ( log ` 1 ) ) )
35 25 33 34 sylancl 
 |-  ( ph -> ( ( F ` P ) < 1 <-> ( log ` ( F ` P ) ) < ( log ` 1 ) ) )
36 8 35 mpbid 
 |-  ( ph -> ( log ` ( F ` P ) ) < ( log ` 1 ) )
37 log1 
 |-  ( log ` 1 ) = 0
38 36 37 breqtrdi 
 |-  ( ph -> ( log ` ( F ` P ) ) < 0 )
39 29 rpcnd 
 |-  ( ph -> ( log ` P ) e. CC )
40 39 mul01d 
 |-  ( ph -> ( ( log ` P ) x. 0 ) = 0 )
41 38 40 breqtrrd 
 |-  ( ph -> ( log ` ( F ` P ) ) < ( ( log ` P ) x. 0 ) )
42 0red 
 |-  ( ph -> 0 e. RR )
43 26 42 29 ltdivmuld 
 |-  ( ph -> ( ( ( log ` ( F ` P ) ) / ( log ` P ) ) < 0 <-> ( log ` ( F ` P ) ) < ( ( log ` P ) x. 0 ) ) )
44 41 43 mpbird 
 |-  ( ph -> ( ( log ` ( F ` P ) ) / ( log ` P ) ) < 0 )
45 30 lt0neg1d 
 |-  ( ph -> ( ( ( log ` ( F ` P ) ) / ( log ` P ) ) < 0 <-> 0 < -u ( ( log ` ( F ` P ) ) / ( log ` P ) ) ) )
46 44 45 mpbid 
 |-  ( ph -> 0 < -u ( ( log ` ( F ` P ) ) / ( log ` P ) ) )
47 46 9 breqtrrdi 
 |-  ( ph -> 0 < R )
48 32 47 elrpd 
 |-  ( ph -> R e. RR+ )
49 1 2 3 padicabvcxp 
 |-  ( ( P e. Prime /\ R e. RR+ ) -> ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) e. A )
50 7 48 49 syl2anc 
 |-  ( ph -> ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) e. A )
51 fveq2 
 |-  ( y = P -> ( ( J ` P ) ` y ) = ( ( J ` P ) ` P ) )
52 51 oveq1d 
 |-  ( y = P -> ( ( ( J ` P ) ` y ) ^c R ) = ( ( ( J ` P ) ` P ) ^c R ) )
53 eqid 
 |-  ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) = ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) )
54 ovex 
 |-  ( ( ( J ` P ) ` P ) ^c R ) e. _V
55 52 53 54 fvmpt 
 |-  ( P e. QQ -> ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` P ) = ( ( ( J ` P ) ` P ) ^c R ) )
56 17 55 syl 
 |-  ( ph -> ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` P ) = ( ( ( J ` P ) ` P ) ^c R ) )
57 3 padicval 
 |-  ( ( P e. Prime /\ P e. QQ ) -> ( ( J ` P ) ` P ) = if ( P = 0 , 0 , ( P ^ -u ( P pCnt P ) ) ) )
58 7 17 57 syl2anc 
 |-  ( ph -> ( ( J ` P ) ` P ) = if ( P = 0 , 0 , ( P ^ -u ( P pCnt P ) ) ) )
59 21 neneqd 
 |-  ( ph -> -. P = 0 )
60 59 iffalsed 
 |-  ( ph -> if ( P = 0 , 0 , ( P ^ -u ( P pCnt P ) ) ) = ( P ^ -u ( P pCnt P ) ) )
61 15 nncnd 
 |-  ( ph -> P e. CC )
62 61 exp1d 
 |-  ( ph -> ( P ^ 1 ) = P )
63 62 oveq2d 
 |-  ( ph -> ( P pCnt ( P ^ 1 ) ) = ( P pCnt P ) )
64 1z 
 |-  1 e. ZZ
65 pcid 
 |-  ( ( P e. Prime /\ 1 e. ZZ ) -> ( P pCnt ( P ^ 1 ) ) = 1 )
66 7 64 65 sylancl 
 |-  ( ph -> ( P pCnt ( P ^ 1 ) ) = 1 )
67 63 66 eqtr3d 
 |-  ( ph -> ( P pCnt P ) = 1 )
68 67 negeqd 
 |-  ( ph -> -u ( P pCnt P ) = -u 1 )
69 68 oveq2d 
 |-  ( ph -> ( P ^ -u ( P pCnt P ) ) = ( P ^ -u 1 ) )
70 neg1z 
 |-  -u 1 e. ZZ
71 70 a1i 
 |-  ( ph -> -u 1 e. ZZ )
72 61 21 71 cxpexpzd 
 |-  ( ph -> ( P ^c -u 1 ) = ( P ^ -u 1 ) )
73 69 72 eqtr4d 
 |-  ( ph -> ( P ^ -u ( P pCnt P ) ) = ( P ^c -u 1 ) )
74 58 60 73 3eqtrd 
 |-  ( ph -> ( ( J ` P ) ` P ) = ( P ^c -u 1 ) )
75 74 oveq1d 
 |-  ( ph -> ( ( ( J ` P ) ` P ) ^c R ) = ( ( P ^c -u 1 ) ^c R ) )
76 32 recnd 
 |-  ( ph -> R e. CC )
77 76 mulm1d 
 |-  ( ph -> ( -u 1 x. R ) = -u R )
78 9 negeqi 
 |-  -u R = -u -u ( ( log ` ( F ` P ) ) / ( log ` P ) )
79 30 recnd 
 |-  ( ph -> ( ( log ` ( F ` P ) ) / ( log ` P ) ) e. CC )
80 79 negnegd 
 |-  ( ph -> -u -u ( ( log ` ( F ` P ) ) / ( log ` P ) ) = ( ( log ` ( F ` P ) ) / ( log ` P ) ) )
81 78 80 eqtrid 
 |-  ( ph -> -u R = ( ( log ` ( F ` P ) ) / ( log ` P ) ) )
82 77 81 eqtrd 
 |-  ( ph -> ( -u 1 x. R ) = ( ( log ` ( F ` P ) ) / ( log ` P ) ) )
83 82 oveq2d 
 |-  ( ph -> ( P ^c ( -u 1 x. R ) ) = ( P ^c ( ( log ` ( F ` P ) ) / ( log ` P ) ) ) )
84 15 nnrpd 
 |-  ( ph -> P e. RR+ )
85 neg1rr 
 |-  -u 1 e. RR
86 85 a1i 
 |-  ( ph -> -u 1 e. RR )
87 84 86 76 cxpmuld 
 |-  ( ph -> ( P ^c ( -u 1 x. R ) ) = ( ( P ^c -u 1 ) ^c R ) )
88 61 21 79 cxpefd 
 |-  ( ph -> ( P ^c ( ( log ` ( F ` P ) ) / ( log ` P ) ) ) = ( exp ` ( ( ( log ` ( F ` P ) ) / ( log ` P ) ) x. ( log ` P ) ) ) )
89 26 recnd 
 |-  ( ph -> ( log ` ( F ` P ) ) e. CC )
90 29 rpne0d 
 |-  ( ph -> ( log ` P ) =/= 0 )
91 89 39 90 divcan1d 
 |-  ( ph -> ( ( ( log ` ( F ` P ) ) / ( log ` P ) ) x. ( log ` P ) ) = ( log ` ( F ` P ) ) )
92 91 fveq2d 
 |-  ( ph -> ( exp ` ( ( ( log ` ( F ` P ) ) / ( log ` P ) ) x. ( log ` P ) ) ) = ( exp ` ( log ` ( F ` P ) ) ) )
93 25 reeflogd 
 |-  ( ph -> ( exp ` ( log ` ( F ` P ) ) ) = ( F ` P ) )
94 88 92 93 3eqtrd 
 |-  ( ph -> ( P ^c ( ( log ` ( F ` P ) ) / ( log ` P ) ) ) = ( F ` P ) )
95 83 87 94 3eqtr3d 
 |-  ( ph -> ( ( P ^c -u 1 ) ^c R ) = ( F ` P ) )
96 56 75 95 3eqtrrd 
 |-  ( ph -> ( F ` P ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` P ) )
97 fveq2 
 |-  ( P = p -> ( F ` P ) = ( F ` p ) )
98 fveq2 
 |-  ( P = p -> ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` P ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) )
99 97 98 eqeq12d 
 |-  ( P = p -> ( ( F ` P ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` P ) <-> ( F ` p ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) ) )
100 96 99 syl5ibcom 
 |-  ( ph -> ( P = p -> ( F ` p ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) ) )
101 100 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( P = p -> ( F ` p ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) ) )
102 prmnn 
 |-  ( p e. Prime -> p e. NN )
103 102 ad2antlr 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> p e. NN )
104 nnq 
 |-  ( p e. NN -> p e. QQ )
105 103 104 syl 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> p e. QQ )
106 fveq2 
 |-  ( y = p -> ( ( J ` P ) ` y ) = ( ( J ` P ) ` p ) )
107 106 oveq1d 
 |-  ( y = p -> ( ( ( J ` P ) ` y ) ^c R ) = ( ( ( J ` P ) ` p ) ^c R ) )
108 ovex 
 |-  ( ( ( J ` P ) ` p ) ^c R ) e. _V
109 107 53 108 fvmpt 
 |-  ( p e. QQ -> ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) = ( ( ( J ` P ) ` p ) ^c R ) )
110 105 109 syl 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) = ( ( ( J ` P ) ` p ) ^c R ) )
111 76 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> R e. CC )
112 111 1cxpd 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( 1 ^c R ) = 1 )
113 7 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> P e. Prime )
114 3 padicval 
 |-  ( ( P e. Prime /\ p e. QQ ) -> ( ( J ` P ) ` p ) = if ( p = 0 , 0 , ( P ^ -u ( P pCnt p ) ) ) )
115 113 105 114 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( ( J ` P ) ` p ) = if ( p = 0 , 0 , ( P ^ -u ( P pCnt p ) ) ) )
116 103 nnne0d 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> p =/= 0 )
117 116 neneqd 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> -. p = 0 )
118 117 iffalsed 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> if ( p = 0 , 0 , ( P ^ -u ( P pCnt p ) ) ) = ( P ^ -u ( P pCnt p ) ) )
119 pceq0 
 |-  ( ( P e. Prime /\ p e. NN ) -> ( ( P pCnt p ) = 0 <-> -. P || p ) )
120 7 102 119 syl2an 
 |-  ( ( ph /\ p e. Prime ) -> ( ( P pCnt p ) = 0 <-> -. P || p ) )
121 dvdsprm 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ p e. Prime ) -> ( P || p <-> P = p ) )
122 12 121 sylan 
 |-  ( ( ph /\ p e. Prime ) -> ( P || p <-> P = p ) )
123 122 necon3bbid 
 |-  ( ( ph /\ p e. Prime ) -> ( -. P || p <-> P =/= p ) )
124 120 123 bitrd 
 |-  ( ( ph /\ p e. Prime ) -> ( ( P pCnt p ) = 0 <-> P =/= p ) )
125 124 biimpar 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( P pCnt p ) = 0 )
126 125 negeqd 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> -u ( P pCnt p ) = -u 0 )
127 neg0 
 |-  -u 0 = 0
128 126 127 eqtrdi 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> -u ( P pCnt p ) = 0 )
129 128 oveq2d 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( P ^ -u ( P pCnt p ) ) = ( P ^ 0 ) )
130 61 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> P e. CC )
131 130 exp0d 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( P ^ 0 ) = 1 )
132 129 131 eqtrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( P ^ -u ( P pCnt p ) ) = 1 )
133 115 118 132 3eqtrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( ( J ` P ) ` p ) = 1 )
134 133 oveq1d 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( ( ( J ` P ) ` p ) ^c R ) = ( 1 ^c R ) )
135 2re 
 |-  2 e. RR
136 135 a1i 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> 2 e. RR )
137 5 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> F e. A )
138 2 18 abvcl 
 |-  ( ( F e. A /\ p e. QQ ) -> ( F ` p ) e. RR )
139 137 105 138 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( F ` p ) e. RR )
140 2 18 22 abvgt0 
 |-  ( ( F e. A /\ p e. QQ /\ p =/= 0 ) -> 0 < ( F ` p ) )
141 137 105 116 140 syl3anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> 0 < ( F ` p ) )
142 139 141 elrpd 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( F ` p ) e. RR+ )
143 142 adantrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( F ` p ) e. RR+ )
144 25 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( F ` P ) e. RR+ )
145 143 144 ifcld 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) ) e. RR+ )
146 10 145 eqeltrid 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> S e. RR+ )
147 146 rprecred 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( 1 / S ) e. RR )
148 simprr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( F ` p ) < 1 )
149 8 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( F ` P ) < 1 )
150 breq1 
 |-  ( ( F ` p ) = if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) ) -> ( ( F ` p ) < 1 <-> if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) ) < 1 ) )
151 breq1 
 |-  ( ( 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 150 151 ifboth 
 |-  ( ( ( F ` p ) < 1 /\ ( F ` P ) < 1 ) -> if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) ) < 1 )
153 148 149 152 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) ) < 1 )
154 10 153 eqbrtrid 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> S < 1 )
155 146 reclt1d 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( S < 1 <-> 1 < ( 1 / S ) ) )
156 154 155 mpbid 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> 1 < ( 1 / S ) )
157 expnbnd 
 |-  ( ( 2 e. RR /\ ( 1 / S ) e. RR /\ 1 < ( 1 / S ) ) -> E. k e. NN 2 < ( ( 1 / S ) ^ k ) )
158 136 147 156 157 syl3anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> E. k e. NN 2 < ( ( 1 / S ) ^ k ) )
159 146 rpcnd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> S e. CC )
160 159 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> S e. CC )
161 146 rpne0d 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> S =/= 0 )
162 161 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> S =/= 0 )
163 nnz 
 |-  ( k e. NN -> k e. ZZ )
164 163 adantl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> k e. ZZ )
165 160 162 164 exprecd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( ( 1 / S ) ^ k ) = ( 1 / ( S ^ k ) ) )
166 5 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> F e. A )
167 ax-1ne0 
 |-  1 =/= 0
168 1 qrng1 
 |-  1 = ( 1r ` Q )
169 2 168 22 abv1z 
 |-  ( ( F e. A /\ 1 =/= 0 ) -> ( F ` 1 ) = 1 )
170 166 167 169 sylancl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( F ` 1 ) = 1 )
171 15 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> P e. NN )
172 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
173 nnexpcl 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( P ^ k ) e. NN )
174 171 172 173 syl2an 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( P ^ k ) e. NN )
175 174 nnzd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( P ^ k ) e. ZZ )
176 102 ad2antlr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> p e. NN )
177 nnexpcl 
 |-  ( ( p e. NN /\ k e. NN0 ) -> ( p ^ k ) e. NN )
178 176 172 177 syl2an 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( p ^ k ) e. NN )
179 178 nnzd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( p ^ k ) e. ZZ )
180 bezout 
 |-  ( ( ( 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 ) ) )
181 175 179 180 syl2anc 
 |-  ( ( ( ( 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 ) ) )
182 simprl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> P =/= p )
183 7 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> P e. Prime )
184 simplr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> p e. Prime )
185 prmrp 
 |-  ( ( P e. Prime /\ p e. Prime ) -> ( ( P gcd p ) = 1 <-> P =/= p ) )
186 183 184 185 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( ( P gcd p ) = 1 <-> P =/= p ) )
187 182 186 mpbird 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( P gcd p ) = 1 )
188 187 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( P gcd p ) = 1 )
189 171 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> P e. NN )
190 176 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> p e. NN )
191 simpr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> k e. NN )
192 rppwr 
 |-  ( ( P e. NN /\ p e. NN /\ k e. NN ) -> ( ( P gcd p ) = 1 -> ( ( P ^ k ) gcd ( p ^ k ) ) = 1 ) )
193 189 190 191 192 syl3anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( ( P gcd p ) = 1 -> ( ( P ^ k ) gcd ( p ^ k ) ) = 1 ) )
194 188 193 mpd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( ( P ^ k ) gcd ( p ^ k ) ) = 1 )
195 194 adantrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( P ^ k ) gcd ( p ^ k ) ) = 1 )
196 195 eqeq1d 
 |-  ( ( ( ( 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 ) ) ) )
197 5 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> F e. A )
198 174 adantrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( P ^ k ) e. NN )
199 nnq 
 |-  ( ( P ^ k ) e. NN -> ( P ^ k ) e. QQ )
200 198 199 syl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( P ^ k ) e. QQ )
201 simprrl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> a e. ZZ )
202 zq 
 |-  ( a e. ZZ -> a e. QQ )
203 201 202 syl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> a e. QQ )
204 qmulcl 
 |-  ( ( ( P ^ k ) e. QQ /\ a e. QQ ) -> ( ( P ^ k ) x. a ) e. QQ )
205 200 203 204 syl2anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( P ^ k ) x. a ) e. QQ )
206 178 adantrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( p ^ k ) e. NN )
207 nnq 
 |-  ( ( p ^ k ) e. NN -> ( p ^ k ) e. QQ )
208 206 207 syl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( p ^ k ) e. QQ )
209 simprrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> b e. ZZ )
210 zq 
 |-  ( b e. ZZ -> b e. QQ )
211 209 210 syl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> b e. QQ )
212 qmulcl 
 |-  ( ( ( p ^ k ) e. QQ /\ b e. QQ ) -> ( ( p ^ k ) x. b ) e. QQ )
213 208 211 212 syl2anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( p ^ k ) x. b ) e. QQ )
214 qaddcl 
 |-  ( ( ( ( P ^ k ) x. a ) e. QQ /\ ( ( p ^ k ) x. b ) e. QQ ) -> ( ( ( P ^ k ) x. a ) + ( ( p ^ k ) x. b ) ) e. QQ )
215 205 213 214 syl2anc 
 |-  ( ( ( ( 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 )
216 2 18 abvcl 
 |-  ( ( F e. A /\ ( ( ( P ^ k ) x. a ) + ( ( p ^ k ) x. b ) ) e. QQ ) -> ( F ` ( ( ( P ^ k ) x. a ) + ( ( p ^ k ) x. b ) ) ) e. RR )
217 197 215 216 syl2anc 
 |-  ( ( ( ( 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 )
218 2 18 abvcl 
 |-  ( ( F e. A /\ ( ( P ^ k ) x. a ) e. QQ ) -> ( F ` ( ( P ^ k ) x. a ) ) e. RR )
219 197 205 218 syl2anc 
 |-  ( ( ( ( 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 )
220 2 18 abvcl 
 |-  ( ( F e. A /\ ( ( p ^ k ) x. b ) e. QQ ) -> ( F ` ( ( p ^ k ) x. b ) ) e. RR )
221 197 213 220 syl2anc 
 |-  ( ( ( ( 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 )
222 219 221 readdcld 
 |-  ( ( ( ( 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 )
223 rpexpcl 
 |-  ( ( S e. RR+ /\ k e. ZZ ) -> ( S ^ k ) e. RR+ )
224 146 163 223 syl2an 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( S ^ k ) e. RR+ )
225 224 rpred 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( S ^ k ) e. RR )
226 225 adantrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( S ^ k ) e. RR )
227 remulcl 
 |-  ( ( 2 e. RR /\ ( S ^ k ) e. RR ) -> ( 2 x. ( S ^ k ) ) e. RR )
228 135 226 227 sylancr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( 2 x. ( S ^ k ) ) e. RR )
229 qex 
 |-  QQ e. _V
230 cnfldadd 
 |-  + = ( +g ` CCfld )
231 1 230 ressplusg 
 |-  ( QQ e. _V -> + = ( +g ` Q ) )
232 229 231 ax-mp 
 |-  + = ( +g ` Q )
233 2 18 232 abvtri 
 |-  ( ( 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 ) ) ) )
234 197 205 213 233 syl3anc 
 |-  ( ( ( ( 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 ) ) ) )
235 cnfldmul 
 |-  x. = ( .r ` CCfld )
236 1 235 ressmulr 
 |-  ( QQ e. _V -> x. = ( .r ` Q ) )
237 229 236 ax-mp 
 |-  x. = ( .r ` Q )
238 2 18 237 abvmul 
 |-  ( ( F e. A /\ ( P ^ k ) e. QQ /\ a e. QQ ) -> ( F ` ( ( P ^ k ) x. a ) ) = ( ( F ` ( P ^ k ) ) x. ( F ` a ) ) )
239 197 200 203 238 syl3anc 
 |-  ( ( ( ( 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 ) ) )
240 17 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> P e. QQ )
241 172 ad2antrl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> k e. NN0 )
242 1 2 qabvexp 
 |-  ( ( F e. A /\ P e. QQ /\ k e. NN0 ) -> ( F ` ( P ^ k ) ) = ( ( F ` P ) ^ k ) )
243 197 240 241 242 syl3anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` ( P ^ k ) ) = ( ( F ` P ) ^ k ) )
244 243 oveq1d 
 |-  ( ( ( ( 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 ) ) )
245 239 244 eqtrd 
 |-  ( ( ( ( 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 ) ) )
246 197 240 19 syl2anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` P ) e. RR )
247 246 241 reexpcld 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( F ` P ) ^ k ) e. RR )
248 2 18 abvcl 
 |-  ( ( F e. A /\ a e. QQ ) -> ( F ` a ) e. RR )
249 197 203 248 syl2anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` a ) e. RR )
250 247 249 remulcld 
 |-  ( ( ( ( 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 )
251 elz 
 |-  ( a e. ZZ <-> ( a e. RR /\ ( a = 0 \/ a e. NN \/ -u a e. NN ) ) )
252 251 simprbi 
 |-  ( a e. ZZ -> ( a = 0 \/ a e. NN \/ -u a e. NN ) )
253 252 adantl 
 |-  ( ( ph /\ a e. ZZ ) -> ( a = 0 \/ a e. NN \/ -u a e. NN ) )
254 2 22 abv0 
 |-  ( F e. A -> ( F ` 0 ) = 0 )
255 5 254 syl 
 |-  ( ph -> ( F ` 0 ) = 0 )
256 0le1 
 |-  0 <_ 1
257 255 256 eqbrtrdi 
 |-  ( ph -> ( F ` 0 ) <_ 1 )
258 257 adantr 
 |-  ( ( ph /\ a e. ZZ ) -> ( F ` 0 ) <_ 1 )
259 fveq2 
 |-  ( a = 0 -> ( F ` a ) = ( F ` 0 ) )
260 259 breq1d 
 |-  ( a = 0 -> ( ( F ` a ) <_ 1 <-> ( F ` 0 ) <_ 1 ) )
261 258 260 syl5ibrcom 
 |-  ( ( ph /\ a e. ZZ ) -> ( a = 0 -> ( F ` a ) <_ 1 ) )
262 nnq 
 |-  ( n e. NN -> n e. QQ )
263 2 18 abvcl 
 |-  ( ( F e. A /\ n e. QQ ) -> ( F ` n ) e. RR )
264 5 262 263 syl2an 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. RR )
265 1re 
 |-  1 e. RR
266 lenlt 
 |-  ( ( ( F ` n ) e. RR /\ 1 e. RR ) -> ( ( F ` n ) <_ 1 <-> -. 1 < ( F ` n ) ) )
267 264 265 266 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( ( F ` n ) <_ 1 <-> -. 1 < ( F ` n ) ) )
268 267 ralbidva 
 |-  ( ph -> ( A. n e. NN ( F ` n ) <_ 1 <-> A. n e. NN -. 1 < ( F ` n ) ) )
269 6 268 mpbird 
 |-  ( ph -> A. n e. NN ( F ` n ) <_ 1 )
270 fveq2 
 |-  ( n = a -> ( F ` n ) = ( F ` a ) )
271 270 breq1d 
 |-  ( n = a -> ( ( F ` n ) <_ 1 <-> ( F ` a ) <_ 1 ) )
272 271 rspccv 
 |-  ( A. n e. NN ( F ` n ) <_ 1 -> ( a e. NN -> ( F ` a ) <_ 1 ) )
273 269 272 syl 
 |-  ( ph -> ( a e. NN -> ( F ` a ) <_ 1 ) )
274 273 adantr 
 |-  ( ( ph /\ a e. ZZ ) -> ( a e. NN -> ( F ` a ) <_ 1 ) )
275 5 adantr 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> F e. A )
276 202 ad2antrl 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> a e. QQ )
277 eqid 
 |-  ( invg ` Q ) = ( invg ` Q )
278 2 18 277 abvneg 
 |-  ( ( F e. A /\ a e. QQ ) -> ( F ` ( ( invg ` Q ) ` a ) ) = ( F ` a ) )
279 275 276 278 syl2anc 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> ( F ` ( ( invg ` Q ) ` a ) ) = ( F ` a ) )
280 fveq2 
 |-  ( n = ( ( invg ` Q ) ` a ) -> ( F ` n ) = ( F ` ( ( invg ` Q ) ` a ) ) )
281 280 breq1d 
 |-  ( n = ( ( invg ` Q ) ` a ) -> ( ( F ` n ) <_ 1 <-> ( F ` ( ( invg ` Q ) ` a ) ) <_ 1 ) )
282 269 adantr 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> A. n e. NN ( F ` n ) <_ 1 )
283 1 qrngneg 
 |-  ( a e. QQ -> ( ( invg ` Q ) ` a ) = -u a )
284 276 283 syl 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> ( ( invg ` Q ) ` a ) = -u a )
285 simprr 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> -u a e. NN )
286 284 285 eqeltrd 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> ( ( invg ` Q ) ` a ) e. NN )
287 281 282 286 rspcdva 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> ( F ` ( ( invg ` Q ) ` a ) ) <_ 1 )
288 279 287 eqbrtrrd 
 |-  ( ( ph /\ ( a e. ZZ /\ -u a e. NN ) ) -> ( F ` a ) <_ 1 )
289 288 expr 
 |-  ( ( ph /\ a e. ZZ ) -> ( -u a e. NN -> ( F ` a ) <_ 1 ) )
290 261 274 289 3jaod 
 |-  ( ( ph /\ a e. ZZ ) -> ( ( a = 0 \/ a e. NN \/ -u a e. NN ) -> ( F ` a ) <_ 1 ) )
291 253 290 mpd 
 |-  ( ( ph /\ a e. ZZ ) -> ( F ` a ) <_ 1 )
292 291 ralrimiva 
 |-  ( ph -> A. a e. ZZ ( F ` a ) <_ 1 )
293 292 ad3antrrr 
 |-  ( ( ( ( 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 )
294 rsp 
 |-  ( A. a e. ZZ ( F ` a ) <_ 1 -> ( a e. ZZ -> ( F ` a ) <_ 1 ) )
295 293 201 294 sylc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` a ) <_ 1 )
296 265 a1i 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> 1 e. RR )
297 163 ad2antrl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> k e. ZZ )
298 24 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> 0 < ( F ` P ) )
299 expgt0 
 |-  ( ( ( F ` P ) e. RR /\ k e. ZZ /\ 0 < ( F ` P ) ) -> 0 < ( ( F ` P ) ^ k ) )
300 246 297 298 299 syl3anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> 0 < ( ( F ` P ) ^ k ) )
301 lemul2 
 |-  ( ( ( 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 ) ) )
302 249 296 247 300 301 syl112anc 
 |-  ( ( ( ( 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 ) ) )
303 295 302 mpbid 
 |-  ( ( ( ( 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 ) )
304 247 recnd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( F ` P ) ^ k ) e. CC )
305 304 mulridd 
 |-  ( ( ( ( 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 ) )
306 303 305 breqtrd 
 |-  ( ( ( ( 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 ) )
307 146 rpred 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> S e. RR )
308 307 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> S e. RR )
309 144 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` P ) e. RR+ )
310 309 rpge0d 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> 0 <_ ( F ` P ) )
311 176 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> p e. NN )
312 311 104 syl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> p e. QQ )
313 197 312 138 syl2anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` p ) e. RR )
314 max1 
 |-  ( ( ( F ` P ) e. RR /\ ( F ` p ) e. RR ) -> ( F ` P ) <_ if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) ) )
315 246 313 314 syl2anc 
 |-  ( ( ( ( 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 ) ) )
316 315 10 breqtrrdi 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` P ) <_ S )
317 leexp1a 
 |-  ( ( ( ( F ` P ) e. RR /\ S e. RR /\ k e. NN0 ) /\ ( 0 <_ ( F ` P ) /\ ( F ` P ) <_ S ) ) -> ( ( F ` P ) ^ k ) <_ ( S ^ k ) )
318 246 308 241 310 316 317 syl32anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( F ` P ) ^ k ) <_ ( S ^ k ) )
319 250 247 226 306 318 letrd 
 |-  ( ( ( ( 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 ) )
320 245 319 eqbrtrd 
 |-  ( ( ( ( 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 ) )
321 2 18 237 abvmul 
 |-  ( ( F e. A /\ ( p ^ k ) e. QQ /\ b e. QQ ) -> ( F ` ( ( p ^ k ) x. b ) ) = ( ( F ` ( p ^ k ) ) x. ( F ` b ) ) )
322 197 208 211 321 syl3anc 
 |-  ( ( ( ( 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 ) ) )
323 1 2 qabvexp 
 |-  ( ( F e. A /\ p e. QQ /\ k e. NN0 ) -> ( F ` ( p ^ k ) ) = ( ( F ` p ) ^ k ) )
324 197 312 241 323 syl3anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` ( p ^ k ) ) = ( ( F ` p ) ^ k ) )
325 324 oveq1d 
 |-  ( ( ( ( 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 ) ) )
326 322 325 eqtrd 
 |-  ( ( ( ( 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 ) ) )
327 313 241 reexpcld 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( F ` p ) ^ k ) e. RR )
328 2 18 abvcl 
 |-  ( ( F e. A /\ b e. QQ ) -> ( F ` b ) e. RR )
329 197 211 328 syl2anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` b ) e. RR )
330 327 329 remulcld 
 |-  ( ( ( ( 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 )
331 fveq2 
 |-  ( a = b -> ( F ` a ) = ( F ` b ) )
332 331 breq1d 
 |-  ( a = b -> ( ( F ` a ) <_ 1 <-> ( F ` b ) <_ 1 ) )
333 332 293 209 rspcdva 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` b ) <_ 1 )
334 311 nnne0d 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> p =/= 0 )
335 197 312 334 140 syl3anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> 0 < ( F ` p ) )
336 expgt0 
 |-  ( ( ( F ` p ) e. RR /\ k e. ZZ /\ 0 < ( F ` p ) ) -> 0 < ( ( F ` p ) ^ k ) )
337 313 297 335 336 syl3anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> 0 < ( ( F ` p ) ^ k ) )
338 lemul2 
 |-  ( ( ( 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 ) ) )
339 329 296 327 337 338 syl112anc 
 |-  ( ( ( ( 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 ) ) )
340 333 339 mpbid 
 |-  ( ( ( ( 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 ) )
341 327 recnd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( F ` p ) ^ k ) e. CC )
342 341 mulridd 
 |-  ( ( ( ( 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 ) )
343 340 342 breqtrd 
 |-  ( ( ( ( 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 ) )
344 143 adantr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` p ) e. RR+ )
345 344 rpge0d 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> 0 <_ ( F ` p ) )
346 max2 
 |-  ( ( ( F ` P ) e. RR /\ ( F ` p ) e. RR ) -> ( F ` p ) <_ if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) ) )
347 246 313 346 syl2anc 
 |-  ( ( ( ( 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 ) ) )
348 347 10 breqtrrdi 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( F ` p ) <_ S )
349 leexp1a 
 |-  ( ( ( ( F ` p ) e. RR /\ S e. RR /\ k e. NN0 ) /\ ( 0 <_ ( F ` p ) /\ ( F ` p ) <_ S ) ) -> ( ( F ` p ) ^ k ) <_ ( S ^ k ) )
350 313 308 241 345 348 349 syl32anc 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ ( k e. NN /\ ( a e. ZZ /\ b e. ZZ ) ) ) -> ( ( F ` p ) ^ k ) <_ ( S ^ k ) )
351 330 327 226 343 350 letrd 
 |-  ( ( ( ( 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 ) )
352 326 351 eqbrtrd 
 |-  ( ( ( ( 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 ) )
353 219 221 226 226 320 352 le2addd 
 |-  ( ( ( ( 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 ) ) )
354 224 rpcnd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( S ^ k ) e. CC )
355 354 2timesd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( 2 x. ( S ^ k ) ) = ( ( S ^ k ) + ( S ^ k ) ) )
356 355 adantrr 
 |-  ( ( ( ( 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 ) ) )
357 353 356 breqtrrd 
 |-  ( ( ( ( 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 ) ) )
358 217 222 228 234 357 letrd 
 |-  ( ( ( ( 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 ) ) )
359 fveq2 
 |-  ( 1 = ( ( ( P ^ k ) x. a ) + ( ( p ^ k ) x. b ) ) -> ( F ` 1 ) = ( F ` ( ( ( P ^ k ) x. a ) + ( ( p ^ k ) x. b ) ) ) )
360 359 breq1d 
 |-  ( 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 ) ) ) )
361 358 360 syl5ibrcom 
 |-  ( ( ( ( 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 ) ) ) )
362 196 361 sylbid 
 |-  ( ( ( ( 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 ) ) ) )
363 362 anassrs 
 |-  ( ( ( ( ( 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 ) ) ) )
364 363 rexlimdvva 
 |-  ( ( ( ( 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 ) ) ) )
365 181 364 mpd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( F ` 1 ) <_ ( 2 x. ( S ^ k ) ) )
366 170 365 eqbrtrrd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> 1 <_ ( 2 x. ( S ^ k ) ) )
367 224 rpregt0d 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( ( S ^ k ) e. RR /\ 0 < ( S ^ k ) ) )
368 ledivmul2 
 |-  ( ( 1 e. RR /\ 2 e. RR /\ ( ( S ^ k ) e. RR /\ 0 < ( S ^ k ) ) ) -> ( ( 1 / ( S ^ k ) ) <_ 2 <-> 1 <_ ( 2 x. ( S ^ k ) ) ) )
369 265 135 367 368 mp3an12i 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( ( 1 / ( S ^ k ) ) <_ 2 <-> 1 <_ ( 2 x. ( S ^ k ) ) ) )
370 366 369 mpbird 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( 1 / ( S ^ k ) ) <_ 2 )
371 165 370 eqbrtrd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( ( 1 / S ) ^ k ) <_ 2 )
372 reexpcl 
 |-  ( ( ( 1 / S ) e. RR /\ k e. NN0 ) -> ( ( 1 / S ) ^ k ) e. RR )
373 147 172 372 syl2an 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( ( 1 / S ) ^ k ) e. RR )
374 lenlt 
 |-  ( ( ( ( 1 / S ) ^ k ) e. RR /\ 2 e. RR ) -> ( ( ( 1 / S ) ^ k ) <_ 2 <-> -. 2 < ( ( 1 / S ) ^ k ) ) )
375 373 135 374 sylancl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( ( ( 1 / S ) ^ k ) <_ 2 <-> -. 2 < ( ( 1 / S ) ^ k ) ) )
376 371 375 mpbid 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> -. 2 < ( ( 1 / S ) ^ k ) )
377 376 pm2.21d 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) /\ k e. NN ) -> ( 2 < ( ( 1 / S ) ^ k ) -> -. ( F ` p ) < 1 ) )
378 377 rexlimdva 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> ( E. k e. NN 2 < ( ( 1 / S ) ^ k ) -> -. ( F ` p ) < 1 ) )
379 158 378 mpd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( P =/= p /\ ( F ` p ) < 1 ) ) -> -. ( F ` p ) < 1 )
380 379 expr 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( ( F ` p ) < 1 -> -. ( F ` p ) < 1 ) )
381 380 pm2.01d 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> -. ( F ` p ) < 1 )
382 fveq2 
 |-  ( n = p -> ( F ` n ) = ( F ` p ) )
383 382 breq2d 
 |-  ( n = p -> ( 1 < ( F ` n ) <-> 1 < ( F ` p ) ) )
384 383 notbid 
 |-  ( n = p -> ( -. 1 < ( F ` n ) <-> -. 1 < ( F ` p ) ) )
385 6 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> A. n e. NN -. 1 < ( F ` n ) )
386 384 385 103 rspcdva 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> -. 1 < ( F ` p ) )
387 lttri3 
 |-  ( ( ( F ` p ) e. RR /\ 1 e. RR ) -> ( ( F ` p ) = 1 <-> ( -. ( F ` p ) < 1 /\ -. 1 < ( F ` p ) ) ) )
388 139 265 387 sylancl 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( ( F ` p ) = 1 <-> ( -. ( F ` p ) < 1 /\ -. 1 < ( F ` p ) ) ) )
389 381 386 388 mpbir2and 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( F ` p ) = 1 )
390 112 134 389 3eqtr4d 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( ( ( J ` P ) ` p ) ^c R ) = ( F ` p ) )
391 110 390 eqtr2d 
 |-  ( ( ( ph /\ p e. Prime ) /\ P =/= p ) -> ( F ` p ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) )
392 391 ex 
 |-  ( ( ph /\ p e. Prime ) -> ( P =/= p -> ( F ` p ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) ) )
393 101 392 pm2.61dne 
 |-  ( ( ph /\ p e. Prime ) -> ( F ` p ) = ( ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) ` p ) )
394 1 2 5 50 393 ostthlem2 
 |-  ( ph -> F = ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) )
395 oveq2 
 |-  ( a = R -> ( ( ( J ` P ) ` y ) ^c a ) = ( ( ( J ` P ) ` y ) ^c R ) )
396 395 mpteq2dv 
 |-  ( a = R -> ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c a ) ) = ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) )
397 396 rspceeqv 
 |-  ( ( 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 ) ) )
398 48 394 397 syl2anc 
 |-  ( ph -> E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c a ) ) )