Theorem zs12half

Description: Half of a dyadic is a dyadic. (Contributed by Scott Fenton, 11-Dec-2025)

	Ref	Expression
Assertion	zs12half	⊢ ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 /su 2s ) ∈ ℤs[1/2] )

Proof

Step	Hyp	Ref	Expression
1		elzs12	⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑎 ∈ ℤs ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) )
2		2sno	⊢ 2s ∈ No
3		exps1	⊢ ( 2s ∈ No → ( 2s ↑s 1s ) = 2s )
4	2 3	ax-mp	⊢ ( 2s ↑s 1s ) = 2s
5	4	oveq2i	⊢ ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) /su ( 2s ↑s 1s ) ) = ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) /su 2s )
6		zno	⊢ ( 𝑎 ∈ ℤs → 𝑎 ∈ No )
7	6	adantr	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → 𝑎 ∈ No )
8		simpr	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → 𝑛 ∈ ℕ0s )
9		1n0s	⊢ 1s ∈ ℕ0s
10	9	a1i	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → 1s ∈ ℕ0s )
11	7 8 10	pw2divscan4d	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝑎 /su ( 2s ↑s 𝑛 ) ) = ( ( ( 2s ↑s 1s ) ·s 𝑎 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
12	4 2	eqeltri	⊢ ( 2s ↑s 1s ) ∈ No
13	12	a1i	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 1s ) ∈ No )
14		peano2n0s	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) ∈ ℕ0s )
15	14	adantl	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝑛 +s 1s ) ∈ ℕ0s )
16	13 7 15	pw2divsassd	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( ( ( 2s ↑s 1s ) ·s 𝑎 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ↑s 1s ) ·s ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
17	11 16	eqtr2d	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( ( 2s ↑s 1s ) ·s ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) )
18	7 8	pw2divscld	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∈ No )
19	7 15	pw2divscld	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ No )
20	18 19 10	pw2divsmuld	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) /su ( 2s ↑s 1s ) ) = ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ↔ ( ( 2s ↑s 1s ) ·s ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ) )
21	17 20	mpbird	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) /su ( 2s ↑s 1s ) ) = ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
22	5 21	eqtr3id	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) /su 2s ) = ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
23		oveq1	⊢ ( 𝑏 = 𝑎 → ( 𝑏 /su ( 2s ↑s 𝑚 ) ) = ( 𝑎 /su ( 2s ↑s 𝑚 ) ) )
24	23	eqeq2d	⊢ ( 𝑏 = 𝑎 → ( ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) ↔ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑎 /su ( 2s ↑s 𝑚 ) ) ) )
25		oveq2	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 2s ↑s 𝑚 ) = ( 2s ↑s ( 𝑛 +s 1s ) ) )
26	25	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑎 /su ( 2s ↑s 𝑚 ) ) = ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
27	26	eqeq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑎 /su ( 2s ↑s 𝑚 ) ) ↔ ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
28		simpl	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → 𝑎 ∈ ℤs )
29		eqidd	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
30	24 27 28 15 29	2rspcedvdw	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ∃ 𝑏 ∈ ℤs ∃ 𝑚 ∈ ℕ0s ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) )
31		elzs12	⊢ ( ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ ℤs[1/2] ↔ ∃ 𝑏 ∈ ℤs ∃ 𝑚 ∈ ℕ0s ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑏 /su ( 2s ↑s 𝑚 ) ) )
32	30 31	sylibr	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝑎 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ∈ ℤs[1/2] )
33	22 32	eqeltrd	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) /su 2s ) ∈ ℤs[1/2] )
34		oveq1	⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) → ( 𝐴 /su 2s ) = ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) /su 2s ) )
35	34	eleq1d	⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) → ( ( 𝐴 /su 2s ) ∈ ℤs[1/2] ↔ ( ( 𝑎 /su ( 2s ↑s 𝑛 ) ) /su 2s ) ∈ ℤs[1/2] ) )
36	33 35	syl5ibrcom	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) → ( 𝐴 /su 2s ) ∈ ℤs[1/2] ) )
37	36	rexlimivv	⊢ ( ∃ 𝑎 ∈ ℤs ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) → ( 𝐴 /su 2s ) ∈ ℤs[1/2] )
38	1 37	sylbi	⊢ ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 /su 2s ) ∈ ℤs[1/2] )