Metamath Proof Explorer

Theorem prmpwdvds

Description: A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014)

Ref Expression
Assertion prmpwdvds 
|- ( ( ( K e. ZZ /\ D e. ZZ ) /\ ( P e. Prime /\ N e. NN ) /\ ( D || ( K x. ( P ^ N ) ) /\ -. D || ( K x. ( P ^ ( N - 1 ) ) ) ) ) -> ( P ^ N ) || D )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( k = K -> ( k x. ( P ^ N ) ) = ( K x. ( P ^ N ) ) )
2 1 breq2d 
 |-  ( k = K -> ( D || ( k x. ( P ^ N ) ) <-> D || ( K x. ( P ^ N ) ) ) )
3 oveq1 
 |-  ( k = K -> ( k x. ( P ^ ( N - 1 ) ) ) = ( K x. ( P ^ ( N - 1 ) ) ) )
4 3 breq2d 
 |-  ( k = K -> ( D || ( k x. ( P ^ ( N - 1 ) ) ) <-> D || ( K x. ( P ^ ( N - 1 ) ) ) ) )
5 4 notbid 
 |-  ( k = K -> ( -. D || ( k x. ( P ^ ( N - 1 ) ) ) <-> -. D || ( K x. ( P ^ ( N - 1 ) ) ) ) )
6 2 5 anbi12d 
 |-  ( k = K -> ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) <-> ( D || ( K x. ( P ^ N ) ) /\ -. D || ( K x. ( P ^ ( N - 1 ) ) ) ) ) )
7 6 imbi1d 
 |-  ( k = K -> ( ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) <-> ( ( D || ( K x. ( P ^ N ) ) /\ -. D || ( K x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) ) )
8 oveq2 
 |-  ( x = 1 -> ( P ^ x ) = ( P ^ 1 ) )
9 8 oveq2d 
 |-  ( x = 1 -> ( k x. ( P ^ x ) ) = ( k x. ( P ^ 1 ) ) )
10 9 breq2d 
 |-  ( x = 1 -> ( D || ( k x. ( P ^ x ) ) <-> D || ( k x. ( P ^ 1 ) ) ) )
11 oveq1 
 |-  ( x = 1 -> ( x - 1 ) = ( 1 - 1 ) )
12 11 oveq2d 
 |-  ( x = 1 -> ( P ^ ( x - 1 ) ) = ( P ^ ( 1 - 1 ) ) )
13 12 oveq2d 
 |-  ( x = 1 -> ( k x. ( P ^ ( x - 1 ) ) ) = ( k x. ( P ^ ( 1 - 1 ) ) ) )
14 13 breq2d 
 |-  ( x = 1 -> ( D || ( k x. ( P ^ ( x - 1 ) ) ) <-> D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) )
15 14 notbid 
 |-  ( x = 1 -> ( -. D || ( k x. ( P ^ ( x - 1 ) ) ) <-> -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) )
16 10 15 anbi12d 
 |-  ( x = 1 -> ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) <-> ( D || ( k x. ( P ^ 1 ) ) /\ -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) ) )
17 8 breq1d 
 |-  ( x = 1 -> ( ( P ^ x ) || D <-> ( P ^ 1 ) || D ) )
18 16 17 imbi12d 
 |-  ( x = 1 -> ( ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) <-> ( ( D || ( k x. ( P ^ 1 ) ) /\ -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) -> ( P ^ 1 ) || D ) ) )
19 18 ralbidv 
 |-  ( x = 1 -> ( A. k e. ZZ ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) <-> A. k e. ZZ ( ( D || ( k x. ( P ^ 1 ) ) /\ -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) -> ( P ^ 1 ) || D ) ) )
20 19 imbi2d 
 |-  ( x = 1 -> ( ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) ) <-> ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ 1 ) ) /\ -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) -> ( P ^ 1 ) || D ) ) ) )
21 oveq2 
 |-  ( x = n -> ( P ^ x ) = ( P ^ n ) )
