padicabvf

Description: The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-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)})))$
Assertion	padicabvf	$⊢ J : ℙ ⟶ 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		qex	$⊢ ℚ \in V$
5	4	mptex	$⊢ (x \in ℚ ⟼ if (x = 0, 0, q^{- (q pCnt x)})) \in V$
6	5 3	fnmpti	$⊢ J Fn ℙ$
7	3	padicfval	$⊢ p \in ℙ \to J (p) = (x \in ℚ ⟼ if (x = 0, 0, p^{- (p pCnt x)}))$
8		prmnn	$⊢ p \in ℙ \to p \in ℕ$
9	8	ad2antrr	$⊢ ((p \in ℙ \land x \in ℚ) \land \neg x = 0) \to p \in ℕ$
10	9	nncnd	$⊢ ((p \in ℙ \land x \in ℚ) \land \neg x = 0) \to p \in ℂ$
11	9	nnne0d	$⊢ ((p \in ℙ \land x \in ℚ) \land \neg x = 0) \to p \neq 0$
12		df-ne	$⊢ x \neq 0 \leftrightarrow \neg x = 0$
13		pcqcl	$⊢ (p \in ℙ \land (x \in ℚ \land x \neq 0)) \to p pCnt x \in ℤ$
14	13	anassrs	$⊢ ((p \in ℙ \land x \in ℚ) \land x \neq 0) \to p pCnt x \in ℤ$
15	12 14	sylan2br	$⊢ ((p \in ℙ \land x \in ℚ) \land \neg x = 0) \to p pCnt x \in ℤ$
16	10 11 15	expnegd	$⊢ ((p \in ℙ \land x \in ℚ) \land \neg x = 0) \to p^{- (p pCnt x)} = \frac{1}{p^{p pCnt x}}$
17	10 11 15	exprecd	$⊢ ((p \in ℙ \land x \in ℚ) \land \neg x = 0) \to {(\frac{1}{p})}^{p pCnt x} = \frac{1}{p^{p pCnt x}}$
18	16 17	eqtr4d	$⊢ ((p \in ℙ \land x \in ℚ) \land \neg x = 0) \to p^{- (p pCnt x)} = {(\frac{1}{p})}^{p pCnt x}$
19	18	ifeq2da	$⊢ (p \in ℙ \land x \in ℚ) \to if (x = 0, 0, p^{- (p pCnt x)}) = if (x = 0, 0, {(\frac{1}{p})}^{p pCnt x})$
20	19	mpteq2dva	$⊢ p \in ℙ \to (x \in ℚ ⟼ if (x = 0, 0, p^{- (p pCnt x)})) = (x \in ℚ ⟼ if (x = 0, 0, {(\frac{1}{p})}^{p pCnt x}))$
21	7 20	eqtrd	$⊢ p \in ℙ \to J (p) = (x \in ℚ ⟼ if (x = 0, 0, {(\frac{1}{p})}^{p pCnt x}))$
22	8	nnrecred	$⊢ p \in ℙ \to \frac{1}{p} \in ℝ$
23	8	nnred	$⊢ p \in ℙ \to p \in ℝ$
24		prmgt1	$⊢ p \in ℙ \to 1 < p$
25		recgt1i	$⊢ (p \in ℝ \land 1 < p) \to (0 < \frac{1}{p} \land \frac{1}{p} < 1)$
26	23 24 25	syl2anc	$⊢ p \in ℙ \to (0 < \frac{1}{p} \land \frac{1}{p} < 1)$
27	26	simpld	$⊢ p \in ℙ \to 0 < \frac{1}{p}$
28	26	simprd	$⊢ p \in ℙ \to \frac{1}{p} < 1$
29		0xr	$⊢ 0 \in ℝ^{*}$
30		1xr	$⊢ 1 \in ℝ^{*}$
31		elioo2	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (\frac{1}{p} \in (0, 1) \leftrightarrow (\frac{1}{p} \in ℝ \land 0 < \frac{1}{p} \land \frac{1}{p} < 1))$
32	29 30 31	mp2an	$⊢ \frac{1}{p} \in (0, 1) \leftrightarrow (\frac{1}{p} \in ℝ \land 0 < \frac{1}{p} \land \frac{1}{p} < 1)$
33	22 27 28 32	syl3anbrc	$⊢ p \in ℙ \to \frac{1}{p} \in (0, 1)$
34		eqid	$⊢ (x \in ℚ ⟼ if (x = 0, 0, {(\frac{1}{p})}^{p pCnt x})) = (x \in ℚ ⟼ if (x = 0, 0, {(\frac{1}{p})}^{p pCnt x}))$
35	1 2 34	padicabv	$⊢ (p \in ℙ \land \frac{1}{p} \in (0, 1)) \to (x \in ℚ ⟼ if (x = 0, 0, {(\frac{1}{p})}^{p pCnt x})) \in A$
36	33 35	mpdan	$⊢ p \in ℙ \to (x \in ℚ ⟼ if (x = 0, 0, {(\frac{1}{p})}^{p pCnt x})) \in A$
37	21 36	eqeltrd	$⊢ p \in ℙ \to J (p) \in A$
38	37	rgen	$⊢ \forall p \in ℙ J (p) \in A$
39		ffnfv	$⊢ J : ℙ ⟶ A \leftrightarrow (J Fn ℙ \land \forall p \in ℙ J (p) \in A)$
40	6 38 39	mpbir2an	$⊢ J : ℙ ⟶ A$

Metamath Proof Explorer

Theorem padicabvf

Proof