MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  padicabv Structured version   Visualization version   GIF version
Theorem padicabv 27123
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.
StepHypRef Expression
1 qabsabv.a . . 3 𝐴 = (AbsValβ€˜π‘„)
21a1i 11 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝐴 = (AbsValβ€˜π‘„))
3 qrng.q . . . 4 𝑄 = (β„‚fld β†Ύs β„š)
43qrngbas 27112 . . 3 β„š = (Baseβ€˜π‘„)
54a1i 11 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ β„š = (Baseβ€˜π‘„))
6 qex 12942 . . 3 β„š ∈ V
7 cnfldadd 20942 . . . 4 + = (+gβ€˜β„‚fld)
83, 7ressplusg 17232 . . 3 (β„š ∈ V β†’ + = (+gβ€˜π‘„))
96, 8mp1i 13 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ + = (+gβ€˜π‘„))
10 cnfldmul 20943 . . . 4 Β· = (.rβ€˜β„‚fld)
113, 10ressmulr 17249 . . 3 (β„š ∈ V β†’ Β· = (.rβ€˜π‘„))
126, 11mp1i 13 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ Β· = (.rβ€˜π‘„))
133qrng0 27114 . . 3 0 = (0gβ€˜π‘„)
1413a1i 11 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 0 = (0gβ€˜π‘„))
153qdrng 27113 . . 3 𝑄 ∈ DivRing
16 drngring 20315 . . 3 (𝑄 ∈ DivRing β†’ 𝑄 ∈ Ring)
1715, 16mp1i 13 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑄 ∈ Ring)
18 0red 11214 . . . 4 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ π‘₯ = 0) β†’ 0 ∈ ℝ)
19 ioossre 13382 . . . . . . 7 (0(,)1) βŠ† ℝ
20 simpr 486 . . . . . . 7 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 ∈ (0(,)1))
2119, 20sselid 3980 . . . . . 6 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 ∈ ℝ)
2221ad2antrr 725 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ Β¬ π‘₯ = 0) β†’ 𝑁 ∈ ℝ)
23 eliooord 13380 . . . . . . . . . 10 (𝑁 ∈ (0(,)1) β†’ (0 < 𝑁 ∧ 𝑁 < 1))
2423adantl 483 . . . . . . . . 9 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ (0 < 𝑁 ∧ 𝑁 < 1))
2524simpld 496 . . . . . . . 8 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 0 < 𝑁)
2621, 25elrpd 13010 . . . . . . 7 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 ∈ ℝ+)
2726rpne0d 13018 . . . . . 6 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 β‰  0)
2827ad2antrr 725 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ Β¬ π‘₯ = 0) β†’ 𝑁 β‰  0)
29 df-ne 2942 . . . . . 6 (π‘₯ β‰  0 ↔ Β¬ π‘₯ = 0)
30 pcqcl 16786 . . . . . . . 8 ((𝑃 ∈ β„™ ∧ (π‘₯ ∈ β„š ∧ π‘₯ β‰  0)) β†’ (𝑃 pCnt π‘₯) ∈ β„€)
3130adantlr 714 . . . . . . 7 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (π‘₯ ∈ β„š ∧ π‘₯ β‰  0)) β†’ (𝑃 pCnt π‘₯) ∈ β„€)
3231anassrs 469 . . . . . 6 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ π‘₯ β‰  0) β†’ (𝑃 pCnt π‘₯) ∈ β„€)
3329, 32sylan2br 596 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ Β¬ π‘₯ = 0) β†’ (𝑃 pCnt π‘₯) ∈ β„€)
3422, 28, 33reexpclzd 14209 . . . 4 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ Β¬ π‘₯ = 0) β†’ (𝑁↑(𝑃 pCnt π‘₯)) ∈ ℝ)
3518, 34ifclda 4563 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) ∈ ℝ)
36 padic.f . . 3 𝐹 = (π‘₯ ∈ β„š ↦ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))))
3735, 36fmptd 7111 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝐹:β„šβŸΆβ„)
38 0z 12566 . . . 4 0 ∈ β„€
39 zq 12935 . . . 4 (0 ∈ β„€ β†’ 0 ∈ β„š)
4038, 39ax-mp 5 . . 3 0 ∈ β„š
41 iftrue 4534 . . . 4 (π‘₯ = 0 β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = 0)
42 c0ex 11205 . . . 4 0 ∈ V
4341, 36, 42fvmpt 6996 . . 3 (0 ∈ β„š β†’ (πΉβ€˜0) = 0)
4440, 43mp1i 13 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ (πΉβ€˜0) = 0)
45213ad2ant1 1134 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 𝑁 ∈ ℝ)
46 pcqcl 16786 . . . . . 6 ((𝑃 ∈ β„™ ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0)) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
4746adantlr 714 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0)) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
48473impb 1116 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
49253ad2ant1 1134 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 0 < 𝑁)
50 expgt0 14058 . . . 4 ((𝑁 ∈ ℝ ∧ (𝑃 pCnt 𝑦) ∈ β„€ ∧ 0 < 𝑁) β†’ 0 < (𝑁↑(𝑃 pCnt 𝑦)))
5145, 48, 49, 50syl3anc 1372 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 0 < (𝑁↑(𝑃 pCnt 𝑦)))
52 eqeq1 2737 . . . . . . 7 (π‘₯ = 𝑦 β†’ (π‘₯ = 0 ↔ 𝑦 = 0))
53 oveq2 7414 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (𝑃 pCnt π‘₯) = (𝑃 pCnt 𝑦))
5453oveq2d 7422 . . . . . . 7 (π‘₯ = 𝑦 β†’ (𝑁↑(𝑃 pCnt π‘₯)) = (𝑁↑(𝑃 pCnt 𝑦)))
5552, 54ifbieq2d 4554 . . . . . 6 (π‘₯ = 𝑦 β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
56 ovex 7439 . . . . . . 7 (𝑁↑(𝑃 pCnt 𝑦)) ∈ V
5742, 56ifex 4578 . . . . . 6 if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) ∈ V
5855, 36, 57fvmpt 6996 . . . . 5 (𝑦 ∈ β„š β†’ (πΉβ€˜π‘¦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
59583ad2ant2 1135 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ (πΉβ€˜π‘¦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
60 simp3 1139 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 𝑦 β‰  0)
6160neneqd 2946 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ Β¬ 𝑦 = 0)
6261iffalsed 4539 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) = (𝑁↑(𝑃 pCnt 𝑦)))
6359, 62eqtrd 2773 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ (πΉβ€˜π‘¦) = (𝑁↑(𝑃 pCnt 𝑦)))
6451, 63breqtrrd 5176 . 2 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 0 < (πΉβ€˜π‘¦))
65 pcqmul 16783 . . . . . 6 ((𝑃 ∈ β„™ ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt (𝑦 Β· 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
66653adant1r 1178 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt (𝑦 Β· 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
6766oveq2d 7422 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))) = (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))))
6821recnd 11239 . . . . . 6 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 ∈ β„‚)
69683ad2ant1 1134 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑁 ∈ β„‚)
70273ad2ant1 1134 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑁 β‰  0)
71473adant3 1133 . . . . 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 16786 . . . . . 6 ((𝑃 ∈ β„™ ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt 𝑧) ∈ β„€)
7672, 73, 74, 75syl12anc 836 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt 𝑧) ∈ β„€)
77 expaddz 14069 . . . . 5 (((𝑁 ∈ β„‚ ∧ 𝑁 β‰  0) ∧ ((𝑃 pCnt 𝑦) ∈ β„€ ∧ (𝑃 pCnt 𝑧) ∈ β„€)) β†’ (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) Β· (𝑁↑(𝑃 pCnt 𝑧))))
7869, 70, 71, 76, 77syl22anc 838 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) Β· (𝑁↑(𝑃 pCnt 𝑧))))
7967, 78eqtrd 2773 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) Β· (𝑁↑(𝑃 pCnt 𝑧))))
80 simp2l 1200 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑦 ∈ β„š)
81 qmulcl 12948 . . . . . 6 ((𝑦 ∈ β„š ∧ 𝑧 ∈ β„š) β†’ (𝑦 Β· 𝑧) ∈ β„š)
8280, 73, 81syl2anc 585 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑦 Β· 𝑧) ∈ β„š)
83 eqeq1 2737 . . . . . . 7 (π‘₯ = (𝑦 Β· 𝑧) β†’ (π‘₯ = 0 ↔ (𝑦 Β· 𝑧) = 0))
84 oveq2 7414 . . . . . . . 8 (π‘₯ = (𝑦 Β· 𝑧) β†’ (𝑃 pCnt π‘₯) = (𝑃 pCnt (𝑦 Β· 𝑧)))
8584oveq2d 7422 . . . . . . 7 (π‘₯ = (𝑦 Β· 𝑧) β†’ (𝑁↑(𝑃 pCnt π‘₯)) = (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))))
8683, 85ifbieq2d 4554 . . . . . 6 (π‘₯ = (𝑦 Β· 𝑧) β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))))
87 ovex 7439 . . . . . . 7 (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))) ∈ V
8842, 87ifex 4578 . . . . . 6 if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))) ∈ V
8986, 36, 88fvmpt 6996 . . . . 5 ((𝑦 Β· 𝑧) ∈ β„š β†’ (πΉβ€˜(𝑦 Β· 𝑧)) = if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))))
9082, 89syl 17 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 Β· 𝑧)) = if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))))
91 qcn 12944 . . . . . . . 8 (𝑦 ∈ β„š β†’ 𝑦 ∈ β„‚)
9280, 91syl 17 . . . . . . 7 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑦 ∈ β„‚)
93 qcn 12944 . . . . . . . 8 (𝑧 ∈ β„š β†’ 𝑧 ∈ β„‚)
9473, 93syl 17 . . . . . . 7 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑧 ∈ β„‚)
95 simp2r 1201 . . . . . . 7 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑦 β‰  0)
9692, 94, 95, 74mulne0d 11863 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑦 Β· 𝑧) β‰  0)
9796neneqd 2946 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ Β¬ (𝑦 Β· 𝑧) = 0)
9897iffalsed 4539 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))))
9990, 98eqtrd 2773 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 Β· 𝑧)) = (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))))
100633expb 1121 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0)) β†’ (πΉβ€˜π‘¦) = (𝑁↑(𝑃 pCnt 𝑦)))
1011003adant3 1133 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜π‘¦) = (𝑁↑(𝑃 pCnt 𝑦)))
102 eqeq1 2737 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (π‘₯ = 0 ↔ 𝑧 = 0))
103 oveq2 7414 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (𝑃 pCnt π‘₯) = (𝑃 pCnt 𝑧))
104103oveq2d 7422 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (𝑁↑(𝑃 pCnt π‘₯)) = (𝑁↑(𝑃 pCnt 𝑧)))
105102, 104ifbieq2d 4554 . . . . . . 7 (π‘₯ = 𝑧 β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
106 ovex 7439 . . . . . . . 8 (𝑁↑(𝑃 pCnt 𝑧)) ∈ V
10742, 106ifex 4578 . . . . . . 7 if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) ∈ V
108105, 36, 107fvmpt 6996 . . . . . 6 (𝑧 ∈ β„š β†’ (πΉβ€˜π‘§) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
10973, 108syl 17 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜π‘§) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
11074neneqd 2946 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ Β¬ 𝑧 = 0)
111110iffalsed 4539 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) = (𝑁↑(𝑃 pCnt 𝑧)))
112109, 111eqtrd 2773 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜π‘§) = (𝑁↑(𝑃 pCnt 𝑧)))
113101, 112oveq12d 7424 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ ((πΉβ€˜π‘¦) Β· (πΉβ€˜π‘§)) = ((𝑁↑(𝑃 pCnt 𝑦)) Β· (𝑁↑(𝑃 pCnt 𝑧))))
11479, 99, 1133eqtr4d 2783 . 2 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 Β· 𝑧)) = ((πΉβ€˜π‘¦) Β· (πΉβ€˜π‘§)))
115 iftrue 4534 . . . . 5 ((𝑦 + 𝑧) = 0 β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = 0)
116115breq1d 5158 . . . 4 ((𝑦 + 𝑧) = 0 β†’ (if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ↔ 0 ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
117 ifnefalse 4540 . . . . . 6 ((𝑦 + 𝑧) β‰  0 β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
118117adantl 483 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
11971adantr 482 . . . . . . 7 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
120119zred 12663 . . . . . 6 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt 𝑦) ∈ ℝ)
12176adantr 482 . . . . . . 7 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt 𝑧) ∈ β„€)
122121zred 12663 . . . . . 6 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt 𝑧) ∈ ℝ)
123213ad2ant1 1134 . . . . . . . . 9 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑁 ∈ ℝ)
124123ad2antrr 725 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑁 ∈ ℝ)
12570ad2antrr 725 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑁 β‰  0)
12672adantr 482 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 𝑃 ∈ β„™)
127 qaddcl 12946 . . . . . . . . . . . 12 ((𝑦 ∈ β„š ∧ 𝑧 ∈ β„š) β†’ (𝑦 + 𝑧) ∈ β„š)
12880, 73, 127syl2anc 585 . . . . . . . . . . 11 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑦 + 𝑧) ∈ β„š)
129128adantr 482 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑦 + 𝑧) ∈ β„š)
130 simpr 486 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑦 + 𝑧) β‰  0)
131 pcqcl 16786 . . . . . . . . . 10 ((𝑃 ∈ β„™ ∧ ((𝑦 + 𝑧) ∈ β„š ∧ (𝑦 + 𝑧) β‰  0)) β†’ (𝑃 pCnt (𝑦 + 𝑧)) ∈ β„€)
132126, 129, 130, 131syl12anc 836 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt (𝑦 + 𝑧)) ∈ β„€)
133132adantr 482 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑃 pCnt (𝑦 + 𝑧)) ∈ β„€)
134124, 125, 133reexpclzd 14209 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
135119adantr 482 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
136124, 125, 135reexpclzd 14209 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
137 simpl1 1192 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)))
138137, 21syl 17 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 𝑁 ∈ ℝ)
139137, 27syl 17 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 𝑁 β‰  0)
140138, 139, 119reexpclzd 14209 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
141138, 139, 121reexpclzd 14209 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
142140, 141readdcld 11240 . . . . . . . 8 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
143142adantr 482 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
144126adantr 482 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑃 ∈ β„™)
14580ad2antrr 725 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑦 ∈ β„š)
14673ad2antrr 725 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑧 ∈ β„š)
147 simpr 486 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧))
148144, 145, 146, 147pcadd 16819 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt (𝑦 + 𝑧)))
149137, 26syl 17 . . . . . . . . . . . 12 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 𝑁 ∈ ℝ+)
15024simprd 497 . . . . . . . . . . . . 13 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 < 1)
151137, 150syl 17 . . . . . . . . . . . 12 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 𝑁 < 1)
152149, 119, 132, 151ltexp2rd 14208 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦) ↔ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
153152notbid 318 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (Β¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦) ↔ Β¬ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
154132zred 12663 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℝ)
155120, 154lenltd 11357 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt 𝑦) ≀ (𝑃 pCnt (𝑦 + 𝑧)) ↔ Β¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦)))
156138, 139, 132reexpclzd 14209 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
157156, 140lenltd 11357 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑦)) ↔ Β¬ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
158153, 155, 1573bitr4d 311 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt 𝑦) ≀ (𝑃 pCnt (𝑦 + 𝑧)) ↔ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑦))))
159158biimpa 478 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt (𝑦 + 𝑧))) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑦)))
160148, 159syldan 592 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑦)))
161263ad2ant1 1134 . . . . . . . . . . . 12 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑁 ∈ ℝ+)
162161, 76rpexpcld 14207 . . . . . . . . . . 11 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ+)
163162adantr 482 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ+)
164163rpge0d 13017 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 0 ≀ (𝑁↑(𝑃 pCnt 𝑧)))
165140, 141addge01d 11799 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (0 ≀ (𝑁↑(𝑃 pCnt 𝑧)) ↔ (𝑁↑(𝑃 pCnt 𝑦)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
166164, 165mpbid 231 . . . . . . . 8 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
167166adantr 482 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
168134, 136, 143, 160, 167letrd 11368 . . . . . 6 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
169156adantr 482 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
170141adantr 482 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
171142adantr 482 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
172126adantr 482 . . . . . . . . . 10 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ 𝑃 ∈ β„™)
17373ad2antrr 725 . . . . . . . . . 10 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ 𝑧 ∈ β„š)
17480ad2antrr 725 . . . . . . . . . 10 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ 𝑦 ∈ β„š)
175 simpr 486 . . . . . . . . . 10 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦))
176172, 173, 174, 175pcadd 16819 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑧 + 𝑦)))
17792, 94addcomd 11413 . . . . . . . . . . 11 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑦 + 𝑧) = (𝑧 + 𝑦))
178177oveq2d 7422 . . . . . . . . . 10 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
179178ad2antrr 725 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
180176, 179breqtrrd 5176 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑦 + 𝑧)))
181149, 121, 132, 151ltexp2rd 14208 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧) ↔ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
182181notbid 318 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (Β¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧) ↔ Β¬ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
183122, 154lenltd 11357 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑦 + 𝑧)) ↔ Β¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧)))
184156, 141lenltd 11357 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑧)) ↔ Β¬ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
185182, 183, 1843bitr4d 311 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑦 + 𝑧)) ↔ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑧))))
186185biimpa 478 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑦 + 𝑧))) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑧)))
187180, 186syldan 592 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑧)))
188161, 71rpexpcld 14207 . . . . . . . . . . 11 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ+)
189188adantr 482 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ+)
190189rpge0d 13017 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 0 ≀ (𝑁↑(𝑃 pCnt 𝑦)))
191141, 140addge02d 11800 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (0 ≀ (𝑁↑(𝑃 pCnt 𝑦)) ↔ (𝑁↑(𝑃 pCnt 𝑧)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
192190, 191mpbid 231 . . . . . . . 8 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
193192adantr 482 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
194169, 170, 171, 187, 193letrd 11368 . . . . . 6 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
195120, 122, 168, 194lecasei 11317 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
196118, 195eqbrtrd 5170 . . . 4 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
197188, 162rpaddcld 13028 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ+)
198197rpge0d 13017 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 0 ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
199116, 196, 198pm2.61ne 3028 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
200 eqeq1 2737 . . . . . 6 (π‘₯ = (𝑦 + 𝑧) β†’ (π‘₯ = 0 ↔ (𝑦 + 𝑧) = 0))
201 oveq2 7414 . . . . . . 7 (π‘₯ = (𝑦 + 𝑧) β†’ (𝑃 pCnt π‘₯) = (𝑃 pCnt (𝑦 + 𝑧)))
202201oveq2d 7422 . . . . . 6 (π‘₯ = (𝑦 + 𝑧) β†’ (𝑁↑(𝑃 pCnt π‘₯)) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
203200, 202ifbieq2d 4554 . . . . 5 (π‘₯ = (𝑦 + 𝑧) β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
204 ovex 7439 . . . . . 6 (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ V
20542, 204ifex 4578 . . . . 5 if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ∈ V
206203, 36, 205fvmpt 6996 . . . 4 ((𝑦 + 𝑧) ∈ β„š β†’ (πΉβ€˜(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
207128, 206syl 17 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
208101, 112oveq12d 7424 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ ((πΉβ€˜π‘¦) + (πΉβ€˜π‘§)) = ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
209199, 207, 2083brtr4d 5180 . 2 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 + 𝑧)) ≀ ((πΉβ€˜π‘¦) + (πΉβ€˜π‘§)))
2102, 5, 9, 12, 14, 17, 37, 44, 64, 114, 209isabvd 20421 1 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝐹 ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  Vcvv 3475  ifcif 4528   class class class wbr 5148   ↦ cmpt 5231  β€˜cfv 6541  (class class class)co 7406  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   Β· cmul 11112   < clt 11245   ≀ cle 11246  β„€cz 12555  β„šcq 12929  β„+crp 12971  (,)cioo 13321  β†‘cexp 14024  β„™cprime 16605   pCnt cpc 16766  Basecbs 17141   β†Ύs cress 17170  +gcplusg 17194  .rcmulr 17195  0gc0g 17382  Ringcrg 20050  DivRingcdr 20308  AbsValcabv 20417  β„‚fldccnfld 20937
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-tpos 8208  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-sup 9434  df-inf 9435  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-ioo 13325  df-ico 13327  df-fz 13482  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-dvds 16195  df-gcd 16433  df-prm 16606  df-pc 16767  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-0g 17384  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-grp 18819  df-minusg 18820  df-subg 18998  df-cmn 19645  df-mgp 19983  df-ur 20000  df-ring 20052  df-cring 20053  df-oppr 20143  df-dvdsr 20164  df-unit 20165  df-invr 20195  df-dvr 20208  df-drng 20310  df-subrg 20354  df-abv 20418  df-cnfld 20938
This theorem is referenced by:  padicabvf  27124  padicabvcxp  27125
  Copyright terms: Public domain W3C validator