Metamath Proof Explorer

Theorem aks6d1c2p2

Description: Injective condition for countability argument assuming that N is not a prime power. (Contributed by metakunt, 7-Jan-2025)

Ref Expression
Hypotheses aks6d1c2p2.1 
|- ( ph -> N e. NN )
aks6d1c2p2.2 
|- ( ph -> P e. Prime )
aks6d1c2p2.3 
|- ( ph -> P || N )
aks6d1c2p2.4 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c2p2.5 
|- ( ph -> Q e. Prime )
aks6d1c2p2.6 
|- ( ph -> Q || N )
aks6d1c2p2.7 
|- ( ph -> P =/= Q )
Assertion aks6d1c2p2 
|- ( ph -> E : ( NN0 X. NN0 ) -1-1-> NN )

Proof

Step Hyp Ref Expression
1 aks6d1c2p2.1 
 |-  ( ph -> N e. NN )
2 aks6d1c2p2.2 
 |-  ( ph -> P e. Prime )
3 aks6d1c2p2.3 
 |-  ( ph -> P || N )
4 aks6d1c2p2.4 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
5 aks6d1c2p2.5 
 |-  ( ph -> Q e. Prime )
6 aks6d1c2p2.6 
 |-  ( ph -> Q || N )
7 aks6d1c2p2.7 
 |-  ( ph -> P =/= Q )
8 1 2 3 4 aks6d1c2p1 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> NN )
9 neneq 
 |-  ( b =/= d -> -. b = d )
10 9 orcd 
 |-  ( b =/= d -> ( -. b = d \/ -. a = c ) )
11 simpr 
 |-  ( ( b = d /\ a =/= c ) -> a =/= c )
12 11 neneqd 
 |-  ( ( b = d /\ a =/= c ) -> -. a = c )
13 12 olcd 
 |-  ( ( b = d /\ a =/= c ) -> ( -. b = d \/ -. a = c ) )
14 10 13 jaoi 
 |-  ( ( b =/= d \/ ( b = d /\ a =/= c ) ) -> ( -. b = d \/ -. a = c ) )
15 neqne 
 |-  ( -. b = d -> b =/= d )
16 15 orcd 
 |-  ( -. b = d -> ( b =/= d \/ ( b = d /\ a =/= c ) ) )
17 neqne 
 |-  ( -. a = c -> a =/= c )
18 17 anim1ci 
 |-  ( ( -. a = c /\ b = d ) -> ( b = d /\ a =/= c ) )
19 18 olcd 
 |-  ( ( -. a = c /\ b = d ) -> ( b =/= d \/ ( b = d /\ a =/= c ) ) )
20 16 adantl 
 |-  ( ( -. a = c /\ -. b = d ) -> ( b =/= d \/ ( b = d /\ a =/= c ) ) )
21 19 20 pm2.61dan 
 |-  ( -. a = c -> ( b =/= d \/ ( b = d /\ a =/= c ) ) )
22 16 21 jaoi 
 |-  ( ( -. b = d \/ -. a = c ) -> ( b =/= d \/ ( b = d /\ a =/= c ) ) )
23 14 22 impbii 
 |-  ( ( b =/= d \/ ( b = d /\ a =/= c ) ) <-> ( -. b = d \/ -. a = c ) )
24 orcom 
 |-  ( ( -. b = d \/ -. a = c ) <-> ( -. a = c \/ -. b = d ) )
25 23 24 bitri 
 |-  ( ( b =/= d \/ ( b = d /\ a =/= c ) ) <-> ( -. a = c \/ -. b = d ) )
26 ianor 
 |-  ( -. ( a = c /\ b = d ) <-> ( -. a = c \/ -. b = d ) )
27 26 bicomi 
 |-  ( ( -. a = c \/ -. b = d ) <-> -. ( a = c /\ b = d ) )
28 25 27 bitri 
 |-  ( ( b =/= d \/ ( b = d /\ a =/= c ) ) <-> -. ( a = c /\ b = d ) )
29 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> Q e. Prime )
30 simpr 
 |-  ( ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) /\ p = Q ) -> p = Q )
