Theorem nohalf

Description: An explicit expression for one half. This theorem avoids the axiom of infinity. (Contributed by Scott Fenton, 23-Jul-2025)

	Ref	Expression
Assertion	nohalf	|- ( 1s /su 2s ) = ( { 0s } |s { 1s } )

Proof

Step	Hyp	Ref	Expression
1		twocut	|- ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s
2		1sno	|- 1s e. No
3	2	a1i	|- ( T. -> 1s e. No )
4		0sno	|- 0s e. No
5	4	a1i	|- ( T. -> 0s e. No )
6		0slt1s	|- 0s
7	6	a1i	|- ( T. -> 0s
8	5 3 7	ssltsn	|- ( T. -> { 0s } <
9	8	scutcld	|- ( T. -> ( { 0s } |s { 1s } ) e. No )
10		2sno	|- 2s e. No
11	10	a1i	|- ( T. -> 2s e. No )
12		2ne0s	|- 2s =/= 0s
13	12	a1i	|- ( T. -> 2s =/= 0s )
14		oveq2	|- ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) )
15	14	eqeq1d	|- ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) )
16	1	a1i	|- ( T. -> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s )
17	15 9 16	rspcedvdw	|- ( T. -> E. x e. No ( 2s x.s x ) = 1s )
18	3 9 11 13 17	divsmulwd	|- ( T. -> ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) )
19	1 18	mpbiri	|- ( T. -> ( 1s /su 2s ) = ( { 0s } |s { 1s } ) )
20	19	mptru	|- ( 1s /su 2s ) = ( { 0s } |s { 1s } )