Theorem zzs12

Description: A surreal integer is a dyadic fraction. (Contributed by Scott Fenton, 7-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		2sno	⊢ 2s ∈ No
2		exps0	⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
3	1 2	ax-mp	⊢ ( 2s ↑s 0s ) = 1s
4	3	oveq2i	⊢ ( 𝐴 /su ( 2s ↑s 0s ) ) = ( 𝐴 /su 1s )
5		zno	⊢ ( 𝐴 ∈ ℤs → 𝐴 ∈ No )
6		divs1	⊢ ( 𝐴 ∈ No → ( 𝐴 /su 1s ) = 𝐴 )
7	5 6	syl	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 /su 1s ) = 𝐴 )
8	4 7	eqtr2id	⊢ ( 𝐴 ∈ ℤs → 𝐴 = ( 𝐴 /su ( 2s ↑s 0s ) ) )
9		0n0s	⊢ 0s ∈ ℕ0s
10		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 /su ( 2s ↑s 𝑦 ) ) = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) )
11	10	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ↔ 𝐴 = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) ) )
12		oveq2	⊢ ( 𝑦 = 0s → ( 2s ↑s 𝑦 ) = ( 2s ↑s 0s ) )
13	12	oveq2d	⊢ ( 𝑦 = 0s → ( 𝐴 /su ( 2s ↑s 𝑦 ) ) = ( 𝐴 /su ( 2s ↑s 0s ) ) )
14	13	eqeq2d	⊢ ( 𝑦 = 0s → ( 𝐴 = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) ↔ 𝐴 = ( 𝐴 /su ( 2s ↑s 0s ) ) ) )
15	11 14	rspc2ev	⊢ ( ( 𝐴 ∈ ℤs ∧ 0s ∈ ℕ0s ∧ 𝐴 = ( 𝐴 /su ( 2s ↑s 0s ) ) ) → ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
16	9 15	mp3an2	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝐴 = ( 𝐴 /su ( 2s ↑s 0s ) ) ) → ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
17	8 16	mpdan	⊢ ( 𝐴 ∈ ℤs → ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
18		elzs12	⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
19	17 18	sylibr	⊢ ( 𝐴 ∈ ℤs → 𝐴 ∈ ℤs[1/2] )