Metamath Proof Explorer

Theorem lazsubcl

Description: The extended integers are closed under subtraction. (Contributed by AV, 25-Oct-2026)

Ref Expression
Hypothesis laznegcl.r No typesetting found for |- R = ( Z[]l ` S ) with typecode |-
Assertion lazsubcl ⊢ S ∈ ℂ → A ∈ R ∧ B ∈ R → A − B ∈ R

Proof

Step Hyp Ref Expression
1 laznegcl.r Could not format R = ( Z[]l ` S ) : No typesetting found for |- R = ( Z[]l ` S ) with typecode |-
2 1 eleq2i Could not format ( A e. R <-> A e. ( Z[]l ` S ) ) : No typesetting found for |- ( A e. R <-> A e. ( Z[]l ` S ) ) with typecode |-
3 lazcn Could not format ( S e. CC -> ( A e. ( Z[]l ` S ) -> A e. CC ) ) : No typesetting found for |- ( S e. CC -> ( A e. ( Z[]l ` S ) -> A e. CC ) ) with typecode |-
4 3 a1dd Could not format ( S e. CC -> ( A e. ( Z[]l ` S ) -> ( B e. R -> A e. CC ) ) ) : No typesetting found for |- ( S e. CC -> ( A e. ( Z[]l ` S ) -> ( B e. R -> A e. CC ) ) ) with typecode |-
5 2 4 biimtrid ⊢ S ∈ ℂ → A ∈ R → B ∈ R → A ∈ ℂ
6 5 imp32 ⊢ S ∈ ℂ ∧ A ∈ R ∧ B ∈ R → A ∈ ℂ
7 1 eleq2i Could not format ( B e. R <-> B e. ( Z[]l ` S ) ) : No typesetting found for |- ( B e. R <-> B e. ( Z[]l ` S ) ) with typecode |-
8 lazcn Could not format ( S e. CC -> ( B e. ( Z[]l ` S ) -> B e. CC ) ) : No typesetting found for |- ( S e. CC -> ( B e. ( Z[]l ` S ) -> B e. CC ) ) with typecode |-
9 7 8 biimtrid ⊢ S ∈ ℂ → B ∈ R → B ∈ ℂ
10 9 adantld ⊢ S ∈ ℂ → A ∈ R ∧ B ∈ R → B ∈ ℂ
11 10 imp ⊢ S ∈ ℂ ∧ A ∈ R ∧ B ∈ R → B ∈ ℂ
12 6 11 negsubd ⊢ S ∈ ℂ ∧ A ∈ R ∧ B ∈ R → A + − B = A − B
13 1 laznegcl ⊢ S ∈ ℂ → B ∈ R → − B ∈ R
14 13 anim2d ⊢ S ∈ ℂ → A ∈ R ∧ B ∈ R → A ∈ R ∧ − B ∈ R
15 14 imp ⊢ S ∈ ℂ ∧ A ∈ R ∧ B ∈ R → A ∈ R ∧ − B ∈ R
16 1 lazaddcl ⊢ S ∈ ℂ → A ∈ R ∧ − B ∈ R → A + − B ∈ R
17 16 imp ⊢ S ∈ ℂ ∧ A ∈ R ∧ − B ∈ R → A + − B ∈ R
18 15 17 syldan ⊢ S ∈ ℂ ∧ A ∈ R ∧ B ∈ R → A + − B ∈ R
19 12 18 eqeltrrd ⊢ S ∈ ℂ ∧ A ∈ R ∧ B ∈ R → A − B ∈ R
20 19 ex ⊢ S ∈ ℂ → A ∈ R ∧ B ∈ R → A − B ∈ R