Metamath Proof Explorer

Theorem bezoutlem1

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

Ref Expression
Hypotheses bezout.1 ⊢ M = z ∈ ℕ | ∃ x ∈ ℤ ∃ y ∈ ℤ z = A ⁢ x + B ⁢ y
bezout.3 ⊢ φ → A ∈ ℤ
bezout.4 ⊢ φ → B ∈ ℤ
Assertion bezoutlem1 ⊢ φ → A ≠ 0 → A ∈ M

Proof

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