Metamath Proof Explorer

Theorem cutpw2

Description: A cut expression for inverses of powers of two. (Contributed by Scott Fenton, 7-Aug-2025)

Ref Expression
Assertion cutpw2 
|- ( N e. NN0_s -> ( 1s /su ( 2s ^su ( N +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su N ) ) } ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( m = 0s -> ( m +s 1s ) = ( 0s +s 1s ) )
2 1sno 
 |-  1s e. No
3 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
4 2 3 ax-mp 
 |-  ( 0s +s 1s ) = 1s
5 1 4 eqtrdi 
 |-  ( m = 0s -> ( m +s 1s ) = 1s )
6 5 oveq2d 
 |-  ( m = 0s -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su 1s ) )
7 2sno 
 |-  2s e. No
8 exps1 
 |-  ( 2s e. No -> ( 2s ^su 1s ) = 2s )
9 7 8 ax-mp 
 |-  ( 2s ^su 1s ) = 2s
10 6 9 eqtrdi 
 |-  ( m = 0s -> ( 2s ^su ( m +s 1s ) ) = 2s )
11 10 oveq2d 
 |-  ( m = 0s -> ( 1s /su ( 2s ^su ( m +s 1s ) ) ) = ( 1s /su 2s ) )
12 oveq2 
 |-  ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) )
13 exps0 
 |-  ( 2s e. No -> ( 2s ^su 0s ) = 1s )
14 7 13 ax-mp 
 |-  ( 2s ^su 0s ) = 1s
15 12 14 eqtrdi 
 |-  ( m = 0s -> ( 2s ^su m ) = 1s )
16 15 oveq2d 
 |-  ( m = 0s -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su 1s ) )
17 divs1 
 |-  ( 1s e. No -> ( 1s /su 1s ) = 1s )
18 2 17 ax-mp 
 |-  ( 1s /su 1s ) = 1s
19 16 18 eqtrdi 
 |-  ( m = 0s -> ( 1s /su ( 2s ^su m ) ) = 1s )
20 19 sneqd 
 |-  ( m = 0s -> { ( 1s /su ( 2s ^su m ) ) } = { 1s } )
21 20 oveq2d 
 |-  ( m = 0s -> ( { 0s } |s { ( 1s /su ( 2s ^su m ) ) } ) = ( { 0s } |s { 1s } ) )
22 11 21 eqeq12d 
 |-  ( m = 0s -> ( ( 1s /su ( 2s ^su ( m +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su m ) ) } ) <-> ( 1s /su 2s ) = ( { 0s } |s { 1s } ) ) )
23 oveq1 
 |-  ( m = n -> ( m +s 1s ) = ( n +s 1s ) )
24 23 oveq2d 
 |-  ( m = n -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( n +s 1s ) ) )
25 24 oveq2d 
 |-  ( m = n -> ( 1s /su ( 2s ^su ( m +s 1s ) ) ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
26 oveq2 
 |-  ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) )
27 26 oveq2d 
 |-  ( m = n -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su n ) ) )
28 27 sneqd 
 |-  ( m = n -> { ( 1s /su ( 2s ^su m ) ) } = { ( 1s /su ( 2s ^su n ) ) } )
29 28 oveq2d 
 |-  ( m = n -> ( { 0s } |s { ( 1s /su ( 2s ^su m ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) )
30 25 29 eqeq12d 
 |-  ( m = n -> ( ( 1s /su ( 2s ^su ( m +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su m ) ) } ) <-> ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) )
31 oveq1 
 |-  ( m = ( n +s 1s ) -> ( m +s 1s ) = ( ( n +s 1s ) +s 1s ) )
32 31 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( ( n +s 1s ) +s 1s ) ) )
33 32 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( 1s /su ( 2s ^su ( m +s 1s ) ) ) = ( 1s /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) )
34 oveq2 
 |-  ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) )
35 34 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
36 35 sneqd 
 |-  ( m = ( n +s 1s ) -> { ( 1s /su ( 2s ^su m ) ) } = { ( 1s /su ( 2s ^su ( n +s 1s ) ) ) } )
