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 27541

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 27530	. . 3 ⊢ ℚ = (Base‘𝑄)
5	4	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → ℚ = (Base‘𝑄))
6		qex 12920	. . 3 ⊢ ℚ ∈ V
7		cnfldadd 21270	. . . 4 ⊢ + = (+_g‘ℂ_fld)
8	3, 7	ressplusg 17254	. . 3 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
9	6, 8	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → + = (+_g‘𝑄))
10		cnfldmul 21272	. . . 4 ⊢ · = (._r‘ℂ_fld)
11	3, 10	ressmulr 17270	. . 3 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
12	6, 11	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → · = (._r‘𝑄))
13	3	qrng0 27532	. . 3 ⊢ 0 = (0_g‘𝑄)
14	13	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 0 = (0_g‘𝑄))
15	3	qdrng 27531	. . 3 ⊢ 𝑄 ∈ DivRing
16		drngring 20645	. . 3 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
17	15, 16	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑄 ∈ Ring)
18		0red 11177	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ 𝑥 = 0) → 0 ∈ ℝ)
19		ioossre 13368	. . . . . . 7 ⊢ (0(,)1) ⊆ ℝ
20		simpr 484	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ (0(,)1))
21	19, 20	sselid 3944	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℝ)
22	21	ad2antrr 726	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → 𝑁 ∈ ℝ)
23		eliooord 13366	. . . . . . . . . 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 12992	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℝ⁺)
27	26	rpne0d 13000	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ≠ 0)
28	27	ad2antrr 726	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → 𝑁 ≠ 0)
29		df-ne 2926	. . . . . 6 ⊢ (𝑥 ≠ 0 ↔ ¬ 𝑥 = 0)
30		pcqcl 16827	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℚ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ)
31	30	adantlr 715	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑥 ∈ ℚ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ)
32	31	anassrs 467	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ 𝑥 ≠ 0) → (𝑃 pCnt 𝑥) ∈ ℤ)
33	29, 32	sylan2br 595	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → (𝑃 pCnt 𝑥) ∈ ℤ)
34	22, 28, 33	reexpclzd 14214	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → (𝑁↑(𝑃 pCnt 𝑥)) ∈ ℝ)
35	18, 34	ifclda 4524	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) ∈ ℝ)
36		padic.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))))
37	35, 36	fmptd 7086	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹:ℚ⟶ℝ)
38		0z 12540	. . . 4 ⊢ 0 ∈ ℤ
39		zq 12913	. . . 4 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
40	38, 39	ax-mp 5	. . 3 ⊢ 0 ∈ ℚ
41		iftrue 4494	. . . 4 ⊢ (𝑥 = 0 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = 0)
42		c0ex 11168	. . . 4 ⊢ 0 ∈ V
43	41, 36, 42	fvmpt 6968	. . 3 ⊢ (0 ∈ ℚ → (𝐹‘0) = 0)
44	40, 43	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → (𝐹‘0) = 0)
45	21	3ad2ant1 1133	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 𝑁 ∈ ℝ)
46		pcqcl 16827	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
47	46	adantlr 715	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
48	47	3impb 1114	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℤ)
49	25	3ad2ant1 1133	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < 𝑁)
50		expgt0 14060	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑃 pCnt 𝑦) ∈ ℤ ∧ 0 < 𝑁) → 0 < (𝑁↑(𝑃 pCnt 𝑦)))
51	45, 48, 49, 50	syl3anc 1373	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < (𝑁↑(𝑃 pCnt 𝑦)))
52		eqeq1 2733	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 0 ↔ 𝑦 = 0))
53		oveq2 7395	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑃 pCnt 𝑥) = (𝑃 pCnt 𝑦))
54	53	oveq2d 7403	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt 𝑦)))
55	52, 54	ifbieq2d 4515	. . . . . 6 ⊢ (𝑥 = 𝑦 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
56		ovex 7420	. . . . . . 7 ⊢ (𝑁↑(𝑃 pCnt 𝑦)) ∈ V
57	42, 56	ifex 4539	. . . . . 6 ⊢ if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) ∈ V
58	55, 36, 57	fvmpt 6968	. . . . 5 ⊢ (𝑦 ∈ ℚ → (𝐹‘𝑦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
59	58	3ad2ant2 1134	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝐹‘𝑦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
60		simp3 1138	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 𝑦 ≠ 0)
61	60	neneqd 2930	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → ¬ 𝑦 = 0)
62	61	iffalsed 4499	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) = (𝑁↑(𝑃 pCnt 𝑦)))
63	59, 62	eqtrd 2764	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
64	51, 63	breqtrrd 5135	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < (𝐹‘𝑦))
65		pcqmul 16824	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
66	65	3adant1r 1178	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
67	66	oveq2d 7403	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) = (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))))
68	21	recnd 11202	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℂ)
69	68	3ad2ant1 1133	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℂ)
70	27	3ad2ant1 1133	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ≠ 0)
71	47	3adant3 1132	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
72		simp1l 1198	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑃 ∈ ℙ)
73		simp3l 1202	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ∈ ℚ)
74		simp3r 1203	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ≠ 0)
75		pcqcl 16827	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℤ)
76	72, 73, 74, 75	syl12anc 836	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℤ)
77		expaddz 14071	. . . . 5 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑃 pCnt 𝑦) ∈ ℤ ∧ (𝑃 pCnt 𝑧) ∈ ℤ)) → (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
78	69, 70, 71, 76, 77	syl22anc 838	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
79	67, 78	eqtrd 2764	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
80		simp2l 1200	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ∈ ℚ)
81		qmulcl 12926	. . . . . 6 ⊢ ((𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝑦 · 𝑧) ∈ ℚ)
82	80, 73, 81	syl2anc 584	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 · 𝑧) ∈ ℚ)
83		eqeq1 2733	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 = 0 ↔ (𝑦 · 𝑧) = 0))
84		oveq2 7395	. . . . . . . 8 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑃 pCnt 𝑥) = (𝑃 pCnt (𝑦 · 𝑧)))
85	84	oveq2d 7403	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
86	83, 85	ifbieq2d 4515	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
87		ovex 7420	. . . . . . 7 ⊢ (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) ∈ V
88	42, 87	ifex 4539	. . . . . 6 ⊢ if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))) ∈ V
89	86, 36, 88	fvmpt 6968	. . . . 5 ⊢ ((𝑦 · 𝑧) ∈ ℚ → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
90	82, 89	syl 17	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
91		qcn 12922	. . . . . . . 8 ⊢ (𝑦 ∈ ℚ → 𝑦 ∈ ℂ)
92	80, 91	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ∈ ℂ)
93		qcn 12922	. . . . . . . 8 ⊢ (𝑧 ∈ ℚ → 𝑧 ∈ ℂ)
94	73, 93	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ∈ ℂ)
95		simp2r 1201	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ≠ 0)
96	92, 94, 95, 74	mulne0d 11830	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 · 𝑧) ≠ 0)
97	96	neneqd 2930	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ¬ (𝑦 · 𝑧) = 0)
98	97	iffalsed 4499	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
99	90, 98	eqtrd 2764	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
100	63	3expb 1120	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
101	100	3adant3 1132	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
102		eqeq1 2733	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 0 ↔ 𝑧 = 0))
103		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑃 pCnt 𝑥) = (𝑃 pCnt 𝑧))
104	103	oveq2d 7403	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt 𝑧)))
105	102, 104	ifbieq2d 4515	. . . . . . 7 ⊢ (𝑥 = 𝑧 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
106		ovex 7420	. . . . . . . 8 ⊢ (𝑁↑(𝑃 pCnt 𝑧)) ∈ V
107	42, 106	ifex 4539	. . . . . . 7 ⊢ if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) ∈ V
108	105, 36, 107	fvmpt 6968	. . . . . 6 ⊢ (𝑧 ∈ ℚ → (𝐹‘𝑧) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
109	73, 108	syl 17	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑧) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
110	74	neneqd 2930	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ¬ 𝑧 = 0)
111	110	iffalsed 4499	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) = (𝑁↑(𝑃 pCnt 𝑧)))
112	109, 111	eqtrd 2764	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑧) = (𝑁↑(𝑃 pCnt 𝑧)))
113	101, 112	oveq12d 7405	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝐹‘𝑦) · (𝐹‘𝑧)) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
114	79, 99, 113	3eqtr4d 2774	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧)))
115		iftrue 4494	. . . . 5 ⊢ ((𝑦 + 𝑧) = 0 → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = 0)
116	115	breq1d 5117	. . . 4 ⊢ ((𝑦 + 𝑧) = 0 → (if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ↔ 0 ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
117		ifnefalse 4500	. . . . . 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 12638	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℝ)
121	76	adantr 480	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑧) ∈ ℤ)
122	121	zred 12638	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑧) ∈ ℝ)
123	21	3ad2ant1 1133	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℝ)
124	123	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑁 ∈ ℝ)
125	70	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑁 ≠ 0)
126	72	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑃 ∈ ℙ)
127		qaddcl 12924	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝑦 + 𝑧) ∈ ℚ)
128	80, 73, 127	syl2anc 584	. . . . . . . . . . 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 16827	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ((𝑦 + 𝑧) ∈ ℚ ∧ (𝑦 + 𝑧) ≠ 0)) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
132	126, 129, 130, 131	syl12anc 836	. . . . . . . . 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 14214	. . . . . . 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 14214	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
137		simpl1 1192	. . . . . . . . . . 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 14214	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
141	138, 139, 121	reexpclzd 14214	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
142	140, 141	readdcld 11203	. . . . . . . 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 726	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑦 ∈ ℚ)
146	73	ad2antrr 726	. . . . . . . . 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 16860	. . . . . . . 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 14213	. . . . . . . . . . 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 12638	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℝ)
155	120, 154	lenltd 11320	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ ¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦)))
156	138, 139, 132	reexpclzd 14214	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
157	156, 140	lenltd 11320	. . . . . . . . . 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 591	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑦)))
161	26	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℝ⁺)
162	161, 76	rpexpcld 14212	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ⁺)
163	162	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ⁺)
164	163	rpge0d 12999	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 0 ≤ (𝑁↑(𝑃 pCnt 𝑧)))
165	140, 141	addge01d 11766	. . . . . . . . 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 11331	. . . . . 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 726	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑧 ∈ ℚ)
174	80	ad2antrr 726	. . . . . . . . . 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 16860	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑧 + 𝑦)))
177	92, 94	addcomd 11376	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 + 𝑧) = (𝑧 + 𝑦))
178	177	oveq2d 7403	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
179	178	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
180	176, 179	breqtrrd 5135	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)))
181	149, 121, 132, 151	ltexp2rd 14213	. . . . . . . . . . 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 11320	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ ¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧)))
184	156, 141	lenltd 11320	. . . . . . . . . 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 591	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ (𝑁↑(𝑃 pCnt 𝑧)))
188	161, 71	rpexpcld 14212	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ⁺)
189	188	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ⁺)
190	189	rpge0d 12999	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 0 ≤ (𝑁↑(𝑃 pCnt 𝑦)))
191	141, 140	addge02d 11767	. . . . . . . . 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 11331	. . . . . 6 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
195	120, 122, 168, 194	lecasei 11280	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
196	118, 195	eqbrtrd 5129	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
197	188, 162	rpaddcld 13010	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ⁺)
198	197	rpge0d 12999	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 0 ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
199	116, 196, 198	pm2.61ne 3010	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
200		eqeq1 2733	. . . . . 6 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑥 = 0 ↔ (𝑦 + 𝑧) = 0))
201		oveq2 7395	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑃 pCnt 𝑥) = (𝑃 pCnt (𝑦 + 𝑧)))
202	201	oveq2d 7403	. . . . . 6 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
203	200, 202	ifbieq2d 4515	. . . . 5 ⊢ (𝑥 = (𝑦 + 𝑧) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
204		ovex 7420	. . . . . 6 ⊢ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ V
205	42, 204	ifex 4539	. . . . 5 ⊢ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ∈ V
206	203, 36, 205	fvmpt 6968	. . . 4 ⊢ ((𝑦 + 𝑧) ∈ ℚ → (𝐹‘(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
207	128, 206	syl 17	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
208	101, 112	oveq12d 7405	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝐹‘𝑦) + (𝐹‘𝑧)) = ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
209	199, 207, 208	3brtr4d 5139	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 + 𝑧)) ≤ ((𝐹‘𝑦) + (𝐹‘𝑧)))
210	2, 5, 9, 12, 14, 17, 37, 44, 64, 114, 209	isabvd 20721	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹 ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 Vcvv 3447 ifcif 4488 class class class wbr 5107 ↦ cmpt 5188 ‘cfv 6511 (class class class)co 7387 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 < clt 11208 ≤ cle 11209 ℤcz 12529 ℚcq 12907 ℝ⁺crp 12951 (,)cioo 13306 ↑cexp 14026 ℙcprime 16641 pCnt cpc 16807 Basecbs 17179 ↾_s cress 17200 +_gcplusg 17220 ._rcmulr 17221 0_gc0g 17402 Ringcrg 20142 DivRingcdr 20638 AbsValcabv 20717 ℂ_fldccnfld 21264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147 ax-mulf 11148

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-tpos 8205 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-sup 9393 df-inf 9394 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-ioo 13310 df-ico 13312 df-fz 13469 df-fl 13754 df-mod 13832 df-seq 13967 df-exp 14027 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-dvds 16223 df-gcd 16465 df-prm 16642 df-pc 16808 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-0g 17404 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-grp 18868 df-minusg 18869 df-subg 19055 df-cmn 19712 df-abl 19713 df-mgp 20050 df-rng 20062 df-ur 20091 df-ring 20144 df-cring 20145 df-oppr 20246 df-dvdsr 20266 df-unit 20267 df-invr 20297 df-dvr 20310 df-subrng 20455 df-subrg 20479 df-drng 20640 df-abv 20718 df-cnfld 21265

This theorem is referenced by: padicabvf 27542 padicabvcxp 27543

W3C validator