Theorem pw2recs

Description: Any power of two has a multiplicative inverse. Note that this theorem does not require the axiom of infinity. (Contributed by Scott Fenton, 5-Sep-2025)

	Ref	Expression
Assertion	pw2recs	Could not format assertion : No typesetting found for |- ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq2	Could not format ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) ) : No typesetting found for |- ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) ) with typecode |-
2		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
3		exps0	Could not format ( 2s e. No -> ( 2s ^su 0s ) = 1s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) with typecode |-
4	2 3	ax-mp	Could not format ( 2s ^su 0s ) = 1s : No typesetting found for |- ( 2s ^su 0s ) = 1s with typecode |-
5	1 4	eqtrdi	Could not format ( m = 0s -> ( 2s ^su m ) = 1s ) : No typesetting found for |- ( m = 0s -> ( 2s ^su m ) = 1s ) with typecode |-
6	5	oveq1d	Could not format ( m = 0s -> ( ( 2s ^su m ) x.s x ) = ( 1s x.s x ) ) : No typesetting found for |- ( m = 0s -> ( ( 2s ^su m ) x.s x ) = ( 1s x.s x ) ) with typecode |-
7	6	eqeq1d	Could not format ( m = 0s -> ( ( ( 2s ^su m ) x.s x ) = 1s <-> ( 1s x.s x ) = 1s ) ) : No typesetting found for |- ( m = 0s -> ( ( ( 2s ^su m ) x.s x ) = 1s <-> ( 1s x.s x ) = 1s ) ) with typecode |-
8	7	rexbidv	Could not format ( m = 0s -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. x e. No ( 1s x.s x ) = 1s ) ) : No typesetting found for |- ( m = 0s -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. x e. No ( 1s x.s x ) = 1s ) ) with typecode |-
9		oveq2	Could not format ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) ) : No typesetting found for |- ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) ) with typecode |-
10	9	oveq1d	Could not format ( m = n -> ( ( 2s ^su m ) x.s x ) = ( ( 2s ^su n ) x.s x ) ) : No typesetting found for |- ( m = n -> ( ( 2s ^su m ) x.s x ) = ( ( 2s ^su n ) x.s x ) ) with typecode |-
11	10	eqeq1d	Could not format ( m = n -> ( ( ( 2s ^su m ) x.s x ) = 1s <-> ( ( 2s ^su n ) x.s x ) = 1s ) ) : No typesetting found for |- ( m = n -> ( ( ( 2s ^su m ) x.s x ) = 1s <-> ( ( 2s ^su n ) x.s x ) = 1s ) ) with typecode |-
12	11	rexbidv	Could not format ( m = n -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. x e. No ( ( 2s ^su n ) x.s x ) = 1s ) ) : No typesetting found for |- ( m = n -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. x e. No ( ( 2s ^su n ) x.s x ) = 1s ) ) with typecode |-
13		oveq2	Could not format ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) ) with typecode |-
14	13	oveq1d	Could not format ( m = ( n +s 1s ) -> ( ( 2s ^su m ) x.s x ) = ( ( 2s ^su ( n +s 1s ) ) x.s x ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( 2s ^su m ) x.s x ) = ( ( 2s ^su ( n +s 1s ) ) x.s x ) ) with typecode |-
15	14	eqeq1d	Could not format ( m = ( n +s 1s ) -> ( ( ( 2s ^su m ) x.s x ) = 1s <-> ( ( 2s ^su ( n +s 1s ) ) x.s x ) = 1s ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( ( 2s ^su m ) x.s x ) = 1s <-> ( ( 2s ^su ( n +s 1s ) ) x.s x ) = 1s ) ) with typecode |-
16	15	rexbidv	Could not format ( m = ( n +s 1s ) -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. x e. No ( ( 2s ^su ( n +s 1s ) ) x.s x ) = 1s ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. x e. No ( ( 2s ^su ( n +s 1s ) ) x.s x ) = 1s ) ) with typecode |-
17		oveq2	Could not format ( x = y -> ( ( 2s ^su ( n +s 1s ) ) x.s x ) = ( ( 2s ^su ( n +s 1s ) ) x.s y ) ) : No typesetting found for |- ( x = y -> ( ( 2s ^su ( n +s 1s ) ) x.s x ) = ( ( 2s ^su ( n +s 1s ) ) x.s y ) ) with typecode |-
18	17	eqeq1d	Could not format ( x = y -> ( ( ( 2s ^su ( n +s 1s ) ) x.s x ) = 1s <-> ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) ) : No typesetting found for |- ( x = y -> ( ( ( 2s ^su ( n +s 1s ) ) x.s x ) = 1s <-> ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) ) with typecode |-
19	18	cbvrexvw	Could not format ( E. x e. No ( ( 2s ^su ( n +s 1s ) ) x.s x ) = 1s <-> E. y e. No ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) : No typesetting found for |- ( E. x e. No ( ( 2s ^su ( n +s 1s ) ) x.s x ) = 1s <-> E. y e. No ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) with typecode |-
20	16 19	bitrdi	Could not format ( m = ( n +s 1s ) -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. y e. No ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. y e. No ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) ) with typecode |-
21		oveq2	Could not format ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) ) : No typesetting found for |- ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) ) with typecode |-
22	21	oveq1d	Could not format ( m = N -> ( ( 2s ^su m ) x.s x ) = ( ( 2s ^su N ) x.s x ) ) : No typesetting found for |- ( m = N -> ( ( 2s ^su m ) x.s x ) = ( ( 2s ^su N ) x.s x ) ) with typecode |-
23	22	eqeq1d	Could not format ( m = N -> ( ( ( 2s ^su m ) x.s x ) = 1s <-> ( ( 2s ^su N ) x.s x ) = 1s ) ) : No typesetting found for |- ( m = N -> ( ( ( 2s ^su m ) x.s x ) = 1s <-> ( ( 2s ^su N ) x.s x ) = 1s ) ) with typecode |-
24	23	rexbidv	Could not format ( m = N -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) ) : No typesetting found for |- ( m = N -> ( E. x e. No ( ( 2s ^su m ) x.s x ) = 1s <-> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) ) with typecode |-
25		1sno	$$⊢1_s\in \mathrm{No}$$
26		mulsrid	$$⊢1_s\in \mathrm{No}\to 1_s{\cdot }_s{1}_s=1_s$$
27	25 26	ax-mp	$$⊢1_s{\cdot }_s{1}_s=1_s$$
28		oveq2	$$⊢x=1_s\to 1_s{\cdot }_{s}x=1_s{\cdot }_s{1}_s$$
29	28	eqeq1d	$$⊢x=1_s\to \left(1_s{\cdot }_{s}x=1_s\leftrightarrow 1_s{\cdot }_s{1}_s=1_s\right)$$
30	29	rspcev	$$⊢\left(1_s\in \mathrm{No}\wedge 1_s{\cdot }_s{1}_s=1_s\right)\to \exists x\in \mathrm{No}{1}_s{\cdot }_{s}x=1_s$$
31	25 27 30	mp2an	$$⊢\exists x\in \mathrm{No}{1}_s{\cdot }_{s}x=1_s$$
32		oveq2	Could not format ( y = ( x x.s ( { 0s } |s { 1s } ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s y ) = ( ( 2s ^su ( n +s 1s ) ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) ) : No typesetting found for |- ( y = ( x x.s ( { 0s } |s { 1s } ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s y ) = ( ( 2s ^su ( n +s 1s ) ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) ) with typecode |-
33	32	eqeq1d	Could not format ( y = ( x x.s ( { 0s } |s { 1s } ) ) -> ( ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s <-> ( ( 2s ^su ( n +s 1s ) ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) = 1s ) ) : No typesetting found for |- ( y = ( x x.s ( { 0s } |s { 1s } ) ) -> ( ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s <-> ( ( 2s ^su ( n +s 1s ) ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) = 1s ) ) with typecode |-
34		simprl	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> x e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> x e. No ) with typecode |-
35		0sno	$$⊢0_s\in \mathrm{No}$$
36	35	a1i	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> 0s e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> 0s e. No ) with typecode |-
37	25	a1i	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> 1s e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> 1s e. No ) with typecode |-
38		0slt1s	$$⊢0_s{<}_s{1}_s$$
39	38	a1i	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> 0s 0s
40	36 37 39	ssltsn	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> { 0s } < { 0s } <
41	40	scutcld	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( { 0s } |s { 1s } ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( { 0s } |s { 1s } ) e. No ) with typecode |-
42	34 41	mulscld	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( x x.s ( { 0s } |s { 1s } ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( x x.s ( { 0s } |s { 1s } ) ) e. No ) with typecode |-
43		expsp1	Could not format ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) : No typesetting found for |- ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) with typecode |-
44	2 43	mpan	Could not format ( n e. NN0_s -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) : No typesetting found for |- ( n e. NN0_s -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) with typecode |-
45	44	adantr	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) with typecode |-
46	45	oveq1d	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) = ( ( ( 2s ^su n ) x.s 2s ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) = ( ( ( 2s ^su n ) x.s 2s ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) ) with typecode |-
47		expscl	Could not format ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No ) with typecode |-
48	2 47	mpan	Could not format ( n e. NN0_s -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( n e. NN0_s -> ( 2s ^su n ) e. No ) with typecode |-
49	48	adantr	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( 2s ^su n ) e. No ) with typecode |-
50	2	a1i	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> 2s e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> 2s e. No ) with typecode |-
51	49 50 34 41	muls4d	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( ( 2s ^su n ) x.s 2s ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) = ( ( ( 2s ^su n ) x.s x ) x.s ( 2s x.s ( { 0s } |s { 1s } ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( ( 2s ^su n ) x.s 2s ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) = ( ( ( 2s ^su n ) x.s x ) x.s ( 2s x.s ( { 0s } |s { 1s } ) ) ) ) with typecode |-
52		simprr	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( 2s ^su n ) x.s x ) = 1s ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( 2s ^su n ) x.s x ) = 1s ) with typecode |-
53		twocut	Could not format ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s : No typesetting found for |- ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s with typecode |-
54	53	a1i	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) with typecode |-
55	52 54	oveq12d	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( ( 2s ^su n ) x.s x ) x.s ( 2s x.s ( { 0s } |s { 1s } ) ) ) = ( 1s x.s 1s ) ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( ( 2s ^su n ) x.s x ) x.s ( 2s x.s ( { 0s } |s { 1s } ) ) ) = ( 1s x.s 1s ) ) with typecode |-
56	55 27	eqtrdi	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( ( 2s ^su n ) x.s x ) x.s ( 2s x.s ( { 0s } |s { 1s } ) ) ) = 1s ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( ( 2s ^su n ) x.s x ) x.s ( 2s x.s ( { 0s } |s { 1s } ) ) ) = 1s ) with typecode |-
57	46 51 56	3eqtrd	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) = 1s ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s ( x x.s ( { 0s } |s { 1s } ) ) ) = 1s ) with typecode |-
58	33 42 57	rspcedvdw	Could not format ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> E. y e. No ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) : No typesetting found for |- ( ( n e. NN0_s /\ ( x e. No /\ ( ( 2s ^su n ) x.s x ) = 1s ) ) -> E. y e. No ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) with typecode |-
59	58	rexlimdvaa	Could not format ( n e. NN0_s -> ( E. x e. No ( ( 2s ^su n ) x.s x ) = 1s -> E. y e. No ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) ) : No typesetting found for |- ( n e. NN0_s -> ( E. x e. No ( ( 2s ^su n ) x.s x ) = 1s -> E. y e. No ( ( 2s ^su ( n +s 1s ) ) x.s y ) = 1s ) ) with typecode |-
60	8 12 20 24 31 59	n0sind	Could not format ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) : No typesetting found for |- ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s ) with typecode |-