31 30 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) /\ p = Q ) -> ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( Q pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) )
32 30 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) /\ p = Q ) -> ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) = ( Q pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
33 31 32 neeq12d 
 |-  ( ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) /\ p = Q ) -> ( ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) <-> ( Q pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( Q pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
34 0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> 0 e. CC )
35 prmnn 
 |-  ( P e. Prime -> P e. NN )
36 2 35 syl 
 |-  ( ph -> P e. NN )
37 1 36 jca 
 |-  ( ph -> ( N e. NN /\ P e. NN ) )
38 nndivdvds 
 |-  ( ( N e. NN /\ P e. NN ) -> ( P || N <-> ( N / P ) e. NN ) )
39 37 38 syl 
 |-  ( ph -> ( P || N <-> ( N / P ) e. NN ) )
40 3 39 mpbid 
 |-  ( ph -> ( N / P ) e. NN )
41 40 adantr 
 |-  ( ( ph /\ a e. NN0 ) -> ( N / P ) e. NN )
42 41 adantr 
 |-  ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) -> ( N / P ) e. NN )
43 42 ad2antrr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( N / P ) e. NN )
44 43 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( N / P ) e. NN )
45 simp-4r 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> b e. NN0 )
46 44 45 nnexpcld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( ( N / P ) ^ b ) e. NN )
47 29 46 pccld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( N / P ) ^ b ) ) e. NN0 )
48 47 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( N / P ) ^ b ) ) e. CC )
49 simplr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> d e. NN0 )
50 44 49 nnexpcld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( ( N / P ) ^ d ) e. NN )
51 29 50 pccld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( N / P ) ^ d ) ) e. NN0 )
52 51 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( N / P ) ^ d ) ) e. CC )
53 simpr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> b =/= d )
54 45 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> b e. CC )
55 49 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> d e. CC )
56 29 44 pccld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( N / P ) ) e. NN0 )
57 56 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( N / P ) ) e. CC )
58 simp-5l 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ph )
59 1 nncnd 
 |-  ( ph -> N e. CC )
60 36 nncnd 
 |-  ( ph -> P e. CC )
61 36 nnne0d 
 |-  ( ph -> P =/= 0 )
62 59 60 61 divcan2d 
 |-  ( ph -> ( P x. ( N / P ) ) = N )
63 62 eqcomd 
 |-  ( ph -> N = ( P x. ( N / P ) ) )
64 63 breq2d 
 |-  ( ph -> ( Q || N <-> Q || ( P x. ( N / P ) ) ) )
65 6 64 mpbid 
 |-  ( ph -> Q || ( P x. ( N / P ) ) )
66 36 nnzd 
 |-  ( ph -> P e. ZZ )
67 40 nnzd 
 |-  ( ph -> ( N / P ) e. ZZ )
68 euclemma 
 |-  ( ( Q e. Prime /\ P e. ZZ /\ ( N / P ) e. ZZ ) -> ( Q || ( P x. ( N / P ) ) <-> ( Q || P \/ Q || ( N / P ) ) ) )
69 5 66 67 68 syl3anc 
 |-  ( ph -> ( Q || ( P x. ( N / P ) ) <-> ( Q || P \/ Q || ( N / P ) ) ) )
70 69 biimpd 
 |-  ( ph -> ( Q || ( P x. ( N / P ) ) -> ( Q || P \/ Q || ( N / P ) ) ) )
71 65 70 mpd 
 |-  ( ph -> ( Q || P \/ Q || ( N / P ) ) )
72 necom 
 |-  ( P =/= Q <-> Q =/= P )
73 72 imbi2i 
 |-  ( ( ph -> P =/= Q ) <-> ( ph -> Q =/= P ) )
74 7 73 mpbi 
 |-  ( ph -> Q =/= P )
75 74 neneqd 
 |-  ( ph -> -. Q = P )
76 1red 
 |-  ( ph -> 1 e. RR )
77 prmgt1 
 |-  ( Q e. Prime -> 1 < Q )
78 5 77 syl 
 |-  ( ph -> 1 < Q )
79 76 78 ltned 
 |-  ( ph -> 1 =/= Q )
80 79 necomd 
 |-  ( ph -> Q =/= 1 )
