Theorem elzs12i

Description: Inference form of membership in the dyadic fractions. (Contributed by Scott Fenton, 21-Feb-2026)

	Ref	Expression
Assertion	elzs12i	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ∈ ℤs[1/2] )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 /su ( 2s ↑s 𝑁 ) )
2		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 /su ( 2s ↑s 𝑛 ) ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) )
3	2	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝑥 /su ( 2s ↑s 𝑛 ) ) ↔ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) ) )
4		oveq2	⊢ ( 𝑛 = 𝑁 → ( 2s ↑s 𝑛 ) = ( 2s ↑s 𝑁 ) )
5	4	oveq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐴 /su ( 2s ↑s 𝑛 ) ) = ( 𝐴 /su ( 2s ↑s 𝑁 ) ) )
6	5	eqeq2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 /su ( 2s ↑s 𝑛 ) ) ↔ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) )
7	3 6	rspc2ev	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ∧ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) → ∃ 𝑥 ∈ ℤs ∃ 𝑛 ∈ ℕ0s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝑥 /su ( 2s ↑s 𝑛 ) ) )
8	1 7	mp3an3	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ) → ∃ 𝑥 ∈ ℤs ∃ 𝑛 ∈ ℕ0s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝑥 /su ( 2s ↑s 𝑛 ) ) )
9		elzs12	⊢ ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑛 ∈ ℕ0s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝑥 /su ( 2s ↑s 𝑛 ) ) )
10	8 9	sylibr	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ∈ ℤs[1/2] )