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 ·s ( { 0s } |s { 1s } ) ) = 1s
2		1sno	⊢ 1s ∈ No
3	2	a1i	⊢ ( ⊤ → 1s ∈ No )
4		0sno	⊢ 0s ∈ No
5	4	a1i	⊢ ( ⊤ → 0s ∈ No )
6		0slt1s	⊢ 0s <s 1s
7	6	a1i	⊢ ( ⊤ → 0s <s 1s )
8	5 3 7	ssltsn	⊢ ( ⊤ → { 0s } <<s { 1s } )
9	8	scutcld	⊢ ( ⊤ → ( { 0s } |s { 1s } ) ∈ No )
10		2sno	⊢ 2s ∈ No
11	10	a1i	⊢ ( ⊤ → 2s ∈ No )
12		2ne0s	⊢ 2s ≠ 0s
13	12	a1i	⊢ ( ⊤ → 2s ≠ 0s )
14		oveq2	⊢ ( 𝑥 = ( { 0s } |s { 1s } ) → ( 2s ·s 𝑥 ) = ( 2s ·s ( { 0s } |s { 1s } ) ) )
15	14	eqeq1d	⊢ ( 𝑥 = ( { 0s } |s { 1s } ) → ( ( 2s ·s 𝑥 ) = 1s ↔ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s ) )
16	1	a1i	⊢ ( ⊤ → ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s )
17	15 9 16	rspcedvdw	⊢ ( ⊤ → ∃ 𝑥 ∈ No ( 2s ·s 𝑥 ) = 1s )
18	3 9 11 13 17	divsmulwd	⊢ ( ⊤ → ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) ↔ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s ) )
19	1 18	mpbiri	⊢ ( ⊤ → ( 1s /su 2s ) = ( { 0s } |s { 1s } ) )
20	19	mptru	⊢ ( 1s /su 2s ) = ( { 0s } |s { 1s } )