Metamath Proof Explorer

Theorem z12addscl

Description: The dyadics are closed under addition. (Contributed by Scott Fenton, 11-Dec-2025)

Ref Expression
Assertion z12addscl ( ( 𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2] ) → ( 𝐴 +s 𝐵 ) ∈ ℤs[1/2] )

Proof

Step Hyp Ref Expression
1 elz12s ⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑎 ∈ ℤs ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) )
2 elz12s ⊢ ( 𝐵 ∈ ℤs[1/2] ↔ ∃ 𝑏 ∈ ℤs ∃ 𝑚 ∈ ℕ0s 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) )
3 reeanv ⊢ ( ∃ 𝑛 ∈ ℕ0s ∃ 𝑚 ∈ ℕ0s ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ ∃ 𝑚 ∈ ℕ0s 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) )
4 3 2rexbii ⊢ ( ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℤs ∃ 𝑛 ∈ ℕ0s ∃ 𝑚 ∈ ℕ0s ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) ↔ ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℤs ( ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ ∃ 𝑚 ∈ ℕ0s 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) )
5 reeanv ⊢ ( ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℤs ( ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ ∃ 𝑚 ∈ ℕ0s 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) ↔ ( ∃ 𝑎 ∈ ℤs ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ ∃ 𝑏 ∈ ℤs ∃ 𝑚 ∈ ℕ0s 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) )
6 4 5 bitri ⊢ ( ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℤs ∃ 𝑛 ∈ ℕ0s ∃ 𝑚 ∈ ℕ0s ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) ↔ ( ∃ 𝑎 ∈ ℤs ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ ∃ 𝑏 ∈ ℤs ∃ 𝑚 ∈ ℕ0s 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) )
7 simpll ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → 𝑎 ∈ ℤs )
8 7 znod ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → 𝑎 ∈ No )
9 simprl ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → 𝑛 ∈ ℕ0s )
10 simprr ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → 𝑚 ∈ ℕ0s )
11 8 9 10 pw2divscan4d ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 𝑎 /su ( 2s ↑s 𝑛 ) ) = ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) )
12 simplr ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → 𝑏 ∈ ℤs )
13 12 znod ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → 𝑏 ∈ No )
14 13 10 9 pw2divscan4d ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 𝑏 /su ( 2s ↑s 𝑚 ) ) = ( ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) /su ( 2s ↑s ( 𝑚 +s 𝑛 ) ) ) )
15 10 n0nod ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → 𝑚 ∈ No )
16 9 n0nod ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → 𝑛 ∈ No )
17 15 16 addscomd ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 𝑚 +s 𝑛 ) = ( 𝑛 +s 𝑚 ) )
18 17 oveq2d ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 2s ↑s ( 𝑚 +s 𝑛 ) ) = ( 2s ↑s ( 𝑛 +s 𝑚 ) ) )
19 18 oveq2d ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) /su ( 2s ↑s ( 𝑚 +s 𝑛 ) ) ) = ( ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) )
20 14 19 eqtrd ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 𝑏 /su ( 2s ↑s 𝑚 ) ) = ( ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) )
21 11 20 oveq12d ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) +s ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) +s ( ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) ) )
22 2no ⊢ 2s ∈ No
23 expscl ⊢ ( ( 2s ∈ No ∧ 𝑚 ∈ ℕ0s ) → ( 2s ↑s 𝑚 ) ∈ No )
24 22 10 23 sylancr ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 2s ↑s 𝑚 ) ∈ No )
25 24 8 mulscld ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) ∈ No )
26 expscl ⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ∈ No )
27 22 9 26 sylancr ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 2s ↑s 𝑛 ) ∈ No )
28 27 13 mulscld ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ∈ No )
29 n0addscl ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) → ( 𝑛 +s 𝑚 ) ∈ ℕ0s )
30 29 adantl ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 𝑛 +s 𝑚 ) ∈ ℕ0s )
31 25 28 30 pw2divsdird ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) +s ( ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) ) )
32 21 31 eqtr4d ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) +s ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) )
33 oveq1 ⊢ ( 𝑐 = ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) → ( 𝑐 /su ( 2s ↑s 𝑝 ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s 𝑝 ) ) )
34 33 eqeq2d ⊢ ( 𝑐 = ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) → ( ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) = ( 𝑐 /su ( 2s ↑s 𝑝 ) ) ↔ ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s 𝑝 ) ) ) )
35 oveq2 ⊢ ( 𝑝 = ( 𝑛 +s 𝑚 ) → ( 2s ↑s 𝑝 ) = ( 2s ↑s ( 𝑛 +s 𝑚 ) ) )
36 35 oveq2d ⊢ ( 𝑝 = ( 𝑛 +s 𝑚 ) → ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s 𝑝 ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) )
37 36 eqeq2d ⊢ ( 𝑝 = ( 𝑛 +s 𝑚 ) → ( ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s 𝑝 ) ) ↔ ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) ) )
38 2nns ⊢ 2s ∈ ℕs
39 nnzs ⊢ ( 2s ∈ ℕs → 2s ∈ ℤs )
40 38 39 ax-mp ⊢ 2s ∈ ℤs
41 zexpscl ⊢ ( ( 2s ∈ ℤs ∧ 𝑚 ∈ ℕ0s ) → ( 2s ↑s 𝑚 ) ∈ ℤs )
42 40 10 41 sylancr ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 2s ↑s 𝑚 ) ∈ ℤs )
43 42 7 zmulscld ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) ∈ ℤs )
44 zexpscl ⊢ ( ( 2s ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ∈ ℤs )
45 40 9 44 sylancr ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( 2s ↑s 𝑛 ) ∈ ℤs )
46 45 12 zmulscld ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ∈ ℤs )
47 43 46 zaddscld ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) ∈ ℤs )
48 eqidd ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) = ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) )
49 34 37 47 30 48 2rspcedvdw ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ∃ 𝑐 ∈ ℤs ∃ 𝑝 ∈ ℕ0s ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) = ( 𝑐 /su ( 2s ↑s 𝑝 ) ) )
50 elz12s ⊢ ( ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) ∈ ℤs[1/2] ↔ ∃ 𝑐 ∈ ℤs ∃ 𝑝 ∈ ℕ0s ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) = ( 𝑐 /su ( 2s ↑s 𝑝 ) ) )
51 49 50 sylibr ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( ( ( 2s ↑s 𝑚 ) ·s 𝑎 ) +s ( ( 2s ↑s 𝑛 ) ·s 𝑏 ) ) /su ( 2s ↑s ( 𝑛 +s 𝑚 ) ) ) ∈ ℤs[1/2] )
52 32 51 eqeltrd ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) +s ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) ∈ ℤs[1/2] )
53 oveq12 ⊢ ( ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) → ( 𝐴 +s 𝐵 ) = ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) +s ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) )
54 53 eleq1d ⊢ ( ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) → ( ( 𝐴 +s 𝐵 ) ∈ ℤs[1/2] ↔ ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) +s ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) ∈ ℤs[1/2] ) )
55 52 54 syl5ibrcom ⊢ ( ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) ∧ ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ) → ( ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) → ( 𝐴 +s 𝐵 ) ∈ ℤs[1/2] ) )
56 55 rexlimdvva ⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℤs ) → ( ∃ 𝑛 ∈ ℕ0s ∃ 𝑚 ∈ ℕ0s ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) → ( 𝐴 +s 𝐵 ) ∈ ℤs[1/2] ) )
57 56 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℤs ∃ 𝑛 ∈ ℕ0s ∃ 𝑚 ∈ ℕ0s ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) → ( 𝐴 +s 𝐵 ) ∈ ℤs[1/2] )
58 6 57 sylbir ⊢ ( ( ∃ 𝑎 ∈ ℤs ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∧ ∃ 𝑏 ∈ ℤs ∃ 𝑚 ∈ ℕ0s 𝐵 = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ) → ( 𝐴 +s 𝐵 ) ∈ ℤs[1/2] )
59 1 2 58 syl2anb ⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2] ) → ( 𝐴 +s 𝐵 ) ∈ ℤs[1/2] )