ostth3

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

	Ref	Expression
Hypotheses	qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	qabsabv.a	$⊢ A = AbsVal (Q)$
	padic.j	$⊢ J = (q \in ℙ ⟼ (x \in ℚ ⟼ if (x = 0, 0, q^{- (q pCnt x)})))$
	ostth.k	$⊢ K = (x \in ℚ ⟼ if (x = 0, 0, 1))$
	ostth.1	$⊢ φ \to F \in A$
	ostth3.2	$⊢ φ \to \forall n \in ℕ \neg 1 < F (n)$
	ostth3.3	$⊢ φ \to P \in ℙ$
	ostth3.4	$⊢ φ \to F (P) < 1$
	ostth3.5	$⊢ R = - \frac{\log F (P)}{\log P}$
	ostth3.6	$⊢ S = if (F (P) \leq F (p), F (p), F (P))$
Assertion	ostth3	$⊢ φ \to \exists a \in ℝ^{+} F = (y \in ℚ ⟼ {J (P) (y)}^{a})$

Proof

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

Metamath Proof Explorer

Theorem ostth3

Proof