Theorem bezout

Description: Bézout's identity: For any integers A and B , there are integers x , y such that ( A gcd B ) = A x. x + B x. y . This is Metamath 100 proof #60. (Contributed by Mario Carneiro, 22-Feb-2014)

	Ref	Expression
Assertion	bezout	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑧 = 𝑡 → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑡 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
2	1	2rexbidv	⊢ ( 𝑧 = 𝑡 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑡 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
3		oveq2	⊢ ( 𝑥 = 𝑢 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑢 ) )
4	3	oveq1d	⊢ ( 𝑥 = 𝑢 → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) )
5	4	eqeq2d	⊢ ( 𝑥 = 𝑢 → ( 𝑡 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑡 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) ) )
6		oveq2	⊢ ( 𝑦 = 𝑣 → ( 𝐵 · 𝑦 ) = ( 𝐵 · 𝑣 ) )
7	6	oveq2d	⊢ ( 𝑦 = 𝑣 → ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
8	7	eqeq2d	⊢ ( 𝑦 = 𝑣 → ( 𝑡 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑡 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
9	5 8	cbvrex2vw	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑡 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑡 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
10	2 9	bitrdi	⊢ ( 𝑧 = 𝑡 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑡 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
11	10	cbvrabv	⊢ { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } = { 𝑡 ∈ ℕ ∣ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑡 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) }
12		simpll	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → 𝐴 ∈ ℤ )
13		simplr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → 𝐵 ∈ ℤ )
14		eqid	⊢ inf ( { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } , ℝ , < ) = inf ( { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } , ℝ , < )
15		simpr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
16	11 12 13 14 15	bezoutlem4	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } )
17		eqeq1	⊢ ( 𝑧 = ( 𝐴 gcd 𝐵 ) → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
18	17	2rexbidv	⊢ ( 𝑧 = ( 𝐴 gcd 𝐵 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
19	18	elrab	⊢ ( ( 𝐴 gcd 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } ↔ ( ( 𝐴 gcd 𝐵 ) ∈ ℕ ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
20	19	simprbi	⊢ ( ( 𝐴 gcd 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
21	16 20	syl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
22	21	ex	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
23		0z	⊢ 0 ∈ ℤ
24		00id	⊢ ( 0 + 0 ) = 0
25		0cn	⊢ 0 ∈ ℂ
26	25	mul01i	⊢ ( 0 · 0 ) = 0
27	26 26	oveq12i	⊢ ( ( 0 · 0 ) + ( 0 · 0 ) ) = ( 0 + 0 )
28		gcd0val	⊢ ( 0 gcd 0 ) = 0
29	24 27 28	3eqtr4ri	⊢ ( 0 gcd 0 ) = ( ( 0 · 0 ) + ( 0 · 0 ) )
30		oveq2	⊢ ( 𝑥 = 0 → ( 0 · 𝑥 ) = ( 0 · 0 ) )
31	30	oveq1d	⊢ ( 𝑥 = 0 → ( ( 0 · 𝑥 ) + ( 0 · 𝑦 ) ) = ( ( 0 · 0 ) + ( 0 · 𝑦 ) ) )
32	31	eqeq2d	⊢ ( 𝑥 = 0 → ( ( 0 gcd 0 ) = ( ( 0 · 𝑥 ) + ( 0 · 𝑦 ) ) ↔ ( 0 gcd 0 ) = ( ( 0 · 0 ) + ( 0 · 𝑦 ) ) ) )
33		oveq2	⊢ ( 𝑦 = 0 → ( 0 · 𝑦 ) = ( 0 · 0 ) )
34	33	oveq2d	⊢ ( 𝑦 = 0 → ( ( 0 · 0 ) + ( 0 · 𝑦 ) ) = ( ( 0 · 0 ) + ( 0 · 0 ) ) )
35	34	eqeq2d	⊢ ( 𝑦 = 0 → ( ( 0 gcd 0 ) = ( ( 0 · 0 ) + ( 0 · 𝑦 ) ) ↔ ( 0 gcd 0 ) = ( ( 0 · 0 ) + ( 0 · 0 ) ) ) )
36	32 35	rspc2ev	⊢ ( ( 0 ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 0 gcd 0 ) = ( ( 0 · 0 ) + ( 0 · 0 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 0 gcd 0 ) = ( ( 0 · 𝑥 ) + ( 0 · 𝑦 ) ) )
37	23 23 29 36	mp3an	⊢ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 0 gcd 0 ) = ( ( 0 · 𝑥 ) + ( 0 · 𝑦 ) )
38		oveq12	⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 0 ) )
39		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 · 𝑥 ) = ( 0 · 𝑥 ) )
40		oveq1	⊢ ( 𝐵 = 0 → ( 𝐵 · 𝑦 ) = ( 0 · 𝑦 ) )
41	39 40	oveqan12d	⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 0 · 𝑥 ) + ( 0 · 𝑦 ) ) )
42	38 41	eqeq12d	⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( 0 gcd 0 ) = ( ( 0 · 𝑥 ) + ( 0 · 𝑦 ) ) ) )
43	42	2rexbidv	⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 0 gcd 0 ) = ( ( 0 · 𝑥 ) + ( 0 · 𝑦 ) ) ) )
44	37 43	mpbiri	⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
45	22 44	pm2.61d2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )