Metamath Proof Explorer

Theorem zs12addscl

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

Ref Expression
Assertion zs12addscl 
|- ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A +s B ) e. ZZ_s[1/2] )

Proof

Step Hyp Ref Expression
1 elzs12 
 |-  ( A e. ZZ_s[1/2] <-> E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) )
2 elzs12 
 |-  ( B e. ZZ_s[1/2] <-> E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) )
3 reeanv 
 |-  ( E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) )
4 3 2rexbii 
 |-  ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> E. a e. ZZ_s E. b e. ZZ_s ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) )
5 reeanv 
 |-  ( E. a e. ZZ_s E. b e. ZZ_s ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) <-> ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) )
6 4 5 bitri 
 |-  ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) )
7 simpll 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> a e. ZZ_s )
8 7 znod 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> a e. No )
9 simprl 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> n e. NN0_s )
10 simprr 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> m e. NN0_s )
11 8 9 10 pw2divscan4d 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( a /su ( 2s ^su n ) ) = ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) )
12 simplr 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> b e. ZZ_s )
13 12 znod 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> b e. No )
14 13 10 9 pw2divscan4d 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( b /su ( 2s ^su m ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( m +s n ) ) ) )
15 10 n0snod 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> m e. No )
16 9 n0snod 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> n e. No )
17 15 16 addscomd 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( m +s n ) = ( n +s m ) )
18 17 oveq2d 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su ( m +s n ) ) = ( 2s ^su ( n +s m ) ) )
19 18 oveq2d 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( m +s n ) ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) )
20 14 19 eqtrd 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( b /su ( 2s ^su m ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) )
21 11 20 oveq12d 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) +s ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) )
22 2sno 
 |-  2s e. No
23 expscl 
 |-  ( ( 2s e. No /\ m e. NN0_s ) -> ( 2s ^su m ) e. No )
24 22 10 23 sylancr 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su m ) e. No )
25 24 8 mulscld 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su m ) x.s a ) e. No )
26 expscl 
 |-  ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No )
27 22 9 26 sylancr 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su n ) e. No )
28 27 13 mulscld 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su n ) x.s b ) e. No )
29 n0addscl 
 |-  ( ( n e. NN0_s /\ m e. NN0_s ) -> ( n +s m ) e. NN0_s )
30 29 adantl 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( n +s m ) e. NN0_s )
31 25 28 30 pw2divsdird 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) +s ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) )
32 21 31 eqtr4d 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) )
33 oveq1 
 |-  ( c = ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) -> ( c /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) )
34 33 eqeq2d 
 |-  ( c = ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) -> ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) <-> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) ) )
35 oveq2 
 |-  ( p = ( n +s m ) -> ( 2s ^su p ) = ( 2s ^su ( n +s m ) ) )
36 35 oveq2d 
 |-  ( p = ( n +s m ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) )
37 36 eqeq2d 
 |-  ( p = ( n +s m ) -> ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) <-> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) )
38 2nns 
 |-  2s e. NN_s
39 nnzs 
 |-  ( 2s e. NN_s -> 2s e. ZZ_s )
40 38 39 ax-mp 
 |-  2s e. ZZ_s
41 zexpscl 
 |-  ( ( 2s e. ZZ_s /\ m e. NN0_s ) -> ( 2s ^su m ) e. ZZ_s )
42 40 10 41 sylancr 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su m ) e. ZZ_s )
43 42 7 zmulscld 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su m ) x.s a ) e. ZZ_s )
44 zexpscl 
 |-  ( ( 2s e. ZZ_s /\ n e. NN0_s ) -> ( 2s ^su n ) e. ZZ_s )
45 40 9 44 sylancr 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su n ) e. ZZ_s )
46 45 12 zmulscld 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su n ) x.s b ) e. ZZ_s )
47 43 46 zaddscld 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) e. ZZ_s )
48 eqidd 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) )
49 34 37 47 30 48 2rspcedvdw 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> E. c e. ZZ_s E. p e. NN0_s ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) )
50 elzs12 
 |-  ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) e. ZZ_s[1/2] <-> E. c e. ZZ_s E. p e. NN0_s ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) )
51 49 50 sylibr 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) e. ZZ_s[1/2] )
52 32 51 eqeltrd 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) e. ZZ_s[1/2] )
53 oveq12 
 |-  ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) = ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) )
54 53 eleq1d 
 |-  ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( ( A +s B ) e. ZZ_s[1/2] <-> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) e. ZZ_s[1/2] ) )
55 52 54 syl5ibrcom 
 |-  ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) )
56 55 rexlimdvva 
 |-  ( ( a e. ZZ_s /\ b e. ZZ_s ) -> ( E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) )
57 56 rexlimivv 
 |-  ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] )
58 6 57 sylbir 
 |-  ( ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] )
59 1 2 58 syl2anb 
 |-  ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A +s B ) e. ZZ_s[1/2] )