Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nn0prpwlem Unicode version

Theorem nn0prpwlem 26016
Description: Lemma for nn0prpw 26017. Use strong induction to show that every natural number has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.)
Assertion
Ref Expression
nn0prpwlem  |-  ( A  e.  NN  ->  A. k  e.  NN  ( k  < 
A  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  A ) ) )
Distinct variable group:    k, n, p, A

Proof of Theorem nn0prpwlem
Dummy variables  m  q  r  t  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 4157 . . . 4  |-  ( x  =  A  ->  (
k  <  x  <->  k  <  A ) )
2 breq2 4157 . . . . . . 7  |-  ( x  =  A  ->  (
( p ^ n
)  ||  x  <->  ( p ^ n )  ||  A ) )
32bibi2d 310 . . . . . 6  |-  ( x  =  A  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  ( (
p ^ n ) 
||  k  <->  ( p ^ n )  ||  A ) ) )
43notbid 286 . . . . 5  |-  ( x  =  A  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  -.  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  A ) ) )
542rexbidv 2692 . . . 4  |-  ( x  =  A  ->  ( E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  A ) ) )
61, 5imbi12d 312 . . 3  |-  ( x  =  A  ->  (
( k  <  x  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x ) )  <-> 
( k  <  A  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  A ) ) ) )
76ralbidv 2669 . 2  |-  ( x  =  A  ->  ( A. k  e.  NN  ( k  <  x  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x ) )  <->  A. k  e.  NN  ( k  <  A  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  A ) ) ) )
8 breq2 4157 . . . . 5  |-  ( x  =  1  ->  (
k  <  x  <->  k  <  1 ) )
9 breq2 4157 . . . . . . . 8  |-  ( x  =  1  ->  (
( p ^ n
)  ||  x  <->  ( p ^ n )  ||  1 ) )
109bibi2d 310 . . . . . . 7  |-  ( x  =  1  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  ( (
p ^ n ) 
||  k  <->  ( p ^ n )  ||  1 ) ) )
1110notbid 286 . . . . . 6  |-  ( x  =  1  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  -.  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  1 ) ) )
12112rexbidv 2692 . . . . 5  |-  ( x  =  1  ->  ( E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  1 ) ) )
138, 12imbi12d 312 . . . 4  |-  ( x  =  1  ->  (
( k  <  x  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x ) )  <-> 
( k  <  1  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  1 ) ) ) )
1413ralbidv 2669 . . 3  |-  ( x  =  1  ->  ( A. k  e.  NN  ( k  <  x  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x ) )  <->  A. k  e.  NN  ( k  <  1  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  1 ) ) ) )
15 breq2 4157 . . . . 5  |-  ( x  =  y  ->  (
k  <  x  <->  k  <  y ) )
16 breq2 4157 . . . . . . . 8  |-  ( x  =  y  ->  (
( p ^ n
)  ||  x  <->  ( p ^ n )  ||  y ) )
1716bibi2d 310 . . . . . . 7  |-  ( x  =  y  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  ( (
p ^ n ) 
||  k  <->  ( p ^ n )  ||  y ) ) )
1817notbid 286 . . . . . 6  |-  ( x  =  y  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  -.  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  y ) ) )
19182rexbidv 2692 . . . . 5  |-  ( x  =  y  ->  ( E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )
2015, 19imbi12d 312 . . . 4  |-  ( x  =  y  ->  (
( k  <  x  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x ) )  <-> 
( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) ) )
2120ralbidv 2669 . . 3  |-  ( x  =  y  ->  ( A. k  e.  NN  ( k  <  x  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x ) )  <->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) ) )
22 nnnlt1 9962 . . . . 5  |-  ( k  e.  NN  ->  -.  k  <  1 )
2322pm2.21d 100 . . . 4  |-  ( k  e.  NN  ->  (
k  <  1  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^ n ) 
||  k  <->  ( p ^ n )  ||  1 ) ) )
2423rgen 2714 . . 3  |-  A. k  e.  NN  ( k  <  1  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  1 ) )
25 exprmfct 13037 . . . 4  |-  ( x  e.  ( ZZ>= `  2
)  ->  E. q  e.  Prime  q  ||  x
)
26 prmz 13010 . . . . . . . . . . . . . . . 16  |-  ( q  e.  Prime  ->  q  e.  ZZ )
2726adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  q  e.  ZZ )
28 prmnn 13009 . . . . . . . . . . . . . . . . 17  |-  ( q  e.  Prime  ->  q  e.  NN )
2928nnne0d 9976 . . . . . . . . . . . . . . . 16  |-  ( q  e.  Prime  ->  q  =/=  0 )
3029adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  q  =/=  0 )
31 nnz 10235 . . . . . . . . . . . . . . . 16  |-  ( t  e.  NN  ->  t  e.  ZZ )
3231adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  t  e.  ZZ )
33 dvdsval2 12782 . . . . . . . . . . . . . . 15  |-  ( ( q  e.  ZZ  /\  q  =/=  0  /\  t  e.  ZZ )  ->  (
q  ||  t  <->  ( t  /  q )  e.  ZZ ) )
3427, 30, 32, 33syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  (
q  ||  t  <->  ( t  /  q )  e.  ZZ ) )
3534biimpd 199 . . . . . . . . . . . . 13  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  (
q  ||  t  ->  ( t  /  q )  e.  ZZ ) )
36353ad2antl2 1120 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  t  e.  NN )  ->  (
q  ||  t  ->  ( t  /  q )  e.  ZZ ) )
3736adantrl 697 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  /\  t  e.  NN ) )  -> 
( q  ||  t  ->  ( t  /  q
)  e.  ZZ ) )
38 simprr 734 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  (
t  e.  NN  /\  ( t  /  q
)  e.  ZZ ) )  ->  ( t  /  q )  e.  ZZ )
39 nnre 9939 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  NN  ->  t  e.  RR )
40 nngt0 9961 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  NN  ->  0  <  t )
4139, 40jca 519 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  NN  ->  (
t  e.  RR  /\  0  <  t ) )
42 nnre 9939 . . . . . . . . . . . . . . . . . . 19  |-  ( q  e.  NN  ->  q  e.  RR )
43 nngt0 9961 . . . . . . . . . . . . . . . . . . 19  |-  ( q  e.  NN  ->  0  <  q )
4442, 43jca 519 . . . . . . . . . . . . . . . . . 18  |-  ( q  e.  NN  ->  (
q  e.  RR  /\  0  <  q ) )
4528, 44syl 16 . . . . . . . . . . . . . . . . 17  |-  ( q  e.  Prime  ->  ( q  e.  RR  /\  0  <  q ) )
46 divgt0 9810 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  RR  /\  0  <  t )  /\  ( q  e.  RR  /\  0  < 
q ) )  -> 
0  <  ( t  /  q ) )
4741, 45, 46syl2anr 465 . . . . . . . . . . . . . . . 16  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  0  <  ( t  /  q
) )
48473ad2antl2 1120 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  t  e.  NN )  ->  0  <  ( t  /  q
) )
4948adantrr 698 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  (
t  e.  NN  /\  ( t  /  q
)  e.  ZZ ) )  ->  0  <  ( t  /  q ) )
50 elnnz 10224 . . . . . . . . . . . . . 14  |-  ( ( t  /  q )  e.  NN  <->  ( (
t  /  q )  e.  ZZ  /\  0  <  ( t  /  q
) ) )
5138, 49, 50sylanbrc 646 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  (
t  e.  NN  /\  ( t  /  q
)  e.  ZZ ) )  ->  ( t  /  q )  e.  NN )
5251expr 599 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  t  e.  NN )  ->  (
( t  /  q
)  e.  ZZ  ->  ( t  /  q )  e.  NN ) )
5352adantrl 697 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  /\  t  e.  NN ) )  -> 
( ( t  / 
q )  e.  ZZ  ->  ( t  /  q
)  e.  NN ) )
5426adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  q  e.  ZZ )
5529adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  q  =/=  0 )
56 eluzelz 10428 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ZZ>= `  2
)  ->  x  e.  ZZ )
5756adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  x  e.  ZZ )
58 dvdsval2 12782 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  ZZ  /\  q  =/=  0  /\  x  e.  ZZ )  ->  (
q  ||  x  <->  ( x  /  q )  e.  ZZ ) )
5954, 55, 57, 58syl3anc 1184 . . . . . . . . . . . . . . . . 17  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( q  ||  x  <->  ( x  / 
q )  e.  ZZ ) )
60 eluzelre 10429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ZZ>= `  2
)  ->  x  e.  RR )
61 2z 10244 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  ZZ
6261eluz1i 10427 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( ZZ>= `  2
)  <->  ( x  e.  ZZ  /\  2  <_  x ) )
63 2pos 10014 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  <  2
64 zre 10218 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ZZ  ->  x  e.  RR )
65 0re 9024 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  RR
66 2re 10001 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  e.  RR
67 ltletr 9099 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 0  e.  RR  /\  2  e.  RR  /\  x  e.  RR )  ->  (
( 0  <  2  /\  2  <_  x )  ->  0  <  x
) )
6865, 66, 67mp3an12 1269 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  ->  (
( 0  <  2  /\  2  <_  x )  ->  0  <  x
) )
6964, 68syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ZZ  ->  (
( 0  <  2  /\  2  <_  x )  ->  0  <  x
) )
7063, 69mpani 658 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ZZ  ->  (
2  <_  x  ->  0  <  x ) )
7170imp 419 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  ZZ  /\  2  <_  x )  -> 
0  <  x )
7262, 71sylbi 188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ZZ>= `  2
)  ->  0  <  x )
7360, 72jca 519 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ZZ>= `  2
)  ->  ( x  e.  RR  /\  0  < 
x ) )
74 divgt0 9810 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( x  e.  RR  /\  0  <  x )  /\  ( q  e.  RR  /\  0  < 
q ) )  -> 
0  <  ( x  /  q ) )
7573, 45, 74syl2anr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  0  <  ( x  /  q ) )
7675a1d 23 . . . . . . . . . . . . . . . . . . 19  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( (
x  /  q )  e.  ZZ  ->  0  <  ( x  /  q
) ) )
7776ancld 537 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( (
x  /  q )  e.  ZZ  ->  (
( x  /  q
)  e.  ZZ  /\  0  <  ( x  / 
q ) ) ) )
78 elnnz 10224 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  /  q )  e.  NN  <->  ( (
x  /  q )  e.  ZZ  /\  0  <  ( x  /  q
) ) )
7977, 78syl6ibr 219 . . . . . . . . . . . . . . . . 17  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( (
x  /  q )  e.  ZZ  ->  (
x  /  q )  e.  NN ) )
8059, 79sylbid 207 . . . . . . . . . . . . . . . 16  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( q  ||  x  ->  ( x  /  q )  e.  NN ) )
8180ancoms 440 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  (
q  ||  x  ->  ( x  /  q )  e.  NN ) )
82 breq1 4156 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  / 
q )  ->  (
y  <  x  <->  ( x  /  q )  < 
x ) )
83 breq2 4157 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  / 
q )  ->  (
k  <  y  <->  k  <  ( x  /  q ) ) )
84 breq2 4157 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  ( x  / 
q )  ->  (
( p ^ n
)  ||  y  <->  ( p ^ n )  ||  ( x  /  q
) ) )
8584bibi2d 310 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  / 
q )  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y )  <->  ( (
p ^ n ) 
||  k  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )
8685notbid 286 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  / 
q )  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y )  <->  -.  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )
87862rexbidv 2692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  / 
q )  ->  ( E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y )  <->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) ) )
8883, 87imbi12d 312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
q )  ->  (
( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) )  <-> 
( k  <  (
x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) ) ) )
8988ralbidv 2669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  / 
q )  ->  ( A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) )  <->  A. k  e.  NN  ( k  <  (
x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) ) ) )
9082, 89imbi12d 312 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( x  / 
q )  ->  (
( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  <->  ( ( x  /  q )  < 
x  ->  A. k  e.  NN  ( k  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) ) ) ) )
9190rspcv 2991 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  /  q )  e.  NN  ->  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  ->  ( (
x  /  q )  <  x  ->  A. k  e.  NN  ( k  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) ) ) ) )
92913ad2ant1 978 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  ( A. y  e.  NN  ( y  < 
x  ->  A. k  e.  NN  ( k  < 
y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  ->  ( (
x  /  q )  <  x  ->  A. k  e.  NN  ( k  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) ) ) ) )
9392adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( A. y  e.  NN  (
y  <  x  ->  A. k  e.  NN  (
k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^ n ) 
||  k  <->  ( p ^ n )  ||  y ) ) )  ->  ( ( x  /  q )  < 
x  ->  A. k  e.  NN  ( k  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) ) ) ) )
9460recnd 9047 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ZZ>= `  2
)  ->  x  e.  CC )
9594mulid2d 9039 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ZZ>= `  2
)  ->  ( 1  x.  x )  =  x )
9695ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( 1  x.  x )  =  x )
97 prmuz2 13024 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  Prime  ->  q  e.  ( ZZ>= `  2 )
)
9861eluz1i 10427 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( q  e.  ( ZZ>= `  2
)  <->  ( q  e.  ZZ  /\  2  <_ 
q ) )
99 1lt2 10074 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  <  2
100 zre 10218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( q  e.  ZZ  ->  q  e.  RR )
101 1re 9023 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1  e.  RR
102 ltletr 9099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 1  e.  RR  /\  2  e.  RR  /\  q  e.  RR )  ->  (
( 1  <  2  /\  2  <_  q )  ->  1  <  q
) )
103101, 66, 102mp3an12 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( q  e.  RR  ->  (
( 1  <  2  /\  2  <_  q )  ->  1  <  q
) )
104100, 103syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( q  e.  ZZ  ->  (
( 1  <  2  /\  2  <_  q )  ->  1  <  q
) )
10599, 104mpani 658 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( q  e.  ZZ  ->  (
2  <_  q  ->  1  <  q ) )
106105imp 419 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( q  e.  ZZ  /\  2  <_  q )  -> 
1  <  q )
10798, 106sylbi 188 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  ( ZZ>= `  2
)  ->  1  <  q )
10897, 107syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( q  e.  Prime  ->  1  < 
q )
109108ad2antlr 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  1  <  q )
110101a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  1  e.  RR )
11128nnred 9947 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  Prime  ->  q  e.  RR )
112111ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  q  e.  RR )
11360ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  x  e.  RR )
11472ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  0  <  x )
115 ltmul1 9792 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  RR  /\  q  e.  RR  /\  (
x  e.  RR  /\  0  <  x ) )  ->  ( 1  < 
q  <->  ( 1  x.  x )  <  (
q  x.  x ) ) )
116110, 112, 113, 114, 115syl112anc 1188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( 1  <  q  <->  ( 1  x.  x )  < 
( q  x.  x
) ) )
117109, 116mpbid 202 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( 1  x.  x )  < 
( q  x.  x
) )
11896, 117eqbrtrrd 4175 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  x  <  ( q  x.  x ) )
11928, 43syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( q  e.  Prime  ->  0  < 
q )
120119ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  0  <  q )
121 ltdivmul 9814 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  x  e.  RR  /\  (
q  e.  RR  /\  0  <  q ) )  ->  ( ( x  /  q )  < 
x  <->  x  <  ( q  x.  x ) ) )
122113, 113, 112, 120, 121syl112anc 1188 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( (
x  /  q )  <  x  <->  x  <  ( q  x.  x ) ) )
123118, 122mpbird 224 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( x  /  q )  < 
x )
124 breq1 4156 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( t  / 
q )  ->  (
k  <  ( x  /  q )  <->  ( t  /  q )  < 
( x  /  q
) ) )
125 breq2 4157 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  ( t  / 
q )  ->  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  ( t  /  q
) ) )
126125bibi1d 311 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( t  / 
q )  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) )  <->  ( (
p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )
127126notbid 286 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( t  / 
q )  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) )  <->  -.  (
( p ^ n
)  ||  ( t  /  q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )
1281272rexbidv 2692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( t  / 
q )  ->  ( E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) )  <->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) ) )
129124, 128imbi12d 312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  ( t  / 
q )  ->  (
( k  <  (
x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) )  <-> 
( ( t  / 
q )  <  (
x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) ) ) )
130129rspcv 2991 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( t  /  q )  e.  NN  ->  ( A. k  e.  NN  ( k  <  (
x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) )  ->  ( ( t  /  q )  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) ) ) )
1311303ad2ant2 979 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  ( A. k  e.  NN  ( k  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) )  ->  ( ( t  /  q )  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) ) ) )
132131adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( A. k  e.  NN  (
k  <  ( x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) )  ->  ( ( t  /  q )  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) ) ) )
133393ad2ant3 980 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  t  e.  RR )
134133adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  t  e.  RR )
135 ltdiv1 9806 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( t  e.  RR  /\  x  e.  RR  /\  (
q  e.  RR  /\  0  <  q ) )  ->  ( t  < 
x  <->  ( t  / 
q )  <  (
x  /  q ) ) )
136134, 113, 112, 120, 135syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( t  <  x  <->  ( t  / 
q )  <  (
x  /  q ) ) )
137136biimpa 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( x  e.  ( ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  ( t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  -> 
( t  /  q
)  <  ( x  /  q ) )
138 simprll 739 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )  ->  p  e.  Prime )
139 peano2nn 9944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  e.  NN  ->  (
n  +  1 )  e.  NN )
140139adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( p  e.  Prime  /\  n  e.  NN )  ->  (
n  +  1 )  e.  NN )
141140ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( q ^ n ) 
||  ( t  / 
q )  <->  ( q ^ n )  ||  ( x  /  q
) ) ) )  ->  ( n  + 
1 )  e.  NN )
14226ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  q  e.  ZZ )
143 nnnn0 10160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  e.  NN  ->  n  e.  NN0 )
144143ad2antll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  n  e.  NN0 )
145 zexpcl 11323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( q  e.  ZZ  /\  n  e.  NN0 )  -> 
( q ^ n
)  e.  ZZ )
146142, 144, 145syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( q ^ n )  e.  ZZ )
147 nnz 10235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( t  /  q )  e.  NN  ->  (
t  /  q )  e.  ZZ )
1481473ad2ant2 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  ( t  /  q
)  e.  ZZ )
149148ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( t  /  q )  e.  ZZ )
15029ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  q  =/=  0 )
151 dvdsmulcr 12806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( q ^ n
)  e.  ZZ  /\  ( t  /  q
)  e.  ZZ  /\  ( q  e.  ZZ  /\  q  =/=  0 ) )  ->  ( (
( q ^ n
)  x.  q ) 
||  ( ( t  /  q )  x.  q )  <->  ( q ^ n )  ||  ( t  /  q
) ) )
152146, 149, 142, 150, 151syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
( q ^ n
)  x.  q ) 
||  ( ( t  /  q )  x.  q )  <->  ( q ^ n )  ||  ( t  /  q
) ) )
15328nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( q  e.  Prime  ->  q  e.  CC )
154153ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  q  e.  CC )
155154, 144expp1d 11451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( q ^ ( n  + 
1 ) )  =  ( ( q ^
n )  x.  q
) )
156155eqcomd 2392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
q ^ n )  x.  q )  =  ( q ^ (
n  +  1 ) ) )
157 nncn 9940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( t  e.  NN  ->  t  e.  CC )
1581573ad2ant3 980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  t  e.  CC )
159158ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  t  e.  CC )
160159, 154, 150divcan1d 9723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
t  /  q )  x.  q )  =  t )
161156, 160breq12d 4166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
( q ^ n
)  x.  q ) 
||  ( ( t  /  q )  x.  q )  <->  ( q ^ ( n  + 
1 ) )  ||  t ) )
162152, 161bitr3d 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
q ^ n ) 
||  ( t  / 
q )  <->  ( q ^ ( n  + 
1 ) )  ||  t ) )
163 nnz 10235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x  /  q )  e.  NN  ->  (
x  /  q )  e.  ZZ )
1641633ad2ant1 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  ( x  /  q
)  e.  ZZ )
165164ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( x  /  q )  e.  ZZ )
166 dvdsmulcr 12806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( q ^ n
)  e.  ZZ  /\  ( x  /  q
)  e.  ZZ  /\  ( q  e.  ZZ  /\  q  =/=  0 ) )  ->  ( (
( q ^ n
)  x.  q ) 
||  ( ( x  /  q )  x.  q )  <->  ( q ^ n )  ||  ( x  /  q
) ) )
167146, 165, 142, 150, 166syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
( q ^ n
)  x.  q ) 
||  ( ( x  /  q )  x.  q )  <->  ( q ^ n )  ||  ( x  /  q
) ) )
16894ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  x  e.  CC )
169168, 154, 150divcan1d 9723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
x  /  q )  x.  q )  =  x )
170156, 169breq12d 4166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
( q ^ n
)  x.  q ) 
||  ( ( x  /  q )  x.  q )  <->  ( q ^ ( n  + 
1 ) )  ||  x ) )
171167, 170bitr3d 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
q ^ n ) 
||  ( x  / 
q )  <->  ( q ^ ( n  + 
1 ) )  ||  x ) )
172162, 171bibi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( (
( q ^ n
)  ||  ( t  /  q )  <->  ( q ^ n )  ||  ( x  /  q
) )  <->  ( (
q ^ ( n  +  1 ) ) 
||  t  <->  ( q ^ ( n  + 
1 ) )  ||  x ) ) )
173172notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( -.  ( ( q ^
n )  ||  (
t  /  q )  <-> 
( q ^ n
)  ||  ( x  /  q ) )  <->  -.  ( ( q ^
( n  +  1 ) )  ||  t  <->  ( q ^ ( n  +  1 ) ) 
||  x ) ) )
174173biimpd 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( -.  ( ( q ^
n )  ||  (
t  /  q )  <-> 
( q ^ n
)  ||  ( x  /  q ) )  ->  -.  ( (
q ^ ( n  +  1 ) ) 
||  t  <->  ( q ^ ( n  + 
1 ) )  ||  x ) ) )
175174impr 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( q ^ n ) 
||  ( t  / 
q )  <->  ( q ^ n )  ||  ( x  /  q
) ) ) )  ->  -.  ( (
q ^ ( n  +  1 ) ) 
||  t  <->  ( q ^ ( n  + 
1 ) )  ||  x ) )
176 oveq2 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  ( n  + 
1 )  ->  (
q ^ m )  =  ( q ^
( n  +  1 ) ) )
177176breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  ( n  + 
1 )  ->  (
( q ^ m
)  ||  t  <->  ( q ^ ( n  + 
1 ) )  ||  t ) )
178176breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  ( n  + 
1 )  ->  (
( q ^ m
)  ||  x  <->  ( q ^ ( n  + 
1 ) )  ||  x ) )
179177, 178bibi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  ( n  + 
1 )  ->  (
( ( q ^
m )  ||  t  <->  ( q ^ m ) 
||  x )  <->  ( (
q ^ ( n  +  1 ) ) 
||  t  <->  ( q ^ ( n  + 
1 ) )  ||  x ) ) )
180179notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( m  =  ( n  + 
1 )  ->  ( -.  ( ( q ^
m )  ||  t  <->  ( q ^ m ) 
||  x )  <->  -.  (
( q ^ (
n  +  1 ) )  ||  t  <->  ( q ^ ( n  + 
1 ) )  ||  x ) ) )
181180rspcev 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( n  +  1 )  e.  NN  /\  -.  ( ( q ^
( n  +  1 ) )  ||  t  <->  ( q ^ ( n  +  1 ) ) 
||  x ) )  ->  E. m  e.  NN  -.  ( ( q ^
m )  ||  t  <->  ( q ^ m ) 
||  x ) )
182141, 175, 181syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( q ^ n ) 
||  ( t  / 
q )  <->  ( q ^ n )  ||  ( x  /  q
) ) ) )  ->  E. m  e.  NN  -.  ( ( q ^
m )  ||  t  <->  ( q ^ m ) 
||  x ) )
183 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( p  =  q  ->  (
p ^ n )  =  ( q ^
n ) )
184183breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( p  =  q  ->  (
( p ^ n
)  ||  ( t  /  q )  <->  ( q ^ n )  ||  ( t  /  q
) ) )
185183breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( p  =  q  ->  (
( p ^ n
)  ||  ( x  /  q )  <->  ( q ^ n )  ||  ( x  /  q
) ) )
186184, 185bibi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( p  =  q  ->  (
( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) )  <-> 
( ( q ^
n )  ||  (
t  /  q )  <-> 
( q ^ n
)  ||  ( x  /  q ) ) ) )
187186notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( p  =  q  ->  ( -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) )  <->  -.  ( ( q ^
n )  ||  (
t  /  q )  <-> 
( q ^ n
)  ||  ( x  /  q ) ) ) )
188187anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( p  =  q  ->  (
( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) ) )  <->  ( (
p  e.  Prime  /\  n  e.  NN )  /\  -.  ( ( q ^
n )  ||  (
t  /  q )  <-> 
( q ^ n
)  ||  ( x  /  q ) ) ) ) )
189188anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  =  q  ->  (
( ( ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  /\  (
( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  /\  t  <  x )  /\  ( ( p  e.  Prime  /\  n  e.  NN )  /\  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) ) )  <->  ( (
( ( x  e.  ( ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  ( t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( q ^ n ) 
||  ( t  / 
q )  <->  ( q ^ n )  ||  ( x  /  q
) ) ) ) ) )
190 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( p  =  q  ->  (
p ^ m )  =  ( q ^
m ) )
191190breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( p  =  q  ->  (
( p ^ m
)  ||  t  <->  ( q ^ m )  ||  t ) )
192190breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( p  =  q  ->  (
( p ^ m
)  ||  x  <->  ( q ^ m )  ||  x ) )
193191, 192bibi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( p  =  q  ->  (
( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  ( (
q ^ m ) 
||  t  <->  ( q ^ m )  ||  x ) ) )
194193notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( p  =  q  ->  ( -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  -.  (
( q ^ m
)  ||  t  <->  ( q ^ m )  ||  x ) ) )
195194rexbidv 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  =  q  ->  ( E. m  e.  NN  -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  E. m  e.  NN  -.  ( ( q ^ m ) 
||  t  <->  ( q ^ m )  ||  x ) ) )
196189, 195imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( p  =  q  ->  (
( ( ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  /\  t  <  x )  /\  ( ( p  e.  Prime  /\  n  e.  NN )  /\  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) ) )  ->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) )  <->  ( (
( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( q ^ n ) 
||  ( t  / 
q )  <->  ( q ^ n )  ||  ( x  /  q
) ) ) )  ->  E. m  e.  NN  -.  ( ( q ^
m )  ||  t  <->  ( q ^ m ) 
||  x ) ) ) )
197182, 196mpbiri 225 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( p  =  q  ->  (
( ( ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  /\  (
( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  /\  t  <  x )  /\  ( ( p  e.  Prime  /\  n  e.  NN )  /\  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) ) )  ->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) )
198197com12 29 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )  ->  ( p  =  q  ->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) )
199 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( p  e.  Prime  /\  n  e.  NN )  /\  -.  p  =  q )  ->  n  e.  NN )
200199ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  /\  (
( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  /\  t  <  x )  /\  ( ( p  e.  Prime  /\  n  e.  NN )  /\  -.  p  =  q )
)  /\  -.  (
( p ^ n
)  ||  ( t  /  q )  <->  ( p ^ n )  ||  ( x  /  q
) ) )  ->  n  e.  NN )
201 prmz 13010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( p  e.  Prime  ->  p  e.  ZZ )
202201adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( p  e.  Prime  /\  n  e.  NN )  ->  p  e.  ZZ )
203202ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  ->  p  e.  ZZ )
204143adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( p  e.  Prime  /\  n  e.  NN )  ->  n  e.  NN0 )
205204ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  ->  n  e.  NN0 )
206 zexpcl 11323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( p  e.  ZZ  /\  n  e.  NN0 )  -> 
( p ^ n
)  e.  ZZ )
207203, 205, 206syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( p ^ n
)  e.  ZZ )
20826ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
q  e.  ZZ )
209148ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( t  /  q
)  e.  ZZ )
210 dvdsmultr2 12812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( p ^ n
)  e.  ZZ  /\  q  e.  ZZ  /\  (
t  /  q )  e.  ZZ )  -> 
( ( p ^
n )  ||  (
t  /  q )  ->  ( p ^
n )  ||  (
q  x.  ( t  /  q ) ) ) )
211207, 208, 209, 210syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
t  /  q )  ->  ( p ^
n )  ||  (
q  x.  ( t  /  q ) ) ) )
212 gcdcom 12947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( p ^ n
)  e.  ZZ  /\  q  e.  ZZ )  ->  ( ( p ^
n )  gcd  q
)  =  ( q  gcd  ( p ^
n ) ) )
213207, 208, 212syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  gcd  q
)  =  ( q  gcd  ( p ^
n ) ) )
214 simp-4r 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  q  e.  Prime )
215 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  p  e.  Prime )
216 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  n  e.  NN )
217 prmdvdsexpb 13042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( q  e.  Prime  /\  p  e.  Prime  /\  n  e.  NN )  ->  ( q 
||  ( p ^
n )  <->  q  =  p ) )
218 equcom 1687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( q  =  p  <->  p  =  q )
219217, 218syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( q  e.  Prime  /\  p  e.  Prime  /\  n  e.  NN )  ->  ( q 
||  ( p ^
n )  <->  p  =  q ) )
220219biimpd 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( q  e.  Prime  /\  p  e.  Prime  /\  n  e.  NN )  ->  ( q 
||  ( p ^
n )  ->  p  =  q ) )
221214, 215, 216, 220syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( q  ||  ( p ^ n
)  ->  p  =  q ) )
222221con3d 127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( -.  p  =  q  ->  -.  q  ||  ( p ^ n ) ) )
223222impr 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  ->  -.  q  ||  ( p ^ n ) )
224 simp-4r 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
q  e.  Prime )
225 coprm 13027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( q  e.  Prime  /\  (
p ^ n )  e.  ZZ )  -> 
( -.  q  ||  ( p ^ n
)  <->  ( q  gcd  ( p ^ n
) )  =  1 ) )
226224, 207, 225syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( -.  q  ||  ( p ^ n
)  <->  ( q  gcd  ( p ^ n
) )  =  1 ) )
227223, 226mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( q  gcd  (
p ^ n ) )  =  1 )
228213, 227eqtrd 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  gcd  q
)  =  1 )
229 coprmdvds 13029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( p ^ n
)  e.  ZZ  /\  q  e.  ZZ  /\  (
t  /  q )  e.  ZZ )  -> 
( ( ( p ^ n )  ||  ( q  x.  (
t  /  q ) )  /\  ( ( p ^ n )  gcd  q )  =  1 )  ->  (
p ^ n ) 
||  ( t  / 
q ) ) )
230207, 208, 209, 229syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( ( p ^ n )  ||  ( q  x.  (
t  /  q ) )  /\  ( ( p ^ n )  gcd  q )  =  1 )  ->  (
p ^ n ) 
||  ( t  / 
q ) ) )
231228, 230mpan2d 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
q  x.  ( t  /  q ) )  ->  ( p ^
n )  ||  (
t  /  q ) ) )
232211, 231impbid 184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( q  x.  ( t  /  q
) ) ) )
233158ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
t  e.  CC )
234153ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
q  e.  CC )
23529ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
q  =/=  0 )
236233, 234, 235divcan2d 9724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( q  x.  (
t  /  q ) )  =  t )
237236breq2d 4165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
q  x.  ( t  /  q ) )  <-> 
( p ^ n
)  ||  t )
)
238232, 237bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  t )
)
239164ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( x  /  q
)  e.  ZZ )
240 dvdsmultr2 12812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( p ^ n
)  e.  ZZ  /\  q  e.  ZZ  /\  (
x  /  q )  e.  ZZ )  -> 
( ( p ^
n )  ||  (
x  /  q )  ->  ( p ^
n )  ||  (
q  x.  ( x  /  q ) ) ) )
241207, 208, 239, 240syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
x  /  q )  ->  ( p ^
n )  ||  (
q  x.  ( x  /  q ) ) ) )
242 coprmdvds 13029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( p ^ n
)  e.  ZZ  /\  q  e.  ZZ  /\  (
x  /  q )  e.  ZZ )  -> 
( ( ( p ^ n )  ||  ( q  x.  (
x  /  q ) )  /\  ( ( p ^ n )  gcd  q )  =  1 )  ->  (
p ^ n ) 
||  ( x  / 
q ) ) )
243207, 208, 239, 242syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( ( p ^ n )  ||  ( q  x.  (
x  /  q ) )  /\  ( ( p ^ n )  gcd  q )  =  1 )  ->  (
p ^ n ) 
||  ( x  / 
q ) ) )
244228, 243mpan2d 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
q  x.  ( x  /  q ) )  ->  ( p ^
n )  ||  (
x  /  q ) ) )
245241, 244impbid 184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
x  /  q )  <-> 
( p ^ n
)  ||  ( q  x.  ( x  /  q
) ) ) )
24694ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  ->  x  e.  CC )
247246, 234, 235divcan2d 9724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( q  x.  (
x  /  q ) )  =  x )
248247breq2d 4165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
q  x.  ( x  /  q ) )  <-> 
( p ^ n
)  ||  x )
)
249245, 248bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( p ^
n )  ||  (
x  /  q )  <-> 
( p ^ n
)  ||  x )
)
250238, 249bibi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( ( ( p ^ n )  ||  ( t  /  q
)  <->  ( p ^
n )  ||  (
x  /  q ) )  <->  ( ( p ^ n )  ||  t 
<->  ( p ^ n
)  ||  x )
) )
251250notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( -.  ( ( p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) )  <->  -.  (
( p ^ n
)  ||  t  <->  ( p ^ n )  ||  x ) ) )
252251biimpa 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  /\  (
( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  /\  t  <  x )  /\  ( ( p  e.  Prime  /\  n  e.  NN )  /\  -.  p  =  q )
)  /\  -.  (
( p ^ n
)  ||  ( t  /  q )  <->  ( p ^ n )  ||  ( x  /  q
) ) )  ->  -.  ( ( p ^
n )  ||  t  <->  ( p ^ n ) 
||  x ) )
253 oveq2 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  =  n  ->  (
p ^ m )  =  ( p ^
n ) )
254253breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  =  n  ->  (
( p ^ m
)  ||  t  <->  ( p ^ n )  ||  t ) )
255253breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  =  n  ->  (
( p ^ m
)  ||  x  <->  ( p ^ n )  ||  x ) )
256254, 255bibi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  n  ->  (
( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  ( (
p ^ n ) 
||  t  <->  ( p ^ n )  ||  x ) ) )
257256notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  n  ->  ( -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  -.  (
( p ^ n
)  ||  t  <->  ( p ^ n )  ||  x ) ) )
258257rspcev 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( n  e.  NN  /\  -.  ( ( p ^
n )  ||  t  <->  ( p ^ n ) 
||  x ) )  ->  E. m  e.  NN  -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x ) )
259200, 252, 258syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  /\  (
( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  /\  t  <  x )  /\  ( ( p  e.  Prime  /\  n  e.  NN )  /\  -.  p  =  q )
)  /\  -.  (
( p ^ n
)  ||  ( t  /  q )  <->  ( p ^ n )  ||  ( x  /  q
) ) )  ->  E. m  e.  NN  -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x ) )
260259ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  p  =  q ) )  -> 
( -.  ( ( p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) )  ->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) )
261260expr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( -.  p  =  q  ->  ( -.  ( ( p ^ n )  ||  ( t  /  q
)  <->  ( p ^
n )  ||  (
x  /  q ) )  ->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) ) )
262261com23 74 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( p  e.  Prime  /\  n  e.  NN ) )  ->  ( -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) )  ->  ( -.  p  =  q  ->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) ) )
263262impr 603 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )  ->  ( -.  p  =  q  ->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) )
264198, 263pm2.61d 152 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )  ->  E. m  e.  NN  -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x ) )
265 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( r  =  p  ->  (
r ^ m )  =  ( p ^
m ) )
266265breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( r  =  p  ->  (
( r ^ m
)  ||  t  <->  ( p ^ m )  ||  t ) )
267265breq1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( r  =  p  ->  (
( r ^ m
)  ||  x  <->  ( p ^ m )  ||  x ) )
268266, 267bibi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( r  =  p  ->  (
( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x )  <->  ( (
p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) )
269268notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( r  =  p  ->  ( -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x )  <->  -.  (
( p ^ m
)  ||  t  <->  ( p ^ m )  ||  x ) ) )
270269rexbidv 2670 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( r  =  p  ->  ( E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x )  <->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) )
271270rspcev 2995 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( p  e.  Prime  /\  E. m  e.  NN  -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x ) )  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) )
272138, 264, 271syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( x  e.  ( ZZ>= `  2
)  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  (
t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  /\  ( ( p  e. 
Prime  /\  n  e.  NN )  /\  -.  ( ( p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) )
273272exp32 589 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( x  e.  ( ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  ( t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  -> 
( ( p  e. 
Prime  /\  n  e.  NN )  ->  ( -.  (
( p ^ n
)  ||  ( t  /  q )  <->  ( p ^ n )  ||  ( x  /  q
) )  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) )
274273rexlimdvv 2779 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( x  e.  ( ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  ( t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  -> 
( E. p  e. 
Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) )  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) )
275137, 274embantd 52 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( x  e.  ( ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  /  q )  e.  NN  /\  ( t  /  q )  e.  NN  /\  t  e.  NN ) )  /\  t  <  x )  -> 
( ( ( t  /  q )  < 
( x  /  q
)  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) )  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) )
276275ex 424 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( t  <  x  ->  ( (
( t  /  q
)  <  ( x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) )  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) )
277276com23 74 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( (
( t  /  q
)  <  ( x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) ) )  ->  ( t  <  x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) )
278132, 277syld 42 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( A. k  e.  NN  (
k  <  ( x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) )  ->  ( t  < 
x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) )
279123, 278embantd 52 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( (
( x  /  q
)  <  x  ->  A. k  e.  NN  (
k  <  ( x  /  q )  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) ) ) )  ->  ( t  <  x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) )
28093, 279syld 42 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( A. y  e.  NN  (
y  <  x  ->  A. k  e.  NN  (
k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^ n ) 
||  k  <->  ( p ^ n )  ||  y ) ) )  ->  ( t  < 
x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) )
2812803exp2 1171 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  (
( x  /  q
)  e.  NN  ->  ( ( t  /  q
)  e.  NN  ->  ( t  e.  NN  ->  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  ->  ( t  <  x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) ) ) ) )
28281, 281syld 42 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  (
q  ||  x  ->  ( ( t  /  q
)  e.  NN  ->  ( t  e.  NN  ->  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  ->  ( t  <  x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) ) ) ) )
2832823impia 1150 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime  /\  q  ||  x )  ->  (
( t  /  q
)  e.  NN  ->  ( t  e.  NN  ->  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  ->  ( t  <  x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) ) ) )
284283com24 83 . . . . . . . . . . . 12  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime  /\  q  ||  x )  ->  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  ->  ( t  e.  NN  ->  ( (
t  /  q )  e.  NN  ->  (
t  <  x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^ m ) 
||  t  <->  ( r ^ m )  ||  x ) ) ) ) ) )
285284imp32 423 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  /\  t  e.  NN ) )  -> 
( ( t  / 
q )  e.  NN  ->  ( t  <  x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) )
28637, 53, 2853syld 53 . . . . . . . . . 10  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  ( A. y  e.  NN  ( y  <  x  ->  A. k  e.  NN  ( k  <  y  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y ) ) )  /\  t  e.  NN ) )  -> 
( q  ||  t  ->  ( t  <  x  ->  E. r  e.  Prime  E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x ) ) ) )
287 simpl2 961 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  (
t  e.  NN  /\  ( -.  q  ||  t  /\  t  <  x
) ) )  -> 
q  e.  Prime )
288 1nn 9943 . . . . . . . . . . . . . . 15  |-  1  e.  NN
289288a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  (
t  e.  NN  /\  ( -.  q  ||  t  /\  t  <  x
) ) )  -> 
1  e.  NN )
290153exp1d 11445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( q  e.  Prime  ->  ( q ^ 1 )  =  q )
291290breq1d 4163 . . . . . . . . . . . . . . . . . . . . 21  |-  ( q  e.  Prime  ->  ( ( q ^ 1 ) 
||  t  <->  q  ||  t ) )
292291notbid 286 . . . . . . . . . . . . . . . . . . . 20  |-  ( q  e.  Prime  ->  ( -.  ( q ^ 1 )  ||  t  <->  -.  q  ||  t ) )
293292biimpar 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( q  e.  Prime  /\  -.  q  ||  t )  ->  -.  ( q ^ 1 )  ||  t )
294293