Metamath Proof Explorer

Theorem padicabv

Description: The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Hypotheses qrng.q 
|- Q = ( CCfld |`s QQ )
qabsabv.a 
|- A = ( AbsVal ` Q )
padic.f 
|- F = ( x e. QQ |-> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) )
Assertion padicabv 
|- ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> F e. A )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qabsabv.a 
 |-  A = ( AbsVal ` Q )
3 padic.f 
 |-  F = ( x e. QQ |-> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) )
4 2 a1i 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> A = ( AbsVal ` Q ) )
5 1 qrngbas 
 |-  QQ = ( Base ` Q )
6 5 a1i 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> QQ = ( Base ` Q ) )
7 qex 
 |-  QQ e. _V
8 cnfldadd 
 |-  + = ( +g ` CCfld )
9 1 8 ressplusg 
 |-  ( QQ e. _V -> + = ( +g ` Q ) )
10 7 9 mp1i 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> + = ( +g ` Q ) )
11 cnfldmul 
 |-  x. = ( .r ` CCfld )
12 1 11 ressmulr 
 |-  ( QQ e. _V -> x. = ( .r ` Q ) )
13 7 12 mp1i 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> x. = ( .r ` Q ) )
14 1 qrng0 
 |-  0 = ( 0g ` Q )
15 14 a1i 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> 0 = ( 0g ` Q ) )
16 1 qdrng 
 |-  Q e. DivRing
17 drngring 
 |-  ( Q e. DivRing -> Q e. Ring )
18 16 17 mp1i 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> Q e. Ring )
19 0red 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ x e. QQ ) /\ x = 0 ) -> 0 e. RR )
20 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
21 simpr 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> N e. ( 0 (,) 1 ) )
22 20 21 sselid 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> N e. RR )
23 22 ad2antrr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ x e. QQ ) /\ -. x = 0 ) -> N e. RR )
24 eliooord 
 |-  ( N e. ( 0 (,) 1 ) -> ( 0 < N /\ N < 1 ) )
25 24 adantl 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> ( 0 < N /\ N < 1 ) )
26 25 simpld 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> 0 < N )
27 22 26 elrpd 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> N e. RR+ )
28 27 rpne0d 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> N =/= 0 )
29 28 ad2antrr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ x e. QQ ) /\ -. x = 0 ) -> N =/= 0 )
30 df-ne 
 |-  ( x =/= 0 <-> -. x = 0 )
31 pcqcl 
 |-  ( ( P e. Prime /\ ( x e. QQ /\ x =/= 0 ) ) -> ( P pCnt x ) e. ZZ )
32 31 adantlr 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( x e. QQ /\ x =/= 0 ) ) -> ( P pCnt x ) e. ZZ )
33 32 anassrs 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ x e. QQ ) /\ x =/= 0 ) -> ( P pCnt x ) e. ZZ )
34 30 33 sylan2br 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ x e. QQ ) /\ -. x = 0 ) -> ( P pCnt x ) e. ZZ )
35 23 29 34 reexpclzd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ x e. QQ ) /\ -. x = 0 ) -> ( N ^ ( P pCnt x ) ) e. RR )
36 19 35 ifclda 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ x e. QQ ) -> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) e. RR )
37 36 3 fmptd 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> F : QQ --> RR )
38 0z 
 |-  0 e. ZZ
39 zq 
 |-  ( 0 e. ZZ -> 0 e. QQ )
40 38 39 ax-mp 
 |-  0 e. QQ
41 iftrue 
 |-  ( x = 0 -> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) = 0 )
42 c0ex 
 |-  0 e. _V
43 41 3 42 fvmpt 
 |-  ( 0 e. QQ -> ( F ` 0 ) = 0 )
44 40 43 mp1i 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> ( F ` 0 ) = 0 )
45 22 3ad2ant1 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> N e. RR )
46 pcqcl 
 |-  ( ( P e. Prime /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P pCnt y ) e. ZZ )
47 46 adantlr 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( P pCnt y ) e. ZZ )
48 47 3impb 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> ( P pCnt y ) e. ZZ )
49 26 3ad2ant1 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> 0 < N )
50 expgt0 
 |-  ( ( N e. RR /\ ( P pCnt y ) e. ZZ /\ 0 < N ) -> 0 < ( N ^ ( P pCnt y ) ) )