22 21 oveq2d 
 |-  ( x = n -> ( k x. ( P ^ x ) ) = ( k x. ( P ^ n ) ) )
23 22 breq2d 
 |-  ( x = n -> ( D || ( k x. ( P ^ x ) ) <-> D || ( k x. ( P ^ n ) ) ) )
24 oveq1 
 |-  ( x = n -> ( x - 1 ) = ( n - 1 ) )
25 24 oveq2d 
 |-  ( x = n -> ( P ^ ( x - 1 ) ) = ( P ^ ( n - 1 ) ) )
26 25 oveq2d 
 |-  ( x = n -> ( k x. ( P ^ ( x - 1 ) ) ) = ( k x. ( P ^ ( n - 1 ) ) ) )
27 26 breq2d 
 |-  ( x = n -> ( D || ( k x. ( P ^ ( x - 1 ) ) ) <-> D || ( k x. ( P ^ ( n - 1 ) ) ) ) )
28 27 notbid 
 |-  ( x = n -> ( -. D || ( k x. ( P ^ ( x - 1 ) ) ) <-> -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) )
29 23 28 anbi12d 
 |-  ( x = n -> ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) <-> ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) ) )
30 21 breq1d 
 |-  ( x = n -> ( ( P ^ x ) || D <-> ( P ^ n ) || D ) )
31 29 30 imbi12d 
 |-  ( x = n -> ( ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) <-> ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) ) )
32 31 ralbidv 
 |-  ( x = n -> ( A. k e. ZZ ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) <-> A. k e. ZZ ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) ) )
33 32 imbi2d 
 |-  ( x = n -> ( ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) ) <-> ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) ) ) )
34 oveq2 
 |-  ( x = ( n + 1 ) -> ( P ^ x ) = ( P ^ ( n + 1 ) ) )
35 34 oveq2d 
 |-  ( x = ( n + 1 ) -> ( k x. ( P ^ x ) ) = ( k x. ( P ^ ( n + 1 ) ) ) )
36 35 breq2d 
 |-  ( x = ( n + 1 ) -> ( D || ( k x. ( P ^ x ) ) <-> D || ( k x. ( P ^ ( n + 1 ) ) ) ) )
37 oveq1 
 |-  ( x = ( n + 1 ) -> ( x - 1 ) = ( ( n + 1 ) - 1 ) )
38 37 oveq2d 
 |-  ( x = ( n + 1 ) -> ( P ^ ( x - 1 ) ) = ( P ^ ( ( n + 1 ) - 1 ) ) )
39 38 oveq2d 
 |-  ( x = ( n + 1 ) -> ( k x. ( P ^ ( x - 1 ) ) ) = ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) )
40 39 breq2d 
 |-  ( x = ( n + 1 ) -> ( D || ( k x. ( P ^ ( x - 1 ) ) ) <-> D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) )
41 40 notbid 
 |-  ( x = ( n + 1 ) -> ( -. D || ( k x. ( P ^ ( x - 1 ) ) ) <-> -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) )
42 36 41 anbi12d 
 |-  ( x = ( n + 1 ) -> ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) <-> ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) ) )
43 34 breq1d 
 |-  ( x = ( n + 1 ) -> ( ( P ^ x ) || D <-> ( P ^ ( n + 1 ) ) || D ) )
44 42 43 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) <-> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
45 44 ralbidv 
 |-  ( x = ( n + 1 ) -> ( A. k e. ZZ ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) <-> A. k e. ZZ ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
46 45 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) ) <-> ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) ) )
47 oveq2 
 |-  ( x = N -> ( P ^ x ) = ( P ^ N ) )
48 47 oveq2d 
 |-  ( x = N -> ( k x. ( P ^ x ) ) = ( k x. ( P ^ N ) ) )
49 48 breq2d 
 |-  ( x = N -> ( D || ( k x. ( P ^ x ) ) <-> D || ( k x. ( P ^ N ) ) ) )
50 oveq1 
 |-  ( x = N -> ( x - 1 ) = ( N - 1 ) )
