padicabv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > padicabv		Structured version Visualization version GIF version

Theorem padicabv 27601

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

**Hypotheses**
Ref	Expression
qrng.q	⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
qabsabv.a	⊢ 𝐴 = (AbsVal‘𝑄)
padic.f	⊢ 𝐹 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))))

**Assertion**
Ref	Expression
padicabv	⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹 ∈ 𝐴)

Distinct variable groups: 𝑥,𝐴 𝑥,𝑁 𝑥,𝑄 𝑥,𝑃 Allowed substitution hint: 𝐹(𝑥)

Proof of Theorem padicabv Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		qabsabv.a	. . 3 ⊢ 𝐴 = (AbsVal‘𝑄)
2	1	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐴 = (AbsVal‘𝑄))
3		qrng.q	. . . 4 ⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
4	3	qrngbas 27590	. . 3 ⊢ ℚ = (Base‘𝑄)
5	4	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → ℚ = (Base‘𝑄))
6		qex 12878	. . 3 ⊢ ℚ ∈ V
7		cnfldadd 21319	. . . 4 ⊢ + = (+_g‘ℂ_fld)
8	3, 7	ressplusg 17215	. . 3 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
9	6, 8	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → + = (+_g‘𝑄))
10		cnfldmul 21321	. . . 4 ⊢ · = (._r‘ℂ_fld)
11	3, 10	ressmulr 17231	. . 3 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
12	6, 11	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → · = (._r‘𝑄))
13	3	qrng0 27592	. . 3 ⊢ 0 = (0_g‘𝑄)
14	13	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 0 = (0_g‘𝑄))
15	3	qdrng 27591	. . 3 ⊢ 𝑄 ∈ DivRing
16		drngring 20673	. . 3 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
17	15, 16	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑄 ∈ Ring)
18		0red 11139	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ 𝑥 = 0) → 0 ∈ ℝ)
19		ioossre 13327	. . . . . . 7 ⊢ (0(,)1) ⊆ ℝ
20		simpr 484	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ (0(,)1))
21	19, 20	sselid 3932	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℝ)
22	21	ad2antrr 727	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → 𝑁 ∈ ℝ)
23		eliooord 13325	. . . . . . . . . 10 ⊢ (𝑁 ∈ (0(,)1) → (0 < 𝑁 ∧ 𝑁 < 1))
24	23	adantl 481	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → (0 < 𝑁 ∧ 𝑁 < 1))
25	24	simpld 494	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 0 < 𝑁)
26	21, 25	elrpd 12950	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℝ⁺)
27	26	rpne0d 12958	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ≠ 0)
28	27	ad2antrr 727	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → 𝑁 ≠ 0)
29		df-ne 2934	. . . . . 6 ⊢ (𝑥 ≠ 0 ↔ ¬ 𝑥 = 0)
30		pcqcl 16788	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℚ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ)
31	30	adantlr 716	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑥 ∈ ℚ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ)
32	31	anassrs 467	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ 𝑥 ≠ 0) → (𝑃 pCnt 𝑥) ∈ ℤ)
33	29, 32	sylan2br 596	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → (𝑃 pCnt 𝑥) ∈ ℤ)
34	22, 28, 33	reexpclzd 14176	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → (𝑁↑(𝑃 pCnt 𝑥)) ∈ ℝ)
35	18, 34	ifclda 4516	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) ∈ ℝ)
36		padic.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))))
37	35, 36	fmptd 7061	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹:ℚ⟶ℝ)
38		0z 12503	. . . 4 ⊢ 0 ∈ ℤ
39		zq 12871	. . . 4 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
40	38, 39	ax-mp 5	. . 3 ⊢ 0 ∈ ℚ
41		iftrue 4486	. . . 4 ⊢ (𝑥 = 0 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = 0)
42		c0ex 11130	. . . 4 ⊢ 0 ∈ V
43	41, 36, 42	fvmpt 6942	. . 3 ⊢ (0 ∈ ℚ → (𝐹‘0) = 0)
44	40, 43	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → (𝐹‘0) = 0)
45	21	3ad2ant1 1134	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 𝑁 ∈ ℝ)
46		pcqcl 16788	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
47	46	adantlr 716	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
48	47	3impb 1115	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℤ)
49	25	3ad2ant1 1134	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < 𝑁)
50		expgt0 14022	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑃 pCnt 𝑦) ∈ ℤ ∧ 0 < 𝑁) → 0 < (𝑁↑(𝑃 pCnt 𝑦)))
51	45, 48, 49, 50	syl3anc 1374	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < (𝑁↑(𝑃 pCnt 𝑦)))
52		eqeq1 2741	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 0 ↔ 𝑦 = 0))
53		oveq2 7368	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑃 pCnt 𝑥) = (𝑃 pCnt 𝑦))
54	53	oveq2d 7376	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt 𝑦)))
55	52, 54	ifbieq2d 4507	. . . . . 6 ⊢ (𝑥 = 𝑦 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
56		ovex 7393	. . . . . . 7 ⊢ (𝑁↑(𝑃 pCnt 𝑦)) ∈ V
57	42, 56	ifex 4531	. . . . . 6 ⊢ if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) ∈ V
58	55, 36, 57	fvmpt 6942	. . . . 5 ⊢ (𝑦 ∈ ℚ → (𝐹‘𝑦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
59	58	3ad2ant2 1135	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝐹‘𝑦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
60		simp3 1139	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 𝑦 ≠ 0)
61	60	neneqd 2938	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → ¬ 𝑦 = 0)
62	61	iffalsed 4491	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) = (𝑁↑(𝑃 pCnt 𝑦)))
63	59, 62	eqtrd 2772	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
64	51, 63	breqtrrd 5127	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < (𝐹‘𝑦))
65		pcqmul 16785	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
66	65	3adant1r 1179	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
67	66	oveq2d 7376	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) = (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))))
68	21	recnd 11164	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℂ)
69	68	3ad2ant1 1134	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℂ)
70	27	3ad2ant1 1134	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ≠ 0)
71	47	3adant3 1133	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
72		simp1l 1199	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑃 ∈ ℙ)
73		simp3l 1203	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ∈ ℚ)
74		simp3r 1204	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ≠ 0)
75		pcqcl 16788	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℤ)
76	72, 73, 74, 75	syl12anc 837	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℤ)
77		expaddz 14033	. . . . 5 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑃 pCnt 𝑦) ∈ ℤ ∧ (𝑃 pCnt 𝑧) ∈ ℤ)) → (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
78	69, 70, 71, 76, 77	syl22anc 839	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
79	67, 78	eqtrd 2772	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
80		simp2l 1201	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ∈ ℚ)
81		qmulcl 12884	. . . . . 6 ⊢ ((𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝑦 · 𝑧) ∈ ℚ)
82	80, 73, 81	syl2anc 585	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 · 𝑧) ∈ ℚ)
83		eqeq1 2741	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 = 0 ↔ (𝑦 · 𝑧) = 0))
84		oveq2 7368	. . . . . . . 8 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑃 pCnt 𝑥) = (𝑃 pCnt (𝑦 · 𝑧)))
85	84	oveq2d 7376	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
86	83, 85	ifbieq2d 4507	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
87		ovex 7393	. . . . . . 7 ⊢ (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) ∈ V
88	42, 87	ifex 4531	. . . . . 6 ⊢ if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))) ∈ V
89	86, 36, 88	fvmpt 6942	. . . . 5 ⊢ ((𝑦 · 𝑧) ∈ ℚ → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
90	82, 89	syl 17	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
91		qcn 12880	. . . . . . . 8 ⊢ (𝑦 ∈ ℚ → 𝑦 ∈ ℂ)
92	80, 91	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ∈ ℂ)
93		qcn 12880	. . . . . . . 8 ⊢ (𝑧 ∈ ℚ → 𝑧 ∈ ℂ)
94	73, 93	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ∈ ℂ)
95		simp2r 1202	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ≠ 0)
96	92, 94, 95, 74	mulne0d 11793	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 · 𝑧) ≠ 0)
97	96	neneqd 2938	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ¬ (𝑦 · 𝑧) = 0)
98	97	iffalsed 4491	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
99	90, 98	eqtrd 2772	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
100	63	3expb 1121	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
101	100	3adant3 1133	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
102		eqeq1 2741	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 0 ↔ 𝑧 = 0))
103		oveq2 7368	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑃 pCnt 𝑥) = (𝑃 pCnt 𝑧))
104	103	oveq2d 7376	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt 𝑧)))
105	102, 104	ifbieq2d 4507	. . . . . . 7 ⊢ (𝑥 = 𝑧 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
106		ovex 7393	. . . . . . . 8 ⊢ (𝑁↑(𝑃 pCnt 𝑧)) ∈ V
107	42, 106	ifex 4531	. . . . . . 7 ⊢ if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) ∈ V
108	105, 36, 107	fvmpt 6942	. . . . . 6 ⊢ (𝑧 ∈ ℚ → (𝐹‘𝑧) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
109	73, 108	syl 17	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑧) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
110	74	neneqd 2938	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ¬ 𝑧 = 0)
111	110	iffalsed 4491	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) = (𝑁↑(𝑃 pCnt 𝑧)))
112	109, 111	eqtrd 2772	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑧) = (𝑁↑(𝑃 pCnt 𝑧)))
113	101, 112	oveq12d 7378	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝐹‘𝑦) · (𝐹‘𝑧)) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
114	79, 99, 113	3eqtr4d 2782	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧)))
115		iftrue 4486	. . . . 5 ⊢ ((𝑦 + 𝑧) = 0 → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = 0)
116	115	breq1d 5109	. . . 4 ⊢ ((𝑦 + 𝑧) = 0 → (if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ↔ 0 ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
117		ifnefalse 4492	. . . . . 6 ⊢ ((𝑦 + 𝑧) ≠ 0 → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
118	117	adantl 481	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
119	71	adantr 480	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℤ)
120	119	zred 12600	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℝ)
121	76	adantr 480	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑧) ∈ ℤ)
122	121	zred 12600	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑧) ∈ ℝ)
123	21	3ad2ant1 1134	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℝ)
124	123	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑁 ∈ ℝ)
125	70	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑁 ≠ 0)
126	72	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑃 ∈ ℙ)
127		qaddcl 12882	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝑦 + 𝑧) ∈ ℚ)
128	80, 73, 127	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 + 𝑧) ∈ ℚ)
129	128	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑦 + 𝑧) ∈ ℚ)
130		simpr 484	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑦 + 𝑧) ≠ 0)
131		pcqcl 16788	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ((𝑦 + 𝑧) ∈ ℚ ∧ (𝑦 + 𝑧) ≠ 0)) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
132	126, 129, 130, 131	syl12anc 837	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
133	132	adantr 480	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
134	124, 125, 133	reexpclzd 14176	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
135	119	adantr 480	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ∈ ℤ)
136	124, 125, 135	reexpclzd 14176	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
137		simpl1 1193	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)))
138	137, 21	syl 17	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑁 ∈ ℝ)
139	137, 27	syl 17	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑁 ≠ 0)
140	138, 139, 119	reexpclzd 14176	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
141	138, 139, 121	reexpclzd 14176	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
142	140, 141	readdcld 11165	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
143	142	adantr 480	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
144	126	adantr 480	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑃 ∈ ℙ)
145	80	ad2antrr 727	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑦 ∈ ℚ)
146	73	ad2antrr 727	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑧 ∈ ℚ)
147		simpr 484	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧))
148	144, 145, 146, 147	pcadd 16821	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)))
149	137, 26	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑁 ∈ ℝ⁺)
150	24	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 < 1)
151	137, 150	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑁 < 1)
152	149, 119, 132, 151	ltexp2rd 14175	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦) ↔ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
153	152	notbid 318	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦) ↔ ¬ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
154	132	zred 12600	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℝ)
155	120, 154	lenltd 11283	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ ¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦)))
156	138, 139, 132	reexpclzd 14176	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
157	156, 140	lenltd 11283	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦)) ↔ ¬ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
158	153, 155, 157	3bitr4d 311	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦))))
159	158	biimpa 476	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧))) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦)))
160	148, 159	syldan 592	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦)))
161	26	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℝ⁺)
162	161, 76	rpexpcld 14174	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ⁺)
163	162	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ⁺)
164	163	rpge0d 12957	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 0 ≤ (𝑁↑(𝑃 pCnt 𝑧)))
165	140, 141	addge01d 11729	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (0 ≤ (𝑁↑(𝑃 pCnt 𝑧)) ↔ (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
166	164, 165	mpbid 232	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
167	166	adantr 480	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
168	134, 136, 143, 160, 167	letrd 11294	. . . . . 6 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
169	156	adantr 480	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
170	141	adantr 480	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
171	142	adantr 480	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
172	126	adantr 480	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑃 ∈ ℙ)
173	73	ad2antrr 727	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑧 ∈ ℚ)
174	80	ad2antrr 727	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑦 ∈ ℚ)
175		simpr 484	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦))
176	172, 173, 174, 175	pcadd 16821	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑧 + 𝑦)))
177	92, 94	addcomd 11339	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 + 𝑧) = (𝑧 + 𝑦))
178	177	oveq2d 7376	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
179	178	ad2antrr 727	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
180	176, 179	breqtrrd 5127	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)))
181	149, 121, 132, 151	ltexp2rd 14175	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧) ↔ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
182	181	notbid 318	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧) ↔ ¬ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
183	122, 154	lenltd 11283	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ ¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧)))
184	156, 141	lenltd 11283	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧)) ↔ ¬ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
185	182, 183, 184	3bitr4d 311	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧))))
186	185	biimpa 476	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧))) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧)))
187	180, 186	syldan 592	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧)))
188	161, 71	rpexpcld 14174	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ⁺)
189	188	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ⁺)
190	189	rpge0d 12957	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 0 ≤ (𝑁↑(𝑃 pCnt 𝑦)))
191	141, 140	addge02d 11730	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (0 ≤ (𝑁↑(𝑃 pCnt 𝑦)) ↔ (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
192	190, 191	mpbid 232	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
193	192	adantr 480	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
194	169, 170, 171, 187, 193	letrd 11294	. . . . . 6 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
195	120, 122, 168, 194	lecasei 11243	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
196	118, 195	eqbrtrd 5121	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
197	188, 162	rpaddcld 12968	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ⁺)
198	197	rpge0d 12957	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 0 ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
199	116, 196, 198	pm2.61ne 3018	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
200		eqeq1 2741	. . . . . 6 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑥 = 0 ↔ (𝑦 + 𝑧) = 0))
201		oveq2 7368	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑃 pCnt 𝑥) = (𝑃 pCnt (𝑦 + 𝑧)))
202	201	oveq2d 7376	. . . . . 6 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
203	200, 202	ifbieq2d 4507	. . . . 5 ⊢ (𝑥 = (𝑦 + 𝑧) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
204		ovex 7393	. . . . . 6 ⊢ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ V
205	42, 204	ifex 4531	. . . . 5 ⊢ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ∈ V
206	203, 36, 205	fvmpt 6942	. . . 4 ⊢ ((𝑦 + 𝑧) ∈ ℚ → (𝐹‘(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
207	128, 206	syl 17	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
208	101, 112	oveq12d 7378	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝐹‘𝑦) + (𝐹‘𝑧)) = ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
209	199, 207, 208	3brtr4d 5131	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 + 𝑧)) ≤ ((𝐹‘𝑦) + (𝐹‘𝑧)))
210	2, 5, 9, 12, 14, 17, 37, 44, 64, 114, 209	isabvd 20749	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹 ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 Vcvv 3441 ifcif 4480 class class class wbr 5099 ↦ cmpt 5180 ‘cfv 6493 (class class class)co 7360 ℂcc 11028 ℝcr 11029 0cc0 11030 1c1 11031 + caddc 11033 · cmul 11035 < clt 11170 ≤ cle 11171 ℤcz 12492 ℚcq 12865 ℝ⁺crp 12909 (,)cioo 13265 ↑cexp 13988 ℙcprime 16602 pCnt cpc 16768 Basecbs 17140 ↾_s cress 17161 +_gcplusg 17181 ._rcmulr 17182 0_gc0g 17363 Ringcrg 20172 DivRingcdr 20666 AbsValcabv 20745 ℂ_fldccnfld 21313

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108 ax-addf 11109 ax-mulf 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-iun 4949 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-tpos 8170 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-er 8637 df-map 8769 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-sup 9349 df-inf 9350 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12150 df-2 12212 df-3 12213 df-4 12214 df-5 12215 df-6 12216 df-7 12217 df-8 12218 df-9 12219 df-n0 12406 df-z 12493 df-dec 12612 df-uz 12756 df-q 12866 df-rp 12910 df-ioo 13269 df-ico 13271 df-fz 13428 df-fl 13716 df-mod 13794 df-seq 13929 df-exp 13989 df-cj 15026 df-re 15027 df-im 15028 df-sqrt 15162 df-abs 15163 df-dvds 16184 df-gcd 16426 df-prm 16603 df-pc 16769 df-struct 17078 df-sets 17095 df-slot 17113 df-ndx 17125 df-base 17141 df-ress 17162 df-plusg 17194 df-mulr 17195 df-starv 17196 df-tset 17200 df-ple 17201 df-ds 17203 df-unif 17204 df-0g 17365 df-mgm 18569 df-sgrp 18648 df-mnd 18664 df-grp 18870 df-minusg 18871 df-subg 19057 df-cmn 19715 df-abl 19716 df-mgp 20080 df-rng 20092 df-ur 20121 df-ring 20174 df-cring 20175 df-oppr 20277 df-dvdsr 20297 df-unit 20298 df-invr 20328 df-dvr 20341 df-subrng 20483 df-subrg 20507 df-drng 20668 df-abv 20746 df-cnfld 21314

This theorem is referenced by: padicabvf 27602 padicabvcxp 27603

W3C validator