51 45 48 49 50 syl3anc 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> 0 < ( N ^ ( P pCnt y ) ) )
52 eqeq1 
 |-  ( x = y -> ( x = 0 <-> y = 0 ) )
53 oveq2 
 |-  ( x = y -> ( P pCnt x ) = ( P pCnt y ) )
54 53 oveq2d 
 |-  ( x = y -> ( N ^ ( P pCnt x ) ) = ( N ^ ( P pCnt y ) ) )
55 52 54 ifbieq2d 
 |-  ( x = y -> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) = if ( y = 0 , 0 , ( N ^ ( P pCnt y ) ) ) )
56 ovex 
 |-  ( N ^ ( P pCnt y ) ) e. _V
57 42 56 ifex 
 |-  if ( y = 0 , 0 , ( N ^ ( P pCnt y ) ) ) e. _V
58 55 3 57 fvmpt 
 |-  ( y e. QQ -> ( F ` y ) = if ( y = 0 , 0 , ( N ^ ( P pCnt y ) ) ) )
59 58 3ad2ant2 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> ( F ` y ) = if ( y = 0 , 0 , ( N ^ ( P pCnt y ) ) ) )
60 simp3 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> y =/= 0 )
61 60 neneqd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> -. y = 0 )
62 61 iffalsed 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> if ( y = 0 , 0 , ( N ^ ( P pCnt y ) ) ) = ( N ^ ( P pCnt y ) ) )
63 59 62 eqtrd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> ( F ` y ) = ( N ^ ( P pCnt y ) ) )
64 51 63 breqtrrd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ y e. QQ /\ y =/= 0 ) -> 0 < ( F ` y ) )
65 pcqmul 
 |-  ( ( P e. Prime /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( P pCnt ( y x. z ) ) = ( ( P pCnt y ) + ( P pCnt z ) ) )
66 65 3adant1r 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( P pCnt ( y x. z ) ) = ( ( P pCnt y ) + ( P pCnt z ) ) )
67 66 oveq2d 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( N ^ ( P pCnt ( y x. z ) ) ) = ( N ^ ( ( P pCnt y ) + ( P pCnt z ) ) ) )
68 22 recnd 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> N e. CC )
69 68 3ad2ant1 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> N e. CC )
70 28 3ad2ant1 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> N =/= 0 )
71 47 3adant3 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( P pCnt y ) e. ZZ )
72 simp1l 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> P e. Prime )
73 simp3l 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> z e. QQ )
74 simp3r 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> z =/= 0 )
75 pcqcl 
 |-  ( ( P e. Prime /\ ( z e. QQ /\ z =/= 0 ) ) -> ( P pCnt z ) e. ZZ )
76 72 73 74 75 syl12anc 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( P pCnt z ) e. ZZ )
77 expaddz 
 |-  ( ( ( N e. CC /\ N =/= 0 ) /\ ( ( P pCnt y ) e. ZZ /\ ( P pCnt z ) e. ZZ ) ) -> ( N ^ ( ( P pCnt y ) + ( P pCnt z ) ) ) = ( ( N ^ ( P pCnt y ) ) x. ( N ^ ( P pCnt z ) ) ) )
78 69 70 71 76 77 syl22anc 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( N ^ ( ( P pCnt y ) + ( P pCnt z ) ) ) = ( ( N ^ ( P pCnt y ) ) x. ( N ^ ( P pCnt z ) ) ) )
79 67 78 eqtrd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( N ^ ( P pCnt ( y x. z ) ) ) = ( ( N ^ ( P pCnt y ) ) x. ( N ^ ( P pCnt z ) ) ) )
80 simp2l 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> y e. QQ )
81 qmulcl 
 |-  ( ( y e. QQ /\ z e. QQ ) -> ( y x. z ) e. QQ )
82 80 73 81 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( y x. z ) e. QQ )
83 eqeq1 
 |-  ( x = ( y x. z ) -> ( x = 0 <-> ( y x. z ) = 0 ) )
84 oveq2 
 |-  ( x = ( y x. z ) -> ( P pCnt x ) = ( P pCnt ( y x. z ) ) )
85 84 oveq2d 
 |-  ( x = ( y x. z ) -> ( N ^ ( P pCnt x ) ) = ( N ^ ( P pCnt ( y x. z ) ) ) )
86 83 85 ifbieq2d 
 |-  ( x = ( y x. z ) -> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) = if ( ( y x. z ) = 0 , 0 , ( N ^ ( P pCnt ( y x. z ) ) ) ) )