51 50 oveq2d 
 |-  ( x = N -> ( P ^ ( x - 1 ) ) = ( P ^ ( N - 1 ) ) )
52 51 oveq2d 
 |-  ( x = N -> ( k x. ( P ^ ( x - 1 ) ) ) = ( k x. ( P ^ ( N - 1 ) ) ) )
53 52 breq2d 
 |-  ( x = N -> ( D || ( k x. ( P ^ ( x - 1 ) ) ) <-> D || ( k x. ( P ^ ( N - 1 ) ) ) ) )
54 53 notbid 
 |-  ( x = N -> ( -. D || ( k x. ( P ^ ( x - 1 ) ) ) <-> -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) )
55 49 54 anbi12d 
 |-  ( x = N -> ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) <-> ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) ) )
56 47 breq1d 
 |-  ( x = N -> ( ( P ^ x ) || D <-> ( P ^ N ) || D ) )
57 55 56 imbi12d 
 |-  ( x = N -> ( ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) <-> ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) ) )
58 57 ralbidv 
 |-  ( x = N -> ( A. k e. ZZ ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) <-> A. k e. ZZ ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) ) )
59 58 imbi2d 
 |-  ( x = N -> ( ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ x ) ) /\ -. D || ( k x. ( P ^ ( x - 1 ) ) ) ) -> ( P ^ x ) || D ) ) <-> ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) ) ) )
60 breq1 
 |-  ( x = D -> ( x || ( k x. P ) <-> D || ( k x. P ) ) )
61 breq1 
 |-  ( x = D -> ( x || k <-> D || k ) )
62 61 notbid 
 |-  ( x = D -> ( -. x || k <-> -. D || k ) )
63 60 62 anbi12d 
 |-  ( x = D -> ( ( x || ( k x. P ) /\ -. x || k ) <-> ( D || ( k x. P ) /\ -. D || k ) ) )
64 breq2 
 |-  ( x = D -> ( P || x <-> P || D ) )
65 63 64 imbi12d 
 |-  ( x = D -> ( ( ( x || ( k x. P ) /\ -. x || k ) -> P || x ) <-> ( ( D || ( k x. P ) /\ -. D || k ) -> P || D ) ) )
66 65 imbi2d 
 |-  ( x = D -> ( ( ( P e. Prime /\ k e. ZZ ) -> ( ( x || ( k x. P ) /\ -. x || k ) -> P || x ) ) <-> ( ( P e. Prime /\ k e. ZZ ) -> ( ( D || ( k x. P ) /\ -. D || k ) -> P || D ) ) ) )
67 simplrl 
 |-  ( ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) /\ x || ( k x. P ) ) -> P e. Prime )
68 simpll 
 |-  ( ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) /\ x || ( k x. P ) ) -> x e. ZZ )
69 coprm 
 |-  ( ( P e. Prime /\ x e. ZZ ) -> ( -. P || x <-> ( P gcd x ) = 1 ) )
70 67 68 69 syl2anc 
 |-  ( ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) /\ x || ( k x. P ) ) -> ( -. P || x <-> ( P gcd x ) = 1 ) )
71 zcn 
 |-  ( k e. ZZ -> k e. CC )
72 71 ad2antll 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> k e. CC )
73 prmz 
 |-  ( P e. Prime -> P e. ZZ )
74 73 ad2antrl 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> P e. ZZ )
75 74 zcnd 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> P e. CC )
76 72 75 mulcomd 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> ( k x. P ) = ( P x. k ) )
77 76 breq2d 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> ( x || ( k x. P ) <-> x || ( P x. k ) ) )
78 simpl 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> x e. ZZ )
79 74 78 gcdcomd 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P gcd x ) = ( x gcd P ) )
80 79 eqeq1d 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( P gcd x ) = 1 <-> ( x gcd P ) = 1 ) )
81 77 80 anbi12d 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x || ( k x. P ) /\ ( P gcd x ) = 1 ) <-> ( x || ( P x. k ) /\ ( x gcd P ) = 1 ) ) )
82 simprr 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> k e. ZZ )
83 coprmdvds 
 |-  ( ( x e. ZZ /\ P e. ZZ /\ k e. ZZ ) -> ( ( x || ( P x. k ) /\ ( x gcd P ) = 1 ) -> x || k ) )