81 80 neneqd 
 |-  ( ph -> -. Q = 1 )
82 75 81 jca 
 |-  ( ph -> ( -. Q = P /\ -. Q = 1 ) )
83 pm4.56 
 |-  ( ( -. Q = P /\ -. Q = 1 ) <-> -. ( Q = P \/ Q = 1 ) )
84 82 83 sylib 
 |-  ( ph -> -. ( Q = P \/ Q = 1 ) )
85 prmnn 
 |-  ( Q e. Prime -> Q e. NN )
86 5 85 syl 
 |-  ( ph -> Q e. NN )
87 dvdsprime 
 |-  ( ( P e. Prime /\ Q e. NN ) -> ( Q || P <-> ( Q = P \/ Q = 1 ) ) )
88 2 86 87 syl2anc 
 |-  ( ph -> ( Q || P <-> ( Q = P \/ Q = 1 ) ) )
89 84 88 mtbird 
 |-  ( ph -> -. Q || P )
90 71 89 orcnd 
 |-  ( ph -> Q || ( N / P ) )
91 5 40 jca 
 |-  ( ph -> ( Q e. Prime /\ ( N / P ) e. NN ) )
92 pcelnn 
 |-  ( ( Q e. Prime /\ ( N / P ) e. NN ) -> ( ( Q pCnt ( N / P ) ) e. NN <-> Q || ( N / P ) ) )
93 91 92 syl 
 |-  ( ph -> ( ( Q pCnt ( N / P ) ) e. NN <-> Q || ( N / P ) ) )
94 90 93 mpbird 
 |-  ( ph -> ( Q pCnt ( N / P ) ) e. NN )
95 58 94 syl 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( N / P ) ) e. NN )
96 95 nnne0d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( N / P ) ) =/= 0 )
97 54 55 57 96 mulcan2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( ( b x. ( Q pCnt ( N / P ) ) ) = ( d x. ( Q pCnt ( N / P ) ) ) <-> b = d ) )
98 97 necon3bid 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( ( b x. ( Q pCnt ( N / P ) ) ) =/= ( d x. ( Q pCnt ( N / P ) ) ) <-> b =/= d ) )
99 53 98 mpbird 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( b x. ( Q pCnt ( N / P ) ) ) =/= ( d x. ( Q pCnt ( N / P ) ) ) )
100 5 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> Q e. Prime )
101 nnq 
 |-  ( ( N / P ) e. NN -> ( N / P ) e. QQ )
102 43 101 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( N / P ) e. QQ )
103 1 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> N e. NN )
104 103 nncnd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> N e. CC )
105 36 adantr 
 |-  ( ( ph /\ a e. NN0 ) -> P e. NN )
106 105 adantr 
 |-  ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) -> P e. NN )
107 106 ad2antrr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> P e. NN )
108 107 nncnd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> P e. CC )
109 103 nnne0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> N =/= 0 )
110 107 nnne0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> P =/= 0 )
111 104 108 109 110 divne0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( N / P ) =/= 0 )
112 102 111 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( N / P ) e. QQ /\ ( N / P ) =/= 0 ) )
113 simpllr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> b e. NN0 )
114 113 nn0zd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> b e. ZZ )
115 100 112 114 3jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q e. Prime /\ ( ( N / P ) e. QQ /\ ( N / P ) =/= 0 ) /\ b e. ZZ ) )
116 pcexp 
 |-  ( ( Q e. Prime /\ ( ( N / P ) e. QQ /\ ( N / P ) =/= 0 ) /\ b e. ZZ ) -> ( Q pCnt ( ( N / P ) ^ b ) ) = ( b x. ( Q pCnt ( N / P ) ) ) )