87 ovex 
 |-  ( N ^ ( P pCnt ( y x. z ) ) ) e. _V
88 42 87 ifex 
 |-  if ( ( y x. z ) = 0 , 0 , ( N ^ ( P pCnt ( y x. z ) ) ) ) e. _V
89 86 3 88 fvmpt 
 |-  ( ( y x. z ) e. QQ -> ( F ` ( y x. z ) ) = if ( ( y x. z ) = 0 , 0 , ( N ^ ( P pCnt ( y x. z ) ) ) ) )
90 82 89 syl 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( F ` ( y x. z ) ) = if ( ( y x. z ) = 0 , 0 , ( N ^ ( P pCnt ( y x. z ) ) ) ) )
91 qcn 
 |-  ( y e. QQ -> y e. CC )
92 80 91 syl 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> y e. CC )
93 qcn 
 |-  ( z e. QQ -> z e. CC )
94 73 93 syl 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> z e. CC )
95 simp2r 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> y =/= 0 )
96 92 94 95 74 mulne0d 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( y x. z ) =/= 0 )
97 96 neneqd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> -. ( y x. z ) = 0 )
98 97 iffalsed 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> if ( ( y x. z ) = 0 , 0 , ( N ^ ( P pCnt ( y x. z ) ) ) ) = ( N ^ ( P pCnt ( y x. z ) ) ) )
99 90 98 eqtrd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( F ` ( y x. z ) ) = ( N ^ ( P pCnt ( y x. z ) ) ) )
100 63 3expb 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) ) -> ( F ` y ) = ( N ^ ( P pCnt y ) ) )
101 100 3adant3 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( F ` y ) = ( N ^ ( P pCnt y ) ) )
102 eqeq1 
 |-  ( x = z -> ( x = 0 <-> z = 0 ) )
103 oveq2 
 |-  ( x = z -> ( P pCnt x ) = ( P pCnt z ) )
104 103 oveq2d 
 |-  ( x = z -> ( N ^ ( P pCnt x ) ) = ( N ^ ( P pCnt z ) ) )
105 102 104 ifbieq2d 
 |-  ( x = z -> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) = if ( z = 0 , 0 , ( N ^ ( P pCnt z ) ) ) )
106 ovex 
 |-  ( N ^ ( P pCnt z ) ) e. _V
107 42 106 ifex 
 |-  if ( z = 0 , 0 , ( N ^ ( P pCnt z ) ) ) e. _V
108 105 3 107 fvmpt 
 |-  ( z e. QQ -> ( F ` z ) = if ( z = 0 , 0 , ( N ^ ( P pCnt z ) ) ) )