84 78 74 82 83 syl3anc 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x || ( P x. k ) /\ ( x gcd P ) = 1 ) -> x || k ) )
85 81 84 sylbid 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x || ( k x. P ) /\ ( P gcd x ) = 1 ) -> x || k ) )
86 85 expdimp 
 |-  ( ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) /\ x || ( k x. P ) ) -> ( ( P gcd x ) = 1 -> x || k ) )
87 70 86 sylbid 
 |-  ( ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) /\ x || ( k x. P ) ) -> ( -. P || x -> x || k ) )
88 87 con1d 
 |-  ( ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) /\ x || ( k x. P ) ) -> ( -. x || k -> P || x ) )
89 88 expimpd 
 |-  ( ( x e. ZZ /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x || ( k x. P ) /\ -. x || k ) -> P || x ) )
90 89 ex 
 |-  ( x e. ZZ -> ( ( P e. Prime /\ k e. ZZ ) -> ( ( x || ( k x. P ) /\ -. x || k ) -> P || x ) ) )
91 66 90 vtoclga 
 |-  ( D e. ZZ -> ( ( P e. Prime /\ k e. ZZ ) -> ( ( D || ( k x. P ) /\ -. D || k ) -> P || D ) ) )
92 91 impl 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( ( D || ( k x. P ) /\ -. D || k ) -> P || D ) )
93 73 zcnd 
 |-  ( P e. Prime -> P e. CC )
94 93 exp1d 
 |-  ( P e. Prime -> ( P ^ 1 ) = P )
95 94 ad2antlr 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( P ^ 1 ) = P )
96 95 oveq2d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( k x. ( P ^ 1 ) ) = ( k x. P ) )
97 96 breq2d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( D || ( k x. ( P ^ 1 ) ) <-> D || ( k x. P ) ) )
98 1m1e0 
 |-  ( 1 - 1 ) = 0
99 98 oveq2i 
 |-  ( P ^ ( 1 - 1 ) ) = ( P ^ 0 )
100 73 ad2antlr 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> P e. ZZ )
101 100 zcnd 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> P e. CC )
102 101 exp0d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( P ^ 0 ) = 1 )
103 99 102 eqtrid 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( P ^ ( 1 - 1 ) ) = 1 )
104 103 oveq2d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( k x. ( P ^ ( 1 - 1 ) ) ) = ( k x. 1 ) )
105 71 adantl 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> k e. CC )
106 105 mulid1d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( k x. 1 ) = k )
107 104 106 eqtrd 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( k x. ( P ^ ( 1 - 1 ) ) ) = k )
108 107 breq2d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( D || ( k x. ( P ^ ( 1 - 1 ) ) ) <-> D || k ) )
109 108 notbid 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) <-> -. D || k ) )
110 97 109 anbi12d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( ( D || ( k x. ( P ^ 1 ) ) /\ -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) <-> ( D || ( k x. P ) /\ -. D || k ) ) )
111 101 exp1d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( P ^ 1 ) = P )
112 111 breq1d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( ( P ^ 1 ) || D <-> P || D ) )
113 92 110 112 3imtr4d 
 |-  ( ( ( D e. ZZ /\ P e. Prime ) /\ k e. ZZ ) -> ( ( D || ( k x. ( P ^ 1 ) ) /\ -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) -> ( P ^ 1 ) || D ) )
114 113 ralrimiva 
 |-  ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ 1 ) ) /\ -. D || ( k x. ( P ^ ( 1 - 1 ) ) ) ) -> ( P ^ 1 ) || D ) )
115 oveq1 
 |-  ( k = x -> ( k x. ( P ^ n ) ) = ( x x. ( P ^ n ) ) )
116 115 breq2d 
 |-  ( k = x -> ( D || ( k x. ( P ^ n ) ) <-> D || ( x x. ( P ^ n ) ) ) )