117 115 116 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q pCnt ( ( N / P ) ^ b ) ) = ( b x. ( Q pCnt ( N / P ) ) ) )
118 117 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( N / P ) ^ b ) ) = ( b x. ( Q pCnt ( N / P ) ) ) )
119 118 eqcomd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( b x. ( Q pCnt ( N / P ) ) ) = ( Q pCnt ( ( N / P ) ^ b ) ) )
120 simpr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> d e. NN0 )
121 120 nn0zd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> d e. ZZ )
122 100 112 121 3jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q e. Prime /\ ( ( N / P ) e. QQ /\ ( N / P ) =/= 0 ) /\ d e. ZZ ) )
123 pcexp 
 |-  ( ( Q e. Prime /\ ( ( N / P ) e. QQ /\ ( N / P ) =/= 0 ) /\ d e. ZZ ) -> ( Q pCnt ( ( N / P ) ^ d ) ) = ( d x. ( Q pCnt ( N / P ) ) ) )
124 122 123 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q pCnt ( ( N / P ) ^ d ) ) = ( d x. ( Q pCnt ( N / P ) ) ) )
125 124 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( N / P ) ^ d ) ) = ( d x. ( Q pCnt ( N / P ) ) ) )
126 125 eqcomd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( d x. ( Q pCnt ( N / P ) ) ) = ( Q pCnt ( ( N / P ) ^ d ) ) )
127 99 119 126 3netr3d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( N / P ) ^ b ) ) =/= ( Q pCnt ( ( N / P ) ^ d ) ) )
128 34 48 52 127 addneintrd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( 0 + ( Q pCnt ( ( N / P ) ^ b ) ) ) =/= ( 0 + ( Q pCnt ( ( N / P ) ^ d ) ) ) )
129 75 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> -. Q = P )
130 2 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> P e. Prime )
131 simp-4r 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> a e. NN0 )
132 prmdvdsexpr 
 |-  ( ( Q e. Prime /\ P e. Prime /\ a e. NN0 ) -> ( Q || ( P ^ a ) -> Q = P ) )
133 100 130 131 132 syl3anc 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q || ( P ^ a ) -> Q = P ) )
134 133 con3d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( -. Q = P -> -. Q || ( P ^ a ) ) )
135 129 134 mpd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> -. Q || ( P ^ a ) )
136 simplr 
 |-  ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) -> a e. NN0 )
137 106 136 nnexpcld 
 |-  ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) -> ( P ^ a ) e. NN )
138 137 ad2antrr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P ^ a ) e. NN )
139 100 138 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q e. Prime /\ ( P ^ a ) e. NN ) )
140 pceq0 
 |-  ( ( Q e. Prime /\ ( P ^ a ) e. NN ) -> ( ( Q pCnt ( P ^ a ) ) = 0 <-> -. Q || ( P ^ a ) ) )
141 139 140 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( Q pCnt ( P ^ a ) ) = 0 <-> -. Q || ( P ^ a ) ) )
142 135 141 mpbird 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q pCnt ( P ^ a ) ) = 0 )
143 142 eqcomd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> 0 = ( Q pCnt ( P ^ a ) ) )
144 143 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( 0 + ( Q pCnt ( ( N / P ) ^ b ) ) ) = ( ( Q pCnt ( P ^ a ) ) + ( Q pCnt ( ( N / P ) ^ b ) ) ) )
145 144 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( 0 + ( Q pCnt ( ( N / P ) ^ b ) ) ) = ( ( Q pCnt ( P ^ a ) ) + ( Q pCnt ( ( N / P ) ^ b ) ) ) )
146 simplr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> c e. NN0 )
147 prmdvdsexpr 
 |-  ( ( Q e. Prime /\ P e. Prime /\ c e. NN0 ) -> ( Q || ( P ^ c ) -> Q = P ) )
148 100 130 146 147 syl3anc 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q || ( P ^ c ) -> Q = P ) )
149 129 148 mtod 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> -. Q || ( P ^ c ) )
150 107 146 nnexpcld 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P ^ c ) e. NN )
151 100 150 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q e. Prime /\ ( P ^ c ) e. NN ) )
152 pceq0 
 |-  ( ( Q e. Prime /\ ( P ^ c ) e. NN ) -> ( ( Q pCnt ( P ^ c ) ) = 0 <-> -. Q || ( P ^ c ) ) )
