This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bezoutlem4

Description: Lemma for bezout . (Contributed by Mario Carneiro, 22-Feb-2014)

Ref Expression
Hypotheses bezout.1 ⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
bezout.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
bezout.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
bezout.2 ⊢ 𝐺 = inf ( 𝑀 , ℝ , < )
bezout.5 ⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
Assertion bezoutlem4 ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ 𝑀 )

Proof

Step Hyp Ref Expression
1 bezout.1 ⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
2 bezout.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3 bezout.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4 bezout.2 ⊢ 𝐺 = inf ( 𝑀 , ℝ , < )
5 bezout.5 ⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
6 gcddvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
7 2 3 6 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
8 7 simpld ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
9 2 3 gcdcld ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℕ0 )
10 9 nn0zd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
11 divides ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ∃ 𝑠 ∈ ℤ ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ) )
12 10 2 11 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ∃ 𝑠 ∈ ℤ ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ) )
13 8 12 mpbid ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℤ ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 )
14 7 simprd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
15 divides ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ∃ 𝑡 ∈ ℤ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) )
16 10 3 15 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ∃ 𝑡 ∈ ℤ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) )
17 14 16 mpbid ⊢ ( 𝜑 → ∃ 𝑡 ∈ ℤ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 )
18 reeanv ⊢ ( ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) ↔ ( ∃ 𝑠 ∈ ℤ ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ∃ 𝑡 ∈ ℤ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) )
19 1 2 3 4 5 bezoutlem2 ⊢ ( 𝜑 → 𝐺 ∈ 𝑀 )
20 oveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑢 ) )
21 20 oveq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) )
22 21 eqeq2d ⊢ ( 𝑥 = 𝑢 → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) ) )
23 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐵 · 𝑦 ) = ( 𝐵 · 𝑣 ) )
24 23 oveq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
25 24 eqeq2d ⊢ ( 𝑦 = 𝑣 → ( 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
26 22 25 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
27 eqeq1 ⊢ ( 𝑧 = 𝐺 → ( 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ↔ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
28 27 2rexbidv ⊢ ( 𝑧 = 𝐺 → ( ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
29 26 28 bitrid ⊢ ( 𝑧 = 𝐺 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
30 29 1 elrab2 ⊢ ( 𝐺 ∈ 𝑀 ↔ ( 𝐺 ∈ ℕ ∧ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
31 19 30 sylib ⊢ ( 𝜑 → ( 𝐺 ∈ ℕ ∧ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
32 31 simprd ⊢ ( 𝜑 → ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
33 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → 𝑠 ∈ ℤ )
34 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → 𝑢 ∈ ℤ )
35 33 34 zmulcld ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝑠 · 𝑢 ) ∈ ℤ )
36 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → 𝑡 ∈ ℤ )
37 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → 𝑣 ∈ ℤ )
38 36 37 zmulcld ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝑡 · 𝑣 ) ∈ ℤ )
39 35 38 zaddcld ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( ( 𝑠 · 𝑢 ) + ( 𝑡 · 𝑣 ) ) ∈ ℤ )
40 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
41 dvdsmul2 ⊢ ( ( ( ( 𝑠 · 𝑢 ) + ( 𝑡 · 𝑣 ) ) ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( ( 𝑠 · 𝑢 ) + ( 𝑡 · 𝑣 ) ) · ( 𝐴 gcd 𝐵 ) ) )
42 39 40 41 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( ( 𝑠 · 𝑢 ) + ( 𝑡 · 𝑣 ) ) · ( 𝐴 gcd 𝐵 ) ) )
43 35 zcnd ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝑠 · 𝑢 ) ∈ ℂ )
44 40 zcnd ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℂ )
45 38 zcnd ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝑡 · 𝑣 ) ∈ ℂ )
46 33 zcnd ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → 𝑠 ∈ ℂ )
47 34 zcnd ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → 𝑢 ∈ ℂ )
48 46 47 44 mul32d ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( ( 𝑠 · 𝑢 ) · ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) · 𝑢 ) )
49 36 zcnd ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → 𝑡 ∈ ℂ )
50 37 zcnd ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → 𝑣 ∈ ℂ )
51 49 50 44 mul32d ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( ( 𝑡 · 𝑣 ) · ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) · 𝑣 ) )
52 48 51 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( ( ( 𝑠 · 𝑢 ) · ( 𝐴 gcd 𝐵 ) ) + ( ( 𝑡 · 𝑣 ) · ( 𝐴 gcd 𝐵 ) ) ) = ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) · 𝑢 ) + ( ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) · 𝑣 ) ) )
53 43 44 45 52 joinlmuladdmuld ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( ( ( 𝑠 · 𝑢 ) + ( 𝑡 · 𝑣 ) ) · ( 𝐴 gcd 𝐵 ) ) = ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) · 𝑢 ) + ( ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) · 𝑣 ) ) )
54 42 53 breqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) · 𝑢 ) + ( ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) · 𝑣 ) ) )
55 oveq1 ⊢ ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 → ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) · 𝑢 ) = ( 𝐴 · 𝑢 ) )
56 oveq1 ⊢ ( ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 → ( ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) · 𝑣 ) = ( 𝐵 · 𝑣 ) )
57 55 56 oveqan12d ⊢ ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) · 𝑢 ) + ( ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) · 𝑣 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
58 57 breq2d ⊢ ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( ( 𝐴 gcd 𝐵 ) ∥ ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) · 𝑢 ) + ( ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) · 𝑣 ) ) ↔ ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
59 54 58 syl5ibcom ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
60 breq2 ⊢ ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ↔ ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
61 60 imbi2d ⊢ ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ) ↔ ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) ) )
62 59 61 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) ) → ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ) ) )
63 62 expr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) → ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ) ) ) )
64 63 com23 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) → ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ) ) ) )
65 64 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ) ) ) )
66 32 65 mpd ⊢ ( 𝜑 → ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ) ) )
67 66 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ ( ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ) )
68 18 67 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑠 ∈ ℤ ( 𝑠 · ( 𝐴 gcd 𝐵 ) ) = 𝐴 ∧ ∃ 𝑡 ∈ ℤ ( 𝑡 · ( 𝐴 gcd 𝐵 ) ) = 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 ) )
69 13 17 68 mp2and ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∥ 𝐺 )
70 31 simpld ⊢ ( 𝜑 → 𝐺 ∈ ℕ )
71 dvdsle ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐺 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐺 → ( 𝐴 gcd 𝐵 ) ≤ 𝐺 ) )
72 10 70 71 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐺 → ( 𝐴 gcd 𝐵 ) ≤ 𝐺 ) )
73 69 72 mpd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ≤ 𝐺 )
74 breq2 ⊢ ( 𝐴 = 0 → ( 𝐺 ∥ 𝐴 ↔ 𝐺 ∥ 0 ) )
75 1 2 3 bezoutlem1 ⊢ ( 𝜑 → ( 𝐴 ≠ 0 → ( abs ‘ 𝐴 ) ∈ 𝑀 ) )
76 1 2 3 4 5 bezoutlem3 ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ∈ 𝑀 → 𝐺 ∥ ( abs ‘ 𝐴 ) ) )
77 75 76 syld ⊢ ( 𝜑 → ( 𝐴 ≠ 0 → 𝐺 ∥ ( abs ‘ 𝐴 ) ) )
78 70 nnzd ⊢ ( 𝜑 → 𝐺 ∈ ℤ )
79 dvdsabsb ⊢ ( ( 𝐺 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐺 ∥ 𝐴 ↔ 𝐺 ∥ ( abs ‘ 𝐴 ) ) )
80 78 2 79 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∥ 𝐴 ↔ 𝐺 ∥ ( abs ‘ 𝐴 ) ) )
81 77 80 sylibrd ⊢ ( 𝜑 → ( 𝐴 ≠ 0 → 𝐺 ∥ 𝐴 ) )
82 81 imp ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐺 ∥ 𝐴 )
83 dvds0 ⊢ ( 𝐺 ∈ ℤ → 𝐺 ∥ 0 )
84 78 83 syl ⊢ ( 𝜑 → 𝐺 ∥ 0 )
85 74 82 84 pm2.61ne ⊢ ( 𝜑 → 𝐺 ∥ 𝐴 )
86 breq2 ⊢ ( 𝐵 = 0 → ( 𝐺 ∥ 𝐵 ↔ 𝐺 ∥ 0 ) )
87 eqid ⊢ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) }
88 87 3 2 bezoutlem1 ⊢ ( 𝜑 → ( 𝐵 ≠ 0 → ( abs ‘ 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } ) )
89 rexcom ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
90 2 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
92 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
93 92 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝑥 ∈ ℂ )
94 91 93 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
95 3 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
96 95 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
97 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
98 97 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝑦 ∈ ℂ )
99 96 98 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝐵 · 𝑦 ) ∈ ℂ )
100 94 99 addcomd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) )
101 100 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
102 101 2rexbidva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
103 89 102 bitrid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
104 103 rabbidv ⊢ ( 𝜑 → { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } )
105 1 104 eqtrid ⊢ ( 𝜑 → 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } )
106 105 eleq2d ⊢ ( 𝜑 → ( ( abs ‘ 𝐵 ) ∈ 𝑀 ↔ ( abs ‘ 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } ) )
107 88 106 sylibrd ⊢ ( 𝜑 → ( 𝐵 ≠ 0 → ( abs ‘ 𝐵 ) ∈ 𝑀 ) )
108 1 2 3 4 5 bezoutlem3 ⊢ ( 𝜑 → ( ( abs ‘ 𝐵 ) ∈ 𝑀 → 𝐺 ∥ ( abs ‘ 𝐵 ) ) )
109 107 108 syld ⊢ ( 𝜑 → ( 𝐵 ≠ 0 → 𝐺 ∥ ( abs ‘ 𝐵 ) ) )
110 dvdsabsb ⊢ ( ( 𝐺 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐺 ∥ 𝐵 ↔ 𝐺 ∥ ( abs ‘ 𝐵 ) ) )
111 78 3 110 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∥ 𝐵 ↔ 𝐺 ∥ ( abs ‘ 𝐵 ) ) )
112 109 111 sylibrd ⊢ ( 𝜑 → ( 𝐵 ≠ 0 → 𝐺 ∥ 𝐵 ) )
113 112 imp ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → 𝐺 ∥ 𝐵 )
114 86 113 84 pm2.61ne ⊢ ( 𝜑 → 𝐺 ∥ 𝐵 )
115 dvdslegcd ⊢ ( ( ( 𝐺 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐺 ∥ 𝐴 ∧ 𝐺 ∥ 𝐵 ) → 𝐺 ≤ ( 𝐴 gcd 𝐵 ) ) )
116 78 2 3 5 115 syl31anc ⊢ ( 𝜑 → ( ( 𝐺 ∥ 𝐴 ∧ 𝐺 ∥ 𝐵 ) → 𝐺 ≤ ( 𝐴 gcd 𝐵 ) ) )
117 85 114 116 mp2and ⊢ ( 𝜑 → 𝐺 ≤ ( 𝐴 gcd 𝐵 ) )
118 9 nn0red ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℝ )
119 70 nnred ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
120 118 119 letri3d ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) = 𝐺 ↔ ( ( 𝐴 gcd 𝐵 ) ≤ 𝐺 ∧ 𝐺 ≤ ( 𝐴 gcd 𝐵 ) ) ) )
121 73 117 120 mpbir2and ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 𝐺 )
122 121 19 eqeltrd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ 𝑀 )