Metamath Proof Explorer

Theorem lazaddcl

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

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

Proof

Step Hyp Ref Expression
1 laznegcl.r ⊢ 𝑅 = ( Z[]l ‘ 𝑆 )
2 1 eleq2i ⊢ ( 𝐴 ∈ 𝑅 ↔ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) )
3 1 eleq2i ⊢ ( 𝐵 ∈ 𝑅 ↔ 𝐵 ∈ ( Z[]l ‘ 𝑆 ) )
4 2 3 anbi12i ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ↔ ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ∧ 𝐵 ∈ ( Z[]l ‘ 𝑆 ) ) )
5 ellazim ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
6 5 ex ⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
7 ellazim ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐵 ∈ ( Z[]l ‘ 𝑆 ) ) → ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) )
8 7 ex ⊢ ( 𝑆 ∈ ℂ → ( 𝐵 ∈ ( Z[]l ‘ 𝑆 ) → ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) )
9 simpl ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑆 ∈ ℂ )
10 9 adantr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑆 ∈ ℂ )
11 simpl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑎 ∈ ℤ )
12 11 adantl ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
13 simpl ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → 𝑐 ∈ ℤ )
14 zaddcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑐 ∈ ℤ ) → ( 𝑎 + 𝑐 ) ∈ ℤ )
15 12 13 14 syl2an ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑎 + 𝑐 ) ∈ ℤ )
16 simpr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℤ )
17 16 adantl ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
18 simpr ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → 𝑑 ∈ ℤ )
19 zaddcl ⊢ ( ( 𝑏 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( 𝑏 + 𝑑 ) ∈ ℤ )
20 17 18 19 syl2an ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑏 + 𝑑 ) ∈ ℤ )
21 15 20 jca ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 + 𝑐 ) ∈ ℤ ∧ ( 𝑏 + 𝑑 ) ∈ ℤ ) )
22 lazlinz ⊢ ( 𝑆 ∈ ℂ → ( ( ( 𝑎 + 𝑐 ) ∈ ℤ ∧ ( 𝑏 + 𝑑 ) ∈ ℤ ) → ( ( 𝑎 + 𝑐 ) + ( ( 𝑏 + 𝑑 ) · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) ) )
23 10 21 22 sylc ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 + 𝑐 ) + ( ( 𝑏 + 𝑑 ) · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) )
24 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
25 24 ad2antrl ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
26 25 adantr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
27 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
28 27 ad2antll ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
29 28 adantr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
30 29 10 mulcld ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑏 · 𝑆 ) ∈ ℂ )
31 zcn ⊢ ( 𝑐 ∈ ℤ → 𝑐 ∈ ℂ )
32 31 ad2antrl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑐 ∈ ℂ )
33 zcn ⊢ ( 𝑑 ∈ ℤ → 𝑑 ∈ ℂ )
34 33 ad2antll ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑑 ∈ ℂ )
35 34 10 mulcld ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑑 · 𝑆 ) ∈ ℂ )
36 26 30 32 35 add4d ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) + ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) = ( ( 𝑎 + 𝑐 ) + ( ( 𝑏 · 𝑆 ) + ( 𝑑 · 𝑆 ) ) ) )
37 29 34 10 adddird ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑏 + 𝑑 ) · 𝑆 ) = ( ( 𝑏 · 𝑆 ) + ( 𝑑 · 𝑆 ) ) )
38 37 eqcomd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑏 · 𝑆 ) + ( 𝑑 · 𝑆 ) ) = ( ( 𝑏 + 𝑑 ) · 𝑆 ) )
39 38 oveq2d ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 + 𝑐 ) + ( ( 𝑏 · 𝑆 ) + ( 𝑑 · 𝑆 ) ) ) = ( ( 𝑎 + 𝑐 ) + ( ( 𝑏 + 𝑑 ) · 𝑆 ) ) )
40 36 39 eqtrd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) + ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) = ( ( 𝑎 + 𝑐 ) + ( ( 𝑏 + 𝑑 ) · 𝑆 ) ) )
41 1 a1i ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑅 = ( Z[]l ‘ 𝑆 ) )
42 23 40 41 3eltr4d ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) + ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) ∈ 𝑅 )
43 oveq12 ⊢ ( ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∧ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) → ( 𝐴 + 𝐵 ) = ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) + ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) )
44 43 eleq1d ⊢ ( ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∧ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑅 ↔ ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) + ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) ∈ 𝑅 ) )
45 44 ancoms ⊢ ( ( 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑅 ↔ ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) + ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) ∈ 𝑅 ) )
46 42 45 syl5ibrcom ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑅 ) )
47 46 expd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑅 ) ) )
48 47 rexlimdvva ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑅 ) ) )
49 48 com23 ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑅 ) ) )
50 49 rexlimdvva ⊢ ( 𝑆 ∈ ℂ → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑅 ) ) )
51 50 impd ⊢ ( 𝑆 ∈ ℂ → ( ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑅 ) )
52 6 8 51 syl2and ⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ∧ 𝐵 ∈ ( Z[]l ‘ 𝑆 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑅 ) )
53 4 52 biimtrid ⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → ( 𝐴 + 𝐵 ) ∈ 𝑅 ) )