117 oveq1 
 |-  ( k = x -> ( k x. ( P ^ ( n - 1 ) ) ) = ( x x. ( P ^ ( n - 1 ) ) ) )
118 117 breq2d 
 |-  ( k = x -> ( D || ( k x. ( P ^ ( n - 1 ) ) ) <-> D || ( x x. ( P ^ ( n - 1 ) ) ) ) )
119 118 notbid 
 |-  ( k = x -> ( -. D || ( k x. ( P ^ ( n - 1 ) ) ) <-> -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) )
120 116 119 anbi12d 
 |-  ( k = x -> ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) <-> ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) ) )
121 120 imbi1d 
 |-  ( k = x -> ( ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) <-> ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) ) )
122 121 cbvralvw 
 |-  ( A. k e. ZZ ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) <-> A. x e. ZZ ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) )
123 simprr 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> k e. ZZ )
124 73 ad2antrl 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> P e. ZZ )
125 123 124 zmulcld 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( k x. P ) e. ZZ )
126 oveq1 
 |-  ( x = ( k x. P ) -> ( x x. ( P ^ n ) ) = ( ( k x. P ) x. ( P ^ n ) ) )
127 126 breq2d 
 |-  ( x = ( k x. P ) -> ( D || ( x x. ( P ^ n ) ) <-> D || ( ( k x. P ) x. ( P ^ n ) ) ) )
128 oveq1 
 |-  ( x = ( k x. P ) -> ( x x. ( P ^ ( n - 1 ) ) ) = ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) )
129 128 breq2d 
 |-  ( x = ( k x. P ) -> ( D || ( x x. ( P ^ ( n - 1 ) ) ) <-> D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) )
130 129 notbid 
 |-  ( x = ( k x. P ) -> ( -. D || ( x x. ( P ^ ( n - 1 ) ) ) <-> -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) )
131 127 130 anbi12d 
 |-  ( x = ( k x. P ) -> ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) <-> ( D || ( ( k x. P ) x. ( P ^ n ) ) /\ -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) ) )
132 131 imbi1d 
 |-  ( x = ( k x. P ) -> ( ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) <-> ( ( D || ( ( k x. P ) x. ( P ^ n ) ) /\ -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) ) )
133 132 rspcv 
 |-  ( ( k x. P ) e. ZZ -> ( A. x e. ZZ ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) -> ( ( D || ( ( k x. P ) x. ( P ^ n ) ) /\ -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) ) )
134 125 133 syl 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( A. x e. ZZ ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) -> ( ( D || ( ( k x. P ) x. ( P ^ n ) ) /\ -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) ) )
135 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
136 135 ad2antrr 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> n e. NN0 )
137 zexpcl 
 |-  ( ( P e. ZZ /\ n e. NN0 ) -> ( P ^ n ) e. ZZ )
138 124 136 137 syl2anc 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ n ) e. ZZ )
139 simplr 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> D e. ZZ )
140 divides 
 |-  ( ( ( P ^ n ) e. ZZ /\ D e. ZZ ) -> ( ( P ^ n ) || D <-> E. x e. ZZ ( x x. ( P ^ n ) ) = D ) )
141 138 139 140 syl2anc 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( P ^ n ) || D <-> E. x e. ZZ ( x x. ( P ^ n ) ) = D ) )
142 89 adantll 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x || ( k x. P ) /\ -. x || k ) -> P || x ) )
143 prmnn 
 |-  ( P e. Prime -> P e. NN )
