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	Could not format assertion : No typesetting found for |- ( 1s /su 2s ) = ( { 0s } |s { 1s } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		twocut	Could not format ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s : No typesetting found for |- ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s with typecode |-
2		1sno	$$⊢1_s\in \mathrm{No}$$
3	2	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
4		0sno	$$⊢0_s\in \mathrm{No}$$
5	4	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
6		0slt1s	$$⊢0_s{<}_s{1}_s$$
7	6	a1i	$$⊢\top \to 0_s{<}_s{1}_s$$
8	5 3 7	ssltsn	$$⊢\top \to \left\{0_s\right\}{\ll }_s\left\{1_s\right\}$$
9	8	scutcld	$$⊢\top \to \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
10		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
11	10	a1i	Could not format ( T. -> 2s e. No ) : No typesetting found for |- ( T. -> 2s e. No ) with typecode |-
12		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
13	12	a1i	Could not format ( T. -> 2s =/= 0s ) : No typesetting found for |- ( T. -> 2s =/= 0s ) with typecode |-
14		oveq2	Could not format ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) ) : No typesetting found for |- ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) ) with typecode |-
15	14	eqeq1d	Could not format ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) : No typesetting found for |- ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) with typecode |-
16	1	a1i	Could not format ( T. -> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) : No typesetting found for |- ( T. -> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) with typecode |-
17	15 9 16	rspcedvdw	Could not format ( T. -> E. x e. No ( 2s x.s x ) = 1s ) : No typesetting found for |- ( T. -> E. x e. No ( 2s x.s x ) = 1s ) with typecode |-
18	3 9 11 13 17	divsmulwd	Could not format ( T. -> ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) : No typesetting found for |- ( T. -> ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) with typecode |-
19	1 18	mpbiri	Could not format ( T. -> ( 1s /su 2s ) = ( { 0s } |s { 1s } ) ) : No typesetting found for |- ( T. -> ( 1s /su 2s ) = ( { 0s } |s { 1s } ) ) with typecode |-
20	19	mptru	Could not format ( 1s /su 2s ) = ( { 0s } |s { 1s } ) : No typesetting found for |- ( 1s /su 2s ) = ( { 0s } |s { 1s } ) with typecode |-