Metamath Proof Explorer

Theorem zmulscld

Description: The surreal integers are closed under multiplication. (Contributed by Scott Fenton, 20-Aug-2025)

Ref Expression
Hypotheses zmulscld.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤs )
zmulscld.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤs )
Assertion zmulscld ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ ℤs )

Proof

Step Hyp Ref Expression
1 zmulscld.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤs )
2 zmulscld.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤs )
3 elzs ⊢ ( 𝐴 ∈ ℤs ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )
4 1 3 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )
5 elzs ⊢ ( 𝐵 ∈ ℤs ↔ ∃ 𝑧 ∈ ℕs ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) )
6 2 5 sylib ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℕs ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) )
7 reeanv ⊢ ( ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) )
8 7 2rexbii ⊢ ( ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ( ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) )
9 reeanv ⊢ ( ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ( ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) ↔ ( ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑧 ∈ ℕs ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) )
10 8 9 bitri ⊢ ( ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) ↔ ( ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑧 ∈ ℕs ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) )
11 nnsno ⊢ ( 𝑥 ∈ ℕs → 𝑥 ∈ No )
12 11 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑥 ∈ No )
13 nnsno ⊢ ( 𝑦 ∈ ℕs → 𝑦 ∈ No )
14 13 ad2antrl ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑦 ∈ No )
15 12 14 subscld ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑥 -s 𝑦 ) ∈ No )
16 nnsno ⊢ ( 𝑧 ∈ ℕs → 𝑧 ∈ No )
17 16 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑧 ∈ No )
18 nnsno ⊢ ( 𝑤 ∈ ℕs → 𝑤 ∈ No )
19 18 ad2antll ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑤 ∈ No )
20 15 17 19 subsdid ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 -s 𝑦 ) ·s ( 𝑧 -s 𝑤 ) ) = ( ( ( 𝑥 -s 𝑦 ) ·s 𝑧 ) -s ( ( 𝑥 -s 𝑦 ) ·s 𝑤 ) ) )
21 nnmulscl ⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) → ( 𝑥 ·s 𝑧 ) ∈ ℕs )
22 21 adantr ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑥 ·s 𝑧 ) ∈ ℕs )
23 22 nnsnod ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑥 ·s 𝑧 ) ∈ No )
24 simprl ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑦 ∈ ℕs )
25 simplr ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑧 ∈ ℕs )
26 nnmulscl ⊢ ( ( 𝑦 ∈ ℕs ∧ 𝑧 ∈ ℕs ) → ( 𝑦 ·s 𝑧 ) ∈ ℕs )
27 24 25 26 syl2anc ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑦 ·s 𝑧 ) ∈ ℕs )
28 27 nnsnod ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑦 ·s 𝑧 ) ∈ No )
29 23 28 subscld ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 ·s 𝑧 ) -s ( 𝑦 ·s 𝑧 ) ) ∈ No )
30 nnmulscl ⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑤 ∈ ℕs ) → ( 𝑥 ·s 𝑤 ) ∈ ℕs )
31 30 ad2ant2rl ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑥 ·s 𝑤 ) ∈ ℕs )
32 31 nnsnod ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑥 ·s 𝑤 ) ∈ No )
33 nnmulscl ⊢ ( ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) → ( 𝑦 ·s 𝑤 ) ∈ ℕs )
34 33 adantl ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑦 ·s 𝑤 ) ∈ ℕs )
35 34 nnsnod ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( 𝑦 ·s 𝑤 ) ∈ No )
36 29 32 35 subsubs2d ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( ( 𝑥 ·s 𝑧 ) -s ( 𝑦 ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑤 ) -s ( 𝑦 ·s 𝑤 ) ) ) = ( ( ( 𝑥 ·s 𝑧 ) -s ( 𝑦 ·s 𝑧 ) ) +s ( ( 𝑦 ·s 𝑤 ) -s ( 𝑥 ·s 𝑤 ) ) ) )
37 12 14 17 subsdird ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 -s 𝑦 ) ·s 𝑧 ) = ( ( 𝑥 ·s 𝑧 ) -s ( 𝑦 ·s 𝑧 ) ) )
38 12 14 19 subsdird ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 -s 𝑦 ) ·s 𝑤 ) = ( ( 𝑥 ·s 𝑤 ) -s ( 𝑦 ·s 𝑤 ) ) )
39 37 38 oveq12d ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( ( 𝑥 -s 𝑦 ) ·s 𝑧 ) -s ( ( 𝑥 -s 𝑦 ) ·s 𝑤 ) ) = ( ( ( 𝑥 ·s 𝑧 ) -s ( 𝑦 ·s 𝑧 ) ) -s ( ( 𝑥 ·s 𝑤 ) -s ( 𝑦 ·s 𝑤 ) ) ) )
40 23 35 28 32 addsubs4d ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) = ( ( ( 𝑥 ·s 𝑧 ) -s ( 𝑦 ·s 𝑧 ) ) +s ( ( 𝑦 ·s 𝑤 ) -s ( 𝑥 ·s 𝑤 ) ) ) )
41 36 39 40 3eqtr4d ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( ( 𝑥 -s 𝑦 ) ·s 𝑧 ) -s ( ( 𝑥 -s 𝑦 ) ·s 𝑤 ) ) = ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) )
42 20 41 eqtrd ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 -s 𝑦 ) ·s ( 𝑧 -s 𝑤 ) ) = ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) )
43 nnaddscl ⊢ ( ( ( 𝑥 ·s 𝑧 ) ∈ ℕs ∧ ( 𝑦 ·s 𝑤 ) ∈ ℕs ) → ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) ∈ ℕs )
44 22 34 43 syl2anc ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) ∈ ℕs )
45 nnaddscl ⊢ ( ( ( 𝑦 ·s 𝑧 ) ∈ ℕs ∧ ( 𝑥 ·s 𝑤 ) ∈ ℕs ) → ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ∈ ℕs )
46 27 31 45 syl2anc ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ∈ ℕs )
47 eqid ⊢ ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) = ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) )
48 rspceov ⊢ ( ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) ∈ ℕs ∧ ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ∈ ℕs ∧ ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) = ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) ) → ∃ 𝑡 ∈ ℕs ∃ 𝑢 ∈ ℕs ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) = ( 𝑡 -s 𝑢 ) )
49 47 48 mp3an3 ⊢ ( ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) ∈ ℕs ∧ ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ∈ ℕs ) → ∃ 𝑡 ∈ ℕs ∃ 𝑢 ∈ ℕs ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) = ( 𝑡 -s 𝑢 ) )
50 44 46 49 syl2anc ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ∃ 𝑡 ∈ ℕs ∃ 𝑢 ∈ ℕs ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) = ( 𝑡 -s 𝑢 ) )
51 elzs ⊢ ( ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) ∈ ℤs ↔ ∃ 𝑡 ∈ ℕs ∃ 𝑢 ∈ ℕs ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) = ( 𝑡 -s 𝑢 ) )
52 50 51 sylibr ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( ( 𝑥 ·s 𝑧 ) +s ( 𝑦 ·s 𝑤 ) ) -s ( ( 𝑦 ·s 𝑧 ) +s ( 𝑥 ·s 𝑤 ) ) ) ∈ ℤs )
53 42 52 eqeltrd ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 -s 𝑦 ) ·s ( 𝑧 -s 𝑤 ) ) ∈ ℤs )
54 oveq12 ⊢ ( ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 ·s 𝐵 ) = ( ( 𝑥 -s 𝑦 ) ·s ( 𝑧 -s 𝑤 ) ) )
55 54 eleq1d ⊢ ( ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ ℤs ↔ ( ( 𝑥 -s 𝑦 ) ·s ( 𝑧 -s 𝑤 ) ) ∈ ℤs ) )
56 53 55 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 ·s 𝐵 ) ∈ ℤs ) )
57 56 rexlimdvva ⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) → ( ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 ·s 𝐵 ) ∈ ℤs ) )
58 57 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 ·s 𝐵 ) ∈ ℤs )
59 10 58 sylbir ⊢ ( ( ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑧 ∈ ℕs ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 ·s 𝐵 ) ∈ ℤs )
60 4 6 59 syl2anc ⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ ℤs )