153 151 152 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( Q pCnt ( P ^ c ) ) = 0 <-> -. Q || ( P ^ c ) ) )
154 149 153 mpbird 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q pCnt ( P ^ c ) ) = 0 )
155 154 eqcomd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> 0 = ( Q pCnt ( P ^ c ) ) )
156 155 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( 0 + ( Q pCnt ( ( N / P ) ^ d ) ) ) = ( ( Q pCnt ( P ^ c ) ) + ( Q pCnt ( ( N / P ) ^ d ) ) ) )
157 156 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( 0 + ( Q pCnt ( ( N / P ) ^ d ) ) ) = ( ( Q pCnt ( P ^ c ) ) + ( Q pCnt ( ( N / P ) ^ d ) ) ) )
158 128 145 157 3netr3d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( ( Q pCnt ( P ^ a ) ) + ( Q pCnt ( ( N / P ) ^ b ) ) ) =/= ( ( Q pCnt ( P ^ c ) ) + ( Q pCnt ( ( N / P ) ^ d ) ) ) )
159 107 nnzd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> P e. ZZ )
160 159 131 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P e. ZZ /\ a e. NN0 ) )
161 zexpcl 
 |-  ( ( P e. ZZ /\ a e. NN0 ) -> ( P ^ a ) e. ZZ )
162 160 161 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P ^ a ) e. ZZ )
163 131 nn0zd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> a e. ZZ )
164 108 110 163 expne0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P ^ a ) =/= 0 )
165 162 164 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( P ^ a ) e. ZZ /\ ( P ^ a ) =/= 0 ) )
166 43 nnzd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( N / P ) e. ZZ )
167 166 113 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( N / P ) e. ZZ /\ b e. NN0 ) )
168 zexpcl 
 |-  ( ( ( N / P ) e. ZZ /\ b e. NN0 ) -> ( ( N / P ) ^ b ) e. ZZ )
169 167 168 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( N / P ) ^ b ) e. ZZ )
170 104 108 110 divcld 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( N / P ) e. CC )
171 170 111 114 expne0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( N / P ) ^ b ) =/= 0 )
172 169 171 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( N / P ) ^ b ) e. ZZ /\ ( ( N / P ) ^ b ) =/= 0 ) )
173 100 165 172 3jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q e. Prime /\ ( ( P ^ a ) e. ZZ /\ ( P ^ a ) =/= 0 ) /\ ( ( ( N / P ) ^ b ) e. ZZ /\ ( ( N / P ) ^ b ) =/= 0 ) ) )
174 pcmul 
 |-  ( ( Q e. Prime /\ ( ( P ^ a ) e. ZZ /\ ( P ^ a ) =/= 0 ) /\ ( ( ( N / P ) ^ b ) e. ZZ /\ ( ( N / P ) ^ b ) =/= 0 ) ) -> ( Q pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( ( Q pCnt ( P ^ a ) ) + ( Q pCnt ( ( N / P ) ^ b ) ) ) )
175 173 174 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( ( Q pCnt ( P ^ a ) ) + ( Q pCnt ( ( N / P ) ^ b ) ) ) )
176 175 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( ( Q pCnt ( P ^ a ) ) + ( Q pCnt ( ( N / P ) ^ b ) ) ) )
177 176 eqcomd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( ( Q pCnt ( P ^ a ) ) + ( Q pCnt ( ( N / P ) ^ b ) ) ) = ( Q pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) )
178 150 nnzd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P ^ c ) e. ZZ )
179 150 nnne0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P ^ c ) =/= 0 )
180 178 179 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( P ^ c ) e. ZZ /\ ( P ^ c ) =/= 0 ) )
181 43 120 nnexpcld 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( N / P ) ^ d ) e. NN )
182 181 nnzd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( N / P ) ^ d ) e. ZZ )
183 181 nnne0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( N / P ) ^ d ) =/= 0 )
184 182 183 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( N / P ) ^ d ) e. ZZ /\ ( ( N / P ) ^ d ) =/= 0 ) )
185 100 180 184 3jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q e. Prime /\ ( ( P ^ c ) e. ZZ /\ ( P ^ c ) =/= 0 ) /\ ( ( ( N / P ) ^ d ) e. ZZ /\ ( ( N / P ) ^ d ) =/= 0 ) ) )
186 pcmul 
 |-  ( ( Q e. Prime /\ ( ( P ^ c ) e. ZZ /\ ( P ^ c ) =/= 0 ) /\ ( ( ( N / P ) ^ d ) e. ZZ /\ ( ( N / P ) ^ d ) =/= 0 ) ) -> ( Q pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) = ( ( Q pCnt ( P ^ c ) ) + ( Q pCnt ( ( N / P ) ^ d ) ) ) )