109 73 108 syl 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( F ` z ) = if ( z = 0 , 0 , ( N ^ ( P pCnt z ) ) ) )
110 74 neneqd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> -. z = 0 )
111 110 iffalsed 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> if ( z = 0 , 0 , ( N ^ ( P pCnt z ) ) ) = ( N ^ ( P pCnt z ) ) )
112 109 111 eqtrd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( F ` z ) = ( N ^ ( P pCnt z ) ) )
113 101 112 oveq12d 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( ( F ` y ) x. ( F ` z ) ) = ( ( N ^ ( P pCnt y ) ) x. ( N ^ ( P pCnt z ) ) ) )
114 79 99 113 3eqtr4d 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( F ` ( y x. z ) ) = ( ( F ` y ) x. ( F ` z ) ) )
115 iftrue 
 |-  ( ( y + z ) = 0 -> if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) = 0 )
116 115 breq1d 
 |-  ( ( y + z ) = 0 -> ( if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) <-> 0 <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) ) )
117 ifnefalse 
 |-  ( ( y + z ) =/= 0 -> if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) = ( N ^ ( P pCnt ( y + z ) ) ) )
118 117 adantl 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) = ( N ^ ( P pCnt ( y + z ) ) ) )
119 71 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( P pCnt y ) e. ZZ )
120 119 zred 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( P pCnt y ) e. RR )
121 76 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( P pCnt z ) e. ZZ )
122 121 zred 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( P pCnt z ) e. RR )
123 22 3ad2ant1 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> N e. RR )
124 123 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> N e. RR )
125 70 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> N =/= 0 )
126 72 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> P e. Prime )
127 qaddcl 
 |-  ( ( y e. QQ /\ z e. QQ ) -> ( y + z ) e. QQ )
128 80 73 127 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( y + z ) e. QQ )
129 128 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( y + z ) e. QQ )
130 simpr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( y + z ) =/= 0 )
131 pcqcl 
 |-  ( ( P e. Prime /\ ( ( y + z ) e. QQ /\ ( y + z ) =/= 0 ) ) -> ( P pCnt ( y + z ) ) e. ZZ )
132 126 129 130 131 syl12anc 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( P pCnt ( y + z ) ) e. ZZ )
133 132 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( P pCnt ( y + z ) ) e. ZZ )
134 124 125 133 reexpclzd 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( N ^ ( P pCnt ( y + z ) ) ) e. RR )
135 119 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( P pCnt y ) e. ZZ )
136 124 125 135 reexpclzd 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( N ^ ( P pCnt y ) ) e. RR )
137 simpl1 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( P e. Prime /\ N e. ( 0 (,) 1 ) ) )
138 137 22 syl 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> N e. RR )
139 137 28 syl 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> N =/= 0 )
140 138 139 119 reexpclzd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( N ^ ( P pCnt y ) ) e. RR )
141 138 139 121 reexpclzd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( N ^ ( P pCnt z ) ) e. RR )
142 140 141 readdcld 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) e. RR )
143 142 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) e. RR )
144 126 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> P e. Prime )
145 80 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> y e. QQ )
146 73 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> z e. QQ )
147 simpr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( P pCnt y ) <_ ( P pCnt z ) )
148 144 145 146 147 pcadd 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( P pCnt y ) <_ ( P pCnt ( y + z ) ) )
149 137 27 syl 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> N e. RR+ )
150 25 simprd 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> N < 1 )
151 137 150 syl 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> N < 1 )
152 149 119 132 151 ltexp2rd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( P pCnt ( y + z ) ) < ( P pCnt y ) <-> ( N ^ ( P pCnt y ) ) < ( N ^ ( P pCnt ( y + z ) ) ) ) )
153 152 notbid 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( -. ( P pCnt ( y + z ) ) < ( P pCnt y ) <-> -. ( N ^ ( P pCnt y ) ) < ( N ^ ( P pCnt ( y + z ) ) ) ) )
154 132 zred 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( P pCnt ( y + z ) ) e. RR )
155 120 154 lenltd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( P pCnt y ) <_ ( P pCnt ( y + z ) ) <-> -. ( P pCnt ( y + z ) ) < ( P pCnt y ) ) )
156 138 139 132 reexpclzd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( N ^ ( P pCnt ( y + z ) ) ) e. RR )
157 156 140 lenltd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( N ^ ( P pCnt ( y + z ) ) ) <_ ( N ^ ( P pCnt y ) ) <-> -. ( N ^ ( P pCnt y ) ) < ( N ^ ( P pCnt ( y + z ) ) ) ) )
158 153 155 157 3bitr4d 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( P pCnt y ) <_ ( P pCnt ( y + z ) ) <-> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( N ^ ( P pCnt y ) ) ) )
159 158 biimpa 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt ( y + z ) ) ) -> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( N ^ ( P pCnt y ) ) )
160 148 159 syldan 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( N ^ ( P pCnt y ) ) )
161 27 3ad2ant1 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> N e. RR+ )
162 161 76 rpexpcld 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( N ^ ( P pCnt z ) ) e. RR+ )
163 162 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( N ^ ( P pCnt z ) ) e. RR+ )
164 163 rpge0d 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> 0 <_ ( N ^ ( P pCnt z ) ) )
165 140 141 addge01d 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( 0 <_ ( N ^ ( P pCnt z ) ) <-> ( N ^ ( P pCnt y ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) ) )
166 164 165 mpbid 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( N ^ ( P pCnt y ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
167 166 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( N ^ ( P pCnt y ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
168 134 136 143 160 167 letrd 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt y ) <_ ( P pCnt z ) ) -> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
169 156 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( N ^ ( P pCnt ( y + z ) ) ) e. RR )
170 141 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( N ^ ( P pCnt z ) ) e. RR )
171 142 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) e. RR )
172 126 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> P e. Prime )
173 73 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> z e. QQ )
174 80 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> y e. QQ )
175 simpr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( P pCnt z ) <_ ( P pCnt y ) )
176 172 173 174 175 pcadd 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( P pCnt z ) <_ ( P pCnt ( z + y ) ) )
177 92 94 addcomd 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( y + z ) = ( z + y ) )
178 177 oveq2d 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( P pCnt ( y + z ) ) = ( P pCnt ( z + y ) ) )
179 178 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( P pCnt ( y + z ) ) = ( P pCnt ( z + y ) ) )
180 176 179 breqtrrd 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( P pCnt z ) <_ ( P pCnt ( y + z ) ) )
181 149 121 132 151 ltexp2rd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( P pCnt ( y + z ) ) < ( P pCnt z ) <-> ( N ^ ( P pCnt z ) ) < ( N ^ ( P pCnt ( y + z ) ) ) ) )
182 181 notbid 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( -. ( P pCnt ( y + z ) ) < ( P pCnt z ) <-> -. ( N ^ ( P pCnt z ) ) < ( N ^ ( P pCnt ( y + z ) ) ) ) )
183 122 154 lenltd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( P pCnt z ) <_ ( P pCnt ( y + z ) ) <-> -. ( P pCnt ( y + z ) ) < ( P pCnt z ) ) )
184 156 141 lenltd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( N ^ ( P pCnt ( y + z ) ) ) <_ ( N ^ ( P pCnt z ) ) <-> -. ( N ^ ( P pCnt z ) ) < ( N ^ ( P pCnt ( y + z ) ) ) ) )
185 182 183 184 3bitr4d 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( ( P pCnt z ) <_ ( P pCnt ( y + z ) ) <-> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( N ^ ( P pCnt z ) ) ) )
186 185 biimpa 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt ( y + z ) ) ) -> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( N ^ ( P pCnt z ) ) )
187 180 186 syldan 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( N ^ ( P pCnt z ) ) )
188 161 71 rpexpcld 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( N ^ ( P pCnt y ) ) e. RR+ )
189 188 adantr 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( N ^ ( P pCnt y ) ) e. RR+ )
190 189 rpge0d 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> 0 <_ ( N ^ ( P pCnt y ) ) )
191 141 140 addge02d 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( 0 <_ ( N ^ ( P pCnt y ) ) <-> ( N ^ ( P pCnt z ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) ) )
192 190 191 mpbid 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( N ^ ( P pCnt z ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
193 192 adantr 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( N ^ ( P pCnt z ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
194 169 170 171 187 193 letrd 
 |-  ( ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) /\ ( P pCnt z ) <_ ( P pCnt y ) ) -> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
195 120 122 168 194 lecasei 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> ( N ^ ( P pCnt ( y + z ) ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
196 118 195 eqbrtrd 
 |-  ( ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) /\ ( y + z ) =/= 0 ) -> if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
197 188 162 rpaddcld 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) e. RR+ )
198 197 rpge0d 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> 0 <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
199 116 196 198 pm2.61ne 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) <_ ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
200 eqeq1 
 |-  ( x = ( y + z ) -> ( x = 0 <-> ( y + z ) = 0 ) )
201 oveq2 
 |-  ( x = ( y + z ) -> ( P pCnt x ) = ( P pCnt ( y + z ) ) )
202 201 oveq2d 
 |-  ( x = ( y + z ) -> ( N ^ ( P pCnt x ) ) = ( N ^ ( P pCnt ( y + z ) ) ) )
203 200 202 ifbieq2d 
 |-  ( x = ( y + z ) -> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) = if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) )
204 ovex 
 |-  ( N ^ ( P pCnt ( y + z ) ) ) e. _V
205 42 204 ifex 
 |-  if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) e. _V
206 203 3 205 fvmpt 
 |-  ( ( y + z ) e. QQ -> ( F ` ( y + z ) ) = if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) )
207 128 206 syl 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( F ` ( y + z ) ) = if ( ( y + z ) = 0 , 0 , ( N ^ ( P pCnt ( y + z ) ) ) ) )
208 101 112 oveq12d 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( ( F ` y ) + ( F ` z ) ) = ( ( N ^ ( P pCnt y ) ) + ( N ^ ( P pCnt z ) ) ) )
209 199 207 208 3brtr4d 
 |-  ( ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) /\ ( y e. QQ /\ y =/= 0 ) /\ ( z e. QQ /\ z =/= 0 ) ) -> ( F ` ( y + z ) ) <_ ( ( F ` y ) + ( F ` z ) ) )
210 4 6 10 13 15 18 37 44 64 114 209 isabvd 
 |-  ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> F e. A )