Theorem zmulscld 28406

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

Hypotheses

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

Assertion

Ref	Expression
zmulscld	⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ ℤs)

Proof of Theorem zmulscld

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zmulscld.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℤs)
2		elzs 28393	. . 3 ⊢ (𝐴 ∈ ℤs ↔ ∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦))
3	1, 2	sylib 218	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦))
4		zmulscld.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℤs)
5		elzs 28393	. . 3 ⊢ (𝐵 ∈ ℤs ↔ ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤))
6	4, 5	sylib 218	. 2 ⊢ (𝜑 → ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤))
7		reeanv 3210	. . . . 5 ⊢ (∃𝑦 ∈ ℕs ∃𝑤 ∈ ℕs (𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) ↔ (∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤)))
8	7	2rexbii 3114	. . . 4 ⊢ (∃𝑥 ∈ ℕs ∃𝑧 ∈ ℕs ∃𝑦 ∈ ℕs ∃𝑤 ∈ ℕs (𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) ↔ ∃𝑥 ∈ ℕs ∃𝑧 ∈ ℕs (∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤)))
9		reeanv 3210	. . . 4 ⊢ (∃𝑥 ∈ ℕs ∃𝑧 ∈ ℕs (∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤)) ↔ (∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤)))
10	8, 9	bitri 275	. . 3 ⊢ (∃𝑥 ∈ ℕs ∃𝑧 ∈ ℕs ∃𝑦 ∈ ℕs ∃𝑤 ∈ ℕs (𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) ↔ (∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤)))
11		nnno 28333	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℕs → 𝑥 ∈ No )
12	11	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → 𝑥 ∈ No )
13		nnno 28333	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕs → 𝑦 ∈ No )
14	13	ad2antrl 729	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → 𝑦 ∈ No )
15	12, 14	subscld 28072	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑥 -s 𝑦) ∈ No )
16		nnno 28333	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℕs → 𝑧 ∈ No )
17	16	ad2antlr 728	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → 𝑧 ∈ No )
18		nnno 28333	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℕs → 𝑤 ∈ No )
19	18	ad2antll 730	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → 𝑤 ∈ No )
20	15, 17, 19	subsdid 28167	. . . . . . . 8 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝑥 -s 𝑦) ·s (𝑧 -s 𝑤)) = (((𝑥 -s 𝑦) ·s 𝑧) -s ((𝑥 -s 𝑦) ·s 𝑤)))
21		nnmulscl 28356	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) → (𝑥 ·s 𝑧) ∈ ℕs)
22	21	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑥 ·s 𝑧) ∈ ℕs)
23	22	nnnod 28335	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑥 ·s 𝑧) ∈ No )
24		simprl 771	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → 𝑦 ∈ ℕs)
25		simplr 769	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → 𝑧 ∈ ℕs)
26		nnmulscl 28356	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕs ∧ 𝑧 ∈ ℕs) → (𝑦 ·s 𝑧) ∈ ℕs)
27	24, 25, 26	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑦 ·s 𝑧) ∈ ℕs)
28	27	nnnod 28335	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑦 ·s 𝑧) ∈ No )
29	23, 28	subscld 28072	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝑥 ·s 𝑧) -s (𝑦 ·s 𝑧)) ∈ No )
30		nnmulscl 28356	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℕs ∧ 𝑤 ∈ ℕs) → (𝑥 ·s 𝑤) ∈ ℕs)
31	30	ad2ant2rl 750	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑥 ·s 𝑤) ∈ ℕs)
32	31	nnnod 28335	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑥 ·s 𝑤) ∈ No )
33		nnmulscl 28356	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs) → (𝑦 ·s 𝑤) ∈ ℕs)
34	33	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑦 ·s 𝑤) ∈ ℕs)
35	34	nnnod 28335	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (𝑦 ·s 𝑤) ∈ No )
36	29, 32, 35	subsubs2d 28104	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (((𝑥 ·s 𝑧) -s (𝑦 ·s 𝑧)) -s ((𝑥 ·s 𝑤) -s (𝑦 ·s 𝑤))) = (((𝑥 ·s 𝑧) -s (𝑦 ·s 𝑧)) +s ((𝑦 ·s 𝑤) -s (𝑥 ·s 𝑤))))
37	12, 14, 17	subsdird 28168	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝑥 -s 𝑦) ·s 𝑧) = ((𝑥 ·s 𝑧) -s (𝑦 ·s 𝑧)))
38	12, 14, 19	subsdird 28168	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝑥 -s 𝑦) ·s 𝑤) = ((𝑥 ·s 𝑤) -s (𝑦 ·s 𝑤)))
39	37, 38	oveq12d 7379	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (((𝑥 -s 𝑦) ·s 𝑧) -s ((𝑥 -s 𝑦) ·s 𝑤)) = (((𝑥 ·s 𝑧) -s (𝑦 ·s 𝑧)) -s ((𝑥 ·s 𝑤) -s (𝑦 ·s 𝑤))))
40	23, 35, 28, 32	addsubs4d 28110	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (((𝑥 ·s 𝑧) -s (𝑦 ·s 𝑧)) +s ((𝑦 ·s 𝑤) -s (𝑥 ·s 𝑤))))
41	36, 39, 40	3eqtr4d 2782	. . . . . . . 8 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (((𝑥 -s 𝑦) ·s 𝑧) -s ((𝑥 -s 𝑦) ·s 𝑤)) = (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))))
42	20, 41	eqtrd 2772	. . . . . . 7 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝑥 -s 𝑦) ·s (𝑧 -s 𝑤)) = (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))))
43		nnaddscl 28355	. . . . . . . . . 10 ⊢ (((𝑥 ·s 𝑧) ∈ ℕs ∧ (𝑦 ·s 𝑤) ∈ ℕs) → ((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) ∈ ℕs)
44	22, 34, 43	syl2anc 585	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) ∈ ℕs)
45		nnaddscl 28355	. . . . . . . . . 10 ⊢ (((𝑦 ·s 𝑧) ∈ ℕs ∧ (𝑥 ·s 𝑤) ∈ ℕs) → ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤)) ∈ ℕs)
46	27, 31, 45	syl2anc 585	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤)) ∈ ℕs)
47		eqid 2737	. . . . . . . . . 10 ⊢ (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤)))
48		rspceov 7410	. . . . . . . . . 10 ⊢ ((((𝑥 ·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 1453	. . . . . . . . 9 ⊢ ((((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) ∈ ℕs ∧ ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤)) ∈ ℕs) → ∃𝑡 ∈ ℕs ∃𝑢 ∈ ℕs (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (𝑡 -s 𝑢))
50	44, 46, 49	syl2anc 585	. . . . . . . 8 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ∃𝑡 ∈ ℕs ∃𝑢 ∈ ℕs (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (𝑡 -s 𝑢))
51		elzs 28393	. . . . . . . 8 ⊢ ((((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) ∈ ℤs ↔ ∃𝑡 ∈ ℕs ∃𝑢 ∈ ℕs (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (𝑡 -s 𝑢))
52	50, 51	sylibr 234	. . . . . . 7 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) ∈ ℤs)
53	42, 52	eqeltrd 2837	. . . . . 6 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝑥 -s 𝑦) ·s (𝑧 -s 𝑤)) ∈ ℤs)
54		oveq12 7370	. . . . . . 7 ⊢ ((𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) = ((𝑥 -s 𝑦) ·s (𝑧 -s 𝑤)))
55	54	eleq1d 2822	. . . . . 6 ⊢ ((𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → ((𝐴 ·s 𝐵) ∈ ℤs ↔ ((𝑥 -s 𝑦) ·s (𝑧 -s 𝑤)) ∈ ℤs))
56	53, 55	syl5ibrcom 247	. . . . 5 ⊢ (((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs)) → ((𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) ∈ ℤs))
57	56	rexlimdvva 3195	. . . 4 ⊢ ((𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs) → (∃𝑦 ∈ ℕs ∃𝑤 ∈ ℕs (𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) ∈ ℤs))
58	57	rexlimivv 3180	. . 3 ⊢ (∃𝑥 ∈ ℕs ∃𝑧 ∈ ℕs ∃𝑦 ∈ ℕs ∃𝑤 ∈ ℕs (𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) ∈ ℤs)
59	10, 58	sylbir 235	. 2 ⊢ ((∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) ∈ ℤs)
60	3, 6, 59	syl2anc 585	1 ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ ℤs)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  (class class class)co 7361   No csur 27620   +_s cadds 27968   -_s csubs 28029   ·_s cmuls 28115  ℕ_scnns 28322  ℤ_sczs 28387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-ot 4577  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-nadd 8596  df-no 27623  df-lts 27624  df-bday 27625  df-les 27726  df-slts 27767  df-cuts 27769  df-0s 27816  df-1s 27817  df-made 27836  df-old 27837  df-left 27839  df-right 27840  df-norec 27947  df-norec2 27958  df-adds 27969  df-negs 28030  df-subs 28031  df-muls 28116  df-n0s 28323  df-nns 28324  df-zs 28388

This theorem is referenced by:  zsoring  28418  zexpscl  28443  pw2cutp1  28470  z12addscl  28486