144 143 ad2antrl 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> P e. NN )
145 144 nncnd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> P e. CC )
146 135 ad2antrr 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> n e. NN0 )
147 145 146 expp1d 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ ( n + 1 ) ) = ( ( P ^ n ) x. P ) )
148 144 146 nnexpcld 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ n ) e. NN )
149 148 nncnd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ n ) e. CC )
150 149 145 mulcomd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( P ^ n ) x. P ) = ( P x. ( P ^ n ) ) )
151 147 150 eqtrd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ ( n + 1 ) ) = ( P x. ( P ^ n ) ) )
152 151 oveq2d 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( k x. ( P ^ ( n + 1 ) ) ) = ( k x. ( P x. ( P ^ n ) ) ) )
153 71 ad2antll 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> k e. CC )
154 153 145 149 mulassd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( k x. P ) x. ( P ^ n ) ) = ( k x. ( P x. ( P ^ n ) ) ) )
155 152 154 eqtr4d 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( k x. ( P ^ ( n + 1 ) ) ) = ( ( k x. P ) x. ( P ^ n ) ) )
156 155 breq2d 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ ( n + 1 ) ) ) <-> ( x x. ( P ^ n ) ) || ( ( k x. P ) x. ( P ^ n ) ) ) )
157 simplr 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> x e. ZZ )
158 simprr 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> k e. ZZ )
159 144 nnzd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> P e. ZZ )
160 158 159 zmulcld 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( k x. P ) e. ZZ )
161 148 nnzd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ n ) e. ZZ )
162 148 nnne0d 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ n ) =/= 0 )
163 dvdsmulcr 
 |-  ( ( x e. ZZ /\ ( k x. P ) e. ZZ /\ ( ( P ^ n ) e. ZZ /\ ( P ^ n ) =/= 0 ) ) -> ( ( x x. ( P ^ n ) ) || ( ( k x. P ) x. ( P ^ n ) ) <-> x || ( k x. P ) ) )
164 157 160 161 162 163 syl112anc 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x x. ( P ^ n ) ) || ( ( k x. P ) x. ( P ^ n ) ) <-> x || ( k x. P ) ) )
165 156 164 bitrd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ ( n + 1 ) ) ) <-> x || ( k x. P ) ) )
166 dvdsmulcr 
 |-  ( ( x e. ZZ /\ k e. ZZ /\ ( ( P ^ n ) e. ZZ /\ ( P ^ n ) =/= 0 ) ) -> ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) <-> x || k ) )
167 157 158 161 162 166 syl112anc 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) <-> x || k ) )
168 167 notbid 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( -. ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) <-> -. x || k ) )
169 165 168 anbi12d 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) ) <-> ( x || ( k x. P ) /\ -. x || k ) ) )
170 151 breq1d 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( P ^ ( n + 1 ) ) || ( x x. ( P ^ n ) ) <-> ( P x. ( P ^ n ) ) || ( x x. ( P ^ n ) ) ) )
171 dvdsmulcr 
 |-  ( ( P e. ZZ /\ x e. ZZ /\ ( ( P ^ n ) e. ZZ /\ ( P ^ n ) =/= 0 ) ) -> ( ( P x. ( P ^ n ) ) || ( x x. ( P ^ n ) ) <-> P || x ) )
172 159 157 161 162 171 syl112anc 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( P x. ( P ^ n ) ) || ( x x. ( P ^ n ) ) <-> P || x ) )
173 170 172 bitrd 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( P ^ ( n + 1 ) ) || ( x x. ( P ^ n ) ) <-> P || x ) )
174 142 169 173 3imtr4d 
 |-  ( ( ( n e. NN /\ x e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || ( x x. ( P ^ n ) ) ) )
175 174 an32s 
 |-  ( ( ( n e. NN /\ ( P e. Prime /\ k e. ZZ ) ) /\ x e. ZZ ) -> ( ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || ( x x. ( P ^ n ) ) ) )
176 breq1 
 |-  ( ( x x. ( P ^ n ) ) = D -> ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ ( n + 1 ) ) ) <-> D || ( k x. ( P ^ ( n + 1 ) ) ) ) )
177 breq1 
 |-  ( ( x x. ( P ^ n ) ) = D -> ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) <-> D || ( k x. ( P ^ n ) ) ) )
178 177 notbid 
 |-  ( ( x x. ( P ^ n ) ) = D -> ( -. ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) <-> -. D || ( k x. ( P ^ n ) ) ) )
