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

Theorem bezoutlemmain 11598
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 1796 . . . . . . 7  |-  ( w  =  z  ->  ( [ w  /  r ] ph  <->  [ z  /  r ] ph ) )
21anbi2d 459 . . . . . 6  |-  ( w  =  z  ->  (
( th  /\  [
w  /  r ]
ph )  <->  ( th  /\  [ z  /  r ] ph ) ) )
3 sbequ 1796 . . . . . . . . . 10  |-  ( w  =  z  ->  ( [ w  /  x ] ps  <->  [ z  /  x ] ps ) )
43anbi1d 460 . . . . . . . . 9  |-  ( w  =  z  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( [ z  /  x ] ps  /\  ph ) ) )
54rexbidv 2415 . . . . . . . 8  |-  ( w  =  z  ->  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
65imbi2d 229 . . . . . . 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 2414 . . . . . 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 233 . . . . 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 1796 . . . . . . 7  |-  ( w  =  x  ->  ( [ w  /  r ] ph  <->  [ x  /  r ] ph ) )
109anbi2d 459 . . . . . 6  |-  ( w  =  x  ->  (
( th  /\  [
w  /  r ]
ph )  <->  ( th  /\  [ x  /  r ] ph ) ) )
11 sbequ12r 1730 . . . . . . . . . 10  |-  ( w  =  x  ->  ( [ w  /  x ] ps  <->  ps ) )
1211anbi1d 460 . . . . . . . . 9  |-  ( w  =  x  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( ps  /\  ph ) ) )
1312rexbidv 2415 . . . . . . . 8  |-  ( w  =  x  ->  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( ps  /\  ph ) ) )
1413imbi2d 229 . . . . . . 7  |-  ( w  =  x  ->  (
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
)  <->  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
1514ralbidv 2414 . . . . . 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 233 . . . . 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 1493 . . . . . . . . . . 11  |-  F/ y  w  e.  NN0
18 nfcv 2258 . . . . . . . . . . . 12  |-  F/_ y
( 0 ... (
w  -  1 ) )
19 nfv 1493 . . . . . . . . . . . . 13  |-  F/ y ( th  /\  [
z  /  r ]
ph )
20 nfra1 2443 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
2119, 20nfim 1536 . . . . . . . . . . . 12  |-  F/ y ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
2218, 21nfralxy 2448 . . . . . . . . . . 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 1529 . . . . . . . . . 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 1493 . . . . . . . . . 10  |-  F/ y ( th  /\  [
w  /  r ]
ph )
2523, 24nfan 1529 . . . . . . . . 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 1493 . . . . . . . . 9  |-  F/ y  w  =  0
2725, 26nfan 1529 . . . . . . . 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 504 . . . . . . . . . 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 1493 . . . . . . . . . . . . . 14  |-  F/ r A. z  e.  NN0  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y ) )
30 breq2 3903 . . . . . . . . . . . . . . . 16  |-  ( r  =  y  ->  (
z  ||  r  <->  z  ||  y ) )
3130imbi1d 230 . . . . . . . . . . . . . . 15  |-  ( r  =  y  ->  (
( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) )  <->  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y
) ) ) )
3231ralbidv 2414 . . . . . . . . . . . . . 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 1749 . . . . . . . . . . . . 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 9032 . . . . . . . . . . . . . . . 16  |-  ( z  e.  NN0  ->  z  e.  ZZ )
35 dvds0 11420 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ZZ  ->  z  ||  0 )
3634, 35syl 14 . . . . . . . . . . . . . . 15  |-  ( z  e.  NN0  ->  z  ||  0 )
3736biantrurd 303 . . . . . . . . . . . . . 14  |-  ( z  e.  NN0  ->  ( z 
||  y  <->  ( z  ||  0  /\  z  ||  y ) ) )
3837biimpd 143 . . . . . . . . . . . . 13  |-  ( z  e.  NN0  ->  ( z 
||  y  ->  (
z  ||  0  /\  z  ||  y ) ) )
3933, 38mprgbir 2467 . . . . . . . . . . . 12  |-  [ y  /  r ] A. z  e.  NN0  ( z 
||  r  ->  (
z  ||  0  /\  z  ||  y ) )
40 nfv 1493 . . . . . . . . . . . . 13  |-  F/ r  w  =  0
41 dfsbcq2 2885 . . . . . . . . . . . . . 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 2940 . . . . . . . . . . . . . . 15  |-  ( [.
0  /  x ]. ps 
<-> 
[. 0  /  x ]. A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) ) )
44 c0ex 7728 . . . . . . . . . . . . . . . 16  |-  0  e.  _V
45 breq2 3903 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  0  ->  (
z  ||  x  <->  z  ||  0 ) )
4645anbi1d 460 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  0  ->  (
( z  ||  x  /\  z  ||  y )  <-> 
( z  ||  0  /\  z  ||  y ) ) )
4746imbi2d 229 . . . . . . . . . . . . . . . . 17  |-  ( x  =  0  ->  (
( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) )  <->  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y
) ) ) )
4847ralbidv 2414 . . . . . . . . . . . . . . . 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 2915 . . . . . . . . . . . . . . 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 183 . . . . . . . . . . . . . 14  |-  ( [.
0  /  x ]. ps 
<-> 
A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) )
5141, 50syl6bb 195 . . . . . . . . . . . . 13  |-  ( w  =  0  ->  ( [ w  /  x ] ps  <->  A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) ) )
5240, 51sbbid 1802 . . . . . . . . . . . 12  |-  ( w  =  0  ->  ( [ y  /  r ] [ w  /  x ] ps  <->  [ y  /  r ] A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) ) )
5339, 52mpbiri 167 . . . . . . . . . . 11  |-  ( w  =  0  ->  [ y  /  r ] [
w  /  x ] ps )
5453ad3antlr 484 . . . . . . . . . 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 109 . . . . . . . . . 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 1892 . . . . . . . . . . . 12  |-  F/ r [ y  /  r ] [ w  /  x ] ps
57 nfs1v 1892 . . . . . . . . . . . 12  |-  F/ r [ y  /  r ] ph
5856, 57nfan 1529 . . . . . . . . . . 11  |-  F/ r ( [ y  / 
r ] [ w  /  x ] ps  /\  [ y  /  r ]
ph )
59 sbequ12 1729 . . . . . . . . . . . 12  |-  ( r  =  y  ->  ( [ w  /  x ] ps  <->  [ y  /  r ] [ w  /  x ] ps ) )
60 sbequ12 1729 . . . . . . . . . . . 12  |-  ( r  =  y  ->  ( ph 
<->  [ y  /  r ] ph ) )
6159, 60anbi12d 464 . . . . . . . . . . 11  |-  ( r  =  y  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( [ y  / 
r ] [ w  /  x ] ps  /\  [ y  /  r ]
ph ) ) )
6258, 61rspce 2758 . . . . . . . . . 10  |-  ( ( y  e.  NN0  /\  ( [ y  /  r ] [ w  /  x ] ps  /\  [ y  /  r ] ph ) )  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )
6328, 54, 55, 62syl12anc 1199 . . . . . . . . 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 361 . . . . . . . 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 2480 . . . . . . 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 1493 . . . . . . . . . 10  |-  F/ y 0  <  w
6725, 66nfan 1529 . . . . . . . . 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 509 . . . . . . . . . . . . 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 479 . . . . . . . . . . 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 479 . . . . . . . . . . 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 507 . . . . . . . . . . . . 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 109 . . . . . . . . . . . . 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 8979 . . . . . . . . . . . . 13  |-  ( w  e.  NN  <->  ( w  e.  NN0  /\  0  < 
w ) )
7976, 77, 78sylanbrc 413 . . . . . . . . . . . 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 479 . . . . . . . . . . 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 109 . . . . . . . . . . 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 504 . . . . . . . . . . 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 510 . . . . . . . . . . . . 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 2886 . . . . . . . . . . . . 13  |-  ( [ w  /  r ]
ph 
<-> 
[. w  /  r ]. ph )
8583, 84sylib 121 . . . . . . . . . . . 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 479 . . . . . . . . . . 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 3902 . . . . . . . . . . . . . 14  |-  ( z  =  a  ->  (
z  ||  r  <->  a  ||  r ) )
88 breq1 3902 . . . . . . . . . . . . . . 15  |-  ( z  =  a  ->  (
z  ||  x  <->  a  ||  x ) )
89 breq1 3902 . . . . . . . . . . . . . . 15  |-  ( z  =  a  ->  (
z  ||  y  <->  a  ||  y ) )
9088, 89anbi12d 464 . . . . . . . . . . . . . 14  |-  ( z  =  a  ->  (
( z  ||  x  /\  z  ||  y )  <-> 
( a  ||  x  /\  a  ||  y ) ) )
9187, 90imbi12d 233 . . . . . . . . . . . . 13  |-  ( z  =  a  ->  (
( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) )  <->  ( a  ||  r  ->  ( a  ||  x  /\  a  ||  y
) ) ) )
9291cbvralv 2631 . . . . . . . . . . . 12  |-  ( A. z  e.  NN0  ( z 
||  r  ->  (
z  ||  x  /\  z  ||  y ) )  <->  A. a  e.  NN0  ( a  ||  r  ->  ( a  ||  x  /\  a  ||  y ) ) )
9342, 92bitri 183 . . . . . . . . . . 11  |-  ( ps  <->  A. a  e.  NN0  (
a  ||  r  ->  ( a  ||  x  /\  a  ||  y ) ) )
9469ad3antrrr 483 . . . . . . . . . . . . 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 109 . . . . . . . . . . . . 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 304 . . . . . . . . . . . 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 483 . . . . . . . . . . . 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 2885 . . . . . . . . . . . . . . 15  |-  ( z  =  ( y  mod  w )  ->  ( [ z  /  r ] ph  <->  [. ( y  mod  w )  /  r ]. ph ) )
9998anbi2d 459 . . . . . . . . . . . . . 14  |-  ( z  =  ( y  mod  w )  ->  (
( th  /\  [
z  /  r ]
ph )  <->  ( th  /\  [. ( y  mod  w )  /  r ]. ph ) ) )
100 sbsbc 2886 . . . . . . . . . . . . . . . . . . 19  |-  ( [ z  /  x ] [ w  /  y ] ps  <->  [. z  /  x ]. [ w  /  y ] ps )
101 sbsbc 2886 . . . . . . . . . . . . . . . . . . . 20  |-  ( [ w  /  y ] ps  <->  [. w  /  y ]. ps )
102101sbcbii 2940 . . . . . . . . . . . . . . . . . . 19  |-  ( [. z  /  x ]. [
w  /  y ] ps  <->  [. z  /  x ]. [. w  /  y ]. ps )
103100, 102bitri 183 . . . . . . . . . . . . . . . . . 18  |-  ( [ z  /  x ] [ w  /  y ] ps  <->  [. z  /  x ]. [. w  /  y ]. ps )
104103anbi1i 453 . . . . . . . . . . . . . . . . 17  |-  ( ( [ z  /  x ] [ w  /  y ] ps  /\  ph )  <->  (
[. z  /  x ]. [. w  /  y ]. ps  /\  ph )
)
105 dfsbcq 2884 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( y  mod  w )  ->  ( [. z  /  x ]. [. w  /  y ]. ps  <->  [. ( y  mod  w )  /  x ]. [. w  /  y ]. ps ) )
106105anbi1d 460 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( y  mod  w )  ->  (
( [. z  /  x ]. [. w  /  y ]. ps  /\  ph )  <->  (
[. ( y  mod  w )  /  x ]. [. w  /  y ]. ps  /\  ph )
) )
107104, 106syl5bb 191 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( y  mod  w )  ->  (
( [ z  /  x ] [ w  / 
y ] ps  /\  ph )  <->  ( [. (
y  mod  w )  /  x ]. [. w  /  y ]. ps  /\ 
ph ) ) )
108107rexbidv 2415 . . . . . . . . . . . . . . 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 229 . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . 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 503 . . . . . . . . . . . . . 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 109 . . . . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . 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 1493 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y [ w  /  r ] ph
115 nfcv 2258 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ y NN0
116 nfs1v 1892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ y [ w  /  y ] ps
117116nfsbxy 1895 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ y [ z  /  x ] [ w  /  y ] ps
118 nfv 1493 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ y
ph
119117, 118nfan 1529 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ps  /\  ph )
120115, 119nfrexxy 2449 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
121114, 120nfim 1536 . . . . . . . . . . . . . . . . . . 19  |-  F/ y ( [ w  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
)
122 sbequ 1796 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  w  ->  ( [ y  /  r ] ph  <->  [ w  /  r ] ph ) )
123 nfv 1493 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ x  y  =  w
124 sbequ12 1729 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  w  ->  ( ps 
<->  [ w  /  y ] ps ) )
125123, 124sbbid 1802 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  w  ->  ( [ z  /  x ] ps  <->  [ z  /  x ] [ w  /  y ] ps ) )
126125anbi1d 460 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  w  ->  (
( [ z  /  x ] ps  /\  ph ) 
<->  ( [ z  /  x ] [ w  / 
y ] ps  /\  ph ) ) )
127126rexbidv 2415 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  w  ->  ( E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
) )
128122, 127imbi12d 233 . . . . . . . . . . . . . . . . . . 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 2757 . . . . . . . . . . . . . . . . . 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 54 . . . . . . . . . . . . . . . . 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 2477 . . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . 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 281 . . . . . . . . . . . . 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 508 . . . . . . . . . . . . . . 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 9129 . . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . 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 10074 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ZZ  /\  w  e.  NN )  ->  ( y  mod  w
)  e.  ( 0 ... ( w  - 
1 ) ) )
139136, 137, 138syl2anc 408 . . . . . . . . . . . . 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 2768 . . . . . . . . . . . 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 47 . . . . . . . . . . 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 1493 . . . . . . . . . . . . . . . 16  |-  F/ x  w  e.  NN0
143 nfcv 2258 . . . . . . . . . . . . . . . . 17  |-  F/_ x
( 0 ... (
w  -  1 ) )
144 nfv 1493 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( th  /\  [
z  /  r ]
ph )
145 nfcv 2258 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x NN0
146 nfv 1493 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x ph
147146nfsbxy 1895 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x [ y  /  r ] ph
148 nfs1v 1892 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ x [ z  /  x ] ps
149148, 146nfan 1529 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x
( [ z  /  x ] ps  /\  ph )
150145, 149nfrexxy 2449 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
151147, 150nfim 1536 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)
152145, 151nfralxy 2448 . . . . . . . . . . . . . . . . . 18  |-  F/ x A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
153144, 152nfim 1536 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
154143, 153nfralxy 2448 . . . . . . . . . . . . . . . 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 1529 . . . . . . . . . . . . . . 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 1493 . . . . . . . . . . . . . . 15  |-  F/ x
( th  /\  [
w  /  r ]
ph )
157155, 156nfan 1529 . . . . . . . . . . . . . 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 1493 . . . . . . . . . . . . . 14  |-  F/ x
0  <  w
159157, 158nfan 1529 . . . . . . . . . . . . 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 1493 . . . . . . . . . . . . 13  |-  F/ x  y  e.  NN0
161159, 160nfan 1529 . . . . . . . . . . . 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 1529 . . . . . . . . . . 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 1493 . . . . . . . . . . . . . . . 16  |-  F/ r  w  e.  NN0
164 nfcv 2258 . . . . . . . . . . . . . . . . 17  |-  F/_ r
( 0 ... (
w  -  1 ) )
165 nfv 1493 . . . . . . . . . . . . . . . . . . 19  |-  F/ r th
166 nfs1v 1892 . . . . . . . . . . . . . . . . . . 19  |-  F/ r [ z  /  r ] ph
167165, 166nfan 1529 . . . . . . . . . . . . . . . . . 18  |-  F/ r ( th  /\  [
z  /  r ]
ph )
168 nfcv 2258 . . . . . . . . . . . . . . . . . . 19  |-  F/_ r NN0
169 nfre1 2453 . . . . . . . . . . . . . . . . . . . 20  |-  F/ r E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
17057, 169nfim 1536 . . . . . . . . . . . . . . . . . . 19  |-  F/ r ( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)
171168, 170nfralxy 2448 . . . . . . . . . . . . . . . . . 18  |-  F/ r A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
172167, 171nfim 1536 . . . . . . . . . . . . . . . . 17  |-  F/ r ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
173164, 172nfralxy 2448 . . . . . . . . . . . . . . . 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 1529 . . . . . . . . . . . . . . 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 1892 . . . . . . . . . . . . . . . 16  |-  F/ r [ w  /  r ] ph
176165, 175nfan 1529 . . . . . . . . . . . . . . 15  |-  F/ r ( th  /\  [
w  /  r ]
ph )
177174, 176nfan 1529 . . . . . . . . . . . . . 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 1493 . . . . . . . . . . . . . 14  |-  F/ r 0  <  w
179177, 178nfan 1529 . . . . . . . . . . . . 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 1493 . . . . . . . . . . . . 13  |-  F/ r  y  e.  NN0
181179, 180nfan 1529 . . . . . . . . . . . 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 1529 . . . . . . . . . . 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 11597 . . . . . . . . . 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 361 . . . . . . . . 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 2480 . . . . . . . 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 2886 . . . . . . . . . . . 12  |-  ( [ w  /  x ] ps 
<-> 
[. w  /  x ]. ps )
187186anbi1i 453 . . . . . . . . . . 11  |-  ( ( [ w  /  x ] ps  /\  ph )  <->  (
[. w  /  x ]. ps  /\  ph )
)
188187rexbii 2419 . . . . . . . . . 10  |-  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
)
189188imbi2i 225 . . . . . . . . 9  |-  ( ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )  <->  ( [
y  /  r ]
ph  ->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
) )
190189ralbii 2418 . . . . . . . 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 133 . . . . . . 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 8961 . . . . . . . . 9  |-  ( w  e.  NN0  ->  -.  w  <  0 )
193 nn0z 9032 . . . . . . . . . . . 12  |-  ( w  e.  NN0  ->  w  e.  ZZ )
194 ztri3or0 9054 . . . . . . . . . . . 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 950 . . . . . . . . . . 11  |-  ( ( w  <  0  \/  w  =  0  \/  0  <  w )  <-> 
( w  <  0  \/  ( w  =  0  \/  0  <  w
) ) )
197195, 196sylib 121 . . . . . . . . . 10  |-  ( w  e.  NN0  ->  ( w  <  0  \/  (
w  =  0  \/  0  <  w ) ) )
198197orcomd 703 . . . . . . . . 9  |-  ( w  e.  NN0  ->  ( ( w  =  0  \/  0  <  w )  \/  w  <  0
) )
199192, 198ecased 1312 . . . . . . . 8  |-  ( w  e.  NN0  ->  ( w  =  0  \/  0  <  w ) )
200199ad2antrr 479 . . . . . . 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 772 . . . . . 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 361 . . . . 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 10172 . . . 4  |-  ( x  e.  NN0  ->  ( ( th  /\  [ x  /  r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) )
204203expd 256 . . 3  |-  ( x  e.  NN0  ->  ( th 
->  ( [ x  / 
r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) ) )
205204impcom 124 . 2  |-  ( ( th  /\  x  e. 
NN0 )  ->  ( [ x  /  r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
206205ralrimiva 2482 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 103    <-> wb 104    \/ wo 682    \/ w3o 946    = wceq 1316    e. wcel 1465   [wsb 1720   A.wral 2393   E.wrex 2394   [.wsbc 2882   class class class wbr 3899  (class class class)co 5742   0cc0 7588   1c1 7589    + caddc 7591    x. cmul 7593    < clt 7768    - cmin 7901   NNcn 8684   NN0cn0 8935   ZZcz 9012   ...cfz 9745    mod cmo 10050    || cdvds 11405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705  ax-pre-mulext 7706  ax-arch 7707
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-if 3445  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-ilim 4261  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-frec 6256  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-reap 8304  df-ap 8311  df-div 8400  df-inn 8685  df-2 8743  df-n0 8936  df-z 9013  df-uz 9283  df-q 9368  df-rp 9398  df-fz 9746  df-fl 9998  df-mod 10051  df-seqfrec 10174  df-exp 10248  df-cj 10569  df-re 10570  df-im 10571  df-rsqrt 10725  df-abs 10726  df-dvds 11406
This theorem is referenced by:  bezoutlemex  11601
  Copyright terms: Public domain W3C validator