37 36 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( { 0s } |s { ( 1s /su ( 2s ^su m ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ^su ( n +s 1s ) ) ) } ) )
38 33 37 eqeq12d 
 |-  ( m = ( n +s 1s ) -> ( ( 1s /su ( 2s ^su ( m +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su m ) ) } ) <-> ( 1s /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
39 oveq1 
 |-  ( m = N -> ( m +s 1s ) = ( N +s 1s ) )
40 39 oveq2d 
 |-  ( m = N -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( N +s 1s ) ) )
41 40 oveq2d 
 |-  ( m = N -> ( 1s /su ( 2s ^su ( m +s 1s ) ) ) = ( 1s /su ( 2s ^su ( N +s 1s ) ) ) )
42 oveq2 
 |-  ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) )
43 42 oveq2d 
 |-  ( m = N -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su N ) ) )
44 43 sneqd 
 |-  ( m = N -> { ( 1s /su ( 2s ^su m ) ) } = { ( 1s /su ( 2s ^su N ) ) } )
45 44 oveq2d 
 |-  ( m = N -> ( { 0s } |s { ( 1s /su ( 2s ^su m ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ^su N ) ) } ) )
46 41 45 eqeq12d 
 |-  ( m = N -> ( ( 1s /su ( 2s ^su ( m +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su m ) ) } ) <-> ( 1s /su ( 2s ^su ( N +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su N ) ) } ) ) )
47 nohalf 
 |-  ( 1s /su 2s ) = ( { 0s } |s { 1s } )
48 peano2n0s 
 |-  ( n e. NN0_s -> ( n +s 1s ) e. NN0_s )
49 expsp1 
 |-  ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) )
50 7 49 mpan 
 |-  ( ( n +s 1s ) e. NN0_s -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) )
51 48 50 syl 
 |-  ( n e. NN0_s -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) )
52 51 oveq2d 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( 1s /su ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) ) )
53 2 a1i 
 |-  ( n e. NN0_s -> 1s e. No )
54 expscl 
 |-  ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. No )
55 7 54 mpan 
 |-  ( ( n +s 1s ) e. NN0_s -> ( 2s ^su ( n +s 1s ) ) e. No )
56 48 55 syl 
 |-  ( n e. NN0_s -> ( 2s ^su ( n +s 1s ) ) e. No )
57 7 a1i 
 |-  ( n e. NN0_s -> 2s e. No )
58 2ne0s 
 |-  2s =/= 0s
59 expsne0 
 |-  ( ( 2s e. No /\ 2s =/= 0s /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) =/= 0s )
60 7 58 59 mp3an12 
 |-  ( ( n +s 1s ) e. NN0_s -> ( 2s ^su ( n +s 1s ) ) =/= 0s )
61 48 60 syl 
 |-  ( n e. NN0_s -> ( 2s ^su ( n +s 1s ) ) =/= 0s )
62 58 a1i 
 |-  ( n e. NN0_s -> 2s =/= 0s )
63 53 56 57 61 62 divdivs1d 
 |-  ( n e. NN0_s -> ( ( 1s /su ( 2s ^su ( n +s 1s ) ) ) /su 2s ) = ( 1s /su ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) ) )
64 52 63 eqtr4d 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( 1s /su ( 2s ^su ( n +s 1s ) ) ) /su 2s ) )
65 53 56 61 divscld 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su ( n +s 1s ) ) ) e. No )
66 addslid 
 |-  ( ( 1s /su ( 2s ^su ( n +s 1s ) ) ) e. No -> ( 0s +s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
67 65 66 syl 
 |-  ( n e. NN0_s -> ( 0s +s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
68 67 oveq1d 
 |-  ( n e. NN0_s -> ( ( 0s +s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) /su 2s ) = ( ( 1s /su ( 2s ^su ( n +s 1s ) ) ) /su 2s ) )
69 64 68 eqtr4d 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( 0s +s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) /su 2s ) )
70 69 adantr 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( 1s /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( 0s +s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) /su 2s ) )
71 0sno 
 |-  0s e. No
72 71 a1i 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> 0s e. No )
73 2 a1i 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> 1s e. No )
74 56 adantr 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( 2s ^su ( n +s 1s ) ) e. No )
75 61 adantr 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( 2s ^su ( n +s 1s ) ) =/= 0s )
76 73 74 75 divscld 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( 1s /su ( 2s ^su ( n +s 1s ) ) ) e. No )
77 muls02 
 |-  ( ( 2s ^su ( n +s 1s ) ) e. No -> ( 0s x.s ( 2s ^su ( n +s 1s ) ) ) = 0s )
78 74 77 syl 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( 0s x.s ( 2s ^su ( n +s 1s ) ) ) = 0s )
79 0slt1s 
 |-  0s