187 185 186 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( Q pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) = ( ( Q pCnt ( P ^ c ) ) + ( Q pCnt ( ( N / P ) ^ d ) ) ) )
188 187 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) = ( ( Q pCnt ( P ^ c ) ) + ( Q pCnt ( ( N / P ) ^ d ) ) ) )
189 188 eqcomd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( ( Q pCnt ( P ^ c ) ) + ( Q pCnt ( ( N / P ) ^ d ) ) ) = ( Q pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
190 158 177 189 3netr3d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> ( Q pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( Q pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
191 29 33 190 rspcedvd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ b =/= d ) -> E. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
192 2 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> P e. Prime )
193 simpr 
 |-  ( ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) /\ p = P ) -> p = P )
194 193 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) /\ p = P ) -> ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( P pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) )
195 193 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) /\ p = P ) -> ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) = ( P pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
196 194 195 neeq12d 
 |-  ( ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) /\ p = P ) -> ( ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) <-> ( P pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( P pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
197 130 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> P e. Prime )
198 197 35 syl 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> P e. NN )
199 simp-5r 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> a e. NN0 )
200 198 199 nnexpcld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P ^ a ) e. NN )
201 197 200 pccld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( P ^ a ) ) e. NN0 )
202 201 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( P ^ a ) ) e. CC )
203 simpllr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> c e. NN0 )
204 198 203 nnexpcld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P ^ c ) e. NN )
205 197 204 pccld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( P ^ c ) ) e. NN0 )
206 205 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( P ^ c ) ) e. CC )
207 43 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( N / P ) e. NN )
208 simp-4r 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> b e. NN0 )
209 207 208 nnexpcld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( ( N / P ) ^ b ) e. NN )
210 197 209 pccld 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( ( N / P ) ^ b ) ) e. NN0 )
211 210 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( ( N / P ) ^ b ) ) e. CC )
212 11 adantl 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> a =/= c )
213 197 199 jca 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P e. Prime /\ a e. NN0 ) )
214 pcidlem 
 |-  ( ( P e. Prime /\ a e. NN0 ) -> ( P pCnt ( P ^ a ) ) = a )
215 213 214 syl 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( P ^ a ) ) = a )
216 215 eqcomd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> a = ( P pCnt ( P ^ a ) ) )
217 197 203 jca 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P e. Prime /\ c e. NN0 ) )
218 pcidlem 
 |-  ( ( P e. Prime /\ c e. NN0 ) -> ( P pCnt ( P ^ c ) ) = c )