179 176 178 anbi12d 
 |-  ( ( x x. ( P ^ n ) ) = D -> ( ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) ) <-> ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) ) )
180 breq2 
 |-  ( ( x x. ( P ^ n ) ) = D -> ( ( P ^ ( n + 1 ) ) || ( x x. ( P ^ n ) ) <-> ( P ^ ( n + 1 ) ) || D ) )
181 179 180 imbi12d 
 |-  ( ( x x. ( P ^ n ) ) = D -> ( ( ( ( x x. ( P ^ n ) ) || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. ( x x. ( P ^ n ) ) || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || ( x x. ( P ^ n ) ) ) <-> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
182 175 181 syl5ibcom 
 |-  ( ( ( n e. NN /\ ( P e. Prime /\ k e. ZZ ) ) /\ x e. ZZ ) -> ( ( x x. ( P ^ n ) ) = D -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
183 182 rexlimdva 
 |-  ( ( n e. NN /\ ( P e. Prime /\ k e. ZZ ) ) -> ( E. x e. ZZ ( x x. ( P ^ n ) ) = D -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
184 183 adantlr 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( E. x e. ZZ ( x x. ( P ^ n ) ) = D -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
185 141 184 sylbid 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( P ^ n ) || D -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
186 185 com23 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( ( P ^ n ) || D -> ( P ^ ( n + 1 ) ) || D ) ) )
187 186 a2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ n ) || D ) -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
188 71 ad2antll 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> k e. CC )
189 124 zcnd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> P e. CC )
190 138 zcnd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ n ) e. CC )
191 188 189 190 mulassd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( k x. P ) x. ( P ^ n ) ) = ( k x. ( P x. ( P ^ n ) ) ) )
192 189 190 mulcomd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P x. ( P ^ n ) ) = ( ( P ^ n ) x. P ) )
193 189 136 expp1d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ ( n + 1 ) ) = ( ( P ^ n ) x. P ) )
194 192 193 eqtr4d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P x. ( P ^ n ) ) = ( P ^ ( n + 1 ) ) )
195 194 oveq2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( k x. ( P x. ( P ^ n ) ) ) = ( k x. ( P ^ ( n + 1 ) ) ) )
196 191 195 eqtrd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( k x. P ) x. ( P ^ n ) ) = ( k x. ( P ^ ( n + 1 ) ) ) )
197 196 breq2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( D || ( ( k x. P ) x. ( P ^ n ) ) <-> D || ( k x. ( P ^ ( n + 1 ) ) ) ) )
198 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
199 198 ad2antrr 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( n - 1 ) e. NN0 )
200 zexpcl 
 |-  ( ( P e. ZZ /\ ( n - 1 ) e. NN0 ) -> ( P ^ ( n - 1 ) ) e. ZZ )
201 124 199 200 syl2anc 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ ( n - 1 ) ) e. ZZ )
202 201 zcnd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ ( n - 1 ) ) e. CC )
203 188 189 202 mulassd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) = ( k x. ( P x. ( P ^ ( n - 1 ) ) ) ) )
204 189 202 mulcomd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P x. ( P ^ ( n - 1 ) ) ) = ( ( P ^ ( n - 1 ) ) x. P ) )
205 simpll 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> n e. NN )
206 expm1t 
 |-  ( ( P e. CC /\ n e. NN ) -> ( P ^ n ) = ( ( P ^ ( n - 1 ) ) x. P ) )
207 189 205 206 syl2anc 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ n ) = ( ( P ^ ( n - 1 ) ) x. P ) )
208 204 207 eqtr4d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P x. ( P ^ ( n - 1 ) ) ) = ( P ^ n ) )
209 208 oveq2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( k x. ( P x. ( P ^ ( n - 1 ) ) ) ) = ( k x. ( P ^ n ) ) )
210 203 209 eqtrd 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) = ( k x. ( P ^ n ) ) )
211 210 breq2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) <-> D || ( k x. ( P ^ n ) ) ) )
212 211 notbid 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) <-> -. D || ( k x. ( P ^ n ) ) ) )
213 197 212 anbi12d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( D || ( ( k x. P ) x. ( P ^ n ) ) /\ -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) <-> ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) ) )
214 213 imbi1d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( ( D || ( ( k x. P ) x. ( P ^ n ) ) /\ -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) <-> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ n ) || D ) ) )
215 nncn 
 |-  ( n e. NN -> n e. CC )
