padicabvcxp

Description: All positive powers of the p-adic absolute value are absolute values. (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	padicabvcxp	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to (y \in ℚ ⟼ {J (P) (y)}^{R}) \in 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	3	padicval	$⊢ (P \in ℙ \land y \in ℚ) \to J (P) (y) = if (y = 0, 0, P^{- (P pCnt y)})$
5	4	adantlr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \to J (P) (y) = if (y = 0, 0, P^{- (P pCnt y)})$
6	5	oveq1d	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \to {J (P) (y)}^{R} = {if (y = 0, 0, P^{- (P pCnt y)})}^{R}$
7		ovif	$⊢ {if (y = 0, 0, P^{- (P pCnt y)})}^{R} = if (y = 0, 0^{R}, {(P^{- (P pCnt y)})}^{R})$
8		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
9	8	adantl	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to R \in ℝ$
10	9	recnd	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to R \in ℂ$
11		rpne0	$⊢ R \in ℝ^{+} \to R \neq 0$
12	11	adantl	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to R \neq 0$
13	10 12	0cxpd	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to 0^{R} = 0$
14	13	adantr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \to 0^{R} = 0$
15	14	ifeq1d	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \to if (y = 0, 0^{R}, {(P^{- (P pCnt y)})}^{R}) = if (y = 0, 0, {(P^{- (P pCnt y)})}^{R})$
16	7 15	syl5eq	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \to {if (y = 0, 0, P^{- (P pCnt y)})}^{R} = if (y = 0, 0, {(P^{- (P pCnt y)})}^{R})$
17		df-ne	$⊢ y \neq 0 \leftrightarrow \neg y = 0$
18		pcqcl	$⊢ (P \in ℙ \land (y \in ℚ \land y \neq 0)) \to P pCnt y \in ℤ$
19	18	adantlr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P pCnt y \in ℤ$
20	19	zcnd	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P pCnt y \in ℂ$
21	10	adantr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to R \in ℂ$
22		mulneg12	$⊢ (P pCnt y \in ℂ \land R \in ℂ) \to (- (P pCnt y)) R = (P pCnt y) (- R)$
23	20 21 22	syl2anc	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to (- (P pCnt y)) R = (P pCnt y) (- R)$
24	21	negcld	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to - R \in ℂ$
25	20 24	mulcomd	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to (P pCnt y) (- R) = (- R) (P pCnt y)$
26	23 25	eqtrd	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to (- (P pCnt y)) R = (- R) (P pCnt y)$
27	26	oveq2d	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P^{(- (P pCnt y)) R} = P^{(- R) (P pCnt y)}$
28		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
29	28	adantr	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P \in ℤ_{\geq 2}$
30		eluz2b2	$⊢ P \in ℤ_{\geq 2} \leftrightarrow (P \in ℕ \land 1 < P)$
31	29 30	sylib	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to (P \in ℕ \land 1 < P)$
32	31	simpld	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P \in ℕ$
33	32	nnrpd	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P \in ℝ^{+}$
34	33	adantr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P \in ℝ^{+}$
35	19	znegcld	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to - (P pCnt y) \in ℤ$
36	35	zred	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to - (P pCnt y) \in ℝ$
37	34 36 21	cxpmuld	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P^{(- (P pCnt y)) R} = {(P^{- (P pCnt y)})}^{R}$
38	9	renegcld	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to - R \in ℝ$
39	38	adantr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to - R \in ℝ$
40	34 39 20	cxpmuld	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P^{(- R) (P pCnt y)} = {(P^{- R})}^{P pCnt y}$
41	27 37 40	3eqtr3d	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to {(P^{- (P pCnt y)})}^{R} = {(P^{- R})}^{P pCnt y}$
42	32	nnred	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P \in ℝ$
43	42	recnd	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P \in ℂ$
44	43	adantr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P \in ℂ$
45	32	nnne0d	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P \neq 0$
46	45	adantr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P \neq 0$
47	44 46 35	cxpexpzd	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P^{- (P pCnt y)} = P^{- (P pCnt y)}$
48	47	oveq1d	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to {(P^{- (P pCnt y)})}^{R} = {(P^{- (P pCnt y)})}^{R}$
49	33 38	rpcxpcld	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P^{- R} \in ℝ^{+}$
50	49	adantr	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P^{- R} \in ℝ^{+}$
51	50	rpcnd	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P^{- R} \in ℂ$
52	50	rpne0d	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to P^{- R} \neq 0$
53	51 52 19	cxpexpzd	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to {(P^{- R})}^{P pCnt y} = {(P^{- R})}^{P pCnt y}$
54	41 48 53	3eqtr3d	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land (y \in ℚ \land y \neq 0)) \to {(P^{- (P pCnt y)})}^{R} = {(P^{- R})}^{P pCnt y}$
55	54	anassrs	$⊢ (((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \land y \neq 0) \to {(P^{- (P pCnt y)})}^{R} = {(P^{- R})}^{P pCnt y}$
56	17 55	sylan2br	$⊢ (((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \land \neg y = 0) \to {(P^{- (P pCnt y)})}^{R} = {(P^{- R})}^{P pCnt y}$
57	56	ifeq2da	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \to if (y = 0, 0, {(P^{- (P pCnt y)})}^{R}) = if (y = 0, 0, {(P^{- R})}^{P pCnt y})$
58	6 16 57	3eqtrd	$⊢ ((P \in ℙ \land R \in ℝ^{+}) \land y \in ℚ) \to {J (P) (y)}^{R} = if (y = 0, 0, {(P^{- R})}^{P pCnt y})$
59	58	mpteq2dva	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to (y \in ℚ ⟼ {J (P) (y)}^{R}) = (y \in ℚ ⟼ if (y = 0, 0, {(P^{- R})}^{P pCnt y}))$
60		rpre	$⊢ P^{- R} \in ℝ^{+} \to P^{- R} \in ℝ$
61	49 60	syl	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P^{- R} \in ℝ$
62		rpgt0	$⊢ P^{- R} \in ℝ^{+} \to 0 < P^{- R}$
63	49 62	syl	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to 0 < P^{- R}$
64		rpgt0	$⊢ R \in ℝ^{+} \to 0 < R$
65	64	adantl	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to 0 < R$
66	9	lt0neg2d	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to (0 < R \leftrightarrow - R < 0)$
67	65 66	mpbid	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to - R < 0$
68	31	simprd	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to 1 < P$
69		0red	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to 0 \in ℝ$
70	42 68 38 69	cxpltd	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to (- R < 0 \leftrightarrow P^{- R} < P^{0})$
71	67 70	mpbid	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P^{- R} < P^{0}$
72	43	cxp0d	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P^{0} = 1$
73	71 72	breqtrd	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P^{- R} < 1$
74		0xr	$⊢ 0 \in ℝ^{*}$
75		1xr	$⊢ 1 \in ℝ^{*}$
76		elioo2	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (P^{- R} \in (0, 1) \leftrightarrow (P^{- R} \in ℝ \land 0 < P^{- R} \land P^{- R} < 1))$
77	74 75 76	mp2an	$⊢ P^{- R} \in (0, 1) \leftrightarrow (P^{- R} \in ℝ \land 0 < P^{- R} \land P^{- R} < 1)$
78	61 63 73 77	syl3anbrc	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to P^{- R} \in (0, 1)$
79		eqid	$⊢ (y \in ℚ ⟼ if (y = 0, 0, {(P^{- R})}^{P pCnt y})) = (y \in ℚ ⟼ if (y = 0, 0, {(P^{- R})}^{P pCnt y}))$
80	1 2 79	padicabv	$⊢ (P \in ℙ \land P^{- R} \in (0, 1)) \to (y \in ℚ ⟼ if (y = 0, 0, {(P^{- R})}^{P pCnt y})) \in A$
81	78 80	syldan	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to (y \in ℚ ⟼ if (y = 0, 0, {(P^{- R})}^{P pCnt y})) \in A$
82	59 81	eqeltrd	$⊢ (P \in ℙ \land R \in ℝ^{+}) \to (y \in ℚ ⟼ {J (P) (y)}^{R}) \in A$

Metamath Proof Explorer

Theorem padicabvcxp

Proof