bezoutlem1

	Ref	Expression
Hypotheses	bezout.1	\|- M = { z e. NN \| E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) }
	bezout.3	\|- ( ph -> A e. ZZ )
	bezout.4	\|- ( ph -> B e. ZZ )
Assertion	bezoutlem1	\|- ( ph -> ( A =/= 0 -> ( abs ` A ) e. M ) )

Proof

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		fveq2	\|- ( z = A -> ( abs ` z ) = ( abs ` A ) )
5		oveq1	\|- ( z = A -> ( z x. x ) = ( A x. x ) )
6	4 5	eqeq12d	\|- ( z = A -> ( ( abs ` z ) = ( z x. x ) <-> ( abs ` A ) = ( A x. x ) ) )
7	6	rexbidv	\|- ( z = A -> ( E. x e. ZZ ( abs ` z ) = ( z x. x ) <-> E. x e. ZZ ( abs ` A ) = ( A x. x ) ) )
8		zre	\|- ( z e. ZZ -> z e. RR )
9		1z	\|- 1 e. ZZ
10		ax-1rid	\|- ( z e. RR -> ( z x. 1 ) = z )
11	10	eqcomd	\|- ( z e. RR -> z = ( z x. 1 ) )
12		oveq2	\|- ( x = 1 -> ( z x. x ) = ( z x. 1 ) )
13	12	rspceeqv	\|- ( ( 1 e. ZZ /\ z = ( z x. 1 ) ) -> E. x e. ZZ z = ( z x. x ) )
14	9 11 13	sylancr	\|- ( z e. RR -> E. x e. ZZ z = ( z x. x ) )
15		eqeq1	\|- ( ( abs ` z ) = z -> ( ( abs ` z ) = ( z x. x ) <-> z = ( z x. x ) ) )
16	15	rexbidv	\|- ( ( abs ` z ) = z -> ( E. x e. ZZ ( abs ` z ) = ( z x. x ) <-> E. x e. ZZ z = ( z x. x ) ) )
17	14 16	syl5ibrcom	\|- ( z e. RR -> ( ( abs ` z ) = z -> E. x e. ZZ ( abs ` z ) = ( z x. x ) ) )
18		neg1z	\|- -u 1 e. ZZ
19		recn	\|- ( z e. RR -> z e. CC )
20	19	mulm1d	\|- ( z e. RR -> ( -u 1 x. z ) = -u z )
21		neg1cn	\|- -u 1 e. CC
22		mulcom	\|- ( ( -u 1 e. CC /\ z e. CC ) -> ( -u 1 x. z ) = ( z x. -u 1 ) )
23	21 19 22	sylancr	\|- ( z e. RR -> ( -u 1 x. z ) = ( z x. -u 1 ) )
24	20 23	eqtr3d	\|- ( z e. RR -> -u z = ( z x. -u 1 ) )
25		oveq2	\|- ( x = -u 1 -> ( z x. x ) = ( z x. -u 1 ) )
26	25	rspceeqv	\|- ( ( -u 1 e. ZZ /\ -u z = ( z x. -u 1 ) ) -> E. x e. ZZ -u z = ( z x. x ) )
27	18 24 26	sylancr	\|- ( z e. RR -> E. x e. ZZ -u z = ( z x. x ) )
28		eqeq1	\|- ( ( abs ` z ) = -u z -> ( ( abs ` z ) = ( z x. x ) <-> -u z = ( z x. x ) ) )
29	28	rexbidv	\|- ( ( abs ` z ) = -u z -> ( E. x e. ZZ ( abs ` z ) = ( z x. x ) <-> E. x e. ZZ -u z = ( z x. x ) ) )
30	27 29	syl5ibrcom	\|- ( z e. RR -> ( ( abs ` z ) = -u z -> E. x e. ZZ ( abs ` z ) = ( z x. x ) ) )
31		absor	\|- ( z e. RR -> ( ( abs ` z ) = z \/ ( abs ` z ) = -u z ) )
32	17 30 31	mpjaod	\|- ( z e. RR -> E. x e. ZZ ( abs ` z ) = ( z x. x ) )
33	8 32	syl	\|- ( z e. ZZ -> E. x e. ZZ ( abs ` z ) = ( z x. x ) )
34	7 33	vtoclga	\|- ( A e. ZZ -> E. x e. ZZ ( abs ` A ) = ( A x. x ) )
35	2 34	syl	\|- ( ph -> E. x e. ZZ ( abs ` A ) = ( A x. x ) )
36	3	zcnd	\|- ( ph -> B e. CC )
37	36	adantr	\|- ( ( ph /\ x e. ZZ ) -> B e. CC )
38	37	mul01d	\|- ( ( ph /\ x e. ZZ ) -> ( B x. 0 ) = 0 )
39	38	oveq2d	\|- ( ( ph /\ x e. ZZ ) -> ( ( A x. x ) + ( B x. 0 ) ) = ( ( A x. x ) + 0 ) )
40	2	zcnd	\|- ( ph -> A e. CC )
41		zcn	\|- ( x e. ZZ -> x e. CC )
42		mulcl	\|- ( ( A e. CC /\ x e. CC ) -> ( A x. x ) e. CC )
43	40 41 42	syl2an	\|- ( ( ph /\ x e. ZZ ) -> ( A x. x ) e. CC )
44	43	addridd	\|- ( ( ph /\ x e. ZZ ) -> ( ( A x. x ) + 0 ) = ( A x. x ) )
45	39 44	eqtrd	\|- ( ( ph /\ x e. ZZ ) -> ( ( A x. x ) + ( B x. 0 ) ) = ( A x. x ) )
46	45	eqeq2d	\|- ( ( ph /\ x e. ZZ ) -> ( ( abs ` A ) = ( ( A x. x ) + ( B x. 0 ) ) <-> ( abs ` A ) = ( A x. x ) ) )
47		0z	\|- 0 e. ZZ
48		oveq2	\|- ( y = 0 -> ( B x. y ) = ( B x. 0 ) )
49	48	oveq2d	\|- ( y = 0 -> ( ( A x. x ) + ( B x. y ) ) = ( ( A x. x ) + ( B x. 0 ) ) )
50	49	rspceeqv	\|- ( ( 0 e. ZZ /\ ( abs ` A ) = ( ( A x. x ) + ( B x. 0 ) ) ) -> E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) )
51	47 50	mpan	\|- ( ( abs ` A ) = ( ( A x. x ) + ( B x. 0 ) ) -> E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) )
52	46 51	biimtrrdi	\|- ( ( ph /\ x e. ZZ ) -> ( ( abs ` A ) = ( A x. x ) -> E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )
53	52	reximdva	\|- ( ph -> ( E. x e. ZZ ( abs ` A ) = ( A x. x ) -> E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )
54	35 53	mpd	\|- ( ph -> E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) )
55		nnabscl	\|- ( ( A e. ZZ /\ A =/= 0 ) -> ( abs ` A ) e. NN )
56	55	ex	\|- ( A e. ZZ -> ( A =/= 0 -> ( abs ` A ) e. NN ) )
57	2 56	syl	\|- ( ph -> ( A =/= 0 -> ( abs ` A ) e. NN ) )
58		eqeq1	\|- ( z = ( abs ` A ) -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )
59	58	2rexbidv	\|- ( z = ( abs ` A ) -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )
60	59 1	elrab2	\|- ( ( abs ` A ) e. M <-> ( ( abs ` A ) e. NN /\ E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )
61	60	simplbi2com	\|- ( E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) -> ( ( abs ` A ) e. NN -> ( abs ` A ) e. M ) )
62	54 57 61	sylsyld	\|- ( ph -> ( A =/= 0 -> ( abs ` A ) e. M ) )

Metamath Proof Explorer

Theorem bezoutlem1

Proof