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 27615

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 27604	. . 3 ⊢ ℚ = (Base‘𝑄)
5	4	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → ℚ = (Base‘𝑄))
6		qex 12906	. . 3 ⊢ ℚ ∈ V
7		cnfldadd 21357	. . . 4 ⊢ + = (+_g‘ℂ_fld)
8	3, 7	ressplusg 17249	. . 3 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
9	6, 8	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → + = (+_g‘𝑄))
10		cnfldmul 21359	. . . 4 ⊢ · = (._r‘ℂ_fld)
11	3, 10	ressmulr 17265	. . 3 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
12	6, 11	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → · = (._r‘𝑄))
13	3	qrng0 27606	. . 3 ⊢ 0 = (0_g‘𝑄)
14	13	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 0 = (0_g‘𝑄))
15	3	qdrng 27605	. . 3 ⊢ 𝑄 ∈ DivRing
16		drngring 20712	. . 3 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
17	15, 16	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑄 ∈ Ring)
18		0red 11142	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ 𝑥 = 0) → 0 ∈ ℝ)
19		ioossre 13355	. . . . . . 7 ⊢ (0(,)1) ⊆ ℝ
20		simpr 486	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ (0(,)1))
21	19, 20	sselid 3915	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℝ)
22	21	ad2antrr 733	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → 𝑁 ∈ ℝ)
23		eliooord 13353	. . . . . . . . . 10 ⊢ (𝑁 ∈ (0(,)1) → (0 < 𝑁 ∧ 𝑁 < 1))
24	23	adantl 483	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → (0 < 𝑁 ∧ 𝑁 < 1))
25	24	simpld 496	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 0 < 𝑁)
26	21, 25	elrpd 12978	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℝ⁺)
27	26	rpne0d 12986	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ≠ 0)
28	27	ad2antrr 733	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → 𝑁 ≠ 0)
29		df-ne 2937	. . . . . 6 ⊢ (𝑥 ≠ 0 ↔ ¬ 𝑥 = 0)
30		pcqcl 16822	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℚ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ)
31	30	adantlr 722	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑥 ∈ ℚ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ)
32	31	anassrs 469	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ 𝑥 ≠ 0) → (𝑃 pCnt 𝑥) ∈ ℤ)
33	29, 32	sylan2br 602	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → (𝑃 pCnt 𝑥) ∈ ℤ)
34	22, 28, 33	reexpclzd 14206	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → (𝑁↑(𝑃 pCnt 𝑥)) ∈ ℝ)
35	18, 34	ifclda 4493	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) ∈ ℝ)
36		padic.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))))
37	35, 36	fmptd 7059	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹:ℚ⟶ℝ)
38		0z 12530	. . . 4 ⊢ 0 ∈ ℤ
39		zq 12899	. . . 4 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
40	38, 39	ax-mp 5	. . 3 ⊢ 0 ∈ ℚ
41		iftrue 4463	. . . 4 ⊢ (𝑥 = 0 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = 0)
42		c0ex 11133	. . . 4 ⊢ 0 ∈ V
43	41, 36, 42	fvmpt 6939	. . 3 ⊢ (0 ∈ ℚ → (𝐹‘0) = 0)
44	40, 43	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → (𝐹‘0) = 0)
45	21	3ad2ant1 1140	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 𝑁 ∈ ℝ)
46		pcqcl 16822	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
47	46	adantlr 722	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
48	47	3impb 1121	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℤ)
49	25	3ad2ant1 1140	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < 𝑁)
50		expgt0 14052	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑃 pCnt 𝑦) ∈ ℤ ∧ 0 < 𝑁) → 0 < (𝑁↑(𝑃 pCnt 𝑦)))
51	45, 48, 49, 50	syl3anc 1380	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < (𝑁↑(𝑃 pCnt 𝑦)))
52		eqeq1 2745	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 0 ↔ 𝑦 = 0))
53		oveq2 7368	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑃 pCnt 𝑥) = (𝑃 pCnt 𝑦))
54	53	oveq2d 7376	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt 𝑦)))
55	52, 54	ifbieq2d 4484	. . . . . 6 ⊢ (𝑥 = 𝑦 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
56		ovex 7393	. . . . . . 7 ⊢ (𝑁↑(𝑃 pCnt 𝑦)) ∈ V
57	42, 56	ifex 4508	. . . . . 6 ⊢ if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) ∈ V
58	55, 36, 57	fvmpt 6939	. . . . 5 ⊢ (𝑦 ∈ ℚ → (𝐹‘𝑦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
59	58	3ad2ant2 1141	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝐹‘𝑦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
60		simp3 1145	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 𝑦 ≠ 0)
61	60	neneqd 2941	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → ¬ 𝑦 = 0)
62	61	iffalsed 4468	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) = (𝑁↑(𝑃 pCnt 𝑦)))
63	59, 62	eqtrd 2776	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
64	51, 63	breqtrrd 5103	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < (𝐹‘𝑦))
65		pcqmul 16819	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
66	65	3adant1r 1185	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
67	66	oveq2d 7376	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) = (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))))
68	21	recnd 11168	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℂ)
69	68	3ad2ant1 1140	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℂ)
70	27	3ad2ant1 1140	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ≠ 0)
71	47	3adant3 1139	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
72		simp1l 1205	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑃 ∈ ℙ)
73		simp3l 1209	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ∈ ℚ)
74		simp3r 1210	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ≠ 0)
75		pcqcl 16822	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℤ)
76	72, 73, 74, 75	syl12anc 843	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℤ)
77		expaddz 14063	. . . . 5 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑃 pCnt 𝑦) ∈ ℤ ∧ (𝑃 pCnt 𝑧) ∈ ℤ)) → (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
78	69, 70, 71, 76, 77	syl22anc 845	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
79	67, 78	eqtrd 2776	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
80		simp2l 1207	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ∈ ℚ)
81		qmulcl 12912	. . . . . 6 ⊢ ((𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝑦 · 𝑧) ∈ ℚ)
82	80, 73, 81	syl2anc 591	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 · 𝑧) ∈ ℚ)
83		eqeq1 2745	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 = 0 ↔ (𝑦 · 𝑧) = 0))
84		oveq2 7368	. . . . . . . 8 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑃 pCnt 𝑥) = (𝑃 pCnt (𝑦 · 𝑧)))
85	84	oveq2d 7376	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
86	83, 85	ifbieq2d 4484	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
87		ovex 7393	. . . . . . 7 ⊢ (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) ∈ V
88	42, 87	ifex 4508	. . . . . 6 ⊢ if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))) ∈ V
89	86, 36, 88	fvmpt 6939	. . . . 5 ⊢ ((𝑦 · 𝑧) ∈ ℚ → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
90	82, 89	syl 17	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
91		qcn 12908	. . . . . . . 8 ⊢ (𝑦 ∈ ℚ → 𝑦 ∈ ℂ)
92	80, 91	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ∈ ℂ)
93		qcn 12908	. . . . . . . 8 ⊢ (𝑧 ∈ ℚ → 𝑧 ∈ ℂ)
94	73, 93	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ∈ ℂ)
95		simp2r 1208	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ≠ 0)
96	92, 94, 95, 74	mulne0d 11797	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 · 𝑧) ≠ 0)
97	96	neneqd 2941	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ¬ (𝑦 · 𝑧) = 0)
98	97	iffalsed 4468	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
99	90, 98	eqtrd 2776	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
100	63	3expb 1127	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
101	100	3adant3 1139	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
102		eqeq1 2745	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 0 ↔ 𝑧 = 0))
103		oveq2 7368	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑃 pCnt 𝑥) = (𝑃 pCnt 𝑧))
104	103	oveq2d 7376	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt 𝑧)))
105	102, 104	ifbieq2d 4484	. . . . . . 7 ⊢ (𝑥 = 𝑧 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
106		ovex 7393	. . . . . . . 8 ⊢ (𝑁↑(𝑃 pCnt 𝑧)) ∈ V
107	42, 106	ifex 4508	. . . . . . 7 ⊢ if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) ∈ V
108	105, 36, 107	fvmpt 6939	. . . . . 6 ⊢ (𝑧 ∈ ℚ → (𝐹‘𝑧) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
109	73, 108	syl 17	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑧) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
110	74	neneqd 2941	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ¬ 𝑧 = 0)
111	110	iffalsed 4468	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) = (𝑁↑(𝑃 pCnt 𝑧)))
112	109, 111	eqtrd 2776	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑧) = (𝑁↑(𝑃 pCnt 𝑧)))
113	101, 112	oveq12d 7378	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝐹‘𝑦) · (𝐹‘𝑧)) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
114	79, 99, 113	3eqtr4d 2786	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧)))
115		iftrue 4463	. . . . 5 ⊢ ((𝑦 + 𝑧) = 0 → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = 0)
116	115	breq1d 5085	. . . 4 ⊢ ((𝑦 + 𝑧) = 0 → (if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ↔ 0 ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
117		ifnefalse 4469	. . . . . 6 ⊢ ((𝑦 + 𝑧) ≠ 0 → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
118	117	adantl 483	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
119	71	adantr 482	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℤ)
120	119	zred 12628	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℝ)
121	76	adantr 482	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑧) ∈ ℤ)
122	121	zred 12628	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑧) ∈ ℝ)
123	21	3ad2ant1 1140	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℝ)
124	123	ad2antrr 733	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑁 ∈ ℝ)
125	70	ad2antrr 733	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑁 ≠ 0)
126	72	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑃 ∈ ℙ)
127		qaddcl 12910	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝑦 + 𝑧) ∈ ℚ)
128	80, 73, 127	syl2anc 591	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 + 𝑧) ∈ ℚ)
129	128	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑦 + 𝑧) ∈ ℚ)
130		simpr 486	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑦 + 𝑧) ≠ 0)
131		pcqcl 16822	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ((𝑦 + 𝑧) ∈ ℚ ∧ (𝑦 + 𝑧) ≠ 0)) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
132	126, 129, 130, 131	syl12anc 843	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
133	132	adantr 482	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
134	124, 125, 133	reexpclzd 14206	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
135	119	adantr 482	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ∈ ℤ)
136	124, 125, 135	reexpclzd 14206	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
137		simpl1 1199	. . . . . . . . . . 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 14206	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
141	138, 139, 121	reexpclzd 14206	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
142	140, 141	readdcld 11169	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
143	142	adantr 482	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
144	126	adantr 482	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑃 ∈ ℙ)
145	80	ad2antrr 733	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑦 ∈ ℚ)
146	73	ad2antrr 733	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑧 ∈ ℚ)
147		simpr 486	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧))
148	144, 145, 146, 147	pcadd 16855	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)))
149	137, 26	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑁 ∈ ℝ⁺)
150	24	simprd 497	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 < 1)
151	137, 150	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑁 < 1)
152	149, 119, 132, 151	ltexp2rd 14205	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦) ↔ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
153	152	notbid 320	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦) ↔ ¬ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
154	132	zred 12628	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℝ)
155	120, 154	lenltd 11287	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ ¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦)))
156	138, 139, 132	reexpclzd 14206	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
157	156, 140	lenltd 11287	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦)) ↔ ¬ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
158	153, 155, 157	3bitr4d 313	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦))))
159	158	biimpa 478	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧))) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦)))
160	148, 159	syldan 598	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦)))
161	26	3ad2ant1 1140	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℝ⁺)
162	161, 76	rpexpcld 14204	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ⁺)
163	162	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ⁺)
164	163	rpge0d 12985	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 0 ≤ (𝑁↑(𝑃 pCnt 𝑧)))
165	140, 141	addge01d 11733	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (0 ≤ (𝑁↑(𝑃 pCnt 𝑧)) ↔ (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
166	164, 165	mpbid 234	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
167	166	adantr 482	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
168	134, 136, 143, 160, 167	letrd 11298	. . . . . 6 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
169	156	adantr 482	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
170	141	adantr 482	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
171	142	adantr 482	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
172	126	adantr 482	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑃 ∈ ℙ)
173	73	ad2antrr 733	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑧 ∈ ℚ)
174	80	ad2antrr 733	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑦 ∈ ℚ)
175		simpr 486	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦))
176	172, 173, 174, 175	pcadd 16855	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑧 + 𝑦)))
177	92, 94	addcomd 11343	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 + 𝑧) = (𝑧 + 𝑦))
178	177	oveq2d 7376	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
179	178	ad2antrr 733	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
180	176, 179	breqtrrd 5103	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)))
181	149, 121, 132, 151	ltexp2rd 14205	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧) ↔ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
182	181	notbid 320	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧) ↔ ¬ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
183	122, 154	lenltd 11287	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ ¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧)))
184	156, 141	lenltd 11287	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧)) ↔ ¬ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
185	182, 183, 184	3bitr4d 313	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧))))
186	185	biimpa 478	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧))) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧)))
187	180, 186	syldan 598	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧)))
188	161, 71	rpexpcld 14204	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ⁺)
189	188	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ⁺)
190	189	rpge0d 12985	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 0 ≤ (𝑁↑(𝑃 pCnt 𝑦)))
191	141, 140	addge02d 11734	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (0 ≤ (𝑁↑(𝑃 pCnt 𝑦)) ↔ (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
192	190, 191	mpbid 234	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
193	192	adantr 482	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
194	169, 170, 171, 187, 193	letrd 11298	. . . . . 6 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
195	120, 122, 168, 194	lecasei 11247	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
196	118, 195	eqbrtrd 5097	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
197	188, 162	rpaddcld 12996	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ⁺)
198	197	rpge0d 12985	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 0 ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
199	116, 196, 198	pm2.61ne 3021	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
200		eqeq1 2745	. . . . . 6 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑥 = 0 ↔ (𝑦 + 𝑧) = 0))
201		oveq2 7368	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑃 pCnt 𝑥) = (𝑃 pCnt (𝑦 + 𝑧)))
202	201	oveq2d 7376	. . . . . 6 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
203	200, 202	ifbieq2d 4484	. . . . 5 ⊢ (𝑥 = (𝑦 + 𝑧) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
204		ovex 7393	. . . . . 6 ⊢ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ V
205	42, 204	ifex 4508	. . . . 5 ⊢ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ∈ V
206	203, 36, 205	fvmpt 6939	. . . 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 5107	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 + 𝑧)) ≤ ((𝐹‘𝑦) + (𝐹‘𝑧)))
210	2, 5, 9, 12, 14, 17, 37, 44, 64, 114, 209	isabvd 20788	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹 ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 Vcvv 3433 ifcif 4457 class class class wbr 5075 ↦ cmpt 5156 ‘cfv 6489 (class class class)co 7360 ℂcc 11031 ℝcr 11032 0cc0 11033 1c1 11034 + caddc 11036 · cmul 11038 < clt 11174 ≤ cle 11175 ℤcz 12519 ℚcq 12893 ℝ⁺crp 12937 (,)cioo 13293 ↑cexp 14018 ℙcprime 16635 pCnt cpc 16802 Basecbs 17174 ↾_s cress 17195 +_gcplusg 17215 ._rcmulr 17216 0_gc0g 17397 Ringcrg 20209 DivRingcdr 20705 AbsValcabv 20784 ℂ_fldccnfld 21351

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111 ax-addf 11112 ax-mulf 11113

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4842 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 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 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-7 12244 df-8 12245 df-9 12246 df-n0 12433 df-z 12520 df-dec 12640 df-uz 12784 df-q 12894 df-rp 12938 df-ioo 13297 df-ico 13299 df-fz 13457 df-fl 13746 df-mod 13824 df-seq 13959 df-exp 14019 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-dvds 16217 df-gcd 16459 df-prm 16636 df-pc 16803 df-struct 17112 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-starv 17230 df-tset 17234 df-ple 17235 df-ds 17237 df-unif 17238 df-0g 17399 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-grp 18907 df-minusg 18908 df-subg 19094 df-cmn 19752 df-abl 19753 df-mgp 20117 df-rng 20129 df-ur 20158 df-ring 20211 df-cring 20212 df-oppr 20312 df-dvdsr 20332 df-unit 20333 df-invr 20363 df-dvr 20376 df-subrng 20522 df-subrg 20546 df-drng 20707 df-abv 20785 df-cnfld 21352

This theorem is referenced by: padicabvf 27616 padicabvcxp 27617

W3C validator