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

Theorem nn0prpwlem 26341
Description: Lemma for nn0prpw 26342. 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 4043 . . . 4  |-  ( x  =  A  ->  (
k  <  x  <->  k  <  A ) )
2 breq2 4043 . . . . . . 7  |-  ( x  =  A  ->  (
( p ^ n
)  ||  x  <->  ( p ^ n )  ||  A ) )
32bibi2d 309 . . . . . 6  |-  ( x  =  A  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  ( (
p ^ n ) 
||  k  <->  ( p ^ n )  ||  A ) ) )
43notbid 285 . . . . 5  |-  ( x  =  A  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  -.  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  A ) ) )
542rexbidv 2599 . . . 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 311 . . 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 2576 . 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 4043 . . . . 5  |-  ( x  =  1  ->  (
k  <  x  <->  k  <  1 ) )
9 breq2 4043 . . . . . . . 8  |-  ( x  =  1  ->  (
( p ^ n
)  ||  x  <->  ( p ^ n )  ||  1 ) )
109bibi2d 309 . . . . . . 7  |-  ( x  =  1  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  ( (
p ^ n ) 
||  k  <->  ( p ^ n )  ||  1 ) ) )
1110notbid 285 . . . . . 6  |-  ( x  =  1  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  -.  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  1 ) ) )
12112rexbidv 2599 . . . . 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 311 . . . 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 2576 . . 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 4043 . . . . 5  |-  ( x  =  y  ->  (
k  <  x  <->  k  <  y ) )
16 breq2 4043 . . . . . . . 8  |-  ( x  =  y  ->  (
( p ^ n
)  ||  x  <->  ( p ^ n )  ||  y ) )
1716bibi2d 309 . . . . . . 7  |-  ( x  =  y  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  ( (
p ^ n ) 
||  k  <->  ( p ^ n )  ||  y ) ) )
1817notbid 285 . . . . . 6  |-  ( x  =  y  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  x )  <->  -.  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  y ) ) )
19182rexbidv 2599 . . . . 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 311 . . . 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 2576 . . 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 9792 . . . . 5  |-  ( k  e.  NN  ->  -.  k  <  1 )
2322pm2.21d 98 . . . 4  |-  ( k  e.  NN  ->  (
k  <  1  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^ n ) 
||  k  <->  ( p ^ n )  ||  1 ) ) )
2423rgen 2621 . . 3  |-  A. k  e.  NN  ( k  <  1  ->  E. p  e.  Prime  E. n  e.  NN  -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  1 ) )
25 exprmfct 12805 . . . 4  |-  ( x  e.  ( ZZ>= `  2
)  ->  E. q  e.  Prime  q  ||  x
)
26 prmz 12778 . . . . . . . . . . . . . . . 16  |-  ( q  e.  Prime  ->  q  e.  ZZ )
2726adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  q  e.  ZZ )
28 prmnn 12777 . . . . . . . . . . . . . . . . 17  |-  ( q  e.  Prime  ->  q  e.  NN )
2928nnne0d 9806 . . . . . . . . . . . . . . . 16  |-  ( q  e.  Prime  ->  q  =/=  0 )
3029adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  q  =/=  0 )
31 nnz 10061 . . . . . . . . . . . . . . . 16  |-  ( t  e.  NN  ->  t  e.  ZZ )
3231adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  t  e.  ZZ )
33 dvdsval2 12550 . . . . . . . . . . . . . . 15  |-  ( ( q  e.  ZZ  /\  q  =/=  0  /\  t  e.  ZZ )  ->  (
q  ||  t  <->  ( t  /  q )  e.  ZZ ) )
3427, 30, 32, 33syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  (
q  ||  t  <->  ( t  /  q )  e.  ZZ ) )
3534biimpd 198 . . . . . . . . . . . . 13  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  (
q  ||  t  ->  ( t  /  q )  e.  ZZ ) )
36353ad2antl2 1118 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  t  e.  NN )  ->  (
q  ||  t  ->  ( t  /  q )  e.  ZZ ) )
3736adantrl 696 . . . . . . . . . . 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 733 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  (
t  e.  NN  /\  ( t  /  q
)  e.  ZZ ) )  ->  ( t  /  q )  e.  ZZ )
39 nnre 9769 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  NN  ->  t  e.  RR )
40 nngt0 9791 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  NN  ->  0  <  t )
4139, 40jca 518 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  NN  ->  (
t  e.  RR  /\  0  <  t ) )
42 nnre 9769 . . . . . . . . . . . . . . . . . . 19  |-  ( q  e.  NN  ->  q  e.  RR )
43 nngt0 9791 . . . . . . . . . . . . . . . . . . 19  |-  ( q  e.  NN  ->  0  <  q )
4442, 43jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( q  e.  NN  ->  (
q  e.  RR  /\  0  <  q ) )
4528, 44syl 15 . . . . . . . . . . . . . . . . 17  |-  ( q  e.  Prime  ->  ( q  e.  RR  /\  0  <  q ) )
46 divgt0 9640 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  RR  /\  0  <  t )  /\  ( q  e.  RR  /\  0  < 
q ) )  -> 
0  <  ( t  /  q ) )
4741, 45, 46syl2anr 464 . . . . . . . . . . . . . . . 16  |-  ( ( q  e.  Prime  /\  t  e.  NN )  ->  0  <  ( t  /  q
) )
48473ad2antl2 1118 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  t  e.  NN )  ->  0  <  ( t  /  q
) )
4948adantrr 697 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  (
t  e.  NN  /\  ( t  /  q
)  e.  ZZ ) )  ->  0  <  ( t  /  q ) )
50 elnnz 10050 . . . . . . . . . . . . . 14  |-  ( ( t  /  q )  e.  NN  <->  ( (
t  /  q )  e.  ZZ  /\  0  <  ( t  /  q
) ) )
5138, 49, 50sylanbrc 645 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  (
t  e.  NN  /\  ( t  /  q
)  e.  ZZ ) )  ->  ( t  /  q )  e.  NN )
5251expr 598 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime  /\  q  ||  x )  /\  t  e.  NN )  ->  (
( t  /  q
)  e.  ZZ  ->  ( t  /  q )  e.  NN ) )
5352adantrl 696 . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  q  e.  ZZ )
5529adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  q  =/=  0 )
56 eluzelz 10254 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ZZ>= `  2
)  ->  x  e.  ZZ )
5756adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  x  e.  ZZ )
58 dvdsval2 12550 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  ZZ  /\  q  =/=  0  /\  x  e.  ZZ )  ->  (
q  ||  x  <->  ( x  /  q )  e.  ZZ ) )
5954, 55, 57, 58syl3anc 1182 . . . . . . . . . . . . . . . . 17  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( q  ||  x  <->  ( x  / 
q )  e.  ZZ ) )
60 eluzelre 10255 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ZZ>= `  2
)  ->  x  e.  RR )
61 2z 10070 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  ZZ
6261eluz1i 10253 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( ZZ>= `  2
)  <->  ( x  e.  ZZ  /\  2  <_  x ) )
63 2pos 9844 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  <  2
64 zre 10044 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ZZ  ->  x  e.  RR )
65 0re 8854 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  RR
66 2re 9831 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  e.  RR
67 ltletr 8929 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 0  e.  RR  /\  2  e.  RR  /\  x  e.  RR )  ->  (
( 0  <  2  /\  2  <_  x )  ->  0  <  x
) )
6865, 66, 67mp3an12 1267 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  ->  (
( 0  <  2  /\  2  <_  x )  ->  0  <  x
) )
6964, 68syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ZZ  ->  (
( 0  <  2  /\  2  <_  x )  ->  0  <  x
) )
7063, 69mpani 657 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ZZ  ->  (
2  <_  x  ->  0  <  x ) )
7170imp 418 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  ZZ  /\  2  <_  x )  -> 
0  <  x )
7262, 71sylbi 187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ZZ>= `  2
)  ->  0  <  x )
7360, 72jca 518 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ZZ>= `  2
)  ->  ( x  e.  RR  /\  0  < 
x ) )
74 divgt0 9640 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( x  e.  RR  /\  0  <  x )  /\  ( q  e.  RR  /\  0  < 
q ) )  -> 
0  <  ( x  /  q ) )
7573, 45, 74syl2anr 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  0  <  ( x  /  q ) )
7675a1d 22 . . . . . . . . . . . . . . . . . . 19  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( (
x  /  q )  e.  ZZ  ->  0  <  ( x  /  q
) ) )
7776ancld 536 . . . . . . . . . . . . . . . . . 18  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( (
x  /  q )  e.  ZZ  ->  (
( x  /  q
)  e.  ZZ  /\  0  <  ( x  / 
q ) ) ) )
78 elnnz 10050 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  /  q )  e.  NN  <->  ( (
x  /  q )  e.  ZZ  /\  0  <  ( x  /  q
) ) )
7977, 78syl6ibr 218 . . . . . . . . . . . . . . . . 17  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( (
x  /  q )  e.  ZZ  ->  (
x  /  q )  e.  NN ) )
8059, 79sylbid 206 . . . . . . . . . . . . . . . 16  |-  ( ( q  e.  Prime  /\  x  e.  ( ZZ>= `  2 )
)  ->  ( q  ||  x  ->  ( x  /  q )  e.  NN ) )
8180ancoms 439 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  (
q  ||  x  ->  ( x  /  q )  e.  NN ) )
82 breq1 4042 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  / 
q )  ->  (
y  <  x  <->  ( x  /  q )  < 
x ) )
83 breq2 4043 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  / 
q )  ->  (
k  <  y  <->  k  <  ( x  /  q ) ) )
84 breq2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  ( x  / 
q )  ->  (
( p ^ n
)  ||  y  <->  ( p ^ n )  ||  ( x  /  q
) ) )
8584bibi2d 309 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  / 
q )  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y )  <->  ( (
p ^ n ) 
||  k  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )
8685notbid 285 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  / 
q )  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  y )  <->  -.  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )
87862rexbidv 2599 . . . . . . . . . . . . . . . . . . . . . . 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 311 . . . . . . . . . . . . . . . . . . . . . 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 2576 . . . . . . . . . . . . . . . . . . . . 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 311 . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . 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 8877 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ZZ>= `  2
)  ->  x  e.  CC )
9594mulid2d 8869 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ZZ>= `  2
)  ->  ( 1  x.  x )  =  x )
9695ad2antrr 706 . . . . . . . . . . . . . . . . . . . 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 12792 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  Prime  ->  q  e.  ( ZZ>= `  2 )
)
9861eluz1i 10253 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( q  e.  ( ZZ>= `  2
)  <->  ( q  e.  ZZ  /\  2  <_ 
q ) )
99 1lt2 9902 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  <  2
100 zre 10044 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( q  e.  ZZ  ->  q  e.  RR )
101 1re 8853 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1  e.  RR
102 ltletr 8929 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 1  e.  RR  /\  2  e.  RR  /\  q  e.  RR )  ->  (
( 1  <  2  /\  2  <_  q )  ->  1  <  q
) )
103101, 66, 102mp3an12 1267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( q  e.  RR  ->  (
( 1  <  2  /\  2  <_  q )  ->  1  <  q
) )
104100, 103syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( q  e.  ZZ  ->  (
( 1  <  2  /\  2  <_  q )  ->  1  <  q
) )
10599, 104mpani 657 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( q  e.  ZZ  ->  (
2  <_  q  ->  1  <  q ) )
106105imp 418 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( q  e.  ZZ  /\  2  <_  q )  -> 
1  <  q )
10798, 106sylbi 187 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  ( ZZ>= `  2
)  ->  1  <  q )
10897, 107syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( q  e.  Prime  ->  1  < 
q )
109108ad2antlr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  1  <  q )
110101a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  1  e.  RR )
11128nnred 9777 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( q  e.  Prime  ->  q  e.  RR )
112111ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  q  e.  RR )
11360ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  x  e.  RR )
11472ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  0  <  x )
115 ltmul1 9622 . . . . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . . . . . 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 4061 . . . . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( q  e.  Prime  ->  0  < 
q )
120119ad2antlr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  0  <  q )
121 ltdivmul 9644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  x  e.  RR  /\  (
q  e.  RR  /\  0  <  q ) )  ->  ( ( x  /  q )  < 
x  <->  x  <  ( q  x.  x ) ) )
122113, 113, 112, 120, 121syl112anc 1186 . . . . . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( x  /  q )  < 
x )
124 breq1 4042 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( t  / 
q )  ->  (
k  <  ( x  /  q )  <->  ( t  /  q )  < 
( x  /  q
) ) )
125 breq2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  ( t  / 
q )  ->  (
( p ^ n
)  ||  k  <->  ( p ^ n )  ||  ( t  /  q
) ) )
126125bibi1d 310 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( t  / 
q )  ->  (
( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) )  <->  ( (
p ^ n ) 
||  ( t  / 
q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )
127126notbid 285 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( t  / 
q )  ->  ( -.  ( ( p ^
n )  ||  k  <->  ( p ^ n ) 
||  ( x  / 
q ) )  <->  -.  (
( p ^ n
)  ||  ( t  /  q )  <->  ( p ^ n )  ||  ( x  /  q
) ) ) )
1281272rexbidv 2599 . . . . . . . . . . . . . . . . . . . . . . 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 311 . . . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . . . . 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 977 . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . 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 978 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  t  e.  RR )
134133adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  t  e.  RR )
135 ltdiv1 9636 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( t  e.  RR  /\  x  e.  RR  /\  (
q  e.  RR  /\  0  <  q ) )  ->  ( t  < 
x  <->  ( t  / 
q )  <  (
x  /  q ) ) )
136134, 113, 112, 120, 135syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . . . . . . . . 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 9774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  e.  NN  ->  (
n  +  1 )  e.  NN )
140139adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( p  e.  Prime  /\  n  e.  NN )  ->  (
n  +  1 )  e.  NN )
141140ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
14226adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  q  e.  ZZ )
143142ad3antrrr 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 ) )  ->  q  e.  ZZ )
144 nnnn0 9988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  e.  NN  ->  n  e.  NN0 )
145144ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
146 zexpcl 11134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( q  e.  ZZ  /\  n  e.  NN0 )  -> 
( q ^ n
)  e.  ZZ )
147143, 145, 146syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
148 nnz 10061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( t  /  q )  e.  NN  ->  (
t  /  q )  e.  ZZ )
1491483ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  ( t  /  q
)  e.  ZZ )
150149adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( t  /  q )  e.  ZZ )
151150ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
15229adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  q  =/=  0 )
153152ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
154 dvdsmulcr 12574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
155147, 151, 143, 153, 154syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
15628nncnd 9778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( q  e.  Prime  ->  q  e.  CC )
157156adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  q  e.  CC )
158157ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
159158, 145expp1d 11262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
160159eqcomd 2301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
161 nncn 9770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( t  e.  NN  ->  t  e.  CC )
1621613ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  t  e.  CC )
163162adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  t  e.  CC )
164163ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
165164, 158, 153divcan1d 9553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
166160, 165breq12d 4052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
167155, 166bitr3d 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
168 nnz 10061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( x  /  q )  e.  NN  ->  (
x  /  q )  e.  ZZ )
1691683ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( x  /  q
)  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )  ->  ( x  /  q
)  e.  ZZ )
170169adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( x  e.  (
ZZ>= `  2 )  /\  q  e.  Prime )  /\  ( ( x  / 
q )  e.  NN  /\  ( t  /  q
)  e.  NN  /\  t  e.  NN )
)  ->  ( x  /  q )  e.  ZZ )
171170ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
172 dvdsmulcr 12574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
173147, 171, 143, 153, 172syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
17494adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  x  e.  CC )
175174ad3antrrr 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 ) )  ->  x  e.  CC )
176175, 158, 153divcan1d 9553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
177160, 176breq12d 4052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
178173, 177bitr3d 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
179167, 178bibi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
180179notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
181180biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
182181impr 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
183 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  ( n  + 
1 )  ->  (
q ^ m )  =  ( q ^
( n  +  1 ) ) )
184183breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  ( n  + 
1 )  ->  (
( q ^ m
)  ||  t  <->  ( q ^ ( n  + 
1 ) )  ||  t ) )
185183breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  ( n  + 
1 )  ->  (
( q ^ m
)  ||  x  <->  ( q ^ ( n  + 
1 ) )  ||  x ) )
186184, 185bibi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  ( n  + 
1 )  ->  (
( ( q ^
m )  ||  t  <->  ( q ^ m ) 
||  x )  <->  ( (
q ^ ( n  +  1 ) ) 
||  t  <->  ( q ^ ( n  + 
1 ) )  ||  x ) ) )
187186notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( m  =  ( n  + 
1 )  ->  ( -.  ( ( q ^
m )  ||  t  <->  ( q ^ m ) 
||  x )  <->  -.  (
( q ^ (
n  +  1 ) )  ||  t  <->  ( q ^ ( n  + 
1 ) )  ||  x ) ) )
188187rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( n  +  1 )  e.  NN  /\  -.  ( ( q ^
( n  +  1 ) )  ||  t  <->  ( q ^ ( n  +  1 ) ) 
||  x ) )  ->  E. m  e.  NN  -.  ( ( q ^
m )  ||  t  <->  ( q ^ m ) 
||  x ) )
189141, 182, 188syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
190 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( p  =  q  ->  (
p ^ n )  =  ( q ^
n ) )
191190breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( p  =  q  ->  (
( p ^ n
)  ||  ( t  /  q )  <->  ( q ^ n )  ||  ( t  /  q
) ) )
192190breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( p  =  q  ->  (
( p ^ n
)  ||  ( x  /  q )  <->  ( q ^ n )  ||  ( x  /  q
) ) )
193191, 192bibi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( p  =  q  ->  (
( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) )  <-> 
( ( q ^
n )  ||  (
t  /  q )  <-> 
( q ^ n
)  ||  ( x  /  q ) ) ) )
194193notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( p  =  q  ->  ( -.  ( ( p ^
n )  ||  (
t  /  q )  <-> 
( p ^ n
)  ||  ( x  /  q ) )  <->  -.  ( ( q ^
n )  ||  (
t  /  q )  <-> 
( q ^ n
)  ||  ( x  /  q ) ) ) )
195194anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
196195anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
197 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( p  =  q  ->  (
p ^ m )  =  ( q ^
m ) )
198197breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( p  =  q  ->  (
( p ^ m
)  ||  t  <->  ( q ^ m )  ||  t ) )
199197breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( p  =  q  ->  (
( p ^ m
)  ||  x  <->  ( q ^ m )  ||  x ) )
200198, 199bibi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( p  =  q  ->  (
( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  ( (
q ^ m ) 
||  t  <->  ( q ^ m )  ||  x ) ) )
201200notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( p  =  q  ->  ( -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  -.  (
( q ^ m
)  ||  t  <->  ( q ^ m )  ||  x ) ) )
202201rexbidv 2577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  =  q  ->  ( E. m  e.  NN  -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  E. m  e.  NN  -.  ( ( q ^ m ) 
||  t  <->  ( q ^ m )  ||  x ) ) )
203196, 202imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
204189, 203mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
205204com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
206 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( p  e.  Prime  /\  n  e.  NN )  /\  -.  p  =  q )  ->  n  e.  NN )
207206ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
208 prmz 12778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( p  e.  Prime  ->  p  e.  ZZ )
209208adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( p  e.  Prime  /\  n  e.  NN )  ->  p  e.  ZZ )
210209ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
211144adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( p  e.  Prime  /\  n  e.  NN )  ->  n  e.  NN0 )
212211ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
213 zexpcl 11134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( p  e.  ZZ  /\  n  e.  NN0 )  -> 
( p ^ n
)  e.  ZZ )
214210, 212, 213syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
215142ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
216150ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
217 dvdsmultr2 12580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( p ^ n
)  e.  ZZ  /\  q  e.  ZZ  /\  (
t  /  q )  e.  ZZ )  -> 
( ( p ^
n )  ||  (
t  /  q )  ->  ( p ^
n )  ||  (
q  x.  ( t  /  q ) ) ) )
218214, 215, 216, 217syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
219 gcdcom 12715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( p ^ n
)  e.  ZZ  /\  q  e.  ZZ )  ->  ( ( p ^
n )  gcd  q
)  =  ( q  gcd  ( p ^
n ) ) )
220214, 215, 219syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
221 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  q  e.  Prime )  ->  q  e.  Prime )
222221ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
223 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
224 simprr 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 ) )  ->  n  e.  NN )
225 prmdvdsexpb 12810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( q  e.  Prime  /\  p  e.  Prime  /\  n  e.  NN )  ->  ( q 
||  ( p ^
n )  <->  q  =  p ) )
226 equcom 1665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( q  =  p  <->  p  =  q )
227225, 226syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( q  e.  Prime  /\  p  e.  Prime  /\  n  e.  NN )  ->  ( q 
||  ( p ^
n )  <->  p  =  q ) )
228227biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( q  e.  Prime  /\  p  e.  Prime  /\  n  e.  NN )  ->  ( q 
||  ( p ^
n )  ->  p  =  q ) )
229222, 223, 224, 228syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
230229con3d 125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
231230impr 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
232221ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
233 coprm 12795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( q  e.  Prime  /\  (
p ^ n )  e.  ZZ )  -> 
( -.  q  ||  ( p ^ n
)  <->  ( q  gcd  ( p ^ n
) )  =  1 ) )
234232, 214, 233syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
235231, 234mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
236220, 235eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
237 coprmdvds 12797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
238214, 215, 216, 237syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
239236, 238mpan2d 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
240218, 239impbid 183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
241163ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
242157ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
243152ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
244241, 242, 243divcan2d 9554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
245244breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
246240, 245bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
247170ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
248 dvdsmultr2 12580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( p ^ n
)  e.  ZZ  /\  q  e.  ZZ  /\  (
x  /  q )  e.  ZZ )  -> 
( ( p ^
n )  ||  (
x  /  q )  ->  ( p ^
n )  ||  (
q  x.  ( x  /  q ) ) ) )
249214, 215, 247, 248syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
250 coprmdvds 12797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
251214, 215, 247, 250syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
252236, 251mpan2d 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
253249, 252impbid 183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
254174ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
255254, 242, 243divcan2d 9554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
256255breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
257253, 256bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
258246, 257bibi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
259258notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
260259biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
261 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  =  n  ->  (
p ^ m )  =  ( p ^
n ) )
262261breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  =  n  ->  (
( p ^ m
)  ||  t  <->  ( p ^ n )  ||  t ) )
263261breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( m  =  n  ->  (
( p ^ m
)  ||  x  <->  ( p ^ n )  ||  x ) )
264262, 263bibi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  n  ->  (
( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  ( (
p ^ n ) 
||  t  <->  ( p ^ n )  ||  x ) ) )
265264notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  n  ->  ( -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x )  <->  -.  (
( p ^ n
)  ||  t  <->  ( p ^ n )  ||  x ) ) )
266265rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( n  e.  NN  /\  -.  ( ( p ^
n )  ||  t  <->  ( p ^ n ) 
||  x ) )  ->  E. m  e.  NN  -.  ( ( p ^
m )  ||  t  <->  ( p ^ m ) 
||  x ) )
267207, 260, 266syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
268267ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
269268expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
270269com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
271270impr 602 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
272205, 271pm2.61d 150 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
273 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( r  =  p  ->  (
r ^ m )  =  ( p ^
m ) )
274273breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( r  =  p  ->  (
( r ^ m
)  ||  t  <->  ( p ^ m )  ||  t ) )
275273breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( r  =  p  ->  (
( r ^ m
)  ||  x  <->  ( p ^ m )  ||  x ) )
276274, 275bibi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( r  =  p  ->  (
( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x )  <->  ( (
p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) )
277276notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( r  =  p  ->  ( -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x )  <->  -.  (
( p ^ m
)  ||  t  <->  ( p ^ m )  ||  x ) ) )
278277rexbidv 2577 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( r  =  p  ->  ( E. m  e.  NN  -.  ( ( r ^
m )  ||  t  <->  ( r ^ m ) 
||  x )  <->  E. m  e.  NN  -.  ( ( p ^ m ) 
||  t  <->  ( p ^ m )  ||  x ) ) )
279278rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
280138, 272, 279syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
281280exp32 588 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
282281rexlimdvv 2686 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
283137, 282embantd 50 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
284283ex 423 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
285284com23 72 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
286132, 285syld 40 . . . . . . . . . . . . . . . . . 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 ) ) ) )
287123, 286embantd 50 . . . . . . . . . . . . . . . . 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 ) ) ) )
28893, 287syld 40 . . . . . . . . . . . . . . . 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 ) ) ) )
2892883exp2 1169 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
29081, 289syld 40 . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
2912903impia 1148 . . . . . . . . . . . . 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 ) ) ) ) ) )
292291com24 81 . . . . . . . . . . . 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 ) ) ) ) ) )
293292imp32 422 . . . . . . . . . . 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