219 217 218 syl 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( P ^ c ) ) = c )
220 219 eqcomd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> c = ( P pCnt ( P ^ c ) ) )
221 212 216 220 3netr3d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( P ^ a ) ) =/= ( P pCnt ( P ^ c ) ) )
222 202 206 211 221 addneintr2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( ( P pCnt ( P ^ a ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) =/= ( ( P pCnt ( P ^ c ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) )
223 eqidd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( ( P pCnt ( P ^ a ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) = ( ( P pCnt ( P ^ a ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) )
224 simprl 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> b = d )
225 224 oveq2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( ( N / P ) ^ b ) = ( ( N / P ) ^ d ) )
226 225 oveq2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( ( N / P ) ^ b ) ) = ( P pCnt ( ( N / P ) ^ d ) ) )
227 226 oveq2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( ( P pCnt ( P ^ c ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) = ( ( P pCnt ( P ^ c ) ) + ( P pCnt ( ( N / P ) ^ d ) ) ) )
228 222 223 227 3netr3d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( ( P pCnt ( P ^ a ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) =/= ( ( P pCnt ( P ^ c ) ) + ( P pCnt ( ( N / P ) ^ d ) ) ) )
229 130 165 172 3jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P e. Prime /\ ( ( P ^ a ) e. ZZ /\ ( P ^ a ) =/= 0 ) /\ ( ( ( N / P ) ^ b ) e. ZZ /\ ( ( N / P ) ^ b ) =/= 0 ) ) )
230 pcmul 
 |-  ( ( P e. Prime /\ ( ( P ^ a ) e. ZZ /\ ( P ^ a ) =/= 0 ) /\ ( ( ( N / P ) ^ b ) e. ZZ /\ ( ( N / P ) ^ b ) =/= 0 ) ) -> ( P pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( ( P pCnt ( P ^ a ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) )
231 229 230 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( ( P pCnt ( P ^ a ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) )
232 231 eqcomd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( P pCnt ( P ^ a ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) = ( P pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) )
233 232 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( ( P pCnt ( P ^ a ) ) + ( P pCnt ( ( N / P ) ^ b ) ) ) = ( P pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) )
234 130 180 184 3jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( P e. Prime /\ ( ( P ^ c ) e. ZZ /\ ( P ^ c ) =/= 0 ) /\ ( ( ( N / P ) ^ d ) e. ZZ /\ ( ( N / P ) ^ d ) =/= 0 ) ) )
235 pcmul 
 |-  ( ( P e. Prime /\ ( ( P ^ c ) e. ZZ /\ ( P ^ c ) =/= 0 ) /\ ( ( ( N / P ) ^ d ) e. ZZ /\ ( ( N / P ) ^ d ) =/= 0 ) ) -> ( P pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) = ( ( P pCnt ( P ^ c ) ) + ( P pCnt ( ( N / P ) ^ d ) ) ) )
236 235 eqcomd 
 |-  ( ( P e. Prime /\ ( ( P ^ c ) e. ZZ /\ ( P ^ c ) =/= 0 ) /\ ( ( ( N / P ) ^ d ) e. ZZ /\ ( ( N / P ) ^ d ) =/= 0 ) ) -> ( ( P pCnt ( P ^ c ) ) + ( P pCnt ( ( N / P ) ^ d ) ) ) = ( P pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
237 234 236 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( P pCnt ( P ^ c ) ) + ( P pCnt ( ( N / P ) ^ d ) ) ) = ( P pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
238 237 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( ( P pCnt ( P ^ c ) ) + ( P pCnt ( ( N / P ) ^ d ) ) ) = ( P pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
239 228 233 238 3netr3d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> ( P pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( P pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
240 192 196 239 rspcedvd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b = d /\ a =/= c ) ) -> E. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
241 191 240 jaodan 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b =/= d \/ ( b = d /\ a =/= c ) ) ) -> E. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
242 biidd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) = ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) = ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
243 242 necon3abid 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> -. ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) = ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
244 simpr 
 |-  ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) -> b e. NN0 )
245 42 244 nnexpcld 
 |-  ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) -> ( ( N / P ) ^ b ) e. NN )
246 137 245 nnmulcld 
 |-  ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) -> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) e. NN )
247 246 adantr 
 |-  ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) -> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) e. NN )
248 247 adantr 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) e. NN )
249 248 nnnn0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) e. NN0 )
250 150 181 nnmulcld 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) e. NN )
251 250 nnnn0d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) e. NN0 )
252 249 251 jca 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) e. NN0 /\ ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) e. NN0 ) )
253 pc11 
 |-  ( ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) e. NN0 /\ ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) e. NN0 ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) = ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> A. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
254 252 253 syl 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) = ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> A. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
255 254 notbid 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( -. ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) = ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> -. A. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
256 243 255 bitrd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> -. A. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
257 rexnal 
 |-  ( E. p e. Prime -. ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) <-> -. A. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
258 257 bicomi 
 |-  ( -. A. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) <-> E. p e. Prime -. ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
