# 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}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}ℚ$
qabsabv.a ${⊢}{A}=\mathrm{AbsVal}\left({Q}\right)$
padic.j ${⊢}{J}=\left({q}\in ℙ⟼\left({x}\in ℚ⟼if\left({x}=0,0,{{q}}^{-\left({q}\mathrm{pCnt}{x}\right)}\right)\right)\right)$
ostth.k ${⊢}{K}=\left({x}\in ℚ⟼if\left({x}=0,0,1\right)\right)$
ostth.1 ${⊢}{\phi }\to {F}\in {A}$
ostth3.2 ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}¬1<{F}\left({n}\right)$
ostth3.3 ${⊢}{\phi }\to {P}\in ℙ$
ostth3.4 ${⊢}{\phi }\to {F}\left({P}\right)<1$
ostth3.5 ${⊢}{R}=-\frac{\mathrm{log}{F}\left({P}\right)}{\mathrm{log}{P}}$
ostth3.6 ${⊢}{S}=if\left({F}\left({P}\right)\le {F}\left({p}\right),{F}\left({p}\right),{F}\left({P}\right)\right)$
Assertion ostth3 ${⊢}{\phi }\to \exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{F}=\left({y}\in ℚ⟼{{J}\left({P}\right)\left({y}\right)}^{{a}}\right)$

### Proof

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