Theorem z12no

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

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

Proof

Step	Hyp	Ref	Expression
1		elz12s	⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑎 ∈ ℤs ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) )
2		zno	⊢ ( 𝑎 ∈ ℤs → 𝑎 ∈ No )
3	2	adantr	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → 𝑎 ∈ No )
4		simpr	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → 𝑛 ∈ ℕ0s )
5	3 4	pw2divscld	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∈ No )
6		eleq1	⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) → ( 𝐴 ∈ No ↔ ( 𝑎 /su ( 2s ↑s 𝑛 ) ) ∈ No ) )
7	5 6	syl5ibrcom	⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) → 𝐴 ∈ No ) )
8	7	rexlimivv	⊢ ( ∃ 𝑎 ∈ ℤs ∃ 𝑛 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑛 ) ) → 𝐴 ∈ No )
9	1 8	sylbi	⊢ ( 𝐴 ∈ ℤs[1/2] → 𝐴 ∈ No )