Step |
Hyp |
Ref |
Expression |
1 |
|
bezout.1 |
|- M = { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) } |
2 |
|
bezout.3 |
|- ( ph -> A e. ZZ ) |
3 |
|
bezout.4 |
|- ( ph -> B e. ZZ ) |
4 |
|
bezout.2 |
|- G = inf ( M , RR , < ) |
5 |
|
bezout.5 |
|- ( ph -> -. ( A = 0 /\ B = 0 ) ) |
6 |
1
|
ssrab3 |
|- M C_ NN |
7 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
8 |
6 7
|
sseqtri |
|- M C_ ( ZZ>= ` 1 ) |
9 |
1 2 3
|
bezoutlem1 |
|- ( ph -> ( A =/= 0 -> ( abs ` A ) e. M ) ) |
10 |
|
ne0i |
|- ( ( abs ` A ) e. M -> M =/= (/) ) |
11 |
9 10
|
syl6 |
|- ( ph -> ( A =/= 0 -> M =/= (/) ) ) |
12 |
|
eqid |
|- { z e. NN | E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) } = { z e. NN | E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) } |
13 |
12 3 2
|
bezoutlem1 |
|- ( ph -> ( B =/= 0 -> ( abs ` B ) e. { z e. NN | E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) } ) ) |
14 |
|
rexcom |
|- ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. y e. ZZ E. x e. ZZ z = ( ( A x. x ) + ( B x. y ) ) ) |
15 |
2
|
zcnd |
|- ( ph -> A e. CC ) |
16 |
15
|
adantr |
|- ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> A e. CC ) |
17 |
|
zcn |
|- ( x e. ZZ -> x e. CC ) |
18 |
17
|
ad2antll |
|- ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> x e. CC ) |
19 |
16 18
|
mulcld |
|- ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> ( A x. x ) e. CC ) |
20 |
3
|
zcnd |
|- ( ph -> B e. CC ) |
21 |
20
|
adantr |
|- ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> B e. CC ) |
22 |
|
zcn |
|- ( y e. ZZ -> y e. CC ) |
23 |
22
|
ad2antrl |
|- ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> y e. CC ) |
24 |
21 23
|
mulcld |
|- ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> ( B x. y ) e. CC ) |
25 |
19 24
|
addcomd |
|- ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> ( ( A x. x ) + ( B x. y ) ) = ( ( B x. y ) + ( A x. x ) ) ) |
26 |
25
|
eqeq2d |
|- ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> z = ( ( B x. y ) + ( A x. x ) ) ) ) |
27 |
26
|
2rexbidva |
|- ( ph -> ( E. y e. ZZ E. x e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) ) ) |
28 |
14 27
|
syl5bb |
|- ( ph -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) ) ) |
29 |
28
|
rabbidv |
|- ( ph -> { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) } = { z e. NN | E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) } ) |
30 |
1 29
|
eqtrid |
|- ( ph -> M = { z e. NN | E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) } ) |
31 |
30
|
eleq2d |
|- ( ph -> ( ( abs ` B ) e. M <-> ( abs ` B ) e. { z e. NN | E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) } ) ) |
32 |
13 31
|
sylibrd |
|- ( ph -> ( B =/= 0 -> ( abs ` B ) e. M ) ) |
33 |
|
ne0i |
|- ( ( abs ` B ) e. M -> M =/= (/) ) |
34 |
32 33
|
syl6 |
|- ( ph -> ( B =/= 0 -> M =/= (/) ) ) |
35 |
|
neorian |
|- ( ( A =/= 0 \/ B =/= 0 ) <-> -. ( A = 0 /\ B = 0 ) ) |
36 |
5 35
|
sylibr |
|- ( ph -> ( A =/= 0 \/ B =/= 0 ) ) |
37 |
11 34 36
|
mpjaod |
|- ( ph -> M =/= (/) ) |
38 |
|
infssuzcl |
|- ( ( M C_ ( ZZ>= ` 1 ) /\ M =/= (/) ) -> inf ( M , RR , < ) e. M ) |
39 |
8 37 38
|
sylancr |
|- ( ph -> inf ( M , RR , < ) e. M ) |
40 |
4 39
|
eqeltrid |
|- ( ph -> G e. M ) |