ostth2

Description: - Lemma for ostth : regular 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$
	ostth2.2	$⊢ φ \to N \in ℤ_{\geq 2}$
	ostth2.3	$⊢ φ \to 1 < F (N)$
	ostth2.4	$⊢ R = \frac{\log F (N)}{\log N}$
Assertion	ostth2	$⊢ φ \to \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|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		ostth2.2	$⊢ φ \to N \in ℤ_{\geq 2}$
7		ostth2.3	$⊢ φ \to 1 < F (N)$
8		ostth2.4	$⊢ R = \frac{\log F (N)}{\log N}$
9		eluz2b2	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land 1 < N)$
10	6 9	sylib	$⊢ φ \to (N \in ℕ \land 1 < N)$
11	10	simpld	$⊢ φ \to N \in ℕ$
12		nnq	$⊢ N \in ℕ \to N \in ℚ$
13	11 12	syl	$⊢ φ \to N \in ℚ$
14	1	qrngbas	$⊢ ℚ = {Base}_{Q}$
15	2 14	abvcl	$⊢ (F \in A \land N \in ℚ) \to F (N) \in ℝ$
16	5 13 15	syl2anc	$⊢ φ \to F (N) \in ℝ$
17	16 7	rplogcld	$⊢ φ \to \log F (N) \in ℝ^{+}$
18	11	nnred	$⊢ φ \to N \in ℝ$
19	10	simprd	$⊢ φ \to 1 < N$
20	18 19	rplogcld	$⊢ φ \to \log N \in ℝ^{+}$
21	17 20	rpdivcld	$⊢ φ \to \frac{\log F (N)}{\log N} \in ℝ^{+}$
22	8 21	eqeltrid	$⊢ φ \to R \in ℝ^{+}$
23	22	rpred	$⊢ φ \to R \in ℝ$
24	22	rpgt0d	$⊢ φ \to 0 < R$
25	11	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
26	1 2	qabvle	$⊢ (F \in A \land N \in ℕ_{0}) \to F (N) \leq N$
27	5 25 26	syl2anc	$⊢ φ \to F (N) \leq N$
28	11	nnne0d	$⊢ φ \to N \neq 0$
29	1	qrng0	$⊢ 0 = 0_{Q}$
30	2 14 29	abvgt0	$⊢ (F \in A \land N \in ℚ \land N \neq 0) \to 0 < F (N)$
31	5 13 28 30	syl3anc	$⊢ φ \to 0 < F (N)$
32	16 31	elrpd	$⊢ φ \to F (N) \in ℝ^{+}$
33	32	reeflogd	$⊢ φ \to e^{\log F (N)} = F (N)$
34	11	nnrpd	$⊢ φ \to N \in ℝ^{+}$
35	34	reeflogd	$⊢ φ \to e^{\log N} = N$
36	27 33 35	3brtr4d	$⊢ φ \to e^{\log F (N)} \leq e^{\log N}$
37	17	rpred	$⊢ φ \to \log F (N) \in ℝ$
38	34	relogcld	$⊢ φ \to \log N \in ℝ$
39		efle	$⊢ (\log F (N) \in ℝ \land \log N \in ℝ) \to (\log F (N) \leq \log N \leftrightarrow e^{\log F (N)} \leq e^{\log N})$
40	37 38 39	syl2anc	$⊢ φ \to (\log F (N) \leq \log N \leftrightarrow e^{\log F (N)} \leq e^{\log N})$
41	36 40	mpbird	$⊢ φ \to \log F (N) \leq \log N$
42	20	rpcnd	$⊢ φ \to \log N \in ℂ$
43	42	mulid1d	$⊢ φ \to \log N \cdot 1 = \log N$
44	41 43	breqtrrd	$⊢ φ \to \log F (N) \leq \log N \cdot 1$
45		1red	$⊢ φ \to 1 \in ℝ$
46	37 45 20	ledivmuld	$⊢ φ \to (\frac{\log F (N)}{\log N} \leq 1 \leftrightarrow \log F (N) \leq \log N \cdot 1)$
47	44 46	mpbird	$⊢ φ \to \frac{\log F (N)}{\log N} \leq 1$
48	8 47	eqbrtrid	$⊢ φ \to R \leq 1$
49		0xr	$⊢ 0 \in ℝ^{*}$
50		1re	$⊢ 1 \in ℝ$
51		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (R \in (0, 1] \leftrightarrow (R \in ℝ \land 0 < R \land R \leq 1))$
52	49 50 51	mp2an	$⊢ R \in (0, 1] \leftrightarrow (R \in ℝ \land 0 < R \land R \leq 1)$
53	23 24 48 52	syl3anbrc	$⊢ φ \to R \in (0, 1]$
54	1 2	qabsabv	$⊢ {abs ↾}_{ℚ} \in A$
55		fvres	$⊢ y \in ℚ \to ({abs ↾}_{ℚ}) (y) = \|y\|$
56	55	oveq1d	$⊢ y \in ℚ \to {({abs ↾}_{ℚ}) (y)}^{R} = {\|y\|}^{R}$
57	56	mpteq2ia	$⊢ (y \in ℚ ⟼ {({abs ↾}_{ℚ}) (y)}^{R}) = (y \in ℚ ⟼ {\|y\|}^{R})$
58	57	eqcomi	$⊢ (y \in ℚ ⟼ {\|y\|}^{R}) = (y \in ℚ ⟼ {({abs ↾}_{ℚ}) (y)}^{R})$
59	2 14 58	abvcxp	$⊢ ({abs ↾}_{ℚ} \in A \land R \in (0, 1]) \to (y \in ℚ ⟼ {\|y\|}^{R}) \in A$
60	54 53 59	sylancr	$⊢ φ \to (y \in ℚ ⟼ {\|y\|}^{R}) \in A$
61		eluzelz	$⊢ z \in ℤ_{\geq 2} \to z \in ℤ$
62		zq	$⊢ z \in ℤ \to z \in ℚ$
63		fveq2	$⊢ y = z \to \|y\| = \|z\|$
64	63	oveq1d	$⊢ y = z \to {\|y\|}^{R} = {\|z\|}^{R}$
65		eqid	$⊢ (y \in ℚ ⟼ {\|y\|}^{R}) = (y \in ℚ ⟼ {\|y\|}^{R})$
66		ovex	$⊢ {\|z\|}^{R} \in V$
67	64 65 66	fvmpt	$⊢ z \in ℚ \to (y \in ℚ ⟼ {\|y\|}^{R}) (z) = {\|z\|}^{R}$
68	61 62 67	3syl	$⊢ z \in ℤ_{\geq 2} \to (y \in ℚ ⟼ {\|y\|}^{R}) (z) = {\|z\|}^{R}$
69	68	adantl	$⊢ (φ \land z \in ℤ_{\geq 2}) \to (y \in ℚ ⟼ {\|y\|}^{R}) (z) = {\|z\|}^{R}$
70		simpr	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \in ℤ_{\geq 2}$
71		eluz2b2	$⊢ z \in ℤ_{\geq 2} \leftrightarrow (z \in ℕ \land 1 < z)$
72	70 71	sylib	$⊢ (φ \land z \in ℤ_{\geq 2}) \to (z \in ℕ \land 1 < z)$
73	72	simpld	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \in ℕ$
74	73	nnred	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \in ℝ$
75	73	nnnn0d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \in ℕ_{0}$
76	75	nn0ge0d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to 0 \leq z$
77	74 76	absidd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to \|z\| = z$
78	77	oveq1d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to {\|z\|}^{R} = z^{R}$
79	74	recnd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \in ℂ$
80	73	nnne0d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \neq 0$
81	22	rpcnd	$⊢ φ \to R \in ℂ$
82	81	adantr	$⊢ (φ \land z \in ℤ_{\geq 2}) \to R \in ℂ$
83	79 80 82	cxpefd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z^{R} = e^{R \log z}$
84	5	adantr	$⊢ (φ \land z \in ℤ_{\geq 2}) \to F \in A$
85	6	adantr	$⊢ (φ \land z \in ℤ_{\geq 2}) \to N \in ℤ_{\geq 2}$
86	7	adantr	$⊢ (φ \land z \in ℤ_{\geq 2}) \to 1 < F (N)$
87		eqid	$⊢ \frac{\log F (z)}{\log z} = \frac{\log F (z)}{\log z}$
88		eqid	$⊢ if (F (z) \leq 1, 1, F (z)) = if (F (z) \leq 1, 1, F (z))$
89		eqid	$⊢ \frac{\log N}{\log z} = \frac{\log N}{\log z}$
90	1 2 3 4 84 85 86 8 70 87 88 89	ostth2lem4	$⊢ (φ \land z \in ℤ_{\geq 2}) \to (1 < F (z) \land R \leq \frac{\log F (z)}{\log z})$
91	90	simprd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to R \leq \frac{\log F (z)}{\log z}$
92	90	simpld	$⊢ (φ \land z \in ℤ_{\geq 2}) \to 1 < F (z)$
93		eqid	$⊢ if (F (N) \leq 1, 1, F (N)) = if (F (N) \leq 1, 1, F (N))$
94		eqid	$⊢ \frac{\log z}{\log N} = \frac{\log z}{\log N}$
95	1 2 3 4 84 70 92 87 85 8 93 94	ostth2lem4	$⊢ (φ \land z \in ℤ_{\geq 2}) \to (1 < F (N) \land \frac{\log F (z)}{\log z} \leq R)$
96	95	simprd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to \frac{\log F (z)}{\log z} \leq R$
97	23	adantr	$⊢ (φ \land z \in ℤ_{\geq 2}) \to R \in ℝ$
98	61	adantl	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \in ℤ$
99	98 62	syl	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \in ℚ$
100	2 14	abvcl	$⊢ (F \in A \land z \in ℚ) \to F (z) \in ℝ$
101	84 99 100	syl2anc	$⊢ (φ \land z \in ℤ_{\geq 2}) \to F (z) \in ℝ$
102	2 14 29	abvgt0	$⊢ (F \in A \land z \in ℚ \land z \neq 0) \to 0 < F (z)$
103	84 99 80 102	syl3anc	$⊢ (φ \land z \in ℤ_{\geq 2}) \to 0 < F (z)$
104	101 103	elrpd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to F (z) \in ℝ^{+}$
105	104	relogcld	$⊢ (φ \land z \in ℤ_{\geq 2}) \to \log F (z) \in ℝ$
106	73	nnrpd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z \in ℝ^{+}$
107	106	relogcld	$⊢ (φ \land z \in ℤ_{\geq 2}) \to \log z \in ℝ$
108		ef0	$⊢ e^{0} = 1$
109	72	simprd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to 1 < z$
110	106	reeflogd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to e^{\log z} = z$
111	109 110	breqtrrd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to 1 < e^{\log z}$
112	108 111	eqbrtrid	$⊢ (φ \land z \in ℤ_{\geq 2}) \to e^{0} < e^{\log z}$
113		0re	$⊢ 0 \in ℝ$
114		eflt	$⊢ (0 \in ℝ \land \log z \in ℝ) \to (0 < \log z \leftrightarrow e^{0} < e^{\log z})$
115	113 107 114	sylancr	$⊢ (φ \land z \in ℤ_{\geq 2}) \to (0 < \log z \leftrightarrow e^{0} < e^{\log z})$
116	112 115	mpbird	$⊢ (φ \land z \in ℤ_{\geq 2}) \to 0 < \log z$
117	116	gt0ne0d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to \log z \neq 0$
118	105 107 117	redivcld	$⊢ (φ \land z \in ℤ_{\geq 2}) \to \frac{\log F (z)}{\log z} \in ℝ$
119	97 118	letri3d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to (R = \frac{\log F (z)}{\log z} \leftrightarrow (R \leq \frac{\log F (z)}{\log z} \land \frac{\log F (z)}{\log z} \leq R))$
120	91 96 119	mpbir2and	$⊢ (φ \land z \in ℤ_{\geq 2}) \to R = \frac{\log F (z)}{\log z}$
121	120	oveq1d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to R \log z = (\frac{\log F (z)}{\log z}) \log z$
122	105	recnd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to \log F (z) \in ℂ$
123	107	recnd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to \log z \in ℂ$
124	122 123 117	divcan1d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to (\frac{\log F (z)}{\log z}) \log z = \log F (z)$
125	121 124	eqtrd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to R \log z = \log F (z)$
126	125	fveq2d	$⊢ (φ \land z \in ℤ_{\geq 2}) \to e^{R \log z} = e^{\log F (z)}$
127	104	reeflogd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to e^{\log F (z)} = F (z)$
128	83 126 127	3eqtrd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to z^{R} = F (z)$
129	69 78 128	3eqtrrd	$⊢ (φ \land z \in ℤ_{\geq 2}) \to F (z) = (y \in ℚ ⟼ {\|y\|}^{R}) (z)$
130	1 2 5 60 129	ostthlem1	$⊢ φ \to F = (y \in ℚ ⟼ {\|y\|}^{R})$
131		oveq2	$⊢ a = R \to {\|y\|}^{a} = {\|y\|}^{R}$
132	131	mpteq2dv	$⊢ a = R \to (y \in ℚ ⟼ {\|y\|}^{a}) = (y \in ℚ ⟼ {\|y\|}^{R})$
133	132	rspceeqv	$⊢ (R \in (0, 1] \land F = (y \in ℚ ⟼ {\|y\|}^{R})) \to \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a})$
134	53 130 133	syl2anc	$⊢ φ \to \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a})$

Metamath Proof Explorer

Theorem ostth2

Proof