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

Theorem bezoutlemmain 11080
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 1768 . . . . . . 7  |-  ( w  =  z  ->  ( [ w  /  r ] ph  <->  [ z  /  r ] ph ) )
21anbi2d 452 . . . . . 6  |-  ( w  =  z  ->  (
( th  /\  [
w  /  r ]
ph )  <->  ( th  /\  [ z  /  r ] ph ) ) )
3 sbequ 1768 . . . . . . . . . 10  |-  ( w  =  z  ->  ( [ w  /  x ] ps  <->  [ z  /  x ] ps ) )
43anbi1d 453 . . . . . . . . 9  |-  ( w  =  z  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( [ z  /  x ] ps  /\  ph ) ) )
54rexbidv 2381 . . . . . . . 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 2380 . . . . . 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 1768 . . . . . . 7  |-  ( w  =  x  ->  ( [ w  /  r ] ph  <->  [ x  /  r ] ph ) )
109anbi2d 452 . . . . . 6  |-  ( w  =  x  ->  (
( th  /\  [
w  /  r ]
ph )  <->  ( th  /\  [ x  /  r ] ph ) ) )
11 sbequ12r 1702 . . . . . . . . . 10  |-  ( w  =  x  ->  ( [ w  /  x ] ps  <->  ps ) )
1211anbi1d 453 . . . . . . . . 9  |-  ( w  =  x  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( ps  /\  ph ) ) )
1312rexbidv 2381 . . . . . . . 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 2380 . . . . . 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 1466 . . . . . . . . . . 11  |-  F/ y  w  e.  NN0
18 nfcv 2228 . . . . . . . . . . . 12  |-  F/_ y
( 0 ... (
w  -  1 ) )
19 nfv 1466 . . . . . . . . . . . . 13  |-  F/ y ( th  /\  [
z  /  r ]
ph )
20 nfra1 2409 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
2119, 20nfim 1509 . . . . . . . . . . . 12  |-  F/ y ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
2218, 21nfralxy 2414 . . . . . . . . . . 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 1502 . . . . . . . . . 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 1466 . . . . . . . . . 10  |-  F/ y ( th  /\  [
w  /  r ]
ph )
2523, 24nfan 1502 . . . . . . . . 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 1466 . . . . . . . . 9  |-  F/ y  w  =  0
2725, 26nfan 1502 . . . . . . . 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 1466 . . . . . . . . . . . . . 14  |-  F/ r A. z  e.  NN0  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y ) )
30 breq2 3841 . . . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . 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 1721 . . . . . . . . . . . . 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 8740 . . . . . . . . . . . . . . . 16  |-  ( z  e.  NN0  ->  z  e.  ZZ )
35 dvds0 10904 . . . . . . . . . . . . . . . 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 2433 . . . . . . . . . . . 12  |-  [ y  /  r ] A. z  e.  NN0  ( z 
||  r  ->  (
z  ||  0  /\  z  ||  y ) )
40 nfv 1466 . . . . . . . . . . . . 13  |-  F/ r  w  =  0
41 dfsbcq2 2841 . . . . . . . . . . . . . 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 2896 . . . . . . . . . . . . . . 15  |-  ( [.
0  /  x ]. ps 
<-> 
[. 0  /  x ]. A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) ) )
44 c0ex 7461 . . . . . . . . . . . . . . . 16  |-  0  e.  _V
45 breq2 3841 . . . . . . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . . . 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 2871 . . . . . . . . . . . . . . 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 1774 . . . . . . . . . . . 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 1863 . . . . . . . . . . . 12  |-  F/ r [ y  /  r ] [ w  /  x ] ps
57 nfs1v 1863 . . . . . . . . . . . 12  |-  F/ r [ y  /  r ] ph
5856, 57nfan 1502 . . . . . . . . . . 11  |-  F/ r ( [ y  / 
r ] [ w  /  x ] ps  /\  [ y  /  r ]
ph )
59 sbequ12 1701 . . . . . . . . . . . 12  |-  ( r  =  y  ->  ( [ w  /  x ] ps  <->  [ y  /  r ] [ w  /  x ] ps ) )
60 sbequ12 1701 . . . . . . . . . . . 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 2717 . . . . . . . . . 10  |-  ( ( y  e.  NN0  /\  ( [ y  /  r ] [ w  /  x ] ps  /\  [ y  /  r ] ph ) )  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )
6328, 54, 55, 62syl12anc 1172 . . . . . . . . 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 2444 . . . . . . 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 1466 . . . . . . . . . 10  |-  F/ y 0  <  w
6725, 66nfan 1502 . . . . . . . . 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 8687 . . . . . . . . . . . . 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 2842 . . . . . . . . . . . . 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 3840 . . . . . . . . . . . . . 14  |-  ( z  =  a  ->  (
z  ||  r  <->  a  ||  r ) )
88 breq1 3840 . . . . . . . . . . . . . . 15  |-  ( z  =  a  ->  (
z  ||  x  <->  a  ||  x ) )
89 breq1 3840 . . . . . . . . . . . . . . 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 2590 . . . . . . . . . . . 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 dfsbcq2 2841 . . . . . . . . . . . . . . 15  |-  ( z  =  ( y  mod  w )  ->  ( [ z  /  r ] ph  <->  [. ( y  mod  w )  /  r ]. ph ) )
9998anbi2d 452 . . . . . . . . . . . . . 14  |-  ( z  =  ( y  mod  w )  ->  (
( th  /\  [
z  /  r ]
ph )  <->  ( th  /\  [. ( y  mod  w )  /  r ]. ph ) ) )
100 sbsbc 2842 . . . . . . . . . . . . . . . . . . 19  |-  ( [ z  /  x ] [ w  /  y ] ps  <->  [. z  /  x ]. [ w  /  y ] ps )
101 sbsbc 2842 . . . . . . . . . . . . . . . . . . . 20  |-  ( [ w  /  y ] ps  <->  [. w  /  y ]. ps )
102101sbcbii 2896 . . . . . . . . . . . . . . . . . . 19  |-  ( [. z  /  x ]. [
w  /  y ] ps  <->  [. z  /  x ]. [. w  /  y ]. ps )
103100, 102bitri 182 . . . . . . . . . . . . . . . . . 18  |-  ( [ z  /  x ] [ w  /  y ] ps  <->  [. z  /  x ]. [. w  /  y ]. ps )
104103anbi1i 446 . . . . . . . . . . . . . . . . 17  |-  ( ( [ z  /  x ] [ w  /  y ] ps  /\  ph )  <->  (
[. z  /  x ]. [. w  /  y ]. ps  /\  ph )
)
105 dfsbcq 2840 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( y  mod  w )  ->  ( [. z  /  x ]. [. w  /  y ]. ps  <->  [. ( y  mod  w )  /  x ]. [. w  /  y ]. ps ) )
106105anbi1d 453 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( y  mod  w )  ->  (
( [. z  /  x ]. [. w  /  y ]. ps  /\  ph )  <->  (
[. ( y  mod  w )  /  x ]. [. w  /  y ]. ps  /\  ph )
) )
107104, 106syl5bb 190 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( y  mod  w )  ->  (
( [ z  /  x ] [ w  / 
y ] ps  /\  ph )  <->  ( [. (
y  mod  w )  /  x ]. [. w  /  y ]. ps  /\ 
ph ) ) )
108107rexbidv 2381 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) )
109108imbi2d 228 . . . . . . . . . . . . . 14  |-  ( 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 )
) ) )
11099, 109imbi12d 232 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) ) )
111 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 ) )
112 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 )
) ) )
113112ad3antrrr 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 )
) ) )
114 nfv 1466 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y [ w  /  r ] ph
115 nfcv 2228 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ y NN0
116 nfs1v 1863 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ y [ w  /  y ] ps
117116nfsbxy 1866 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ y [ z  /  x ] [ w  /  y ] ps
118 nfv 1466 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ y
ph
119117, 118nfan 1502 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ps  /\  ph )
120115, 119nfrexxy 2415 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
121114, 120nfim 1509 . . . . . . . . . . . . . . . . . . 19  |-  F/ y ( [ w  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
)
122 sbequ 1768 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  w  ->  ( [ y  /  r ] ph  <->  [ w  /  r ] ph ) )
123 nfv 1466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ x  y  =  w
124 sbequ12 1701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  w  ->  ( ps 
<->  [ w  /  y ] ps ) )
125123, 124sbbid 1774 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  w  ->  ( [ z  /  x ] ps  <->  [ z  /  x ] [ w  /  y ] ps ) )
126125anbi1d 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  w  ->  (
( [ z  /  x ] ps  /\  ph ) 
<->  ( [ z  /  x ] [ w  / 
y ] ps  /\  ph ) ) )
127126rexbidv 2381 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  w  ->  ( E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
) )
128122, 127imbi12d 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 )
) ) )
129121, 128rspc 2716 . . . . . . . . . . . . . . . . . 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 )
) ) )
130129imim2d 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 )
) ) ) )
131130ralimdv 2442 . . . . . . . . . . . . . . . 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 )
) ) ) )
132131ad4antr 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 )
) ) ) )
133113, 132mpd 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 )
) ) )
134111, 133sylan 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 )
) ) )
135 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 )
136135nn0zd 8836 . . . . . . . . . . . . . 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 )
13779ad3antrrr 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 )
138 zmodfz 9718 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ZZ  /\  w  e.  NN )  ->  ( y  mod  w
)  e.  ( 0 ... ( w  - 
1 ) ) )
139136, 137, 138syl2anc 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 ) ) )
140110, 134, 139rspcdva 2727 . . . . . . . . . . . 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 )
) ) )
14196, 97, 140mp2d 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 )
)
142 nfv 1466 . . . . . . . . . . . . . . . 16  |-  F/ x  w  e.  NN0
143 nfcv 2228 . . . . . . . . . . . . . . . . 17  |-  F/_ x
( 0 ... (
w  -  1 ) )
144 nfv 1466 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( th  /\  [
z  /  r ]
ph )
145 nfcv 2228 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x NN0
146 nfv 1466 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x ph
147146nfsbxy 1866 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x [ y  /  r ] ph
148 nfs1v 1863 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ x [ z  /  x ] ps
149148, 146nfan 1502 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x
( [ z  /  x ] ps  /\  ph )
150145, 149nfrexxy 2415 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
151147, 150nfim 1509 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)
152145, 151nfralxy 2414 . . . . . . . . . . . . . . . . . 18  |-  F/ x A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
153144, 152nfim 1509 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
154143, 153nfralxy 2414 . . . . . . . . . . . . . . . 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 )
) )
155142, 154nfan 1502 . . . . . . . . . . . . . . 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 )
) ) )
156 nfv 1466 . . . . . . . . . . . . . . 15  |-  F/ x
( th  /\  [
w  /  r ]
ph )
157155, 156nfan 1502 . . . . . . . . . . . . . 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 )
)
158 nfv 1466 . . . . . . . . . . . . . 14  |-  F/ x
0  <  w
159157, 158nfan 1502 . . . . . . . . . . . . 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 )
160 nfv 1466 . . . . . . . . . . . . 13  |-  F/ x  y  e.  NN0
161159, 160nfan 1502 . . . . . . . . . . . 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 )
162161, 147nfan 1502 . . . . . . . . . . 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 )
163 nfv 1466 . . . . . . . . . . . . . . . 16  |-  F/ r  w  e.  NN0
164 nfcv 2228 . . . . . . . . . . . . . . . . 17  |-  F/_ r
( 0 ... (
w  -  1 ) )
165 nfv 1466 . . . . . . . . . . . . . . . . . . 19  |-  F/ r th
166 nfs1v 1863 . . . . . . . . . . . . . . . . . . 19  |-  F/ r [ z  /  r ] ph
167165, 166nfan 1502 . . . . . . . . . . . . . . . . . 18  |-  F/ r ( th  /\  [
z  /  r ]
ph )
168 nfcv 2228 . . . . . . . . . . . . . . . . . . 19  |-  F/_ r NN0
169 nfre1 2419 . . . . . . . . . . . . . . . . . . . 20  |-  F/ r E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
17057, 169nfim 1509 . . . . . . . . . . . . . . . . . . 19  |-  F/ r ( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)
171168, 170nfralxy 2414 . . . . . . . . . . . . . . . . . 18  |-  F/ r A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
172167, 171nfim 1509 . . . . . . . . . . . . . . . . 17  |-  F/ r ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
173164, 172nfralxy 2414 . . . . . . . . . . . . . . . 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 )
) )
174163, 173nfan 1502 . . . . . . . . . . . . . . 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 )
) ) )
175 nfs1v 1863 . . . . . . . . . . . . . . . 16  |-  F/ r [ w  /  r ] ph
176165, 175nfan 1502 . . . . . . . . . . . . . . 15  |-  F/ r ( th  /\  [
w  /  r ]
ph )
177174, 176nfan 1502 . . . . . . . . . . . . . 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 )
)
178 nfv 1466 . . . . . . . . . . . . . 14  |-  F/ r 0  <  w
179177, 178nfan 1502 . . . . . . . . . . . . 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 )
180 nfv 1466 . . . . . . . . . . . . 13  |-  F/ r  y  e.  NN0
181179, 180nfan 1502 . . . . . . . . . . . 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 )
182181, 57nfan 1502 . . . . . . . . . . 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 )
18368, 72, 75, 80, 81, 82, 86, 93, 141, 162, 182bezoutlemstep 11079 . . . . . . . . . 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 ) )
184183exp31 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 )
) ) )
18567, 184ralrimi 2444 . . . . . . . 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 )
) )
186 sbsbc 2842 . . . . . . . . . . . 12  |-  ( [ w  /  x ] ps 
<-> 
[. w  /  x ]. ps )
187186anbi1i 446 . . . . . . . . . . 11  |-  ( ( [ w  /  x ] ps  /\  ph )  <->  (
[. w  /  x ]. ps  /\  ph )
)
188187rexbii 2385 . . . . . . . . . 10  |-  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
)
189188imbi2i 224 . . . . . . . . 9  |-  ( ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )  <->  ( [
y  /  r ]
ph  ->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
) )
190189ralbii 2384 . . . . . . . 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 ) ) )
191185, 190sylibr 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 )
) )
192 nn0nlt0 8669 . . . . . . . . 9  |-  ( w  e.  NN0  ->  -.  w  <  0 )
193 nn0z 8740 . . . . . . . . . . . 12  |-  ( w  e.  NN0  ->  w  e.  ZZ )
194 ztri3or0 8762 . . . . . . . . . . . 12  |-  ( w  e.  ZZ  ->  (
w  <  0  \/  w  =  0  \/  0  <  w ) )
195193, 194syl 14 . . . . . . . . . . 11  |-  ( w  e.  NN0  ->  ( w  <  0  \/  w  =  0  \/  0  <  w ) )
196 3orass 927 . . . . . . . . . . 11  |-  ( ( w  <  0  \/  w  =  0  \/  0  <  w )  <-> 
( w  <  0  \/  ( w  =  0  \/  0  <  w
) ) )
197195, 196sylib 120 . . . . . . . . . 10  |-  ( w  e.  NN0  ->  ( w  <  0  \/  (
w  =  0  \/  0  <  w ) ) )
198197orcomd 683 . . . . . . . . 9  |-  ( w  e.  NN0  ->  ( ( w  =  0  \/  0  <  w )  \/  w  <  0
) )
199192, 198ecased 1285 . . . . . . . 8  |-  ( w  e.  NN0  ->  ( w  =  0  \/  0  <  w ) )
200199ad2antrr 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 ) )
20165, 191, 200mpjaodan 747 . . . . . 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 )
) )
202201exp31 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 )
) ) ) )
2038, 16, 202nn0sinds 9815 . . . 4  |-  ( x  e.  NN0  ->  ( ( th  /\  [ x  /  r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) )
204203expd 254 . . 3  |-  ( x  e.  NN0  ->  ( th 
->  ( [ x  / 
r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) ) )
205204impcom 123 . 2  |-  ( ( th  /\  x  e. 
NN0 )  ->  ( [ x  /  r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
206205ralrimiva 2446 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 664    \/ w3o 923    = wceq 1289    e. wcel 1438   [wsb 1692   A.wral 2359   E.wrex 2360   [.wsbc 2838   class class class wbr 3837  (class class class)co 5634   0cc0 7329   1c1 7330    + caddc 7332    x. cmul 7334    < clt 7501    - cmin 7632   NNcn 8394   NN0cn0 8643   ZZcz 8720   ...cfz 9393    mod cmo 9694    || cdvds 10889
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 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343  ax-iinf 4393  ax-cnex 7415  ax-resscn 7416  ax-1cn 7417  ax-1re 7418  ax-icn 7419  ax-addcl 7420  ax-addrcl 7421  ax-mulcl 7422  ax-mulrcl 7423  ax-addcom 7424  ax-mulcom 7425  ax-addass 7426  ax-mulass 7427  ax-distr 7428  ax-i2m1 7429  ax-0lt1 7430  ax-1rid 7431  ax-0id 7432  ax-rnegex 7433  ax-precex 7434  ax-cnre 7435  ax-pre-ltirr 7436  ax-pre-ltwlin 7437  ax-pre-lttrn 7438  ax-pre-apti 7439  ax-pre-ltadd 7440  ax-pre-mulgt0 7441  ax-pre-mulext 7442  ax-arch 7443
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rmo 2367  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-if 3390  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-id 4111  df-po 4114  df-iso 4115  df-iord 4184  df-on 4186  df-ilim 4187  df-suc 4189  df-iom 4396  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-riota 5590  df-ov 5637  df-oprab 5638  df-mpt2 5639  df-1st 5893  df-2nd 5894  df-recs 6052  df-frec 6138  df-pnf 7503  df-mnf 7504  df-xr 7505  df-ltxr 7506  df-le 7507  df-sub 7634  df-neg 7635  df-reap 8028  df-ap 8035  df-div 8114  df-inn 8395  df-2 8452  df-n0 8644  df-z 8721  df-uz 8989  df-q 9074  df-rp 9104  df-fz 9394  df-fl 9642  df-mod 9695  df-iseq 9818  df-seq3 9819  df-exp 9920  df-cj 10241  df-re 10242  df-im 10243  df-rsqrt 10396  df-abs 10397  df-dvds 10890
This theorem is referenced by:  bezoutlemex  11083
  Copyright terms: Public domain W3C validator