Metamath Proof Explorer

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 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )