Metamath Proof Explorer

Theorem lazmulcl

Description: The extended integers are closed under multiplication if the square of the adjoined complex number is an extended integer. (Contributed by AV, 25-Oct-2026)

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

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 6 8 anim12d ⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ∧ 𝐵 ∈ ( Z[]l ‘ 𝑆 ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) ) )
10 4 9 biimtrid ⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) ) )
11 10 adantr ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) ) )
12 oveq12 ⊢ ( ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∧ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) → ( 𝐴 · 𝐵 ) = ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) · ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) )
13 12 ancoms ⊢ ( ( 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → ( 𝐴 · 𝐵 ) = ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) · ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) )
14 13 adantl ⊢ ( ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) → ( 𝐴 · 𝐵 ) = ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) · ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) )
15 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
16 15 ad2antrl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
17 16 adantr ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
18 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
19 18 ad2antll ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
20 19 adantr ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
21 simplll ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑆 ∈ ℂ )
22 zcn ⊢ ( 𝑐 ∈ ℤ → 𝑐 ∈ ℂ )
23 22 ad2antrl ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑐 ∈ ℂ )
24 zcn ⊢ ( 𝑑 ∈ ℤ → 𝑑 ∈ ℂ )
25 24 ad2antll ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → 𝑑 ∈ ℂ )
26 17 20 21 23 25 addmuldir2d ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) · ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) = ( ( ( 𝑎 · 𝑐 ) + ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ) + ( ( 𝑏 · 𝑑 ) · ( 𝑆 ↑ 2 ) ) ) )
27 simpl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑎 ∈ ℤ )
28 27 adantl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
29 simpl ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → 𝑐 ∈ ℤ )
30 zmulcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑐 ∈ ℤ ) → ( 𝑎 · 𝑐 ) ∈ ℤ )
31 28 29 30 syl2an ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑎 · 𝑐 ) ∈ ℤ )
32 zellaz ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 · 𝑐 ) ∈ ℤ ) → ( 𝑎 · 𝑐 ) ∈ ( Z[]l ‘ 𝑆 ) )
33 21 31 32 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑎 · 𝑐 ) ∈ ( Z[]l ‘ 𝑆 ) )
34 33 1 eleqtrrdi ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑎 · 𝑐 ) ∈ 𝑅 )
35 simpr ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → 𝑑 ∈ ℤ )
36 zmulcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( 𝑎 · 𝑑 ) ∈ ℤ )
37 28 35 36 syl2an ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑎 · 𝑑 ) ∈ ℤ )
38 simpr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℤ )
39 38 adantl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
40 zmulcl ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑐 · 𝑏 ) ∈ ℤ )
41 29 39 40 syl2anr ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑐 · 𝑏 ) ∈ ℤ )
42 37 41 zaddcld ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ∈ ℤ )
43 adcnmulzlaz ⊢ ( ( 𝑆 ∈ ℂ ∧ ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ∈ ℤ ) → ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ∈ ( Z[]l ‘ 𝑆 ) )
44 21 42 43 syl2anc ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ∈ ( Z[]l ‘ 𝑆 ) )
45 44 1 eleqtrrdi ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ∈ 𝑅 )
46 34 45 jca ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 · 𝑐 ) ∈ 𝑅 ∧ ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ∈ 𝑅 ) )
47 1 lazaddcl ⊢ ( 𝑆 ∈ ℂ → ( ( ( 𝑎 · 𝑐 ) ∈ 𝑅 ∧ ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ∈ 𝑅 ) → ( ( 𝑎 · 𝑐 ) + ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ) ∈ 𝑅 ) )
48 21 46 47 sylc ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 · 𝑐 ) + ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ) ∈ 𝑅 )
49 zmulcl ⊢ ( ( 𝑏 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( 𝑏 · 𝑑 ) ∈ ℤ )
50 39 35 49 syl2an ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑏 · 𝑑 ) ∈ ℤ )
51 simpllr ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝑆 ↑ 2 ) ∈ 𝑅 )
52 50 51 jca ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑏 · 𝑑 ) ∈ ℤ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) )
53 1 lazmulzcl ⊢ ( 𝑆 ∈ ℂ → ( ( ( 𝑏 · 𝑑 ) ∈ ℤ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) → ( ( 𝑏 · 𝑑 ) · ( 𝑆 ↑ 2 ) ) ∈ 𝑅 ) )
54 21 52 53 sylc ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑏 · 𝑑 ) · ( 𝑆 ↑ 2 ) ) ∈ 𝑅 )
55 48 54 jca ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( ( 𝑎 · 𝑐 ) + ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ) ∈ 𝑅 ∧ ( ( 𝑏 · 𝑑 ) · ( 𝑆 ↑ 2 ) ) ∈ 𝑅 ) )
56 1 lazaddcl ⊢ ( 𝑆 ∈ ℂ → ( ( ( ( 𝑎 · 𝑐 ) + ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ) ∈ 𝑅 ∧ ( ( 𝑏 · 𝑑 ) · ( 𝑆 ↑ 2 ) ) ∈ 𝑅 ) → ( ( ( 𝑎 · 𝑐 ) + ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ) + ( ( 𝑏 · 𝑑 ) · ( 𝑆 ↑ 2 ) ) ) ∈ 𝑅 ) )
57 21 55 56 sylc ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( ( 𝑎 · 𝑐 ) + ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) · 𝑆 ) ) + ( ( 𝑏 · 𝑑 ) · ( 𝑆 ↑ 2 ) ) ) ∈ 𝑅 )
58 26 57 eqeltrd ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) · ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) ∈ 𝑅 )
59 58 adantr ⊢ ( ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) · ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) ∈ 𝑅 )
60 14 59 eqeltrd ⊢ ( ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑅 )
61 60 exp32 ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑅 ) ) )
62 61 rexlimdvva ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑅 ) ) )
63 62 com23 ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑅 ) ) )
64 63 rexlimdvva ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑅 ) ) )
65 64 impd ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) → ( ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐵 = ( 𝑐 + ( 𝑑 · 𝑆 ) ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑅 ) )
66 11 65 syld ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ 𝑅 ) → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → ( 𝐴 · 𝐵 ) ∈ 𝑅 ) )