ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bezoutlemmain Unicode version

Theorem bezoutlemmain 10594
Description: Lemma for Bézout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.)
Hypotheses
Ref Expression
bezout.is-bezout  |-  ( ph  <->  E. s  e.  ZZ  E. t  e.  ZZ  r  =  ( ( A  x.  s )  +  ( B  x.  t
) ) )
bezout.sub-gcd  |-  ( ps  <->  A. z  e.  NN0  (
z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) ) )
bezout.a  |-  ( th 
->  A  e.  NN0 )
bezout.b  |-  ( th 
->  B  e.  NN0 )
Assertion
Ref Expression
bezoutlemmain  |-  ( th 
->  A. x  e.  NN0  ( [ x  /  r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
Distinct variable groups:    ph, s, t, x, y, z    ps, s, t, z    s, r, t, x, y, z, th    A, r, s, t    B, r, s, t
Allowed substitution hints:    ph( r)    ps( x, y, r)    A( x, y, z)    B( x, y, z)

Proof of Theorem bezoutlemmain
Dummy variables  a  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sbequ 1763 . . . . . . 7  |-  ( w  =  z  ->  ( [ w  /  r ] ph  <->  [ z  /  r ] ph ) )
21anbi2d 452 . . . . . 6  |-  ( w  =  z  ->  (
( th  /\  [
w  /  r ]
ph )  <->  ( th  /\  [ z  /  r ] ph ) ) )
3 sbequ 1763 . . . . . . . . . 10  |-  ( w  =  z  ->  ( [ w  /  x ] ps  <->  [ z  /  x ] ps ) )
43anbi1d 453 . . . . . . . . 9  |-  ( w  =  z  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( [ z  /  x ] ps  /\  ph ) ) )
54rexbidv 2374 . . . . . . . 8  |-  ( w  =  z  ->  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
65imbi2d 228 . . . . . . 7  |-  ( w  =  z  ->  (
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
)  <->  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )
76ralbidv 2373 . . . . . 6  |-  ( w  =  z  ->  ( A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )  <->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )
82, 7imbi12d 232 . . . . 5  |-  ( w  =  z  ->  (
( ( th  /\  [ w  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
) )  <->  ( ( th  /\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) ) )
9 sbequ 1763 . . . . . . 7  |-  ( w  =  x  ->  ( [ w  /  r ] ph  <->  [ x  /  r ] ph ) )
109anbi2d 452 . . . . . 6  |-  ( w  =  x  ->  (
( th  /\  [
w  /  r ]
ph )  <->  ( th  /\  [ x  /  r ] ph ) ) )
11 sbequ12r 1697 . . . . . . . . . 10  |-  ( w  =  x  ->  ( [ w  /  x ] ps  <->  ps ) )
1211anbi1d 453 . . . . . . . . 9  |-  ( w  =  x  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( ps  /\  ph ) ) )
1312rexbidv 2374 . . . . . . . 8  |-  ( w  =  x  ->  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( ps  /\  ph ) ) )
1413imbi2d 228 . . . . . . 7  |-  ( w  =  x  ->  (
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
)  <->  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
1514ralbidv 2373 . . . . . 6  |-  ( w  =  x  ->  ( A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )  <->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
1610, 15imbi12d 232 . . . . 5  |-  ( w  =  x  ->  (
( ( th  /\  [ w  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
) )  <->  ( ( th  /\  [ x  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) ) )
17 nfv 1462 . . . . . . . . . . 11  |-  F/ y  w  e.  NN0
18 nfcv 2223 . . . . . . . . . . . 12  |-  F/_ y
( 0 ... (
w  -  1 ) )
19 nfv 1462 . . . . . . . . . . . . 13  |-  F/ y ( th  /\  [
z  /  r ]
ph )
20 nfra1 2402 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
2119, 20nfim 1505 . . . . . . . . . . . 12  |-  F/ y ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
2218, 21nfralxy 2407 . . . . . . . . . . 11  |-  F/ y A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
2317, 22nfan 1498 . . . . . . . . . 10  |-  F/ y ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )
24 nfv 1462 . . . . . . . . . 10  |-  F/ y ( th  /\  [
w  /  r ]
ph )
2523, 24nfan 1498 . . . . . . . . 9  |-  F/ y ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)
26 nfv 1462 . . . . . . . . 9  |-  F/ y  w  =  0
2725, 26nfan 1498 . . . . . . . 8  |-  F/ y ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  w  = 
0 )
28 simplr 497 . . . . . . . . . 10  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  w  =  0 )  /\  y  e.  NN0 )  /\  [ y  /  r ]
ph )  ->  y  e.  NN0 )
29 nfv 1462 . . . . . . . . . . . . . 14  |-  F/ r A. z  e.  NN0  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y ) )
30 breq2 3809 . . . . . . . . . . . . . . . 16  |-  ( r  =  y  ->  (
z  ||  r  <->  z  ||  y ) )
3130imbi1d 229 . . . . . . . . . . . . . . 15  |-  ( r  =  y  ->  (
( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) )  <->  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y
) ) ) )
3231ralbidv 2373 . . . . . . . . . . . . . 14  |-  ( r  =  y  ->  ( A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) )  <->  A. z  e.  NN0  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y ) ) ) )
3329, 32sbie 1716 . . . . . . . . . . . . 13  |-  ( [ y  /  r ] A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) )  <->  A. z  e.  NN0  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y ) ) )
34 nn0z 8504 . . . . . . . . . . . . . . . 16  |-  ( z  e.  NN0  ->  z  e.  ZZ )
35 dvds0 10418 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ZZ  ->  z  ||  0 )
3634, 35syl 14 . . . . . . . . . . . . . . 15  |-  ( z  e.  NN0  ->  z  ||  0 )
3736biantrurd 299 . . . . . . . . . . . . . 14  |-  ( z  e.  NN0  ->  ( z 
||  y  <->  ( z  ||  0  /\  z  ||  y ) ) )
3837biimpd 142 . . . . . . . . . . . . 13  |-  ( z  e.  NN0  ->  ( z 
||  y  ->  (
z  ||  0  /\  z  ||  y ) ) )
3933, 38mprgbir 2426 . . . . . . . . . . . 12  |-  [ y  /  r ] A. z  e.  NN0  ( z 
||  r  ->  (
z  ||  0  /\  z  ||  y ) )
40 nfv 1462 . . . . . . . . . . . . 13  |-  F/ r  w  =  0
41 dfsbcq2 2827 . . . . . . . . . . . . . 14  |-  ( w  =  0  ->  ( [ w  /  x ] ps  <->  [. 0  /  x ]. ps ) )
42 bezout.sub-gcd . . . . . . . . . . . . . . . 16  |-  ( ps  <->  A. z  e.  NN0  (
z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) ) )
4342sbcbii 2882 . . . . . . . . . . . . . . 15  |-  ( [.
0  /  x ]. ps 
<-> 
[. 0  /  x ]. A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) ) )
44 c0ex 7227 . . . . . . . . . . . . . . . 16  |-  0  e.  _V
45 breq2 3809 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  0  ->  (
z  ||  x  <->  z  ||  0 ) )
4645anbi1d 453 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  0  ->  (
( z  ||  x  /\  z  ||  y )  <-> 
( z  ||  0  /\  z  ||  y ) ) )
4746imbi2d 228 . . . . . . . . . . . . . . . . 17  |-  ( x  =  0  ->  (
( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) )  <->  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y
) ) ) )
4847ralbidv 2373 . . . . . . . . . . . . . . . 16  |-  ( x  =  0  ->  ( A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) )  <->  A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) ) )
4944, 48sbcie 2857 . . . . . . . . . . . . . . 15  |-  ( [.
0  /  x ]. A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) )  <->  A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) )
5043, 49bitri 182 . . . . . . . . . . . . . 14  |-  ( [.
0  /  x ]. ps 
<-> 
A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) )
5141, 50syl6bb 194 . . . . . . . . . . . . 13  |-  ( w  =  0  ->  ( [ w  /  x ] ps  <->  A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) ) )
5240, 51sbbid 1769 . . . . . . . . . . . 12  |-  ( w  =  0  ->  ( [ y  /  r ] [ w  /  x ] ps  <->  [ y  /  r ] A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) ) )
5339, 52mpbiri 166 . . . . . . . . . . 11  |-  ( w  =  0  ->  [ y  /  r ] [
w  /  x ] ps )
5453ad3antlr 477 . . . . . . . . . 10  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  w  =  0 )  /\  y  e.  NN0 )  /\  [ y  /  r ]
ph )  ->  [ y  /  r ] [
w  /  x ] ps )
55 simpr 108 . . . . . . . . . 10  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  w  =  0 )  /\  y  e.  NN0 )  /\  [ y  /  r ]
ph )  ->  [ y  /  r ] ph )
56 nfs1v 1858 . . . . . . . . . . . 12  |-  F/ r [ y  /  r ] [ w  /  x ] ps
57 nfs1v 1858 . . . . . . . . . . . 12  |-  F/ r [ y  /  r ] ph
5856, 57nfan 1498 . . . . . . . . . . 11  |-  F/ r ( [ y  / 
r ] [ w  /  x ] ps  /\  [ y  /  r ]
ph )
59 sbequ12 1696 . . . . . . . . . . . 12  |-  ( r  =  y  ->  ( [ w  /  x ] ps  <->  [ y  /  r ] [ w  /  x ] ps ) )
60 sbequ12 1696 . . . . . . . . . . . 12  |-  ( r  =  y  ->  ( ph 
<->  [ y  /  r ] ph ) )
6159, 60anbi12d 457 . . . . . . . . . . 11  |-  ( r  =  y  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( [ y  / 
r ] [ w  /  x ] ps  /\  [ y  /  r ]
ph ) ) )
6258, 61rspce 2705 . . . . . . . . . 10  |-  ( ( y  e.  NN0  /\  ( [ y  /  r ] [ w  /  x ] ps  /\  [ y  /  r ] ph ) )  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )
6328, 54, 55, 62syl12anc 1168 . . . . . . . . 9  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  w  =  0 )  /\  y  e.  NN0 )  /\  [ y  /  r ]
ph )  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )
6463exp31 356 . . . . . . . 8  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  w  = 
0 )  ->  (
y  e.  NN0  ->  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) ) ) )
6527, 64ralrimi 2437 . . . . . . 7  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  w  = 
0 )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
) )
66 nfv 1462 . . . . . . . . . 10  |-  F/ y 0  <  w
6725, 66nfan 1498 . . . . . . . . 9  |-  F/ y ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )
68 bezout.is-bezout . . . . . . . . . . 11  |-  ( ph  <->  E. s  e.  ZZ  E. t  e.  ZZ  r  =  ( ( A  x.  s )  +  ( B  x.  t
) ) )
69 simplrl 502 . . . . . . . . . . . . 13  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  th )
70 bezout.a . . . . . . . . . . . . 13  |-  ( th 
->  A  e.  NN0 )
7169, 70syl 14 . . . . . . . . . . . 12  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  A  e.  NN0 )
7271ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  ->  A  e.  NN0 )
73 bezout.b . . . . . . . . . . . . 13  |-  ( th 
->  B  e.  NN0 )
7469, 73syl 14 . . . . . . . . . . . 12  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  B  e.  NN0 )
7574ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  ->  B  e.  NN0 )
76 simplll 500 . . . . . . . . . . . . 13  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  w  e.  NN0 )
77 simpr 108 . . . . . . . . . . . . 13  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  0  <  w )
78 elnnnn0b 8451 . . . . . . . . . . . . 13  |-  ( w  e.  NN  <->  ( w  e.  NN0  /\  0  < 
w ) )
7976, 77, 78sylanbrc 408 . . . . . . . . . . . 12  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  w  e.  NN )
8079ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  ->  w  e.  NN )
81 simpr 108 . . . . . . . . . . 11  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  ->  [ y  /  r ] ph )
82 simplr 497 . . . . . . . . . . 11  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  ->  y  e.  NN0 )
83 simplrr 503 . . . . . . . . . . . . 13  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  [ w  /  r ] ph )
84 sbsbc 2828 . . . . . . . . . . . . 13  |-  ( [ w  /  r ]
ph 
<-> 
[. w  /  r ]. ph )
8583, 84sylib 120 . . . . . . . . . . . 12  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  [. w  / 
r ]. ph )
8685ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  ->  [. w  /  r ]. ph )
87 breq1 3808 . . . . . . . . . . . . . 14  |-  ( z  =  a  ->  (
z  ||  r  <->  a  ||  r ) )
88 breq1 3808 . . . . . . . . . . . . . . 15  |-  ( z  =  a  ->  (
z  ||  x  <->  a  ||  x ) )
89 breq1 3808 . . . . . . . . . . . . . . 15  |-  ( z  =  a  ->  (
z  ||  y  <->  a  ||  y ) )
9088, 89anbi12d 457 . . . . . . . . . . . . . 14  |-  ( z  =  a  ->  (
( z  ||  x  /\  z  ||  y )  <-> 
( a  ||  x  /\  a  ||  y ) ) )
9187, 90imbi12d 232 . . . . . . . . . . . . 13  |-  ( z  =  a  ->  (
( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) )  <->  ( a  ||  r  ->  ( a  ||  x  /\  a  ||  y
) ) ) )
9291cbvralv 2582 . . . . . . . . . . . 12  |-  ( A. z  e.  NN0  ( z 
||  r  ->  (
z  ||  x  /\  z  ||  y ) )  <->  A. a  e.  NN0  ( a  ||  r  ->  ( a  ||  x  /\  a  ||  y ) ) )
9342, 92bitri 182 . . . . . . . . . . 11  |-  ( ps  <->  A. a  e.  NN0  (
a  ||  r  ->  ( a  ||  x  /\  a  ||  y ) ) )
9469ad3antrrr 476 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  th )
95 simpr 108 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  [. ( y  mod  w )  /  r ]. ph )
9694, 95jca 300 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  ( th  /\  [. (
y  mod  w )  /  r ]. ph )
)
9783ad3antrrr 476 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  [ w  /  r ] ph )
98 simpllr 501 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  y  e.  NN0 )
9998nn0zd 8600 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  y  e.  ZZ )
10079ad3antrrr 476 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  w  e.  NN )
101 zmodfz 9480 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ZZ  /\  w  e.  NN )  ->  ( y  mod  w
)  e.  ( 0 ... ( w  - 
1 ) ) )
10299, 100, 101syl2anc 403 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  ( y  mod  w
)  e.  ( 0 ... ( w  - 
1 ) ) )
103 simpll 496 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  ->  (
( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w ) )
104 simpr 108 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  ->  A. z  e.  (
0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )
105104ad3antrrr 476 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )
106 nfv 1462 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y [ w  /  r ] ph
107 nfcv 2223 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ y NN0
108 nfs1v 1858 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ y [ w  /  y ] ps
109108nfsbxy 1861 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ y [ z  /  x ] [ w  /  y ] ps
110 nfv 1462 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ y
ph
111109, 110nfan 1498 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ps  /\  ph )
112107, 111nfrexxy 2408 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
113106, 112nfim 1505 . . . . . . . . . . . . . . . . . . 19  |-  F/ y ( [ w  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
)
114 sbequ 1763 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  w  ->  ( [ y  /  r ] ph  <->  [ w  /  r ] ph ) )
115 nfv 1462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ x  y  =  w
116 sbequ12 1696 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  w  ->  ( ps 
<->  [ w  /  y ] ps ) )
117115, 116sbbid 1769 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  w  ->  ( [ z  /  x ] ps  <->  [ z  /  x ] [ w  /  y ] ps ) )
118117anbi1d 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  w  ->  (
( [ z  /  x ] ps  /\  ph ) 
<->  ( [ z  /  x ] [ w  / 
y ] ps  /\  ph ) ) )
119118rexbidv 2374 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  w  ->  ( E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
) )
120114, 119imbi12d 232 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  w  ->  (
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)  <->  ( [ w  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
) ) )
121113, 120rspc 2704 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  NN0  ->  ( A. y  e.  NN0  ( [ y  /  r ]
ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)  ->  ( [
w  /  r ]
ph  ->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
) ) )
122121imim2d 53 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  NN0  ->  ( ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )  ->  (
( th  /\  [
z  /  r ]
ph )  ->  ( [ w  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [
w  /  y ] ps  /\  ph )
) ) ) )
123122ralimdv 2435 . . . . . . . . . . . . . . . 16  |-  ( w  e.  NN0  ->  ( A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )  ->  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  ( [ w  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
) ) ) )
124123ad4antr 478 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  ( A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) )  ->  A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  ( [ w  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [
w  /  y ] ps  /\  ph )
) ) ) )
125105, 124mpd 13 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  ( [ w  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [
w  /  y ] ps  /\  ph )
) ) )
126103, 125sylan 277 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  ( [ w  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [
w  /  y ] ps  /\  ph )
) ) )
127 dfsbcq2 2827 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( y  mod  w )  ->  ( [ z  /  r ] ph  <->  [. ( y  mod  w )  /  r ]. ph ) )
128127anbi2d 452 . . . . . . . . . . . . . . 15  |-  ( z  =  ( y  mod  w )  ->  (
( th  /\  [
z  /  r ]
ph )  <->  ( th  /\  [. ( y  mod  w )  /  r ]. ph ) ) )
129 sbsbc 2828 . . . . . . . . . . . . . . . . . . . 20  |-  ( [ z  /  x ] [ w  /  y ] ps  <->  [. z  /  x ]. [ w  /  y ] ps )
130 sbsbc 2828 . . . . . . . . . . . . . . . . . . . . 21  |-  ( [ w  /  y ] ps  <->  [. w  /  y ]. ps )
131130sbcbii 2882 . . . . . . . . . . . . . . . . . . . 20  |-  ( [. z  /  x ]. [
w  /  y ] ps  <->  [. z  /  x ]. [. w  /  y ]. ps )
132129, 131bitri 182 . . . . . . . . . . . . . . . . . . 19  |-  ( [ z  /  x ] [ w  /  y ] ps  <->  [. z  /  x ]. [. w  /  y ]. ps )
133132anbi1i 446 . . . . . . . . . . . . . . . . . 18  |-  ( ( [ z  /  x ] [ w  /  y ] ps  /\  ph )  <->  (
[. z  /  x ]. [. w  /  y ]. ps  /\  ph )
)
134 dfsbcq 2826 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  ( y  mod  w )  ->  ( [. z  /  x ]. [. w  /  y ]. ps  <->  [. ( y  mod  w )  /  x ]. [. w  /  y ]. ps ) )
135134anbi1d 453 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( y  mod  w )  ->  (
( [. z  /  x ]. [. w  /  y ]. ps  /\  ph )  <->  (
[. ( y  mod  w )  /  x ]. [. w  /  y ]. ps  /\  ph )
) )
136133, 135syl5bb 190 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( y  mod  w )  ->  (
( [ z  /  x ] [ w  / 
y ] ps  /\  ph )  <->  ( [. (
y  mod  w )  /  x ]. [. w  /  y ]. ps  /\ 
ph ) ) )
137136rexbidv 2374 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( y  mod  w )  ->  ( E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )  <->  E. r  e.  NN0  ( [. ( y  mod  w
)  /  x ]. [. w  /  y ]. ps  /\  ph ) ) )
138137imbi2d 228 . . . . . . . . . . . . . . 15  |-  ( z  =  ( y  mod  w )  ->  (
( [ w  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
)  <->  ( [ w  /  r ] ph  ->  E. r  e.  NN0  ( [. ( y  mod  w )  /  x ]. [. w  /  y ]. ps  /\  ph )
) ) )
139128, 138imbi12d 232 . . . . . . . . . . . . . 14  |-  ( z  =  ( y  mod  w )  ->  (
( ( th  /\  [ z  /  r ]
ph )  ->  ( [ w  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [
w  /  y ] ps  /\  ph )
) )  <->  ( ( th  /\  [. ( y  mod  w )  / 
r ]. ph )  -> 
( [ w  / 
r ] ph  ->  E. r  e.  NN0  ( [. ( y  mod  w
)  /  x ]. [. w  /  y ]. ps  /\  ph ) ) ) ) )
140139rspcv 2706 . . . . . . . . . . . . 13  |-  ( ( y  mod  w )  e.  ( 0 ... ( w  -  1 ) )  ->  ( A. z  e.  (
0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  ( [ w  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [
w  /  y ] ps  /\  ph )
) )  ->  (
( th  /\  [. (
y  mod  w )  /  r ]. ph )  ->  ( [ w  / 
r ] ph  ->  E. r  e.  NN0  ( [. ( y  mod  w
)  /  x ]. [. w  /  y ]. ps  /\  ph ) ) ) ) )
141102, 126, 140sylc 61 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  ( ( th  /\  [. ( y  mod  w
)  /  r ]. ph )  ->  ( [
w  /  r ]
ph  ->  E. r  e.  NN0  ( [. ( y  mod  w )  /  x ]. [. w  /  y ]. ps  /\  ph )
) ) )
14296, 97, 141mp2d 46 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  /\  [. (
y  mod  w )  /  r ]. ph )  ->  E. r  e.  NN0  ( [. ( y  mod  w )  /  x ]. [. w  /  y ]. ps  /\  ph )
)
143 nfv 1462 . . . . . . . . . . . . . . . 16  |-  F/ x  w  e.  NN0
144 nfcv 2223 . . . . . . . . . . . . . . . . 17  |-  F/_ x
( 0 ... (
w  -  1 ) )
145 nfv 1462 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( th  /\  [
z  /  r ]
ph )
146 nfcv 2223 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x NN0
147 nfv 1462 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x ph
148147nfsbxy 1861 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x [ y  /  r ] ph
149 nfs1v 1858 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ x [ z  /  x ] ps
150149, 147nfan 1498 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x
( [ z  /  x ] ps  /\  ph )
151146, 150nfrexxy 2408 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
152148, 151nfim 1505 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)
153146, 152nfralxy 2407 . . . . . . . . . . . . . . . . . 18  |-  F/ x A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
154145, 153nfim 1505 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
155144, 154nfralxy 2407 . . . . . . . . . . . . . . . 16  |-  F/ x A. z  e.  (
0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
156143, 155nfan 1498 . . . . . . . . . . . . . . 15  |-  F/ x
( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )
157 nfv 1462 . . . . . . . . . . . . . . 15  |-  F/ x
( th  /\  [
w  /  r ]
ph )
158156, 157nfan 1498 . . . . . . . . . . . . . 14  |-  F/ x
( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)
159 nfv 1462 . . . . . . . . . . . . . 14  |-  F/ x
0  <  w
160158, 159nfan 1498 . . . . . . . . . . . . 13  |-  F/ x
( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )
161 nfv 1462 . . . . . . . . . . . . 13  |-  F/ x  y  e.  NN0
162160, 161nfan 1498 . . . . . . . . . . . 12  |-  F/ x
( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )
163162, 148nfan 1498 . . . . . . . . . . 11  |-  F/ x
( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )
164 nfv 1462 . . . . . . . . . . . . . . . 16  |-  F/ r  w  e.  NN0
165 nfcv 2223 . . . . . . . . . . . . . . . . 17  |-  F/_ r
( 0 ... (
w  -  1 ) )
166 nfv 1462 . . . . . . . . . . . . . . . . . . 19  |-  F/ r th
167 nfs1v 1858 . . . . . . . . . . . . . . . . . . 19  |-  F/ r [ z  /  r ] ph
168166, 167nfan 1498 . . . . . . . . . . . . . . . . . 18  |-  F/ r ( th  /\  [
z  /  r ]
ph )
169 nfcv 2223 . . . . . . . . . . . . . . . . . . 19  |-  F/_ r NN0
170 nfre1 2412 . . . . . . . . . . . . . . . . . . . 20  |-  F/ r E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
17157, 170nfim 1505 . . . . . . . . . . . . . . . . . . 19  |-  F/ r ( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)
172169, 171nfralxy 2407 . . . . . . . . . . . . . . . . . 18  |-  F/ r A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
173168, 172nfim 1505 . . . . . . . . . . . . . . . . 17  |-  F/ r ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
174165, 173nfralxy 2407 . . . . . . . . . . . . . . . 16  |-  F/ r A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
175164, 174nfan 1498 . . . . . . . . . . . . . . 15  |-  F/ r ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )
176 nfs1v 1858 . . . . . . . . . . . . . . . 16  |-  F/ r [ w  /  r ] ph
177166, 176nfan 1498 . . . . . . . . . . . . . . 15  |-  F/ r ( th  /\  [
w  /  r ]
ph )
178175, 177nfan 1498 . . . . . . . . . . . . . 14  |-  F/ r ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)
179 nfv 1462 . . . . . . . . . . . . . 14  |-  F/ r 0  <  w
180178, 179nfan 1498 . . . . . . . . . . . . 13  |-  F/ r ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )
181 nfv 1462 . . . . . . . . . . . . 13  |-  F/ r  y  e.  NN0
182180, 181nfan 1498 . . . . . . . . . . . 12  |-  F/ r ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )
183182, 57nfan 1498 . . . . . . . . . . 11  |-  F/ r ( ( ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )
18468, 72, 75, 80, 81, 82, 86, 93, 142, 163, 183bezoutlemstep 10593 . . . . . . . . . 10  |-  ( ( ( ( ( ( w  e.  NN0  /\  A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  /\  0  <  w )  /\  y  e.  NN0 )  /\  [
y  /  r ]
ph )  ->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph ) )
185184exp31 356 . . . . . . . . 9  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  ( y  e.  NN0  ->  ( [
y  /  r ]
ph  ->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
) ) )
18667, 185ralrimi 2437 . . . . . . . 8  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
) )
187 sbsbc 2828 . . . . . . . . . . . 12  |-  ( [ w  /  x ] ps 
<-> 
[. w  /  x ]. ps )
188187anbi1i 446 . . . . . . . . . . 11  |-  ( ( [ w  /  x ] ps  /\  ph )  <->  (
[. w  /  x ]. ps  /\  ph )
)
189188rexbii 2378 . . . . . . . . . 10  |-  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
)
190189imbi2i 224 . . . . . . . . 9  |-  ( ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )  <->  ( [
y  /  r ]
ph  ->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
) )
191190ralbii 2377 . . . . . . . 8  |-  ( A. y  e.  NN0  ( [ y  /  r ]
ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
)  <->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph ) ) )
192186, 191sylibr 132 . . . . . . 7  |-  ( ( ( ( w  e. 
NN0  /\  A. z  e.  ( 0 ... (
w  -  1 ) ) ( ( th 
/\  [ z  / 
r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) ) ) )  /\  ( th 
/\  [ w  / 
r ] ph )
)  /\  0  <  w )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
) )
193 nn0nlt0 8433 . . . . . . . . 9  |-  ( w  e.  NN0  ->  -.  w  <  0 )
194 nn0z 8504 . . . . . . . . . . . 12  |-  ( w  e.  NN0  ->  w  e.  ZZ )
195 ztri3or0 8526 . . . . . . . . . . . 12  |-  ( w  e.  ZZ  ->  (
w  <  0  \/  w  =  0  \/  0  <  w ) )
196194, 195syl 14 . . . . . . . . . . 11  |-  ( w  e.  NN0  ->  ( w  <  0  \/  w  =  0  \/  0  <  w ) )
197 3orass 923 . . . . . . . . . . 11  |-  ( ( w  <  0  \/  w  =  0  \/  0  <  w )  <-> 
( w  <  0  \/  ( w  =  0  \/  0  <  w
) ) )
198196, 197sylib 120 . . . . . . . . . 10  |-  ( w  e.  NN0  ->  ( w  <  0  \/  (
w  =  0  \/  0  <  w ) ) )
199198orcomd 681 . . . . . . . . 9  |-  ( w  e.  NN0  ->  ( ( w  =  0  \/  0  <  w )  \/  w  <  0
) )
200193, 199ecased 1281 . . . . . . . 8  |-  ( w  e.  NN0  ->  ( w  =  0  \/  0  <  w ) )
201200ad2antrr 472 . . . . . . 7  |-  ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  ->  (
w  =  0  \/  0  <  w ) )
20265, 192, 201mpjaodan 745 . . . . . 6  |-  ( ( ( w  e.  NN0  /\ 
A. z  e.  ( 0 ... ( w  -  1 ) ) ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) ) )  /\  ( th  /\  [ w  /  r ] ph ) )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
) )
203202exp31 356 . . . . 5  |-  ( w  e.  NN0  ->  ( A. z  e.  ( 0 ... ( w  - 
1 ) ) ( ( th  /\  [
z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )  ->  (
( th  /\  [
w  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
) ) ) )
2048, 16, 203nn0sinds 9572 . . . 4  |-  ( x  e.  NN0  ->  ( ( th  /\  [ x  /  r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) )
205204expd 254 . . 3  |-  ( x  e.  NN0  ->  ( th 
->  ( [ x  / 
r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) ) )
206205impcom 123 . 2  |-  ( ( th  /\  x  e. 
NN0 )  ->  ( [ x  /  r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
207206ralrimiva 2439 1  |-  ( th 
->  A. x  e.  NN0  ( [ x  /  r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 662    \/ w3o 919    = wceq 1285    e. wcel 1434   [wsb 1687   A.wral 2353   E.wrex 2354   [.wsbc 2824   class class class wbr 3805  (class class class)co 5563   0cc0 7095   1c1 7096    + caddc 7098    x. cmul 7100    < clt 7267    - cmin 7398   NNcn 8158   NN0cn0 8407   ZZcz 8484   ...cfz 9157    mod cmo 9456    || cdvds 10403
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3913  ax-sep 3916  ax-nul 3924  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308  ax-iinf 4357  ax-cnex 7181  ax-resscn 7182  ax-1cn 7183  ax-1re 7184  ax-icn 7185  ax-addcl 7186  ax-addrcl 7187  ax-mulcl 7188  ax-mulrcl 7189  ax-addcom 7190  ax-mulcom 7191  ax-addass 7192  ax-mulass 7193  ax-distr 7194  ax-i2m1 7195  ax-0lt1 7196  ax-1rid 7197  ax-0id 7198  ax-rnegex 7199  ax-precex 7200  ax-cnre 7201  ax-pre-ltirr 7202  ax-pre-ltwlin 7203  ax-pre-lttrn 7204  ax-pre-apti 7205  ax-pre-ltadd 7206  ax-pre-mulgt0 7207  ax-pre-mulext 7208  ax-arch 7209
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rmo 2361  df-rab 2362  df-v 2612  df-sbc 2825  df-csb 2918  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-if 3369  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-int 3657  df-iun 3700  df-br 3806  df-opab 3860  df-mpt 3861  df-tr 3896  df-id 4076  df-po 4079  df-iso 4080  df-iord 4149  df-on 4151  df-ilim 4152  df-suc 4154  df-iom 4360  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-f1 4957  df-fo 4958  df-f1o 4959  df-fv 4960  df-riota 5519  df-ov 5566  df-oprab 5567  df-mpt2 5568  df-1st 5818  df-2nd 5819  df-recs 5974  df-frec 6060  df-pnf 7269  df-mnf 7270  df-xr 7271  df-ltxr 7272  df-le 7273  df-sub 7400  df-neg 7401  df-reap 7794  df-ap 7801  df-div 7880  df-inn 8159  df-2 8217  df-n0 8408  df-z 8485  df-uz 8753  df-q 8838  df-rp 8868  df-fz 9158  df-fl 9404  df-mod 9457  df-iseq 9574  df-iexp 9625  df-cj 9930  df-re 9931  df-im 9932  df-rsqrt 10085  df-abs 10086  df-dvds 10404
This theorem is referenced by:  bezoutlemex  10597
  Copyright terms: Public domain W3C validator