259 258 a1i 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( -. A. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) <-> E. p e. Prime -. ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
260 256 259 bitrd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> E. p e. Prime -. ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
261 biidd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) <-> ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
262 261 necon3bbid 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( -. ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) <-> ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
263 262 rexbidv 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( E. p e. Prime -. ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) = ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) <-> E. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
264 260 263 bitrd 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> E. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
265 264 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b =/= d \/ ( b = d /\ a =/= c ) ) ) -> ( ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) <-> E. p e. Prime ( p pCnt ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) ) =/= ( p pCnt ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) ) )
266 241 265 mpbird 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( b =/= d \/ ( b = d /\ a =/= c ) ) ) -> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) )
267 28 266 sylan2br 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ -. ( a = c /\ b = d ) ) -> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) )
268 4 a1i 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) )
269 simprl 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = a /\ l = b ) ) -> k = a )
270 269 oveq2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = a /\ l = b ) ) -> ( P ^ k ) = ( P ^ a ) )
271 simprr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = a /\ l = b ) ) -> l = b )
272 271 oveq2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = a /\ l = b ) ) -> ( ( N / P ) ^ l ) = ( ( N / P ) ^ b ) )
273 270 272 oveq12d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = a /\ l = b ) ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) = ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) )
274 268 273 131 113 248 ovmpod 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( a E b ) = ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) )
275 simprl 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = c /\ l = d ) ) -> k = c )
276 275 oveq2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = c /\ l = d ) ) -> ( P ^ k ) = ( P ^ c ) )
277 simprr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = c /\ l = d ) ) -> l = d )
278 277 oveq2d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = c /\ l = d ) ) -> ( ( N / P ) ^ l ) = ( ( N / P ) ^ d ) )
279 276 278 oveq12d 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ ( k = c /\ l = d ) ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) = ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) )
280 268 279 146 120 250 ovmpod 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( c E d ) = ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) )
281 274 280 neeq12d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( a E b ) =/= ( c E d ) <-> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
282 281 adantr 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ -. ( a = c /\ b = d ) ) -> ( ( a E b ) =/= ( c E d ) <-> ( ( P ^ a ) x. ( ( N / P ) ^ b ) ) =/= ( ( P ^ c ) x. ( ( N / P ) ^ d ) ) ) )
283 267 282 mpbird 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ -. ( a = c /\ b = d ) ) -> ( a E b ) =/= ( c E d ) )
284 283 neneqd 
 |-  ( ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ -. ( a = c /\ b = d ) ) -> -. ( a E b ) = ( c E d ) )
285 284 ex 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( -. ( a = c /\ b = d ) -> -. ( a E b ) = ( c E d ) ) )
286 285 con4d 
 |-  ( ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) -> ( ( a E b ) = ( c E d ) -> ( a = c /\ b = d ) ) )
287 286 ralrimiva 
 |-  ( ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) /\ c e. NN0 ) -> A. d e. NN0 ( ( a E b ) = ( c E d ) -> ( a = c /\ b = d ) ) )
288 287 ralrimiva 
 |-  ( ( ( ph /\ a e. NN0 ) /\ b e. NN0 ) -> A. c e. NN0 A. d e. NN0 ( ( a E b ) = ( c E d ) -> ( a = c /\ b = d ) ) )
289 288 ralrimiva 
 |-  ( ( ph /\ a e. NN0 ) -> A. b e. NN0 A. c e. NN0 A. d e. NN0 ( ( a E b ) = ( c E d ) -> ( a = c /\ b = d ) ) )
290 289 ralrimiva 
 |-  ( ph -> A. a e. NN0 A. b e. NN0 A. c e. NN0 A. d e. NN0 ( ( a E b ) = ( c E d ) -> ( a = c /\ b = d ) ) )
291 8 290 jca 
 |-  ( ph -> ( E : ( NN0 X. NN0 ) --> NN /\ A. a e. NN0 A. b e. NN0 A. c e. NN0 A. d e. NN0 ( ( a E b ) = ( c E d ) -> ( a = c /\ b = d ) ) ) )
292 f1opr 
 |-  ( E : ( NN0 X. NN0 ) -1-1-> NN <-> ( E : ( NN0 X. NN0 ) --> NN /\ A. a e. NN0 A. b e. NN0 A. c e. NN0 A. d e. NN0 ( ( a E b ) = ( c E d ) -> ( a = c /\ b = d ) ) ) )
293 291 292 sylibr 
 |-  ( ph -> E : ( NN0 X. NN0 ) -1-1-> NN )