Metamath Proof Explorer

Theorem lazmulzcl

Description: The extended integers are closed under multiplication with an integer. (Contributed by AV, 25-Oct-2026)

Ref Expression
Hypothesis laznegcl.r ⊢ 𝑅 = ( Z[]l ‘ 𝑆 )
Assertion lazmulzcl ( 𝑆 ∈ ℂ → ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ 𝑅 ) → ( 𝐵 · 𝐴 ) ∈ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 laznegcl.r ⊢ 𝑅 = ( Z[]l ‘ 𝑆 )
2 1 eleq2i ⊢ ( 𝐴 ∈ 𝑅 ↔ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) )
3 ellazim ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
4 3 ex ⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
5 4 adantr ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
6 2 5 biimtrid ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ 𝑅 → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
7 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
8 7 adantl ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
9 8 adantr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
10 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
11 10 adantl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℂ )
12 11 adantl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
13 simpll ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑆 ∈ ℂ )
14 9 12 13 mulassd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝐵 · 𝑏 ) · 𝑆 ) = ( 𝐵 · ( 𝑏 · 𝑆 ) ) )
15 14 eqcomd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐵 · ( 𝑏 · 𝑆 ) ) = ( ( 𝐵 · 𝑏 ) · 𝑆 ) )
16 15 oveq2d ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝐵 · 𝑎 ) + ( 𝐵 · ( 𝑏 · 𝑆 ) ) ) = ( ( 𝐵 · 𝑎 ) + ( ( 𝐵 · 𝑏 ) · 𝑆 ) ) )
17 zmulcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ( 𝐵 · 𝑎 ) ∈ ℤ )
18 17 ad2ant2lr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐵 · 𝑎 ) ∈ ℤ )
19 zmulcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝐵 · 𝑏 ) ∈ ℤ )
20 19 ad2ant2l ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐵 · 𝑏 ) ∈ ℤ )
21 18 20 jca ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝐵 · 𝑎 ) ∈ ℤ ∧ ( 𝐵 · 𝑏 ) ∈ ℤ ) )
22 lazlinz ⊢ ( 𝑆 ∈ ℂ → ( ( ( 𝐵 · 𝑎 ) ∈ ℤ ∧ ( 𝐵 · 𝑏 ) ∈ ℤ ) → ( ( 𝐵 · 𝑎 ) + ( ( 𝐵 · 𝑏 ) · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) ) )
23 13 21 22 sylc ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝐵 · 𝑎 ) + ( ( 𝐵 · 𝑏 ) · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) )
24 16 23 eqeltrd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝐵 · 𝑎 ) + ( 𝐵 · ( 𝑏 · 𝑆 ) ) ) ∈ ( Z[]l ‘ 𝑆 ) )
25 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
26 25 adantr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑎 ∈ ℂ )
27 26 adantl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
28 simpl ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) → 𝑆 ∈ ℂ )
29 mulcl ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( 𝑏 · 𝑆 ) ∈ ℂ )
30 11 28 29 syl2anr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 · 𝑆 ) ∈ ℂ )
31 9 27 30 adddid ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐵 · ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) = ( ( 𝐵 · 𝑎 ) + ( 𝐵 · ( 𝑏 · 𝑆 ) ) ) )
32 1 a1i ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑅 = ( Z[]l ‘ 𝑆 ) )
33 24 31 32 3eltr4d ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐵 · ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ∈ 𝑅 )
34 oveq2 ⊢ ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝐵 · 𝐴 ) = ( 𝐵 · ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
35 34 eleq1d ⊢ ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( ( 𝐵 · 𝐴 ) ∈ 𝑅 ↔ ( 𝐵 · ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ∈ 𝑅 ) )
36 33 35 syl5ibrcom ⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝐵 · 𝐴 ) ∈ 𝑅 ) )
37 36 rexlimdvva ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝐵 · 𝐴 ) ∈ 𝑅 ) )
38 6 37 syld ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ 𝑅 → ( 𝐵 · 𝐴 ) ∈ 𝑅 ) )
39 38 expimpd ⊢ ( 𝑆 ∈ ℂ → ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ 𝑅 ) → ( 𝐵 · 𝐴 ) ∈ 𝑅 ) )