80 78 79 eqbrtrdi 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( 0s x.s ( 2s ^su ( n +s 1s ) ) )
81 2nns 
 |-  2s e. NN_s
82 nnsgt0 
 |-  ( 2s e. NN_s -> 0s
83 81 82 ax-mp 
 |-  0s
84 expsgt0 
 |-  ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s /\ 0s  0s
85 7 83 84 mp3an13 
 |-  ( ( n +s 1s ) e. NN0_s -> 0s
86 48 85 syl 
 |-  ( n e. NN0_s -> 0s
87 86 adantr 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> 0s
88 72 73 74 87 sltmuldivd 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( ( 0s x.s ( 2s ^su ( n +s 1s ) ) )  0s
89 80 88 mpbid 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> 0s
90 muls01 
 |-  ( 2s e. No -> ( 2s x.s 0s ) = 0s )
91 7 90 ax-mp 
 |-  ( 2s x.s 0s ) = 0s
92 91 sneqi 
 |-  { ( 2s x.s 0s ) } = { 0s }
93 92 a1i 
 |-  ( n e. NN0_s -> { ( 2s x.s 0s ) } = { 0s } )
94 expsp1 
 |-  ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) )
95 7 94 mpan 
 |-  ( n e. NN0_s -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) )
96 95 oveq2d 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( 1s /su ( ( 2s ^su n ) x.s 2s ) ) )
97 expscl 
 |-  ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No )
98 7 97 mpan 
 |-  ( n e. NN0_s -> ( 2s ^su n ) e. No )
99 expsne0 
 |-  ( ( 2s e. No /\ 2s =/= 0s /\ n e. NN0_s ) -> ( 2s ^su n ) =/= 0s )
100 7 58 99 mp3an12 
 |-  ( n e. NN0_s -> ( 2s ^su n ) =/= 0s )
101 53 98 57 100 62 divdivs1d 
 |-  ( n e. NN0_s -> ( ( 1s /su ( 2s ^su n ) ) /su 2s ) = ( 1s /su ( ( 2s ^su n ) x.s 2s ) ) )
102 96 101 eqtr4d 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 1s /su ( 2s ^su n ) ) /su 2s ) )
103 102 oveq2d 
 |-  ( n e. NN0_s -> ( 2s x.s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 2s x.s ( ( 1s /su ( 2s ^su n ) ) /su 2s ) ) )
104 53 98 100 divscld 
 |-  ( n e. NN0_s -> ( 1s /su ( 2s ^su n ) ) e. No )
105 104 57 62 divscan2d 
 |-  ( n e. NN0_s -> ( 2s x.s ( ( 1s /su ( 2s ^su n ) ) /su 2s ) ) = ( 1s /su ( 2s ^su n ) ) )
106 103 105 eqtrd 
 |-  ( n e. NN0_s -> ( 2s x.s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 1s /su ( 2s ^su n ) ) )
107 106 sneqd 
 |-  ( n e. NN0_s -> { ( 2s x.s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) } = { ( 1s /su ( 2s ^su n ) ) } )
108 93 107 oveq12d 
 |-  ( n e. NN0_s -> ( { ( 2s x.s 0s ) } |s { ( 2s x.s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) )
109 eqcom 
 |-  ( ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) <-> ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
110 109 biimpi 
 |-  ( ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) -> ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
111 108 110 sylan9eq 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( { ( 2s x.s 0s ) } |s { ( 2s x.s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) } ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
112 76 66 syl 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( 0s +s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) )
113 111 112 eqtr4d 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( { ( 2s x.s 0s ) } |s { ( 2s x.s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) } ) = ( 0s +s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) )
114 eqid 
 |-  ( { 0s } |s { ( 1s /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( { 0s } |s { ( 1s /su ( 2s ^su ( n +s 1s ) ) ) } )
115 72 76 89 113 114 halfcut 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( { 0s } |s { ( 1s /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( ( 0s +s ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) /su 2s ) )
116 70 115 eqtr4d 
 |-  ( ( n e. NN0_s /\ ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) -> ( 1s /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su ( n +s 1s ) ) ) } ) )
117 116 ex 
 |-  ( n e. NN0_s -> ( ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) -> ( 1s /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
118 22 30 38 46 47 117 n0sind 
 |-  ( N e. NN0_s -> ( 1s /su ( 2s ^su ( N +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su N ) ) } ) )