MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  padicabv Structured version   Visualization version   GIF version
Theorem padicabv 27478
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 27467 . . 3 β„š = (Baseβ€˜π‘„)
54a1i 11 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ β„š = (Baseβ€˜π‘„))
6 qex 12941 . . 3 β„š ∈ V
7 cnfldadd 21232 . . . 4 + = (+gβ€˜β„‚fld)
83, 7ressplusg 17233 . . 3 (β„š ∈ V β†’ + = (+gβ€˜π‘„))
96, 8mp1i 13 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ + = (+gβ€˜π‘„))
10 cnfldmul 21233 . . . 4 Β· = (.rβ€˜β„‚fld)
113, 10ressmulr 17250 . . 3 (β„š ∈ V β†’ Β· = (.rβ€˜π‘„))
126, 11mp1i 13 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ Β· = (.rβ€˜π‘„))
133qrng0 27469 . . 3 0 = (0gβ€˜π‘„)
1413a1i 11 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 0 = (0gβ€˜π‘„))
153qdrng 27468 . . 3 𝑄 ∈ DivRing
16 drngring 20583 . . 3 (𝑄 ∈ DivRing β†’ 𝑄 ∈ Ring)
1715, 16mp1i 13 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑄 ∈ Ring)
18 0red 11213 . . . 4 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ π‘₯ = 0) β†’ 0 ∈ ℝ)
19 ioossre 13381 . . . . . . 7 (0(,)1) βŠ† ℝ
20 simpr 484 . . . . . . 7 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 ∈ (0(,)1))
2119, 20sselid 3972 . . . . . 6 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 ∈ ℝ)
2221ad2antrr 723 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ Β¬ π‘₯ = 0) β†’ 𝑁 ∈ ℝ)
23 eliooord 13379 . . . . . . . . . 10 (𝑁 ∈ (0(,)1) β†’ (0 < 𝑁 ∧ 𝑁 < 1))
2423adantl 481 . . . . . . . . 9 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ (0 < 𝑁 ∧ 𝑁 < 1))
2524simpld 494 . . . . . . . 8 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 0 < 𝑁)
2621, 25elrpd 13009 . . . . . . 7 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 ∈ ℝ+)
2726rpne0d 13017 . . . . . 6 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 β‰  0)
2827ad2antrr 723 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ Β¬ π‘₯ = 0) β†’ 𝑁 β‰  0)
29 df-ne 2933 . . . . . 6 (π‘₯ β‰  0 ↔ Β¬ π‘₯ = 0)
30 pcqcl 16787 . . . . . . . 8 ((𝑃 ∈ β„™ ∧ (π‘₯ ∈ β„š ∧ π‘₯ β‰  0)) β†’ (𝑃 pCnt π‘₯) ∈ β„€)
3130adantlr 712 . . . . . . 7 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (π‘₯ ∈ β„š ∧ π‘₯ β‰  0)) β†’ (𝑃 pCnt π‘₯) ∈ β„€)
3231anassrs 467 . . . . . 6 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ π‘₯ β‰  0) β†’ (𝑃 pCnt π‘₯) ∈ β„€)
3329, 32sylan2br 594 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ Β¬ π‘₯ = 0) β†’ (𝑃 pCnt π‘₯) ∈ β„€)
3422, 28, 33reexpclzd 14208 . . . 4 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) ∧ Β¬ π‘₯ = 0) β†’ (𝑁↑(𝑃 pCnt π‘₯)) ∈ ℝ)
3518, 34ifclda 4555 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ π‘₯ ∈ β„š) β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) ∈ ℝ)
36 padic.f . . 3 𝐹 = (π‘₯ ∈ β„š ↦ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))))
3735, 36fmptd 7105 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝐹:β„šβŸΆβ„)
38 0z 12565 . . . 4 0 ∈ β„€
39 zq 12934 . . . 4 (0 ∈ β„€ β†’ 0 ∈ β„š)
4038, 39ax-mp 5 . . 3 0 ∈ β„š
41 iftrue 4526 . . . 4 (π‘₯ = 0 β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = 0)
42 c0ex 11204 . . . 4 0 ∈ V
4341, 36, 42fvmpt 6988 . . 3 (0 ∈ β„š β†’ (πΉβ€˜0) = 0)
4440, 43mp1i 13 . 2 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ (πΉβ€˜0) = 0)
45213ad2ant1 1130 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 𝑁 ∈ ℝ)
46 pcqcl 16787 . . . . . 6 ((𝑃 ∈ β„™ ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0)) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
4746adantlr 712 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0)) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
48473impb 1112 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
49253ad2ant1 1130 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 0 < 𝑁)
50 expgt0 14057 . . . 4 ((𝑁 ∈ ℝ ∧ (𝑃 pCnt 𝑦) ∈ β„€ ∧ 0 < 𝑁) β†’ 0 < (𝑁↑(𝑃 pCnt 𝑦)))
5145, 48, 49, 50syl3anc 1368 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 0 < (𝑁↑(𝑃 pCnt 𝑦)))
52 eqeq1 2728 . . . . . . 7 (π‘₯ = 𝑦 β†’ (π‘₯ = 0 ↔ 𝑦 = 0))
53 oveq2 7409 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (𝑃 pCnt π‘₯) = (𝑃 pCnt 𝑦))
5453oveq2d 7417 . . . . . . 7 (π‘₯ = 𝑦 β†’ (𝑁↑(𝑃 pCnt π‘₯)) = (𝑁↑(𝑃 pCnt 𝑦)))
5552, 54ifbieq2d 4546 . . . . . 6 (π‘₯ = 𝑦 β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
56 ovex 7434 . . . . . . 7 (𝑁↑(𝑃 pCnt 𝑦)) ∈ V
5742, 56ifex 4570 . . . . . 6 if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) ∈ V
5855, 36, 57fvmpt 6988 . . . . 5 (𝑦 ∈ β„š β†’ (πΉβ€˜π‘¦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
59583ad2ant2 1131 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ (πΉβ€˜π‘¦) = if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))))
60 simp3 1135 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 𝑦 β‰  0)
6160neneqd 2937 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ Β¬ 𝑦 = 0)
6261iffalsed 4531 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ if(𝑦 = 0, 0, (𝑁↑(𝑃 pCnt 𝑦))) = (𝑁↑(𝑃 pCnt 𝑦)))
6359, 62eqtrd 2764 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ (πΉβ€˜π‘¦) = (𝑁↑(𝑃 pCnt 𝑦)))
6451, 63breqtrrd 5166 . 2 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ 𝑦 ∈ β„š ∧ 𝑦 β‰  0) β†’ 0 < (πΉβ€˜π‘¦))
65 pcqmul 16784 . . . . . 6 ((𝑃 ∈ β„™ ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt (𝑦 Β· 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
66653adant1r 1174 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt (𝑦 Β· 𝑧)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧)))
6766oveq2d 7417 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))) = (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))))
6821recnd 11238 . . . . . 6 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 ∈ β„‚)
69683ad2ant1 1130 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑁 ∈ β„‚)
70273ad2ant1 1130 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑁 β‰  0)
71473adant3 1129 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
72 simp1l 1194 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑃 ∈ β„™)
73 simp3l 1198 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑧 ∈ β„š)
74 simp3r 1199 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑧 β‰  0)
75 pcqcl 16787 . . . . . 6 ((𝑃 ∈ β„™ ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt 𝑧) ∈ β„€)
7672, 73, 74, 75syl12anc 834 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt 𝑧) ∈ β„€)
77 expaddz 14068 . . . . 5 (((𝑁 ∈ β„‚ ∧ 𝑁 β‰  0) ∧ ((𝑃 pCnt 𝑦) ∈ β„€ ∧ (𝑃 pCnt 𝑧) ∈ β„€)) β†’ (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) Β· (𝑁↑(𝑃 pCnt 𝑧))))
7869, 70, 71, 76, 77syl22anc 836 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) Β· (𝑁↑(𝑃 pCnt 𝑧))))
7967, 78eqtrd 2764 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))) = ((𝑁↑(𝑃 pCnt 𝑦)) Β· (𝑁↑(𝑃 pCnt 𝑧))))
80 simp2l 1196 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑦 ∈ β„š)
81 qmulcl 12947 . . . . . 6 ((𝑦 ∈ β„š ∧ 𝑧 ∈ β„š) β†’ (𝑦 Β· 𝑧) ∈ β„š)
8280, 73, 81syl2anc 583 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑦 Β· 𝑧) ∈ β„š)
83 eqeq1 2728 . . . . . . 7 (π‘₯ = (𝑦 Β· 𝑧) β†’ (π‘₯ = 0 ↔ (𝑦 Β· 𝑧) = 0))
84 oveq2 7409 . . . . . . . 8 (π‘₯ = (𝑦 Β· 𝑧) β†’ (𝑃 pCnt π‘₯) = (𝑃 pCnt (𝑦 Β· 𝑧)))
8584oveq2d 7417 . . . . . . 7 (π‘₯ = (𝑦 Β· 𝑧) β†’ (𝑁↑(𝑃 pCnt π‘₯)) = (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))))
8683, 85ifbieq2d 4546 . . . . . 6 (π‘₯ = (𝑦 Β· 𝑧) β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))))
87 ovex 7434 . . . . . . 7 (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))) ∈ V
8842, 87ifex 4570 . . . . . 6 if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))) ∈ V
8986, 36, 88fvmpt 6988 . . . . 5 ((𝑦 Β· 𝑧) ∈ β„š β†’ (πΉβ€˜(𝑦 Β· 𝑧)) = if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))))
9082, 89syl 17 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 Β· 𝑧)) = if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))))
91 qcn 12943 . . . . . . . 8 (𝑦 ∈ β„š β†’ 𝑦 ∈ β„‚)
9280, 91syl 17 . . . . . . 7 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑦 ∈ β„‚)
93 qcn 12943 . . . . . . . 8 (𝑧 ∈ β„š β†’ 𝑧 ∈ β„‚)
9473, 93syl 17 . . . . . . 7 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑧 ∈ β„‚)
95 simp2r 1197 . . . . . . 7 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑦 β‰  0)
9692, 94, 95, 74mulne0d 11862 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑦 Β· 𝑧) β‰  0)
9796neneqd 2937 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ Β¬ (𝑦 Β· 𝑧) = 0)
9897iffalsed 4531 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ if((𝑦 Β· 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))))
9990, 98eqtrd 2764 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 Β· 𝑧)) = (𝑁↑(𝑃 pCnt (𝑦 Β· 𝑧))))
100633expb 1117 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0)) β†’ (πΉβ€˜π‘¦) = (𝑁↑(𝑃 pCnt 𝑦)))
1011003adant3 1129 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜π‘¦) = (𝑁↑(𝑃 pCnt 𝑦)))
102 eqeq1 2728 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (π‘₯ = 0 ↔ 𝑧 = 0))
103 oveq2 7409 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (𝑃 pCnt π‘₯) = (𝑃 pCnt 𝑧))
104103oveq2d 7417 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (𝑁↑(𝑃 pCnt π‘₯)) = (𝑁↑(𝑃 pCnt 𝑧)))
105102, 104ifbieq2d 4546 . . . . . . 7 (π‘₯ = 𝑧 β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
106 ovex 7434 . . . . . . . 8 (𝑁↑(𝑃 pCnt 𝑧)) ∈ V
10742, 106ifex 4570 . . . . . . 7 if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) ∈ V
108105, 36, 107fvmpt 6988 . . . . . 6 (𝑧 ∈ β„š β†’ (πΉβ€˜π‘§) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
10973, 108syl 17 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜π‘§) = if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))))
11074neneqd 2937 . . . . . 6 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ Β¬ 𝑧 = 0)
111110iffalsed 4531 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ if(𝑧 = 0, 0, (𝑁↑(𝑃 pCnt 𝑧))) = (𝑁↑(𝑃 pCnt 𝑧)))
112109, 111eqtrd 2764 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜π‘§) = (𝑁↑(𝑃 pCnt 𝑧)))
113101, 112oveq12d 7419 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ ((πΉβ€˜π‘¦) Β· (πΉβ€˜π‘§)) = ((𝑁↑(𝑃 pCnt 𝑦)) Β· (𝑁↑(𝑃 pCnt 𝑧))))
11479, 99, 1133eqtr4d 2774 . 2 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 Β· 𝑧)) = ((πΉβ€˜π‘¦) Β· (πΉβ€˜π‘§)))
115 iftrue 4526 . . . . 5 ((𝑦 + 𝑧) = 0 β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = 0)
116115breq1d 5148 . . . 4 ((𝑦 + 𝑧) = 0 β†’ (if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ↔ 0 ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
117 ifnefalse 4532 . . . . . 6 ((𝑦 + 𝑧) β‰  0 β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
118117adantl 481 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
11971adantr 480 . . . . . . 7 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
120119zred 12662 . . . . . 6 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt 𝑦) ∈ ℝ)
12176adantr 480 . . . . . . 7 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt 𝑧) ∈ β„€)
122121zred 12662 . . . . . 6 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt 𝑧) ∈ ℝ)
123213ad2ant1 1130 . . . . . . . . 9 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑁 ∈ ℝ)
124123ad2antrr 723 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑁 ∈ ℝ)
12570ad2antrr 723 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑁 β‰  0)
12672adantr 480 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 𝑃 ∈ β„™)
127 qaddcl 12945 . . . . . . . . . . . 12 ((𝑦 ∈ β„š ∧ 𝑧 ∈ β„š) β†’ (𝑦 + 𝑧) ∈ β„š)
12880, 73, 127syl2anc 583 . . . . . . . . . . 11 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑦 + 𝑧) ∈ β„š)
129128adantr 480 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑦 + 𝑧) ∈ β„š)
130 simpr 484 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑦 + 𝑧) β‰  0)
131 pcqcl 16787 . . . . . . . . . 10 ((𝑃 ∈ β„™ ∧ ((𝑦 + 𝑧) ∈ β„š ∧ (𝑦 + 𝑧) β‰  0)) β†’ (𝑃 pCnt (𝑦 + 𝑧)) ∈ β„€)
132126, 129, 130, 131syl12anc 834 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt (𝑦 + 𝑧)) ∈ β„€)
133132adantr 480 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑃 pCnt (𝑦 + 𝑧)) ∈ β„€)
134124, 125, 133reexpclzd 14208 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
135119adantr 480 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑃 pCnt 𝑦) ∈ β„€)
136124, 125, 135reexpclzd 14208 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
137 simpl1 1188 . . . . . . . . . . 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 14208 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ)
141138, 139, 121reexpclzd 14208 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
142140, 141readdcld 11239 . . . . . . . 8 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
143142adantr 480 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
144126adantr 480 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑃 ∈ β„™)
14580ad2antrr 723 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑦 ∈ β„š)
14673ad2antrr 723 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ 𝑧 ∈ β„š)
147 simpr 484 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧))
148144, 145, 146, 147pcadd 16820 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt (𝑦 + 𝑧)))
149137, 26syl 17 . . . . . . . . . . . 12 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 𝑁 ∈ ℝ+)
15024simprd 495 . . . . . . . . . . . . 13 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝑁 < 1)
151137, 150syl 17 . . . . . . . . . . . 12 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 𝑁 < 1)
152149, 119, 132, 151ltexp2rd 14207 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦) ↔ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
153152notbid 318 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (Β¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦) ↔ Β¬ (𝑁↑(𝑃 pCnt 𝑦)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
154132zred 12662 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑃 pCnt (𝑦 + 𝑧)) ∈ ℝ)
155120, 154lenltd 11356 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt 𝑦) ≀ (𝑃 pCnt (𝑦 + 𝑧)) ↔ Β¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑦)))
156138, 139, 132reexpclzd 14208 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
157156, 140lenltd 11356 . . . . . . . . . 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 476 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt (𝑦 + 𝑧))) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑦)))
160148, 159syldan 590 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑦)))
161263ad2ant1 1130 . . . . . . . . . . . 12 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 𝑁 ∈ ℝ+)
162161, 76rpexpcld 14206 . . . . . . . . . . 11 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ+)
163162adantr 480 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ+)
164163rpge0d 13016 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 0 ≀ (𝑁↑(𝑃 pCnt 𝑧)))
165140, 141addge01d 11798 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (0 ≀ (𝑁↑(𝑃 pCnt 𝑧)) ↔ (𝑁↑(𝑃 pCnt 𝑦)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
166164, 165mpbid 231 . . . . . . . 8 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
167166adantr 480 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
168134, 136, 143, 160, 167letrd 11367 . . . . . 6 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑦) ≀ (𝑃 pCnt 𝑧)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
169156adantr 480 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ ℝ)
170141adantr 480 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ∈ ℝ)
171142adantr 480 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ)
172126adantr 480 . . . . . . . . . 10 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ 𝑃 ∈ β„™)
17373ad2antrr 723 . . . . . . . . . 10 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ 𝑧 ∈ β„š)
17480ad2antrr 723 . . . . . . . . . 10 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ 𝑦 ∈ β„š)
175 simpr 484 . . . . . . . . . 10 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦))
176172, 173, 174, 175pcadd 16820 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑧 + 𝑦)))
17792, 94addcomd 11412 . . . . . . . . . . 11 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑦 + 𝑧) = (𝑧 + 𝑦))
178177oveq2d 7417 . . . . . . . . . 10 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
179178ad2antrr 723 . . . . . . . . 9 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑃 pCnt (𝑦 + 𝑧)) = (𝑃 pCnt (𝑧 + 𝑦)))
180176, 179breqtrrd 5166 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑦 + 𝑧)))
181149, 121, 132, 151ltexp2rd 14207 . . . . . . . . . . 11 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧) ↔ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
182181notbid 318 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (Β¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧) ↔ Β¬ (𝑁↑(𝑃 pCnt 𝑧)) < (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
183122, 154lenltd 11356 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ ((𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑦 + 𝑧)) ↔ Β¬ (𝑃 pCnt (𝑦 + 𝑧)) < (𝑃 pCnt 𝑧)))
184156, 141lenltd 11356 . . . . . . . . . 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 476 . . . . . . . 8 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt (𝑦 + 𝑧))) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑧)))
187180, 186syldan 590 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ (𝑁↑(𝑃 pCnt 𝑧)))
188161, 71rpexpcld 14206 . . . . . . . . . . 11 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ+)
189188adantr 480 . . . . . . . . . 10 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑦)) ∈ ℝ+)
190189rpge0d 13016 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ 0 ≀ (𝑁↑(𝑃 pCnt 𝑦)))
191141, 140addge02d 11799 . . . . . . . . 9 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (0 ≀ (𝑁↑(𝑃 pCnt 𝑦)) ↔ (𝑁↑(𝑃 pCnt 𝑧)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧)))))
192190, 191mpbid 231 . . . . . . . 8 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
193192adantr 480 . . . . . . 7 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt 𝑧)) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
194169, 170, 171, 187, 193letrd 11367 . . . . . 6 (((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) ∧ (𝑃 pCnt 𝑧) ≀ (𝑃 pCnt 𝑦)) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
195120, 122, 168, 194lecasei 11316 . . . . 5 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
196118, 195eqbrtrd 5160 . . . 4 ((((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) ∧ (𝑦 + 𝑧) β‰  0) β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
197188, 162rpaddcld 13027 . . . . 5 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))) ∈ ℝ+)
198197rpge0d 13016 . . . 4 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ 0 ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
199116, 196, 198pm2.61ne 3019 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ≀ ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
200 eqeq1 2728 . . . . . 6 (π‘₯ = (𝑦 + 𝑧) β†’ (π‘₯ = 0 ↔ (𝑦 + 𝑧) = 0))
201 oveq2 7409 . . . . . . 7 (π‘₯ = (𝑦 + 𝑧) β†’ (𝑃 pCnt π‘₯) = (𝑃 pCnt (𝑦 + 𝑧)))
202201oveq2d 7417 . . . . . 6 (π‘₯ = (𝑦 + 𝑧) β†’ (𝑁↑(𝑃 pCnt π‘₯)) = (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))))
203200, 202ifbieq2d 4546 . . . . 5 (π‘₯ = (𝑦 + 𝑧) β†’ if(π‘₯ = 0, 0, (𝑁↑(𝑃 pCnt π‘₯))) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
204 ovex 7434 . . . . . 6 (𝑁↑(𝑃 pCnt (𝑦 + 𝑧))) ∈ V
20542, 204ifex 4570 . . . . 5 if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))) ∈ V
206203, 36, 205fvmpt 6988 . . . 4 ((𝑦 + 𝑧) ∈ β„š β†’ (πΉβ€˜(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
207128, 206syl 17 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 + 𝑧)) = if((𝑦 + 𝑧) = 0, 0, (𝑁↑(𝑃 pCnt (𝑦 + 𝑧)))))
208101, 112oveq12d 7419 . . 3 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ ((πΉβ€˜π‘¦) + (πΉβ€˜π‘§)) = ((𝑁↑(𝑃 pCnt 𝑦)) + (𝑁↑(𝑃 pCnt 𝑧))))
209199, 207, 2083brtr4d 5170 . 2 (((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) ∧ (𝑦 ∈ β„š ∧ 𝑦 β‰  0) ∧ (𝑧 ∈ β„š ∧ 𝑧 β‰  0)) β†’ (πΉβ€˜(𝑦 + 𝑧)) ≀ ((πΉβ€˜π‘¦) + (πΉβ€˜π‘§)))
2102, 5, 9, 12, 14, 17, 37, 44, 64, 114, 209isabvd 20652 1 ((𝑃 ∈ β„™ ∧ 𝑁 ∈ (0(,)1)) β†’ 𝐹 ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2932  Vcvv 3466  ifcif 4520   class class class wbr 5138   ↦ cmpt 5221  β€˜cfv 6533  (class class class)co 7401  β„‚cc 11103  β„cr 11104  0cc0 11105  1c1 11106   + caddc 11108   Β· cmul 11110   < clt 11244   ≀ cle 11245  β„€cz 12554  β„šcq 12928  β„+crp 12970  (,)cioo 13320  β†‘cexp 14023  β„™cprime 16604   pCnt cpc 16767  Basecbs 17142   β†Ύs cress 17171  +gcplusg 17195  .rcmulr 17196  0gc0g 17383  Ringcrg 20127  DivRingcdr 20576  AbsValcabv 20648  β„‚fldccnfld 21227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183  ax-addf 11184  ax-mulf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8698  df-map 8817  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-sup 9432  df-inf 9433  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-ioo 13324  df-ico 13326  df-fz 13481  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-dvds 16194  df-gcd 16432  df-prm 16605  df-pc 16768  df-struct 17078  df-sets 17095  df-slot 17113  df-ndx 17125  df-base 17143  df-ress 17172  df-plusg 17208  df-mulr 17209  df-starv 17210  df-tset 17214  df-ple 17215  df-ds 17217  df-unif 17218  df-0g 17385  df-mgm 18562  df-sgrp 18641  df-mnd 18657  df-grp 18855  df-minusg 18856  df-subg 19039  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-ring 20129  df-cring 20130  df-oppr 20225  df-dvdsr 20248  df-unit 20249  df-invr 20279  df-dvr 20292  df-subrng 20435  df-subrg 20460  df-drng 20578  df-abv 20649  df-cnfld 21228
This theorem is referenced by:  padicabvf  27479  padicabvcxp  27480
  Copyright terms: Public domain W3C validator