Metamath Proof Explorer

Theorem adcnmulzlaz

Description: The extended complex number multiplied with an integer is an extended integer. (Contributed by AV, 25-Oct-2026)

Ref Expression
Assertion adcnmulzlaz Could not format assertion : No typesetting found for |- ( ( S e. CC /\ C e. ZZ ) -> ( C x. S ) e. ( Z[]l ` S ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 zcn ⊢ C ∈ ℤ → C ∈ ℂ
2 1 adantl ⊢ S ∈ ℂ ∧ C ∈ ℤ → C ∈ ℂ
3 simpl ⊢ S ∈ ℂ ∧ C ∈ ℤ → S ∈ ℂ
4 2 3 mulcld ⊢ S ∈ ℂ ∧ C ∈ ℤ → C ⁢ S ∈ ℂ
5 oveq1 ⊢ a = 0 → a + b ⁢ S = 0 + b ⁢ S
6 5 eqeq2d ⊢ a = 0 → C ⁢ S = a + b ⁢ S ↔ C ⁢ S = 0 + b ⁢ S
7 oveq1 ⊢ b = C → b ⁢ S = C ⁢ S
8 7 oveq2d ⊢ b = C → 0 + b ⁢ S = 0 + C ⁢ S
9 8 eqeq2d ⊢ b = C → C ⁢ S = 0 + b ⁢ S ↔ C ⁢ S = 0 + C ⁢ S
10 0zd ⊢ S ∈ ℂ ∧ C ∈ ℤ → 0 ∈ ℤ
11 simpr ⊢ S ∈ ℂ ∧ C ∈ ℤ → C ∈ ℤ
12 4 addlidd ⊢ S ∈ ℂ ∧ C ∈ ℤ → 0 + C ⁢ S = C ⁢ S
13 12 eqcomd ⊢ S ∈ ℂ ∧ C ∈ ℤ → C ⁢ S = 0 + C ⁢ S
14 6 9 10 11 13 2rspcedvdw ⊢ S ∈ ℂ ∧ C ∈ ℤ → ∃ a ∈ ℤ ∃ b ∈ ℤ C ⁢ S = a + b ⁢ S
15 ellaz Could not format ( S e. CC -> ( ( C x. S ) e. ( Z[]l ` S ) <-> ( ( C x. S ) e. CC /\ E. a e. ZZ E. b e. ZZ ( C x. S ) = ( a + ( b x. S ) ) ) ) ) : No typesetting found for |- ( S e. CC -> ( ( C x. S ) e. ( Z[]l ` S ) <-> ( ( C x. S ) e. CC /\ E. a e. ZZ E. b e. ZZ ( C x. S ) = ( a + ( b x. S ) ) ) ) ) with typecode |-
16 15 adantr Could not format ( ( S e. CC /\ C e. ZZ ) -> ( ( C x. S ) e. ( Z[]l ` S ) <-> ( ( C x. S ) e. CC /\ E. a e. ZZ E. b e. ZZ ( C x. S ) = ( a + ( b x. S ) ) ) ) ) : No typesetting found for |- ( ( S e. CC /\ C e. ZZ ) -> ( ( C x. S ) e. ( Z[]l ` S ) <-> ( ( C x. S ) e. CC /\ E. a e. ZZ E. b e. ZZ ( C x. S ) = ( a + ( b x. S ) ) ) ) ) with typecode |-
17 4 14 16 mpbir2and Could not format ( ( S e. CC /\ C e. ZZ ) -> ( C x. S ) e. ( Z[]l ` S ) ) : No typesetting found for |- ( ( S e. CC /\ C e. ZZ ) -> ( C x. S ) e. ( Z[]l ` S ) ) with typecode |-