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 26778

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 26767	. . 3 ⊢ ℚ = (Base‘𝑄)
5	4	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → ℚ = (Base‘𝑄))
6		qex 12701	. . 3 ⊢ ℚ ∈ V
7		cnfldadd 20602	. . . 4 ⊢ + = (+_g‘ℂ_fld)
8	3, 7	ressplusg 17000	. . 3 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
9	6, 8	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → + = (+_g‘𝑄))
10		cnfldmul 20603	. . . 4 ⊢ · = (._r‘ℂ_fld)
11	3, 10	ressmulr 17017	. . 3 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
12	6, 11	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → · = (._r‘𝑄))
13	3	qrng0 26769	. . 3 ⊢ 0 = (0_g‘𝑄)
14	13	a1i 11	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 0 = (0_g‘𝑄))
15	3	qdrng 26768	. . 3 ⊢ 𝑄 ∈ DivRing
16		drngring 19998	. . 3 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
17	15, 16	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑄 ∈ Ring)
18		0red 10978	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ 𝑥 = 0) → 0 ∈ ℝ)
19		ioossre 13140	. . . . . . 7 ⊢ (0(,)1) ⊆ ℝ
20		simpr 485	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ (0(,)1))
21	19, 20	sselid 3919	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℝ)
22	21	ad2antrr 723	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → 𝑁 ∈ ℝ)
23		eliooord 13138	. . . . . . . . . 10 ⊢ (𝑁 ∈ (0(,)1) → (0 < 𝑁 ∧ 𝑁 < 1))
24	23	adantl 482	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → (0 < 𝑁 ∧ 𝑁 < 1))
25	24	simpld 495	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 0 < 𝑁)
26	21, 25	elrpd 12769	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℝ⁺)
27	26	rpne0d 12777	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ≠ 0)
28	27	ad2antrr 723	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → 𝑁 ≠ 0)
29		df-ne 2944	. . . . . 6 ⊢ (𝑥 ≠ 0 ↔ ¬ 𝑥 = 0)
30		pcqcl 16557	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℚ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ)
31	30	adantlr 712	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑥 ∈ ℚ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ)
32	31	anassrs 468	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ 𝑥 ≠ 0) → (𝑃 pCnt 𝑥) ∈ ℤ)
33	29, 32	sylan2br 595	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → (𝑃 pCnt 𝑥) ∈ ℤ)
34	22, 28, 33	reexpclzd 13964	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) ∧ ¬ 𝑥 = 0) → (𝑁↑(𝑃 pCnt 𝑥)) ∈ ℝ)
35	18, 34	ifclda 4494	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑥 ∈ ℚ) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) ∈ ℝ)
36		padic.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))))
37	35, 36	fmptd 6988	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹:ℚ⟶ℝ)
38		0z 12330	. . . 4 ⊢ 0 ∈ ℤ
39		zq 12694	. . . 4 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
40	38, 39	ax-mp 5	. . 3 ⊢ 0 ∈ ℚ
41		iftrue 4465	. . . 4 ⊢ (𝑥 = 0 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = 0)
42		c0ex 10969	. . . 4 ⊢ 0 ∈ V
43	41, 36, 42	fvmpt 6875	. . 3 ⊢ (0 ∈ ℚ → (𝐹‘0) = 0)
44	40, 43	mp1i 13	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → (𝐹‘0) = 0)
45	21	3ad2ant1 1132	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 𝑁 ∈ ℝ)
46		pcqcl 16557	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
47	46	adantlr 712	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
48	47	3impb 1114	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℤ)
49	25	3ad2ant1 1132	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < 𝑁)
50		expgt0 13816	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑃 pCnt 𝑦) ∈ ℤ ∧ 0 < 𝑁) → 0 < (𝑁↑(𝑃 pCnt 𝑦)))
51	45, 48, 49, 50	syl3anc 1370	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < (𝑁↑(𝑃 pCnt 𝑦)))
52		eqeq1 2742	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 0 ↔ 𝑦 = 0))
53		oveq2 7283	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑃 pCnt 𝑥) = (𝑃 pCnt 𝑦))
54	53	oveq2d 7291	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt 𝑦)))
55	52, 54	ifbieq2d 4485	. . . . . 6 ⊢ (𝑥 = 𝑦 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
56		ovex 7308	. . . . . . 7 ⊢ (𝑁↑(𝑃 pCnt 𝑦)) ∈ V
57	42, 56	ifex 4509	. . . . . 6 ⊢ if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) ∈ V
58	55, 36, 57	fvmpt 6875	. . . . 5 ⊢ (𝑦 ∈ ℚ → (𝐹‘𝑦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
59	58	3ad2ant2 1133	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝐹‘𝑦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
60		simp3 1137	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 𝑦 ≠ 0)
61	60	neneqd 2948	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → ¬ 𝑦 = 0)
62	61	iffalsed 4470	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) = (𝑁↑(𝑃 pCnt 𝑦)))
63	59, 62	eqtrd 2778	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
64	51, 63	breqtrrd 5102	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → 0 < (𝐹‘𝑦))
65		pcqmul 16554	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
66	65	3adant1r 1176	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
67	66	oveq2d 7291	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) = (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))))
68	21	recnd 11003	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 ∈ ℂ)
69	68	3ad2ant1 1132	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℂ)
70	27	3ad2ant1 1132	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ≠ 0)
71	47	3adant3 1131	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ)
72		simp1l 1196	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑃 ∈ ℙ)
73		simp3l 1200	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ∈ ℚ)
74		simp3r 1201	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ≠ 0)
75		pcqcl 16557	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℤ)
76	72, 73, 74, 75	syl12anc 834	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℤ)
77		expaddz 13827	. . . . 5 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑃 pCnt 𝑦) ∈ ℤ ∧ (𝑃 pCnt 𝑧) ∈ ℤ)) → (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
78	69, 70, 71, 76, 77	syl22anc 836	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
79	67, 78	eqtrd 2778	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
80		simp2l 1198	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ∈ ℚ)
81		qmulcl 12707	. . . . . 6 ⊢ ((𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝑦 · 𝑧) ∈ ℚ)
82	80, 73, 81	syl2anc 584	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 · 𝑧) ∈ ℚ)
83		eqeq1 2742	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 = 0 ↔ (𝑦 · 𝑧) = 0))
84		oveq2 7283	. . . . . . . 8 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑃 pCnt 𝑥) = (𝑃 pCnt (𝑦 · 𝑧)))
85	84	oveq2d 7291	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
86	83, 85	ifbieq2d 4485	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
87		ovex 7308	. . . . . . 7 ⊢ (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))) ∈ V
88	42, 87	ifex 4509	. . . . . 6 ⊢ if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))) ∈ V
89	86, 36, 88	fvmpt 6875	. . . . 5 ⊢ ((𝑦 · 𝑧) ∈ ℚ → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
90	82, 89	syl 17	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))))
91		qcn 12703	. . . . . . . 8 ⊢ (𝑦 ∈ ℚ → 𝑦 ∈ ℂ)
92	80, 91	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ∈ ℂ)
93		qcn 12703	. . . . . . . 8 ⊢ (𝑧 ∈ ℚ → 𝑧 ∈ ℂ)
94	73, 93	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑧 ∈ ℂ)
95		simp2r 1199	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑦 ≠ 0)
96	92, 94, 95, 74	mulne0d 11627	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 · 𝑧) ≠ 0)
97	96	neneqd 2948	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ¬ (𝑦 · 𝑧) = 0)
98	97	iffalsed 4470	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if((𝑦 · 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 · 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
99	90, 98	eqtrd 2778	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = (𝑁↑(𝑃 pCnt (𝑦 · 𝑧))))
100	63	3expb 1119	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
101	100	3adant3 1131	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑦) = (𝑁↑(𝑃 pCnt 𝑦)))
102		eqeq1 2742	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 0 ↔ 𝑧 = 0))
103		oveq2 7283	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑃 pCnt 𝑥) = (𝑃 pCnt 𝑧))
104	103	oveq2d 7291	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt 𝑧)))
105	102, 104	ifbieq2d 4485	. . . . . . 7 ⊢ (𝑥 = 𝑧 → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
106		ovex 7308	. . . . . . . 8 ⊢ (𝑁↑(𝑃 pCnt 𝑧)) ∈ V
107	42, 106	ifex 4509	. . . . . . 7 ⊢ if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) ∈ V
108	105, 36, 107	fvmpt 6875	. . . . . 6 ⊢ (𝑧 ∈ ℚ → (𝐹‘𝑧) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
109	73, 108	syl 17	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑧) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
110	74	neneqd 2948	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ¬ 𝑧 = 0)
111	110	iffalsed 4470	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) = (𝑁↑(𝑃 pCnt 𝑧)))
112	109, 111	eqtrd 2778	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘𝑧) = (𝑁↑(𝑃 pCnt 𝑧)))
113	101, 112	oveq12d 7293	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝐹‘𝑦) · (𝐹‘𝑧)) = ((𝑁↑(𝑃 pCnt 𝑦)) · (𝑁↑(𝑃 pCnt 𝑧))))
114	79, 99, 113	3eqtr4d 2788	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧)))
115		iftrue 4465	. . . . 5 ⊢ ((𝑦 + 𝑧) = 0 → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = 0)
116	115	breq1d 5084	. . . 4 ⊢ ((𝑦 + 𝑧) = 0 → (if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ↔ 0 ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
117		ifnefalse 4471	. . . . . 6 ⊢ ((𝑦 + 𝑧) ≠ 0 → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
118	117	adantl 482	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
119	71	adantr 481	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℤ)
120	119	zred 12426	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑦) ∈ ℝ)
121	76	adantr 481	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑧) ∈ ℤ)
122	121	zred 12426	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt 𝑧) ∈ ℝ)
123	21	3ad2ant1 1132	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℝ)
124	123	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑁 ∈ ℝ)
125	70	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑁 ≠ 0)
126	72	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑃 ∈ ℙ)
127		qaddcl 12705	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ) → (𝑦 + 𝑧) ∈ ℚ)
128	80, 73, 127	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 + 𝑧) ∈ ℚ)
129	128	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑦 + 𝑧) ∈ ℚ)
130		simpr 485	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑦 + 𝑧) ≠ 0)
131		pcqcl 16557	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ((𝑦 + 𝑧) ∈ ℚ ∧ (𝑦 + 𝑧) ≠ 0)) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
132	126, 129, 130, 131	syl12anc 834	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
133	132	adantr 481	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℤ)
134	124, 125, 133	reexpclzd 13964	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
135	119	adantr 481	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ∈ ℤ)
136	124, 125, 135	reexpclzd 13964	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
137		simpl1 1190	. . . . . . . . . . 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 13964	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
141	138, 139, 121	reexpclzd 13964	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
142	140, 141	readdcld 11004	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
143	142	adantr 481	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
144	126	adantr 481	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑃 ∈ ℙ)
145	80	ad2antrr 723	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑦 ∈ ℚ)
146	73	ad2antrr 723	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → 𝑧 ∈ ℚ)
147		simpr 485	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧))
148	144, 145, 146, 147	pcadd 16590	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)))
149	137, 26	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑁 ∈ ℝ⁺)
150	24	simprd 496	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝑁 < 1)
151	137, 150	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 𝑁 < 1)
152	149, 119, 132, 151	ltexp2rd 13963	. . . . . . . . . . 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 12426	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℝ)
155	120, 154	lenltd 11121	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑦) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ ¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦)))
156	138, 139, 132	reexpclzd 13964	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
157	156, 140	lenltd 11121	. . . . . . . . . 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 477	. . . . . . . 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 1132	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 𝑁 ∈ ℝ⁺)
162	161, 76	rpexpcld 13962	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ⁺)
163	162	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ⁺)
164	163	rpge0d 12776	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 0 ≤ (𝑁↑(𝑃 pCnt 𝑧)))
165	140, 141	addge01d 11563	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (0 ≤ (𝑁↑(𝑃 pCnt 𝑧)) ↔ (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
166	164, 165	mpbid 231	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
167	166	adantr 481	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt 𝑦)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
168	134, 136, 143, 160, 167	letrd 11132	. . . . . 6 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑦) ≤ (𝑃 pCnt 𝑧)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
169	156	adantr 481	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
170	141	adantr 481	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
171	142	adantr 481	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
172	126	adantr 481	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑃 ∈ ℙ)
173	73	ad2antrr 723	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑧 ∈ ℚ)
174	80	ad2antrr 723	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → 𝑦 ∈ ℚ)
175		simpr 485	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦))
176	172, 173, 174, 175	pcadd 16590	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑧 + 𝑦)))
177	92, 94	addcomd 11177	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑦 + 𝑧) = (𝑧 + 𝑦))
178	177	oveq2d 7291	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
179	178	ad2antrr 723	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
180	176, 179	breqtrrd 5102	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)))
181	149, 121, 132, 151	ltexp2rd 13963	. . . . . . . . . . 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 11121	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → ((𝑃 pCnt 𝑧) ≤ (𝑃 pCnt (𝑦 + 𝑧)) ↔ ¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧)))
184	156, 141	lenltd 11121	. . . . . . . . . 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 477	. . . . . . . 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 13962	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ⁺)
189	188	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ⁺)
190	189	rpge0d 12776	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → 0 ≤ (𝑁↑(𝑃 pCnt 𝑦)))
191	141, 140	addge02d 11564	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (0 ≤ (𝑁↑(𝑃 pCnt 𝑦)) ↔ (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
192	190, 191	mpbid 231	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
193	192	adantr 481	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt 𝑧)) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
194	169, 170, 171, 187, 193	letrd 11132	. . . . . 6 ⊢ (((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) ∧ (𝑃 pCnt 𝑧) ≤ (𝑃 pCnt 𝑦)) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
195	120, 122, 168, 194	lecasei 11081	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
196	118, 195	eqbrtrd 5096	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) ∧ (𝑦 + 𝑧) ≠ 0) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
197	188, 162	rpaddcld 12787	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ⁺)
198	197	rpge0d 12776	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → 0 ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
199	116, 196, 198	pm2.61ne 3030	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≤ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
200		eqeq1 2742	. . . . . 6 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑥 = 0 ↔ (𝑦 + 𝑧) = 0))
201		oveq2 7283	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑃 pCnt 𝑥) = (𝑃 pCnt (𝑦 + 𝑧)))
202	201	oveq2d 7291	. . . . . 6 ⊢ (𝑥 = (𝑦 + 𝑧) → (𝑁↑(𝑃 pCnt 𝑥)) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
203	200, 202	ifbieq2d 4485	. . . . 5 ⊢ (𝑥 = (𝑦 + 𝑧) → if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
204		ovex 7308	. . . . . 6 ⊢ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ V
205	42, 204	ifex 4509	. . . . 5 ⊢ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ∈ V
206	203, 36, 205	fvmpt 6875	. . . 4 ⊢ ((𝑦 + 𝑧) ∈ ℚ → (𝐹‘(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
207	128, 206	syl 17	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
208	101, 112	oveq12d 7293	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → ((𝐹‘𝑦) + (𝐹‘𝑧)) = ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
209	199, 207, 208	3brtr4d 5106	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) ∧ (𝑧 ∈ ℚ ∧ 𝑧 ≠ 0)) → (𝐹‘(𝑦 + 𝑧)) ≤ ((𝐹‘𝑦) + (𝐹‘𝑧)))
210	2, 5, 9, 12, 14, 17, 37, 44, 64, 114, 209	isabvd 20080	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹 ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 Vcvv 3432 ifcif 4459 class class class wbr 5074 ↦ cmpt 5157 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 < clt 11009 ≤ cle 11010 ℤcz 12319 ℚcq 12688 ℝ⁺crp 12730 (,)cioo 13079 ↑cexp 13782 ℙcprime 16376 pCnt cpc 16537 Basecbs 16912 ↾_s cress 16941 +_gcplusg 16962 ._rcmulr 16963 0_gc0g 17150 Ringcrg 19783 DivRingcdr 19991 AbsValcabv 20076 ℂ_fldccnfld 20597

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949 ax-addf 10950 ax-mulf 10951

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-tpos 8042 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-er 8498 df-map 8617 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-inf 9202 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-q 12689 df-rp 12731 df-ioo 13083 df-ico 13085 df-fz 13240 df-fl 13512 df-mod 13590 df-seq 13722 df-exp 13783 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-dvds 15964 df-gcd 16202 df-prm 16377 df-pc 16538 df-struct 16848 df-sets 16865 df-slot 16883 df-ndx 16895 df-base 16913 df-ress 16942 df-plusg 16975 df-mulr 16976 df-starv 16977 df-tset 16981 df-ple 16982 df-ds 16984 df-unif 16985 df-0g 17152 df-mgm 18326 df-sgrp 18375 df-mnd 18386 df-grp 18580 df-minusg 18581 df-subg 18752 df-cmn 19388 df-mgp 19721 df-ur 19738 df-ring 19785 df-cring 19786 df-oppr 19862 df-dvdsr 19883 df-unit 19884 df-invr 19914 df-dvr 19925 df-drng 19993 df-subrg 20022 df-abv 20077 df-cnfld 20598

This theorem is referenced by: padicabvf 26779 padicabvcxp 26780

W3C validator