Theorem zz12s

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

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

Proof

Step	Hyp	Ref	Expression
1		2no	⊢ 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	5	divs1d	⊢ ( 𝐴 ∈ ℤs → ( 𝐴 /su 1s ) = 𝐴 )
7	4 6	eqtr2id	⊢ ( 𝐴 ∈ ℤs → 𝐴 = ( 𝐴 /su ( 2s ↑s 0s ) ) )
8		0n0s	⊢ 0s ∈ ℕ0s
9		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 /su ( 2s ↑s 𝑦 ) ) = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) )
10	9	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ↔ 𝐴 = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) ) )
11		oveq2	⊢ ( 𝑦 = 0s → ( 2s ↑s 𝑦 ) = ( 2s ↑s 0s ) )
12	11	oveq2d	⊢ ( 𝑦 = 0s → ( 𝐴 /su ( 2s ↑s 𝑦 ) ) = ( 𝐴 /su ( 2s ↑s 0s ) ) )
13	12	eqeq2d	⊢ ( 𝑦 = 0s → ( 𝐴 = ( 𝐴 /su ( 2s ↑s 𝑦 ) ) ↔ 𝐴 = ( 𝐴 /su ( 2s ↑s 0s ) ) ) )
14	10 13	rspc2ev	⊢ ( ( 𝐴 ∈ ℤs ∧ 0s ∈ ℕ0s ∧ 𝐴 = ( 𝐴 /su ( 2s ↑s 0s ) ) ) → ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
15	8 14	mp3an2	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝐴 = ( 𝐴 /su ( 2s ↑s 0s ) ) ) → ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
16	7 15	mpdan	⊢ ( 𝐴 ∈ ℤs → ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
17		elz12s	⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
18	16 17	sylibr	⊢ ( 𝐴 ∈ ℤs → 𝐴 ∈ ℤs[1/2] )