Metamath Proof Explorer

Theorem zlmodzxzldeplem1

Description: Lemma 1 for zlmodzxzldep . (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzldep.z ⊢ Z = ℤ ring freeLMod 0 1
zlmodzxzldep.a ⊢ A = 0 3 1 6
zlmodzxzldep.b ⊢ B = 0 2 1 4
zlmodzxzldeplem.f ⊢ F = A 2 B − 3
Assertion zlmodzxzldeplem1 ⊢ F ∈ ℤ A B

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z ⊢ Z = ℤ ring freeLMod 0 1
2 zlmodzxzldep.a ⊢ A = 0 3 1 6
3 zlmodzxzldep.b ⊢ B = 0 2 1 4
4 zlmodzxzldeplem.f ⊢ F = A 2 B − 3
5 zex ⊢ ℤ ∈ V
6 prex ⊢ A B ∈ V
7 prex ⊢ 0 3 1 6 ∈ V
8 2 7 eqeltri ⊢ A ∈ V
9 prex ⊢ 0 2 1 4 ∈ V
10 3 9 eqeltri ⊢ B ∈ V
11 8 10 pm3.2i ⊢ A ∈ V ∧ B ∈ V
12 11 a1i ⊢ ℤ ∈ V ∧ A B ∈ V → A ∈ V ∧ B ∈ V
13 2z ⊢ 2 ∈ ℤ
14 3nn0 ⊢ 3 ∈ ℕ 0
15 14 nn0negzi ⊢ − 3 ∈ ℤ
16 13 15 pm3.2i ⊢ 2 ∈ ℤ ∧ − 3 ∈ ℤ
17 16 a1i ⊢ ℤ ∈ V ∧ A B ∈ V → 2 ∈ ℤ ∧ − 3 ∈ ℤ
18 1 2 3 zlmodzxzldeplem ⊢ A ≠ B
19 18 a1i ⊢ ℤ ∈ V ∧ A B ∈ V → A ≠ B
20 fprg ⊢ A ∈ V ∧ B ∈ V ∧ 2 ∈ ℤ ∧ − 3 ∈ ℤ ∧ A ≠ B → A 2 B − 3 : A B ⟶ 2 − 3
21 4 feq1i ⊢ F : A B ⟶ 2 − 3 ↔ A 2 B − 3 : A B ⟶ 2 − 3
22 20 21 sylibr ⊢ A ∈ V ∧ B ∈ V ∧ 2 ∈ ℤ ∧ − 3 ∈ ℤ ∧ A ≠ B → F : A B ⟶ 2 − 3
23 12 17 19 22 syl3anc ⊢ ℤ ∈ V ∧ A B ∈ V → F : A B ⟶ 2 − 3
24 prssi ⊢ 2 ∈ ℤ ∧ − 3 ∈ ℤ → 2 − 3 ⊆ ℤ
25 13 15 24 mp2an ⊢ 2 − 3 ⊆ ℤ
26 fss ⊢ F : A B ⟶ 2 − 3 ∧ 2 − 3 ⊆ ℤ → F : A B ⟶ ℤ
27 23 25 26 sylancl ⊢ ℤ ∈ V ∧ A B ∈ V → F : A B ⟶ ℤ
28 elmapg ⊢ ℤ ∈ V ∧ A B ∈ V → F ∈ ℤ A B ↔ F : A B ⟶ ℤ
29 27 28 mpbird ⊢ ℤ ∈ V ∧ A B ∈ V → F ∈ ℤ A B
30 5 6 29 mp2an ⊢ F ∈ ℤ A B