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

Proof

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