Metamath Proof Explorer

Theorem bezoutlem1

Description: Lemma for bezout . (Contributed by Mario Carneiro, 15-Mar-2014)

Ref Expression
Hypotheses bezout.1 ⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
bezout.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
bezout.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
Assertion bezoutlem1 ( 𝜑 → ( 𝐴 ≠ 0 → ( abs ‘ 𝐴 ) ∈ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 bezout.1 ⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
2 bezout.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3 bezout.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4 fveq2 ⊢ ( 𝑧 = 𝐴 → ( abs ‘ 𝑧 ) = ( abs ‘ 𝐴 ) )
5 oveq1 ⊢ ( 𝑧 = 𝐴 → ( 𝑧 · 𝑥 ) = ( 𝐴 · 𝑥 ) )
6 4 5 eqeq12d ⊢ ( 𝑧 = 𝐴 → ( ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) ↔ ( abs ‘ 𝐴 ) = ( 𝐴 · 𝑥 ) ) )
7 6 rexbidv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ ( abs ‘ 𝐴 ) = ( 𝐴 · 𝑥 ) ) )
8 zre ⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
9 1z ⊢ 1 ∈ ℤ
10 ax-1rid ⊢ ( 𝑧 ∈ ℝ → ( 𝑧 · 1 ) = 𝑧 )
11 10 eqcomd ⊢ ( 𝑧 ∈ ℝ → 𝑧 = ( 𝑧 · 1 ) )
12 oveq2 ⊢ ( 𝑥 = 1 → ( 𝑧 · 𝑥 ) = ( 𝑧 · 1 ) )
13 12 rspceeqv ⊢ ( ( 1 ∈ ℤ ∧ 𝑧 = ( 𝑧 · 1 ) ) → ∃ 𝑥 ∈ ℤ 𝑧 = ( 𝑧 · 𝑥 ) )
14 9 11 13 sylancr ⊢ ( 𝑧 ∈ ℝ → ∃ 𝑥 ∈ ℤ 𝑧 = ( 𝑧 · 𝑥 ) )
15 eqeq1 ⊢ ( ( abs ‘ 𝑧 ) = 𝑧 → ( ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) ↔ 𝑧 = ( 𝑧 · 𝑥 ) ) )
16 15 rexbidv ⊢ ( ( abs ‘ 𝑧 ) = 𝑧 → ( ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑧 = ( 𝑧 · 𝑥 ) ) )
17 14 16 syl5ibrcom ⊢ ( 𝑧 ∈ ℝ → ( ( abs ‘ 𝑧 ) = 𝑧 → ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) ) )
18 neg1z ⊢ - 1 ∈ ℤ
19 recn ⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℂ )
20 19 mulm1d ⊢ ( 𝑧 ∈ ℝ → ( - 1 · 𝑧 ) = - 𝑧 )
21 neg1cn ⊢ - 1 ∈ ℂ
22 mulcom ⊢ ( ( - 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( - 1 · 𝑧 ) = ( 𝑧 · - 1 ) )
23 21 19 22 sylancr ⊢ ( 𝑧 ∈ ℝ → ( - 1 · 𝑧 ) = ( 𝑧 · - 1 ) )
24 20 23 eqtr3d ⊢ ( 𝑧 ∈ ℝ → - 𝑧 = ( 𝑧 · - 1 ) )
25 oveq2 ⊢ ( 𝑥 = - 1 → ( 𝑧 · 𝑥 ) = ( 𝑧 · - 1 ) )
26 25 rspceeqv ⊢ ( ( - 1 ∈ ℤ ∧ - 𝑧 = ( 𝑧 · - 1 ) ) → ∃ 𝑥 ∈ ℤ - 𝑧 = ( 𝑧 · 𝑥 ) )
27 18 24 26 sylancr ⊢ ( 𝑧 ∈ ℝ → ∃ 𝑥 ∈ ℤ - 𝑧 = ( 𝑧 · 𝑥 ) )
28 eqeq1 ⊢ ( ( abs ‘ 𝑧 ) = - 𝑧 → ( ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) ↔ - 𝑧 = ( 𝑧 · 𝑥 ) ) )
29 28 rexbidv ⊢ ( ( abs ‘ 𝑧 ) = - 𝑧 → ( ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ - 𝑧 = ( 𝑧 · 𝑥 ) ) )
30 27 29 syl5ibrcom ⊢ ( 𝑧 ∈ ℝ → ( ( abs ‘ 𝑧 ) = - 𝑧 → ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) ) )
31 absor ⊢ ( 𝑧 ∈ ℝ → ( ( abs ‘ 𝑧 ) = 𝑧 ∨ ( abs ‘ 𝑧 ) = - 𝑧 ) )
32 17 30 31 mpjaod ⊢ ( 𝑧 ∈ ℝ → ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) )
33 8 32 syl ⊢ ( 𝑧 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑧 ) = ( 𝑧 · 𝑥 ) )
34 7 33 vtoclga ⊢ ( 𝐴 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( abs ‘ 𝐴 ) = ( 𝐴 · 𝑥 ) )
35 2 34 syl ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ( abs ‘ 𝐴 ) = ( 𝐴 · 𝑥 ) )
36 3 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝐵 ∈ ℂ )
38 37 mul01d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝐵 · 0 ) = 0 )
39 38 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 0 ) ) = ( ( 𝐴 · 𝑥 ) + 0 ) )
40 2 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
41 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
42 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
43 40 41 42 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
44 43 addid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝐴 · 𝑥 ) + 0 ) = ( 𝐴 · 𝑥 ) )
45 39 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 0 ) ) = ( 𝐴 · 𝑥 ) )
46 45 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 0 ) ) ↔ ( abs ‘ 𝐴 ) = ( 𝐴 · 𝑥 ) ) )
47 0z ⊢ 0 ∈ ℤ
48 oveq2 ⊢ ( 𝑦 = 0 → ( 𝐵 · 𝑦 ) = ( 𝐵 · 0 ) )
49 48 oveq2d ⊢ ( 𝑦 = 0 → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 0 ) ) )
50 49 rspceeqv ⊢ ( ( 0 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 0 ) ) ) → ∃ 𝑦 ∈ ℤ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
51 47 50 mpan ⊢ ( ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 0 ) ) → ∃ 𝑦 ∈ ℤ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
52 46 51 syl6bir ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( abs ‘ 𝐴 ) = ( 𝐴 · 𝑥 ) → ∃ 𝑦 ∈ ℤ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
53 52 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℤ ( abs ‘ 𝐴 ) = ( 𝐴 · 𝑥 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
54 35 53 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
55 nnabscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℕ )
56 55 ex ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ≠ 0 → ( abs ‘ 𝐴 ) ∈ ℕ ) )
57 2 56 syl ⊢ ( 𝜑 → ( 𝐴 ≠ 0 → ( abs ‘ 𝐴 ) ∈ ℕ ) )
58 eqeq1 ⊢ ( 𝑧 = ( abs ‘ 𝐴 ) → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
59 58 2rexbidv ⊢ ( 𝑧 = ( abs ‘ 𝐴 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
60 59 1 elrab2 ⊢ ( ( abs ‘ 𝐴 ) ∈ 𝑀 ↔ ( ( abs ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
61 60 simplbi2com ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( abs ‘ 𝐴 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) → ( ( abs ‘ 𝐴 ) ∈ ℕ → ( abs ‘ 𝐴 ) ∈ 𝑀 ) )
62 54 57 61 sylsyld ⊢ ( 𝜑 → ( 𝐴 ≠ 0 → ( abs ‘ 𝐴 ) ∈ 𝑀 ) )