216 215 ad2antrr 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> n e. CC )
217 ax-1cn 
 |-  1 e. CC
218 pncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
219 216 217 218 sylancl 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( n + 1 ) - 1 ) = n )
220 219 oveq2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( P ^ ( ( n + 1 ) - 1 ) ) = ( P ^ n ) )
221 220 oveq2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) = ( k x. ( P ^ n ) ) )
222 221 breq2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) <-> D || ( k x. ( P ^ n ) ) ) )
223 222 notbid 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) <-> -. D || ( k x. ( P ^ n ) ) ) )
224 223 anbi2d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) <-> ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) ) )
225 224 imbi1d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) <-> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ n ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
226 187 214 225 3imtr4d 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( ( ( D || ( ( k x. P ) x. ( P ^ n ) ) /\ -. D || ( ( k x. P ) x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
227 134 226 syld 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ ( P e. Prime /\ k e. ZZ ) ) -> ( A. x e. ZZ ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
228 227 anassrs 
 |-  ( ( ( ( n e. NN /\ D e. ZZ ) /\ P e. Prime ) /\ k e. ZZ ) -> ( A. x e. ZZ ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) -> ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
229 228 ralrimdva 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ P e. Prime ) -> ( A. x e. ZZ ( ( D || ( x x. ( P ^ n ) ) /\ -. D || ( x x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
230 122 229 syl5bi 
 |-  ( ( ( n e. NN /\ D e. ZZ ) /\ P e. Prime ) -> ( A. k e. ZZ ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) )
231 230 expl 
 |-  ( n e. NN -> ( ( D e. ZZ /\ P e. Prime ) -> ( A. k e. ZZ ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) ) )
232 231 a2d 
 |-  ( n e. NN -> ( ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ n ) ) /\ -. D || ( k x. ( P ^ ( n - 1 ) ) ) ) -> ( P ^ n ) || D ) ) -> ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ ( n + 1 ) ) ) /\ -. D || ( k x. ( P ^ ( ( n + 1 ) - 1 ) ) ) ) -> ( P ^ ( n + 1 ) ) || D ) ) ) )
233 20 33 46 59 114 232 nnind 
 |-  ( N e. NN -> ( ( D e. ZZ /\ P e. Prime ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) ) )
234 233 com12 
 |-  ( ( D e. ZZ /\ P e. Prime ) -> ( N e. NN -> A. k e. ZZ ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) ) )
235 234 impr 
 |-  ( ( D e. ZZ /\ ( P e. Prime /\ N e. NN ) ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) )
236 235 adantll 
 |-  ( ( ( K e. ZZ /\ D e. ZZ ) /\ ( P e. Prime /\ N e. NN ) ) -> A. k e. ZZ ( ( D || ( k x. ( P ^ N ) ) /\ -. D || ( k x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) )
237 simpll 
 |-  ( ( ( K e. ZZ /\ D e. ZZ ) /\ ( P e. Prime /\ N e. NN ) ) -> K e. ZZ )
238 7 236 237 rspcdva 
 |-  ( ( ( K e. ZZ /\ D e. ZZ ) /\ ( P e. Prime /\ N e. NN ) ) -> ( ( D || ( K x. ( P ^ N ) ) /\ -. D || ( K x. ( P ^ ( N - 1 ) ) ) ) -> ( P ^ N ) || D ) )
239 238 3impia 
 |-  ( ( ( K e. ZZ /\ D e. ZZ ) /\ ( P e. Prime /\ N e. NN ) /\ ( D || ( K x. ( P ^ N ) ) /\ -. D || ( K x. ( P ^ ( N - 1 ) ) ) ) ) -> ( P ^ N ) || D )