padicabv

Description: The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Hypotheses	qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	qabsabv.a	$⊢ A = AbsVal (Q)$
	padic.f	$⊢ F = (x \in ℚ ⟼ if (x = 0, 0, N^{P pCnt x}))$
Assertion	padicabv	$⊢ (P \in ℙ \land N \in (0, 1)) \to F \in A$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
2		qabsabv.a	$⊢ A = AbsVal (Q)$
3		padic.f	$⊢ F = (x \in ℚ ⟼ if (x = 0, 0, N^{P pCnt x}))$
4	2	a1i	$⊢ (P \in ℙ \land N \in (0, 1)) \to A = AbsVal (Q)$
5	1	qrngbas	$⊢ ℚ = {Base}_{Q}$
6	5	a1i	$⊢ (P \in ℙ \land N \in (0, 1)) \to ℚ = {Base}_{Q}$
7		qex	$⊢ ℚ \in V$
8		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
9	1 8	ressplusg	$⊢ ℚ \in V \to + = +_{Q}$
10	7 9	mp1i	$⊢ (P \in ℙ \land N \in (0, 1)) \to + = +_{Q}$
11		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
12	1 11	ressmulr	$⊢ ℚ \in V \to \times = \cdot_{Q}$
13	7 12	mp1i	$⊢ (P \in ℙ \land N \in (0, 1)) \to \times = \cdot_{Q}$
14	1	qrng0	$⊢ 0 = 0_{Q}$
15	14	a1i	$⊢ (P \in ℙ \land N \in (0, 1)) \to 0 = 0_{Q}$
16	1	qdrng	$⊢ Q \in DivRing$
17		drngring	$⊢ Q \in DivRing \to Q \in Ring$
18	16 17	mp1i	$⊢ (P \in ℙ \land N \in (0, 1)) \to Q \in Ring$
19		0red	$⊢ (((P \in ℙ \land N \in (0, 1)) \land x \in ℚ) \land x = 0) \to 0 \in ℝ$
20		ioossre	$⊢ (0, 1) \subseteq ℝ$
21		simpr	$⊢ (P \in ℙ \land N \in (0, 1)) \to N \in (0, 1)$
22	20 21	sseldi	$⊢ (P \in ℙ \land N \in (0, 1)) \to N \in ℝ$
23	22	ad2antrr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land x \in ℚ) \land \neg x = 0) \to N \in ℝ$
24		eliooord	$⊢ N \in (0, 1) \to (0 < N \land N < 1)$
25	24	adantl	$⊢ (P \in ℙ \land N \in (0, 1)) \to (0 < N \land N < 1)$
26	25	simpld	$⊢ (P \in ℙ \land N \in (0, 1)) \to 0 < N$
27	22 26	elrpd	$⊢ (P \in ℙ \land N \in (0, 1)) \to N \in ℝ^{+}$
28	27	rpne0d	$⊢ (P \in ℙ \land N \in (0, 1)) \to N \neq 0$
29	28	ad2antrr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land x \in ℚ) \land \neg x = 0) \to N \neq 0$
30		df-ne	$⊢ x \neq 0 \leftrightarrow \neg x = 0$
31		pcqcl	$⊢ (P \in ℙ \land (x \in ℚ \land x \neq 0)) \to P pCnt x \in ℤ$
32	31	adantlr	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (x \in ℚ \land x \neq 0)) \to P pCnt x \in ℤ$
33	32	anassrs	$⊢ (((P \in ℙ \land N \in (0, 1)) \land x \in ℚ) \land x \neq 0) \to P pCnt x \in ℤ$
34	30 33	sylan2br	$⊢ (((P \in ℙ \land N \in (0, 1)) \land x \in ℚ) \land \neg x = 0) \to P pCnt x \in ℤ$
35	23 29 34	reexpclzd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land x \in ℚ) \land \neg x = 0) \to N^{P pCnt x} \in ℝ$
36	19 35	ifclda	$⊢ ((P \in ℙ \land N \in (0, 1)) \land x \in ℚ) \to if (x = 0, 0, N^{P pCnt x}) \in ℝ$
37	36 3	fmptd	$⊢ (P \in ℙ \land N \in (0, 1)) \to F : ℚ ⟶ ℝ$
38		0z	$⊢ 0 \in ℤ$
39		zq	$⊢ 0 \in ℤ \to 0 \in ℚ$
40	38 39	ax-mp	$⊢ 0 \in ℚ$
41		iftrue	$⊢ x = 0 \to if (x = 0, 0, N^{P pCnt x}) = 0$
42		c0ex	$⊢ 0 \in V$
43	41 3 42	fvmpt	$⊢ 0 \in ℚ \to F (0) = 0$
44	40 43	mp1i	$⊢ (P \in ℙ \land N \in (0, 1)) \to F (0) = 0$
45	22	3ad2ant1	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to N \in ℝ$
46		pcqcl	$⊢ (P \in ℙ \land (y \in ℚ \land y \neq 0)) \to P pCnt y \in ℤ$
47	46	adantlr	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0)) \to P pCnt y \in ℤ$
48	47	3impb	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to P pCnt y \in ℤ$
49	26	3ad2ant1	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to 0 < N$
50		expgt0	$⊢ (N \in ℝ \land P pCnt y \in ℤ \land 0 < N) \to 0 < N^{P pCnt y}$
51	45 48 49 50	syl3anc	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to 0 < N^{P pCnt y}$
52		eqeq1	$⊢ x = y \to (x = 0 \leftrightarrow y = 0)$
53		oveq2	$⊢ x = y \to P pCnt x = P pCnt y$
54	53	oveq2d	$⊢ x = y \to N^{P pCnt x} = N^{P pCnt y}$
55	52 54	ifbieq2d	$⊢ x = y \to if (x = 0, 0, N^{P pCnt x}) = if (y = 0, 0, N^{P pCnt y})$
56		ovex	$⊢ N^{P pCnt y} \in V$
57	42 56	ifex	$⊢ if (y = 0, 0, N^{P pCnt y}) \in V$
58	55 3 57	fvmpt	$⊢ y \in ℚ \to F (y) = if (y = 0, 0, N^{P pCnt y})$
59	58	3ad2ant2	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to F (y) = if (y = 0, 0, N^{P pCnt y})$
60		simp3	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to y \neq 0$
61	60	neneqd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to \neg y = 0$
62	61	iffalsed	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to if (y = 0, 0, N^{P pCnt y}) = N^{P pCnt y}$
63	59 62	eqtrd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to F (y) = N^{P pCnt y}$
64	51 63	breqtrrd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land y \in ℚ \land y \neq 0) \to 0 < F (y)$
65		pcqmul	$⊢ (P \in ℙ \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to P pCnt y z = (P pCnt y) + (P pCnt z)$
66	65	3adant1r	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to P pCnt y z = (P pCnt y) + (P pCnt z)$
67	66	oveq2d	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N^{P pCnt y z} = N^{(P pCnt y) + (P pCnt z)}$
68	22	recnd	$⊢ (P \in ℙ \land N \in (0, 1)) \to N \in ℂ$
69	68	3ad2ant1	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N \in ℂ$
70	28	3ad2ant1	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N \neq 0$
71	47	3adant3	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to P pCnt y \in ℤ$
72		simp1l	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to P \in ℙ$
73		simp3l	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to z \in ℚ$
74		simp3r	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to z \neq 0$
75		pcqcl	$⊢ (P \in ℙ \land (z \in ℚ \land z \neq 0)) \to P pCnt z \in ℤ$
76	72 73 74 75	syl12anc	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to P pCnt z \in ℤ$
77		expaddz	$⊢ ((N \in ℂ \land N \neq 0) \land (P pCnt y \in ℤ \land P pCnt z \in ℤ)) \to N^{(P pCnt y) + (P pCnt z)} = N^{P pCnt y} N^{P pCnt z}$
78	69 70 71 76 77	syl22anc	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N^{(P pCnt y) + (P pCnt z)} = N^{P pCnt y} N^{P pCnt z}$
79	67 78	eqtrd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N^{P pCnt y z} = N^{P pCnt y} N^{P pCnt z}$
80		simp2l	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to y \in ℚ$
81		qmulcl	$⊢ (y \in ℚ \land z \in ℚ) \to y z \in ℚ$
82	80 73 81	syl2anc	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to y z \in ℚ$
83		eqeq1	$⊢ x = y z \to (x = 0 \leftrightarrow y z = 0)$
84		oveq2	$⊢ x = y z \to P pCnt x = P pCnt y z$
85	84	oveq2d	$⊢ x = y z \to N^{P pCnt x} = N^{P pCnt y z}$
86	83 85	ifbieq2d	$⊢ x = y z \to if (x = 0, 0, N^{P pCnt x}) = if (y z = 0, 0, N^{P pCnt y z})$
87		ovex	$⊢ N^{P pCnt y z} \in V$
88	42 87	ifex	$⊢ if (y z = 0, 0, N^{P pCnt y z}) \in V$
89	86 3 88	fvmpt	$⊢ y z \in ℚ \to F (y z) = if (y z = 0, 0, N^{P pCnt y z})$
90	82 89	syl	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (y z) = if (y z = 0, 0, N^{P pCnt y z})$
91		qcn	$⊢ y \in ℚ \to y \in ℂ$
92	80 91	syl	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to y \in ℂ$
93		qcn	$⊢ z \in ℚ \to z \in ℂ$
94	73 93	syl	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to z \in ℂ$
95		simp2r	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to y \neq 0$
96	92 94 95 74	mulne0d	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to y z \neq 0$
97	96	neneqd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to \neg y z = 0$
98	97	iffalsed	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to if (y z = 0, 0, N^{P pCnt y z}) = N^{P pCnt y z}$
99	90 98	eqtrd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (y z) = N^{P pCnt y z}$
100	63	3expb	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0)) \to F (y) = N^{P pCnt y}$
101	100	3adant3	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (y) = N^{P pCnt y}$
102		eqeq1	$⊢ x = z \to (x = 0 \leftrightarrow z = 0)$
103		oveq2	$⊢ x = z \to P pCnt x = P pCnt z$
104	103	oveq2d	$⊢ x = z \to N^{P pCnt x} = N^{P pCnt z}$
105	102 104	ifbieq2d	$⊢ x = z \to if (x = 0, 0, N^{P pCnt x}) = if (z = 0, 0, N^{P pCnt z})$
106		ovex	$⊢ N^{P pCnt z} \in V$
107	42 106	ifex	$⊢ if (z = 0, 0, N^{P pCnt z}) \in V$
108	105 3 107	fvmpt	$⊢ z \in ℚ \to F (z) = if (z = 0, 0, N^{P pCnt z})$
109	73 108	syl	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (z) = if (z = 0, 0, N^{P pCnt z})$
110	74	neneqd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to \neg z = 0$
111	110	iffalsed	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to if (z = 0, 0, N^{P pCnt z}) = N^{P pCnt z}$
112	109 111	eqtrd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (z) = N^{P pCnt z}$
113	101 112	oveq12d	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (y) F (z) = N^{P pCnt y} N^{P pCnt z}$
114	79 99 113	3eqtr4d	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (y z) = F (y) F (z)$
115		iftrue	$⊢ y + z = 0 \to if (y + z = 0, 0, N^{P pCnt (y + z)}) = 0$
116	115	breq1d	$⊢ y + z = 0 \to (if (y + z = 0, 0, N^{P pCnt (y + z)}) \leq N^{P pCnt y} + N^{P pCnt z} \leftrightarrow 0 \leq N^{P pCnt y} + N^{P pCnt z})$
117		ifnefalse	$⊢ y + z \neq 0 \to if (y + z = 0, 0, N^{P pCnt (y + z)}) = N^{P pCnt (y + z)}$
118	117	adantl	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to if (y + z = 0, 0, N^{P pCnt (y + z)}) = N^{P pCnt (y + z)}$
119	71	adantr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to P pCnt y \in ℤ$
120	119	zred	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to P pCnt y \in ℝ$
121	76	adantr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to P pCnt z \in ℤ$
122	121	zred	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to P pCnt z \in ℝ$
123	22	3ad2ant1	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N \in ℝ$
124	123	ad2antrr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to N \in ℝ$
125	70	ad2antrr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to N \neq 0$
126	72	adantr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to P \in ℙ$
127		qaddcl	$⊢ (y \in ℚ \land z \in ℚ) \to y + z \in ℚ$
128	80 73 127	syl2anc	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to y + z \in ℚ$
129	128	adantr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to y + z \in ℚ$
130		simpr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to y + z \neq 0$
131		pcqcl	$⊢ (P \in ℙ \land (y + z \in ℚ \land y + z \neq 0)) \to P pCnt (y + z) \in ℤ$
132	126 129 130 131	syl12anc	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to P pCnt (y + z) \in ℤ$
133	132	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to P pCnt (y + z) \in ℤ$
134	124 125 133	reexpclzd	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to N^{P pCnt (y + z)} \in ℝ$
135	119	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to P pCnt y \in ℤ$
136	124 125 135	reexpclzd	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to N^{P pCnt y} \in ℝ$
137		simpl1	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (P \in ℙ \land N \in (0, 1))$
138	137 22	syl	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N \in ℝ$
139	137 28	syl	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N \neq 0$
140	138 139 119	reexpclzd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt y} \in ℝ$
141	138 139 121	reexpclzd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt z} \in ℝ$
142	140 141	readdcld	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt y} + N^{P pCnt z} \in ℝ$
143	142	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to N^{P pCnt y} + N^{P pCnt z} \in ℝ$
144	126	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to P \in ℙ$
145	80	ad2antrr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to y \in ℚ$
146	73	ad2antrr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to z \in ℚ$
147		simpr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to P pCnt y \leq P pCnt z$
148	144 145 146 147	pcadd	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to P pCnt y \leq P pCnt (y + z)$
149	137 27	syl	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N \in ℝ^{+}$
150	25	simprd	$⊢ (P \in ℙ \land N \in (0, 1)) \to N < 1$
151	137 150	syl	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N < 1$
152	149 119 132 151	ltexp2rd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (P pCnt (y + z) < P pCnt y \leftrightarrow N^{P pCnt y} < N^{P pCnt (y + z)})$
153	152	notbid	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (\neg P pCnt (y + z) < P pCnt y \leftrightarrow \neg N^{P pCnt y} < N^{P pCnt (y + z)})$
154	132	zred	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to P pCnt (y + z) \in ℝ$
155	120 154	lenltd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (P pCnt y \leq P pCnt (y + z) \leftrightarrow \neg P pCnt (y + z) < P pCnt y)$
156	138 139 132	reexpclzd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt (y + z)} \in ℝ$
157	156 140	lenltd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (N^{P pCnt (y + z)} \leq N^{P pCnt y} \leftrightarrow \neg N^{P pCnt y} < N^{P pCnt (y + z)})$
158	153 155 157	3bitr4d	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (P pCnt y \leq P pCnt (y + z) \leftrightarrow N^{P pCnt (y + z)} \leq N^{P pCnt y})$
159	158	biimpa	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt (y + z)) \to N^{P pCnt (y + z)} \leq N^{P pCnt y}$
160	148 159	syldan	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to N^{P pCnt (y + z)} \leq N^{P pCnt y}$
161	27	3ad2ant1	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N \in ℝ^{+}$
162	161 76	rpexpcld	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N^{P pCnt z} \in ℝ^{+}$
163	162	adantr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt z} \in ℝ^{+}$
164	163	rpge0d	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to 0 \leq N^{P pCnt z}$
165	140 141	addge01d	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (0 \leq N^{P pCnt z} \leftrightarrow N^{P pCnt y} \leq N^{P pCnt y} + N^{P pCnt z})$
166	164 165	mpbid	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt y} \leq N^{P pCnt y} + N^{P pCnt z}$
167	166	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to N^{P pCnt y} \leq N^{P pCnt y} + N^{P pCnt z}$
168	134 136 143 160 167	letrd	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt y \leq P pCnt z) \to N^{P pCnt (y + z)} \leq N^{P pCnt y} + N^{P pCnt z}$
169	156	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to N^{P pCnt (y + z)} \in ℝ$
170	141	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to N^{P pCnt z} \in ℝ$
171	142	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to N^{P pCnt y} + N^{P pCnt z} \in ℝ$
172	126	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to P \in ℙ$
173	73	ad2antrr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to z \in ℚ$
174	80	ad2antrr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to y \in ℚ$
175		simpr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to P pCnt z \leq P pCnt y$
176	172 173 174 175	pcadd	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to P pCnt z \leq P pCnt (z + y)$
177	92 94	addcomd	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to y + z = z + y$
178	177	oveq2d	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to P pCnt (y + z) = P pCnt (z + y)$
179	178	ad2antrr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to P pCnt (y + z) = P pCnt (z + y)$
180	176 179	breqtrrd	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to P pCnt z \leq P pCnt (y + z)$
181	149 121 132 151	ltexp2rd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (P pCnt (y + z) < P pCnt z \leftrightarrow N^{P pCnt z} < N^{P pCnt (y + z)})$
182	181	notbid	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (\neg P pCnt (y + z) < P pCnt z \leftrightarrow \neg N^{P pCnt z} < N^{P pCnt (y + z)})$
183	122 154	lenltd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (P pCnt z \leq P pCnt (y + z) \leftrightarrow \neg P pCnt (y + z) < P pCnt z)$
184	156 141	lenltd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (N^{P pCnt (y + z)} \leq N^{P pCnt z} \leftrightarrow \neg N^{P pCnt z} < N^{P pCnt (y + z)})$
185	182 183 184	3bitr4d	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (P pCnt z \leq P pCnt (y + z) \leftrightarrow N^{P pCnt (y + z)} \leq N^{P pCnt z})$
186	185	biimpa	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt (y + z)) \to N^{P pCnt (y + z)} \leq N^{P pCnt z}$
187	180 186	syldan	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to N^{P pCnt (y + z)} \leq N^{P pCnt z}$
188	161 71	rpexpcld	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N^{P pCnt y} \in ℝ^{+}$
189	188	adantr	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt y} \in ℝ^{+}$
190	189	rpge0d	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to 0 \leq N^{P pCnt y}$
191	141 140	addge02d	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to (0 \leq N^{P pCnt y} \leftrightarrow N^{P pCnt z} \leq N^{P pCnt y} + N^{P pCnt z})$
192	190 191	mpbid	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt z} \leq N^{P pCnt y} + N^{P pCnt z}$
193	192	adantr	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to N^{P pCnt z} \leq N^{P pCnt y} + N^{P pCnt z}$
194	169 170 171 187 193	letrd	$⊢ ((((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \land P pCnt z \leq P pCnt y) \to N^{P pCnt (y + z)} \leq N^{P pCnt y} + N^{P pCnt z}$
195	120 122 168 194	lecasei	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to N^{P pCnt (y + z)} \leq N^{P pCnt y} + N^{P pCnt z}$
196	118 195	eqbrtrd	$⊢ (((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \land y + z \neq 0) \to if (y + z = 0, 0, N^{P pCnt (y + z)}) \leq N^{P pCnt y} + N^{P pCnt z}$
197	188 162	rpaddcld	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to N^{P pCnt y} + N^{P pCnt z} \in ℝ^{+}$
198	197	rpge0d	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to 0 \leq N^{P pCnt y} + N^{P pCnt z}$
199	116 196 198	pm2.61ne	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to if (y + z = 0, 0, N^{P pCnt (y + z)}) \leq N^{P pCnt y} + N^{P pCnt z}$
200		eqeq1	$⊢ x = y + z \to (x = 0 \leftrightarrow y + z = 0)$
201		oveq2	$⊢ x = y + z \to P pCnt x = P pCnt (y + z)$
202	201	oveq2d	$⊢ x = y + z \to N^{P pCnt x} = N^{P pCnt (y + z)}$
203	200 202	ifbieq2d	$⊢ x = y + z \to if (x = 0, 0, N^{P pCnt x}) = if (y + z = 0, 0, N^{P pCnt (y + z)})$
204		ovex	$⊢ N^{P pCnt (y + z)} \in V$
205	42 204	ifex	$⊢ if (y + z = 0, 0, N^{P pCnt (y + z)}) \in V$
206	203 3 205	fvmpt	$⊢ y + z \in ℚ \to F (y + z) = if (y + z = 0, 0, N^{P pCnt (y + z)})$
207	128 206	syl	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (y + z) = if (y + z = 0, 0, N^{P pCnt (y + z)})$
208	101 112	oveq12d	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (y) + F (z) = N^{P pCnt y} + N^{P pCnt z}$
209	199 207 208	3brtr4d	$⊢ ((P \in ℙ \land N \in (0, 1)) \land (y \in ℚ \land y \neq 0) \land (z \in ℚ \land z \neq 0)) \to F (y + z) \leq F (y) + F (z)$
210	4 6 10 13 15 18 37 44 64 114 209	isabvd	$⊢ (P \in ℙ \land N \in (0, 1)) \to F \in A$

Metamath Proof Explorer

Theorem padicabv

Proof