Metamath Proof Explorer

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 
|- ( N e. NN0_s -> E. x e. No ( ( 2s ^su N ) x.s x ) = 1s )

Proof

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