ostth

Description: Ostrowski's theorem, which classifies all absolute values on QQ . Any such absolute value must either be the trivial absolute value K , a constant exponent 0 < a <_ 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (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))$
Assertion	ostth	$⊢ F \in A \leftrightarrow (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (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		simpl	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to F \in A$
6		1re	$⊢ 1 \in ℝ$
7	6	ltnri	$⊢ \neg 1 < 1$
8		ax-1ne0	$⊢ 1 \neq 0$
9	1	qrng1	$⊢ 1 = 1_{Q}$
10	1	qrng0	$⊢ 0 = 0_{Q}$
11	2 9 10	abv1z	$⊢ (F \in A \land 1 \neq 0) \to F (1) = 1$
12	8 11	mpan2	$⊢ F \in A \to F (1) = 1$
13	12	breq2d	$⊢ F \in A \to (1 < F (1) \leftrightarrow 1 < 1)$
14	7 13	mtbiri	$⊢ F \in A \to \neg 1 < F (1)$
15	14	adantr	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to \neg 1 < F (1)$
16		simprr	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to 1 < F (n)$
17		fveq2	$⊢ n = 1 \to F (n) = F (1)$
18	17	breq2d	$⊢ n = 1 \to (1 < F (n) \leftrightarrow 1 < F (1))$
19	16 18	syl5ibcom	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to (n = 1 \to 1 < F (1))$
20	15 19	mtod	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to \neg n = 1$
21		simprl	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to n \in ℕ$
22		elnn1uz2	$⊢ n \in ℕ \leftrightarrow (n = 1 \lor n \in ℤ_{\geq 2})$
23	21 22	sylib	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to (n = 1 \lor n \in ℤ_{\geq 2})$
24	23	ord	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to (\neg n = 1 \to n \in ℤ_{\geq 2})$
25	20 24	mpd	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to n \in ℤ_{\geq 2}$
26		eqid	$⊢ \frac{\log F (n)}{\log n} = \frac{\log F (n)}{\log n}$
27	1 2 3 4 5 25 16 26	ostth2	$⊢ (F \in A \land (n \in ℕ \land 1 < F (n))) \to \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a})$
28	27	rexlimdvaa	$⊢ F \in A \to (\exists n \in ℕ 1 < F (n) \to \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}))$
29		3mix2	$⊢ \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}))$
30	28 29	syl6	$⊢ F \in A \to (\exists n \in ℕ 1 < F (n) \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a})))$
31		ralnex	$⊢ \forall n \in ℕ \neg 1 < F (n) \leftrightarrow \neg \exists n \in ℕ 1 < F (n)$
32		simpll	$⊢ ((F \in A \land \forall n \in ℕ \neg 1 < F (n)) \land (p \in ℙ \land F (p) < 1)) \to F \in A$
33		simplr	$⊢ ((F \in A \land \forall n \in ℕ \neg 1 < F (n)) \land (p \in ℙ \land F (p) < 1)) \to \forall n \in ℕ \neg 1 < F (n)$
34		fveq2	$⊢ n = k \to F (n) = F (k)$
35	34	breq2d	$⊢ n = k \to (1 < F (n) \leftrightarrow 1 < F (k))$
36	35	notbid	$⊢ n = k \to (\neg 1 < F (n) \leftrightarrow \neg 1 < F (k))$
37	36	cbvralvw	$⊢ \forall n \in ℕ \neg 1 < F (n) \leftrightarrow \forall k \in ℕ \neg 1 < F (k)$
38	33 37	sylib	$⊢ ((F \in A \land \forall n \in ℕ \neg 1 < F (n)) \land (p \in ℙ \land F (p) < 1)) \to \forall k \in ℕ \neg 1 < F (k)$
39		simprl	$⊢ ((F \in A \land \forall n \in ℕ \neg 1 < F (n)) \land (p \in ℙ \land F (p) < 1)) \to p \in ℙ$
40		simprr	$⊢ ((F \in A \land \forall n \in ℕ \neg 1 < F (n)) \land (p \in ℙ \land F (p) < 1)) \to F (p) < 1$
41		eqid	$⊢ - \frac{\log F (p)}{\log p} = - \frac{\log F (p)}{\log p}$
42		eqid	$⊢ if (F (p) \leq F (z), F (z), F (p)) = if (F (p) \leq F (z), F (z), F (p))$
43	1 2 3 4 32 38 39 40 41 42	ostth3	$⊢ ((F \in A \land \forall n \in ℕ \neg 1 < F (n)) \land (p \in ℙ \land F (p) < 1)) \to \exists a \in ℝ^{+} F = (y \in ℚ ⟼ {J (p) (y)}^{a})$
44	43	expr	$⊢ ((F \in A \land \forall n \in ℕ \neg 1 < F (n)) \land p \in ℙ) \to (F (p) < 1 \to \exists a \in ℝ^{+} F = (y \in ℚ ⟼ {J (p) (y)}^{a}))$
45	44	reximdva	$⊢ (F \in A \land \forall n \in ℕ \neg 1 < F (n)) \to (\exists p \in ℙ F (p) < 1 \to \exists p \in ℙ \exists a \in ℝ^{+} F = (y \in ℚ ⟼ {J (p) (y)}^{a}))$
46	1 2 3	padicabvf	$⊢ J : ℙ ⟶ A$
47		ffn	$⊢ J : ℙ ⟶ A \to J Fn ℙ$
48		fveq1	$⊢ g = J (p) \to g (y) = J (p) (y)$
49	48	oveq1d	$⊢ g = J (p) \to {g (y)}^{a} = {J (p) (y)}^{a}$
50	49	mpteq2dv	$⊢ g = J (p) \to (y \in ℚ ⟼ {g (y)}^{a}) = (y \in ℚ ⟼ {J (p) (y)}^{a})$
51	50	eqeq2d	$⊢ g = J (p) \to (F = (y \in ℚ ⟼ {g (y)}^{a}) \leftrightarrow F = (y \in ℚ ⟼ {J (p) (y)}^{a}))$
52	51	rexrn	$⊢ J Fn ℙ \to (\exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}) \leftrightarrow \exists p \in ℙ F = (y \in ℚ ⟼ {J (p) (y)}^{a}))$
53	46 47 52	mp2b	$⊢ \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}) \leftrightarrow \exists p \in ℙ F = (y \in ℚ ⟼ {J (p) (y)}^{a})$
54	53	rexbii	$⊢ \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}) \leftrightarrow \exists a \in ℝ^{+} \exists p \in ℙ F = (y \in ℚ ⟼ {J (p) (y)}^{a})$
55		rexcom	$⊢ \exists a \in ℝ^{+} \exists p \in ℙ F = (y \in ℚ ⟼ {J (p) (y)}^{a}) \leftrightarrow \exists p \in ℙ \exists a \in ℝ^{+} F = (y \in ℚ ⟼ {J (p) (y)}^{a})$
56	54 55	bitri	$⊢ \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}) \leftrightarrow \exists p \in ℙ \exists a \in ℝ^{+} F = (y \in ℚ ⟼ {J (p) (y)}^{a})$
57		3mix3	$⊢ \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}) \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}))$
58	56 57	sylbir	$⊢ \exists p \in ℙ \exists a \in ℝ^{+} F = (y \in ℚ ⟼ {J (p) (y)}^{a}) \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}))$
59	45 58	syl6	$⊢ (F \in A \land \forall n \in ℕ \neg 1 < F (n)) \to (\exists p \in ℙ F (p) < 1 \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a})))$
60		ralnex	$⊢ \forall p \in ℙ \neg F (p) < 1 \leftrightarrow \neg \exists p \in ℙ F (p) < 1$
61		simpl	$⊢ (F \in A \land (\forall n \in ℕ \neg 1 < F (n) \land \forall p \in ℙ \neg F (p) < 1)) \to F \in A$
62		simprl	$⊢ (F \in A \land (\forall n \in ℕ \neg 1 < F (n) \land \forall p \in ℙ \neg F (p) < 1)) \to \forall n \in ℕ \neg 1 < F (n)$
63	62 37	sylib	$⊢ (F \in A \land (\forall n \in ℕ \neg 1 < F (n) \land \forall p \in ℙ \neg F (p) < 1)) \to \forall k \in ℕ \neg 1 < F (k)$
64		simprr	$⊢ (F \in A \land (\forall n \in ℕ \neg 1 < F (n) \land \forall p \in ℙ \neg F (p) < 1)) \to \forall p \in ℙ \neg F (p) < 1$
65		fveq2	$⊢ p = k \to F (p) = F (k)$
66	65	breq1d	$⊢ p = k \to (F (p) < 1 \leftrightarrow F (k) < 1)$
67	66	notbid	$⊢ p = k \to (\neg F (p) < 1 \leftrightarrow \neg F (k) < 1)$
68	67	cbvralvw	$⊢ \forall p \in ℙ \neg F (p) < 1 \leftrightarrow \forall k \in ℙ \neg F (k) < 1$
69	64 68	sylib	$⊢ (F \in A \land (\forall n \in ℕ \neg 1 < F (n) \land \forall p \in ℙ \neg F (p) < 1)) \to \forall k \in ℙ \neg F (k) < 1$
70	1 2 3 4 61 63 69	ostth1	$⊢ (F \in A \land (\forall n \in ℕ \neg 1 < F (n) \land \forall p \in ℙ \neg F (p) < 1)) \to F = K$
71	70	3mix1d	$⊢ (F \in A \land (\forall n \in ℕ \neg 1 < F (n) \land \forall p \in ℙ \neg F (p) < 1)) \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}))$
72	71	expr	$⊢ (F \in A \land \forall n \in ℕ \neg 1 < F (n)) \to (\forall p \in ℙ \neg F (p) < 1 \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a})))$
73	60 72	biimtrrid	$⊢ (F \in A \land \forall n \in ℕ \neg 1 < F (n)) \to (\neg \exists p \in ℙ F (p) < 1 \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a})))$
74	59 73	pm2.61d	$⊢ (F \in A \land \forall n \in ℕ \neg 1 < F (n)) \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}))$
75	74	ex	$⊢ F \in A \to (\forall n \in ℕ \neg 1 < F (n) \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a})))$
76	31 75	biimtrrid	$⊢ F \in A \to (\neg \exists n \in ℕ 1 < F (n) \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a})))$
77	30 76	pm2.61d	$⊢ F \in A \to (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}))$
78		id	$⊢ F = K \to F = K$
79	1	qdrng	$⊢ Q \in DivRing$
80	1	qrngbas	$⊢ ℚ = {Base}_{Q}$
81	2 80 10 4	abvtriv	$⊢ Q \in DivRing \to K \in A$
82	79 81	ax-mp	$⊢ K \in A$
83	78 82	eqeltrdi	$⊢ F = K \to F \in A$
84	1 2	qabsabv	$⊢ {abs ↾}_{ℚ} \in A$
85		fvres	$⊢ y \in ℚ \to ({abs ↾}_{ℚ}) (y) = \|y\|$
86	85	oveq1d	$⊢ y \in ℚ \to {({abs ↾}_{ℚ}) (y)}^{a} = {\|y\|}^{a}$
87	86	mpteq2ia	$⊢ (y \in ℚ ⟼ {({abs ↾}_{ℚ}) (y)}^{a}) = (y \in ℚ ⟼ {\|y\|}^{a})$
88	87	eqcomi	$⊢ (y \in ℚ ⟼ {\|y\|}^{a}) = (y \in ℚ ⟼ {({abs ↾}_{ℚ}) (y)}^{a})$
89	2 80 88	abvcxp	$⊢ ({abs ↾}_{ℚ} \in A \land a \in (0, 1]) \to (y \in ℚ ⟼ {\|y\|}^{a}) \in A$
90	84 89	mpan	$⊢ a \in (0, 1] \to (y \in ℚ ⟼ {\|y\|}^{a}) \in A$
91		eleq1	$⊢ F = (y \in ℚ ⟼ {\|y\|}^{a}) \to (F \in A \leftrightarrow (y \in ℚ ⟼ {\|y\|}^{a}) \in A)$
92	90 91	syl5ibrcom	$⊢ a \in (0, 1] \to (F = (y \in ℚ ⟼ {\|y\|}^{a}) \to F \in A)$
93	92	rexlimiv	$⊢ \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \to F \in A$
94	1 2 3	padicabvcxp	$⊢ (p \in ℙ \land a \in ℝ^{+}) \to (y \in ℚ ⟼ {J (p) (y)}^{a}) \in A$
95	94	ancoms	$⊢ (a \in ℝ^{+} \land p \in ℙ) \to (y \in ℚ ⟼ {J (p) (y)}^{a}) \in A$
96		eleq1	$⊢ F = (y \in ℚ ⟼ {J (p) (y)}^{a}) \to (F \in A \leftrightarrow (y \in ℚ ⟼ {J (p) (y)}^{a}) \in A)$
97	95 96	syl5ibrcom	$⊢ (a \in ℝ^{+} \land p \in ℙ) \to (F = (y \in ℚ ⟼ {J (p) (y)}^{a}) \to F \in A)$
98	97	rexlimivv	$⊢ \exists a \in ℝ^{+} \exists p \in ℙ F = (y \in ℚ ⟼ {J (p) (y)}^{a}) \to F \in A$
99	54 98	sylbi	$⊢ \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}) \to F \in A$
100	83 93 99	3jaoi	$⊢ (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a})) \to F \in A$
101	77 100	impbii	$⊢ F \in A \leftrightarrow (F = K \lor \exists a \in (0, 1] F = (y \in ℚ ⟼ {\|y\|}^{a}) \lor \exists a \in ℝ^{+} \exists g \in ran J F = (y \in ℚ ⟼ {g (y)}^{a}))$

Metamath Proof Explorer

Theorem ostth

Proof