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

Theorem bezoutlemmain 12012
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 1850 . . . . . . 7  |-  ( w  =  z  ->  ( [ w  /  r ] ph  <->  [ z  /  r ] ph ) )
21anbi2d 464 . . . . . 6  |-  ( w  =  z  ->  (
( th  /\  [
w  /  r ]
ph )  <->  ( th  /\  [ z  /  r ] ph ) ) )
3 sbequ 1850 . . . . . . . . . 10  |-  ( w  =  z  ->  ( [ w  /  x ] ps  <->  [ z  /  x ] ps ) )
43anbi1d 465 . . . . . . . . 9  |-  ( w  =  z  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( [ z  /  x ] ps  /\  ph ) ) )
54rexbidv 2488 . . . . . . . 8  |-  ( w  =  z  ->  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
65imbi2d 230 . . . . . . 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 2487 . . . . . 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 234 . . . . 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 1850 . . . . . . 7  |-  ( w  =  x  ->  ( [ w  /  r ] ph  <->  [ x  /  r ] ph ) )
109anbi2d 464 . . . . . 6  |-  ( w  =  x  ->  (
( th  /\  [
w  /  r ]
ph )  <->  ( th  /\  [ x  /  r ] ph ) ) )
11 sbequ12r 1782 . . . . . . . . . 10  |-  ( w  =  x  ->  ( [ w  /  x ] ps  <->  ps ) )
1211anbi1d 465 . . . . . . . . 9  |-  ( w  =  x  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( ps  /\  ph ) ) )
1312rexbidv 2488 . . . . . . . 8  |-  ( w  =  x  ->  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( ps  /\  ph ) ) )
1413imbi2d 230 . . . . . . 7  |-  ( w  =  x  ->  (
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )
)  <->  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
1514ralbidv 2487 . . . . . 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 234 . . . . 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 1538 . . . . . . . . . . 11  |-  F/ y  w  e.  NN0
18 nfcv 2329 . . . . . . . . . . . 12  |-  F/_ y
( 0 ... (
w  -  1 ) )
19 nfv 1538 . . . . . . . . . . . . 13  |-  F/ y ( th  /\  [
z  /  r ]
ph )
20 nfra1 2518 . . . . . . . . . . . . 13  |-  F/ y A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
2119, 20nfim 1582 . . . . . . . . . . . 12  |-  F/ y ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
2218, 21nfralxy 2525 . . . . . . . . . . 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 1575 . . . . . . . . . 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 1538 . . . . . . . . . 10  |-  F/ y ( th  /\  [
w  /  r ]
ph )
2523, 24nfan 1575 . . . . . . . . 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 1538 . . . . . . . . 9  |-  F/ y  w  =  0
2725, 26nfan 1575 . . . . . . . 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 528 . . . . . . . . . 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 1538 . . . . . . . . . . . . . 14  |-  F/ r A. z  e.  NN0  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y ) )
30 breq2 4019 . . . . . . . . . . . . . . . 16  |-  ( r  =  y  ->  (
z  ||  r  <->  z  ||  y ) )
3130imbi1d 231 . . . . . . . . . . . . . . 15  |-  ( r  =  y  ->  (
( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) )  <->  ( z  ||  y  ->  ( z  ||  0  /\  z  ||  y
) ) ) )
3231ralbidv 2487 . . . . . . . . . . . . . 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 1801 . . . . . . . . . . . . 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 9286 . . . . . . . . . . . . . . . 16  |-  ( z  e.  NN0  ->  z  e.  ZZ )
35 dvds0 11826 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ZZ  ->  z  ||  0 )
3634, 35syl 14 . . . . . . . . . . . . . . 15  |-  ( z  e.  NN0  ->  z  ||  0 )
3736biantrurd 305 . . . . . . . . . . . . . 14  |-  ( z  e.  NN0  ->  ( z 
||  y  <->  ( z  ||  0  /\  z  ||  y ) ) )
3837biimpd 144 . . . . . . . . . . . . 13  |-  ( z  e.  NN0  ->  ( z 
||  y  ->  (
z  ||  0  /\  z  ||  y ) ) )
3933, 38mprgbir 2545 . . . . . . . . . . . 12  |-  [ y  /  r ] A. z  e.  NN0  ( z 
||  r  ->  (
z  ||  0  /\  z  ||  y ) )
40 nfv 1538 . . . . . . . . . . . . 13  |-  F/ r  w  =  0
41 dfsbcq2 2977 . . . . . . . . . . . . . 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 3034 . . . . . . . . . . . . . . 15  |-  ( [.
0  /  x ]. ps 
<-> 
[. 0  /  x ]. A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) ) )
44 c0ex 7964 . . . . . . . . . . . . . . . 16  |-  0  e.  _V
45 breq2 4019 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  0  ->  (
z  ||  x  <->  z  ||  0 ) )
4645anbi1d 465 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  0  ->  (
( z  ||  x  /\  z  ||  y )  <-> 
( z  ||  0  /\  z  ||  y ) ) )
4746imbi2d 230 . . . . . . . . . . . . . . . . 17  |-  ( x  =  0  ->  (
( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) )  <->  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y
) ) ) )
4847ralbidv 2487 . . . . . . . . . . . . . . . 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 3009 . . . . . . . . . . . . . . 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 184 . . . . . . . . . . . . . 14  |-  ( [.
0  /  x ]. ps 
<-> 
A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) )
5141, 50bitrdi 196 . . . . . . . . . . . . 13  |-  ( w  =  0  ->  ( [ w  /  x ] ps  <->  A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) ) )
5240, 51sbbid 1856 . . . . . . . . . . . 12  |-  ( w  =  0  ->  ( [ y  /  r ] [ w  /  x ] ps  <->  [ y  /  r ] A. z  e.  NN0  ( z  ||  r  ->  ( z  ||  0  /\  z  ||  y ) ) ) )
5339, 52mpbiri 168 . . . . . . . . . . 11  |-  ( w  =  0  ->  [ y  /  r ] [
w  /  x ] ps )
5453ad3antlr 493 . . . . . . . . . 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 110 . . . . . . . . . 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 1949 . . . . . . . . . . . 12  |-  F/ r [ y  /  r ] [ w  /  x ] ps
57 nfs1v 1949 . . . . . . . . . . . 12  |-  F/ r [ y  /  r ] ph
5856, 57nfan 1575 . . . . . . . . . . 11  |-  F/ r ( [ y  / 
r ] [ w  /  x ] ps  /\  [ y  /  r ]
ph )
59 sbequ12 1781 . . . . . . . . . . . 12  |-  ( r  =  y  ->  ( [ w  /  x ] ps  <->  [ y  /  r ] [ w  /  x ] ps ) )
60 sbequ12 1781 . . . . . . . . . . . 12  |-  ( r  =  y  ->  ( ph 
<->  [ y  /  r ] ph ) )
6159, 60anbi12d 473 . . . . . . . . . . 11  |-  ( r  =  y  ->  (
( [ w  /  x ] ps  /\  ph ) 
<->  ( [ y  / 
r ] [ w  /  x ] ps  /\  [ y  /  r ]
ph ) ) )
6258, 61rspce 2848 . . . . . . . . . 10  |-  ( ( y  e.  NN0  /\  ( [ y  /  r ] [ w  /  x ] ps  /\  [ y  /  r ] ph ) )  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )
6328, 54, 55, 62syl12anc 1246 . . . . . . . . 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 364 . . . . . . . 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 2558 . . . . . . 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 1538 . . . . . . . . . 10  |-  F/ y 0  <  w
6725, 66nfan 1575 . . . . . . . . 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 535 . . . . . . . . . . . . 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 488 . . . . . . . . . . 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 488 . . . . . . . . . . 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 533 . . . . . . . . . . . . 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 110 . . . . . . . . . . . . 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 9233 . . . . . . . . . . . . 13  |-  ( w  e.  NN  <->  ( w  e.  NN0  /\  0  < 
w ) )
7976, 77, 78sylanbrc 417 . . . . . . . . . . . 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 488 . . . . . . . . . . 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 110 . . . . . . . . . . 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 528 . . . . . . . . . . 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 536 . . . . . . . . . . . . 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 2978 . . . . . . . . . . . . 13  |-  ( [ w  /  r ]
ph 
<-> 
[. w  /  r ]. ph )
8583, 84sylib 122 . . . . . . . . . . . 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 488 . . . . . . . . . . 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 4018 . . . . . . . . . . . . . 14  |-  ( z  =  a  ->  (
z  ||  r  <->  a  ||  r ) )
88 breq1 4018 . . . . . . . . . . . . . . 15  |-  ( z  =  a  ->  (
z  ||  x  <->  a  ||  x ) )
89 breq1 4018 . . . . . . . . . . . . . . 15  |-  ( z  =  a  ->  (
z  ||  y  <->  a  ||  y ) )
9088, 89anbi12d 473 . . . . . . . . . . . . . 14  |-  ( z  =  a  ->  (
( z  ||  x  /\  z  ||  y )  <-> 
( a  ||  x  /\  a  ||  y ) ) )
9187, 90imbi12d 234 . . . . . . . . . . . . 13  |-  ( z  =  a  ->  (
( z  ||  r  ->  ( z  ||  x  /\  z  ||  y ) )  <->  ( a  ||  r  ->  ( a  ||  x  /\  a  ||  y
) ) ) )
9291cbvralv 2715 . . . . . . . . . . . 12  |-  ( A. z  e.  NN0  ( z 
||  r  ->  (
z  ||  x  /\  z  ||  y ) )  <->  A. a  e.  NN0  ( a  ||  r  ->  ( a  ||  x  /\  a  ||  y ) ) )
9342, 92bitri 184 . . . . . . . . . . 11  |-  ( ps  <->  A. a  e.  NN0  (
a  ||  r  ->  ( a  ||  x  /\  a  ||  y ) ) )
9469ad3antrrr 492 . . . . . . . . . . . . 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 110 . . . . . . . . . . . . 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 306 . . . . . . . . . . . 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 492 . . . . . . . . . . . 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 2977 . . . . . . . . . . . . . . 15  |-  ( z  =  ( y  mod  w )  ->  ( [ z  /  r ] ph  <->  [. ( y  mod  w )  /  r ]. ph ) )
9998anbi2d 464 . . . . . . . . . . . . . 14  |-  ( z  =  ( y  mod  w )  ->  (
( th  /\  [
z  /  r ]
ph )  <->  ( th  /\  [. ( y  mod  w )  /  r ]. ph ) ) )
100 sbsbc 2978 . . . . . . . . . . . . . . . . . . 19  |-  ( [ z  /  x ] [ w  /  y ] ps  <->  [. z  /  x ]. [ w  /  y ] ps )
101 sbsbc 2978 . . . . . . . . . . . . . . . . . . . 20  |-  ( [ w  /  y ] ps  <->  [. w  /  y ]. ps )
102101sbcbii 3034 . . . . . . . . . . . . . . . . . . 19  |-  ( [. z  /  x ]. [
w  /  y ] ps  <->  [. z  /  x ]. [. w  /  y ]. ps )
103100, 102bitri 184 . . . . . . . . . . . . . . . . . 18  |-  ( [ z  /  x ] [ w  /  y ] ps  <->  [. z  /  x ]. [. w  /  y ]. ps )
104103anbi1i 458 . . . . . . . . . . . . . . . . 17  |-  ( ( [ z  /  x ] [ w  /  y ] ps  /\  ph )  <->  (
[. z  /  x ]. [. w  /  y ]. ps  /\  ph )
)
105 dfsbcq 2976 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( y  mod  w )  ->  ( [. z  /  x ]. [. w  /  y ]. ps  <->  [. ( y  mod  w )  /  x ]. [. w  /  y ]. ps ) )
106105anbi1d 465 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( y  mod  w )  ->  (
( [. z  /  x ]. [. w  /  y ]. ps  /\  ph )  <->  (
[. ( y  mod  w )  /  x ]. [. w  /  y ]. ps  /\  ph )
) )
107104, 106bitrid 192 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( y  mod  w )  ->  (
( [ z  /  x ] [ w  / 
y ] ps  /\  ph )  <->  ( [. (
y  mod  w )  /  x ]. [. w  /  y ]. ps  /\ 
ph ) ) )
108107rexbidv 2488 . . . . . . . . . . . . . . 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 230 . . . . . . . . . . . . . 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 234 . . . . . . . . . . . . 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 527 . . . . . . . . . . . . . 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 110 . . . . . . . . . . . . . . . 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 492 . . . . . . . . . . . . . . 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 1538 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y [ w  /  r ] ph
115 nfcv 2329 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ y NN0
116 nfs1v 1949 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ y [ w  /  y ] ps
117116nfsbxy 1952 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ y [ z  /  x ] [ w  /  y ] ps
118 nfv 1538 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ y
ph
119117, 118nfan 1575 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ y ( [ z  /  x ] [ w  / 
y ] ps  /\  ph )
120115, 119nfrexxy 2526 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
121114, 120nfim 1582 . . . . . . . . . . . . . . . . . . 19  |-  F/ y ( [ w  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
)
122 sbequ 1850 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  w  ->  ( [ y  /  r ] ph  <->  [ w  /  r ] ph ) )
123 nfv 1538 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ x  y  =  w
124 sbequ12 1781 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  w  ->  ( ps 
<->  [ w  /  y ] ps ) )
125123, 124sbbid 1856 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  w  ->  ( [ z  /  x ] ps  <->  [ z  /  x ] [ w  /  y ] ps ) )
126125anbi1d 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  w  ->  (
( [ z  /  x ] ps  /\  ph ) 
<->  ( [ z  /  x ] [ w  / 
y ] ps  /\  ph ) ) )
127126rexbidv 2488 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  w  ->  ( E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [ z  /  x ] [ w  /  y ] ps  /\  ph )
) )
128122, 127imbi12d 234 . . . . . . . . . . . . . . . . . . 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 2847 . . . . . . . . . . . . . . . . . 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 2555 . . . . . . . . . . . . . . . 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 494 . . . . . . . . . . . . . . 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 283 . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . 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 9386 . . . . . . . . . . . . . 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 492 . . . . . . . . . . . . . 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 10359 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ZZ  /\  w  e.  NN )  ->  ( y  mod  w
)  e.  ( 0 ... ( w  - 
1 ) ) )
139136, 137, 138syl2anc 411 . . . . . . . . . . . . 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 2858 . . . . . . . . . . . 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 1538 . . . . . . . . . . . . . . . 16  |-  F/ x  w  e.  NN0
143 nfcv 2329 . . . . . . . . . . . . . . . . 17  |-  F/_ x
( 0 ... (
w  -  1 ) )
144 nfv 1538 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( th  /\  [
z  /  r ]
ph )
145 nfcv 2329 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x NN0
146 nfv 1538 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x ph
147146nfsbxy 1952 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x [ y  /  r ] ph
148 nfs1v 1949 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ x [ z  /  x ] ps
149148, 146nfan 1575 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x
( [ z  /  x ] ps  /\  ph )
150145, 149nfrexxy 2526 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
151147, 150nfim 1582 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)
152145, 151nfralxy 2525 . . . . . . . . . . . . . . . . . 18  |-  F/ x A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
153144, 152nfim 1582 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
154143, 153nfralxy 2525 . . . . . . . . . . . . . . . 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 1575 . . . . . . . . . . . . . . 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 1538 . . . . . . . . . . . . . . 15  |-  F/ x
( th  /\  [
w  /  r ]
ph )
157155, 156nfan 1575 . . . . . . . . . . . . . 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 1538 . . . . . . . . . . . . . 14  |-  F/ x
0  <  w
159157, 158nfan 1575 . . . . . . . . . . . . 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 1538 . . . . . . . . . . . . 13  |-  F/ x  y  e.  NN0
161159, 160nfan 1575 . . . . . . . . . . . 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 1575 . . . . . . . . . . 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 1538 . . . . . . . . . . . . . . . 16  |-  F/ r  w  e.  NN0
164 nfcv 2329 . . . . . . . . . . . . . . . . 17  |-  F/_ r
( 0 ... (
w  -  1 ) )
165 nfv 1538 . . . . . . . . . . . . . . . . . . 19  |-  F/ r th
166 nfs1v 1949 . . . . . . . . . . . . . . . . . . 19  |-  F/ r [ z  /  r ] ph
167165, 166nfan 1575 . . . . . . . . . . . . . . . . . 18  |-  F/ r ( th  /\  [
z  /  r ]
ph )
168 nfcv 2329 . . . . . . . . . . . . . . . . . . 19  |-  F/_ r NN0
169 nfre1 2530 . . . . . . . . . . . . . . . . . . . 20  |-  F/ r E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
17057, 169nfim 1582 . . . . . . . . . . . . . . . . . . 19  |-  F/ r ( [ y  / 
r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
)
171168, 170nfralxy 2525 . . . . . . . . . . . . . . . . . 18  |-  F/ r A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\ 
ph ) )
172167, 171nfim 1582 . . . . . . . . . . . . . . . . 17  |-  F/ r ( ( th  /\  [ z  /  r ]
ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ z  /  x ] ps  /\  ph )
) )
173164, 172nfralxy 2525 . . . . . . . . . . . . . . . 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 1575 . . . . . . . . . . . . . . 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 1949 . . . . . . . . . . . . . . . 16  |-  F/ r [ w  /  r ] ph
176165, 175nfan 1575 . . . . . . . . . . . . . . 15  |-  F/ r ( th  /\  [
w  /  r ]
ph )
177174, 176nfan 1575 . . . . . . . . . . . . . 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 1538 . . . . . . . . . . . . . 14  |-  F/ r 0  <  w
179177, 178nfan 1575 . . . . . . . . . . . . 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 1538 . . . . . . . . . . . . 13  |-  F/ r  y  e.  NN0
181179, 180nfan 1575 . . . . . . . . . . . 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 1575 . . . . . . . . . . 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 12011 . . . . . . . . . 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 364 . . . . . . . . 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 2558 . . . . . . . 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 2978 . . . . . . . . . . . 12  |-  ( [ w  /  x ] ps 
<-> 
[. w  /  x ]. ps )
187186anbi1i 458 . . . . . . . . . . 11  |-  ( ( [ w  /  x ] ps  /\  ph )  <->  (
[. w  /  x ]. ps  /\  ph )
)
188187rexbii 2494 . . . . . . . . . 10  |-  ( E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph )  <->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
)
189188imbi2i 226 . . . . . . . . 9  |-  ( ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( [ w  /  x ] ps  /\  ph ) )  <->  ( [
y  /  r ]
ph  ->  E. r  e.  NN0  ( [. w  /  x ]. ps  /\  ph )
) )
190189ralbii 2493 . . . . . . . 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 134 . . . . . . 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 9215 . . . . . . . . 9  |-  ( w  e.  NN0  ->  -.  w  <  0 )
193 nn0z 9286 . . . . . . . . . . . 12  |-  ( w  e.  NN0  ->  w  e.  ZZ )
194 ztri3or0 9308 . . . . . . . . . . . 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 982 . . . . . . . . . . 11  |-  ( ( w  <  0  \/  w  =  0  \/  0  <  w )  <-> 
( w  <  0  \/  ( w  =  0  \/  0  <  w
) ) )
197195, 196sylib 122 . . . . . . . . . 10  |-  ( w  e.  NN0  ->  ( w  <  0  \/  (
w  =  0  \/  0  <  w ) ) )
198197orcomd 730 . . . . . . . . 9  |-  ( w  e.  NN0  ->  ( ( w  =  0  \/  0  <  w )  \/  w  <  0
) )
199192, 198ecased 1359 . . . . . . . 8  |-  ( w  e.  NN0  ->  ( w  =  0  \/  0  <  w ) )
200199ad2antrr 488 . . . . . . 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 799 . . . . . 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 364 . . . . 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 10457 . . . 4  |-  ( x  e.  NN0  ->  ( ( th  /\  [ x  /  r ] ph )  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) )
204203expd 258 . . 3  |-  ( x  e.  NN0  ->  ( th 
->  ( [ x  / 
r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph ) ) ) ) )
205204impcom 125 . 2  |-  ( ( th  /\  x  e. 
NN0 )  ->  ( [ x  /  r ] ph  ->  A. y  e.  NN0  ( [ y  /  r ] ph  ->  E. r  e.  NN0  ( ps  /\  ph )
) ) )
206205ralrimiva 2560 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 104    <-> wb 105    \/ wo 709    \/ w3o 978    = wceq 1363   [wsb 1772    e. wcel 2158   A.wral 2465   E.wrex 2466   [.wsbc 2974   class class class wbr 4015  (class class class)co 5888   0cc0 7824   1c1 7825    + caddc 7827    x. cmul 7829    < clt 8005    - cmin 8141   NNcn 8932   NN0cn0 9189   ZZcz 9266   ...cfz 10021    mod cmo 10335    || cdvds 11807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-frec 6405  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-fz 10022  df-fl 10283  df-mod 10336  df-seqfrec 10459  df-exp 10533  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-dvds 11808
This theorem is referenced by:  bezoutlemex  12015
  Copyright terms: Public domain W3C validator