Theorem pw2cut

Description: Extend halfcut to arbitrary powers of two. Part of theorem 4.2 of Gonshor p. 28. (Contributed by Scott Fenton, 18-Aug-2025)

	Ref	Expression
Hypotheses	pw2cut.1	$$⊢\phi \to A\in \mathrm{No}$$
	pw2cut.2	$$⊢\phi \to B\in \mathrm{No}$$
	pw2cut.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
	pw2cut.4	$$⊢\phi \to A{<}_{s}B$$
	pw2cut.5	No typesetting found for |- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) ) with typecode |-
Assertion	pw2cut	Could not format assertion : No typesetting found for |- ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		pw2cut.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2cut.2	$$⊢\phi \to B\in \mathrm{No}$$
3		pw2cut.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
4		pw2cut.4	$$⊢\phi \to A{<}_{s}B$$
5		pw2cut.5	Could not format ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) ) : No typesetting found for |- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) ) with typecode |-
6		oveq2	Could not format ( x = 0s -> ( 2s ^su x ) = ( 2s ^su 0s ) ) : No typesetting found for |- ( x = 0s -> ( 2s ^su x ) = ( 2s ^su 0s ) ) with typecode |-
7		2no	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
8		exps0	Could not format ( 2s e. No -> ( 2s ^su 0s ) = 1s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) with typecode |-
9	7 8	ax-mp	Could not format ( 2s ^su 0s ) = 1s : No typesetting found for |- ( 2s ^su 0s ) = 1s with typecode |-
10	6 9	eqtrdi	Could not format ( x = 0s -> ( 2s ^su x ) = 1s ) : No typesetting found for |- ( x = 0s -> ( 2s ^su x ) = 1s ) with typecode |-
11	10	oveq2d	Could not format ( x = 0s -> ( A /su ( 2s ^su x ) ) = ( A /su 1s ) ) : No typesetting found for |- ( x = 0s -> ( A /su ( 2s ^su x ) ) = ( A /su 1s ) ) with typecode |-
12	11	sneqd	Could not format ( x = 0s -> { ( A /su ( 2s ^su x ) ) } = { ( A /su 1s ) } ) : No typesetting found for |- ( x = 0s -> { ( A /su ( 2s ^su x ) ) } = { ( A /su 1s ) } ) with typecode |-
13	10	oveq2d	Could not format ( x = 0s -> ( B /su ( 2s ^su x ) ) = ( B /su 1s ) ) : No typesetting found for |- ( x = 0s -> ( B /su ( 2s ^su x ) ) = ( B /su 1s ) ) with typecode |-
14	13	sneqd	Could not format ( x = 0s -> { ( B /su ( 2s ^su x ) ) } = { ( B /su 1s ) } ) : No typesetting found for |- ( x = 0s -> { ( B /su ( 2s ^su x ) ) } = { ( B /su 1s ) } ) with typecode |-
15	12 14	oveq12d	Could not format ( x = 0s -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) ) : No typesetting found for |- ( x = 0s -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) ) with typecode |-
16		oveq1	$$⊢x=0_s\to x{+}_s{1}_s=0_s{+}_s{1}_s$$
17		1no	$$⊢1_s\in \mathrm{No}$$
18		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
19	17 18	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
20	16 19	eqtrdi	$$⊢x=0_s\to x{+}_s{1}_s=1_s$$
21	20	oveq2d	Could not format ( x = 0s -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su 1s ) ) : No typesetting found for |- ( x = 0s -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su 1s ) ) with typecode |-
22		exps1	Could not format ( 2s e. No -> ( 2s ^su 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 1s ) = 2s ) with typecode |-
23	7 22	ax-mp	Could not format ( 2s ^su 1s ) = 2s : No typesetting found for |- ( 2s ^su 1s ) = 2s with typecode |-
24	21 23	eqtrdi	Could not format ( x = 0s -> ( 2s ^su ( x +s 1s ) ) = 2s ) : No typesetting found for |- ( x = 0s -> ( 2s ^su ( x +s 1s ) ) = 2s ) with typecode |-
25	24	oveq2d	Could not format ( x = 0s -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su 2s ) ) : No typesetting found for |- ( x = 0s -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su 2s ) ) with typecode |-
26	15 25	eqeq12d	Could not format ( x = 0s -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) ) ) : No typesetting found for |- ( x = 0s -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) ) ) with typecode |-
27	26	imbi2d	Could not format ( x = 0s -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) ) ) ) : No typesetting found for |- ( x = 0s -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) ) ) ) with typecode |-
28		oveq2	Could not format ( x = y -> ( 2s ^su x ) = ( 2s ^su y ) ) : No typesetting found for |- ( x = y -> ( 2s ^su x ) = ( 2s ^su y ) ) with typecode |-
29	28	oveq2d	Could not format ( x = y -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su y ) ) ) : No typesetting found for |- ( x = y -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su y ) ) ) with typecode |-
30	29	sneqd	Could not format ( x = y -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su y ) ) } ) : No typesetting found for |- ( x = y -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su y ) ) } ) with typecode |-
31	28	oveq2d	Could not format ( x = y -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su y ) ) ) : No typesetting found for |- ( x = y -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su y ) ) ) with typecode |-
32	31	sneqd	Could not format ( x = y -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su y ) ) } ) : No typesetting found for |- ( x = y -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su y ) ) } ) with typecode |-
33	30 32	oveq12d	Could not format ( x = y -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) ) : No typesetting found for |- ( x = y -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) ) with typecode |-
34		oveq1	$$⊢x=y\to x{+}_s{1}_s=y{+}_s{1}_s$$
35	34	oveq2d	Could not format ( x = y -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( y +s 1s ) ) ) : No typesetting found for |- ( x = y -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( y +s 1s ) ) ) with typecode |-
36	35	oveq2d	Could not format ( x = y -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) : No typesetting found for |- ( x = y -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) with typecode |-
37	33 36	eqeq12d	Could not format ( x = y -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) ) : No typesetting found for |- ( x = y -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) ) with typecode |-
38	37	imbi2d	Could not format ( x = y -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) ) ) : No typesetting found for |- ( x = y -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) ) ) with typecode |-
39		oveq2	Could not format ( x = ( y +s 1s ) -> ( 2s ^su x ) = ( 2s ^su ( y +s 1s ) ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( 2s ^su x ) = ( 2s ^su ( y +s 1s ) ) ) with typecode |-
40	39	oveq2d	Could not format ( x = ( y +s 1s ) -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su ( y +s 1s ) ) ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su ( y +s 1s ) ) ) ) with typecode |-
41	40	sneqd	Could not format ( x = ( y +s 1s ) -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su ( y +s 1s ) ) ) } ) : No typesetting found for |- ( x = ( y +s 1s ) -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su ( y +s 1s ) ) ) } ) with typecode |-
42	39	oveq2d	Could not format ( x = ( y +s 1s ) -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su ( y +s 1s ) ) ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su ( y +s 1s ) ) ) ) with typecode |-
43	42	sneqd	Could not format ( x = ( y +s 1s ) -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) : No typesetting found for |- ( x = ( y +s 1s ) -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) with typecode |-
44	41 43	oveq12d	Could not format ( x = ( y +s 1s ) -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) ) with typecode |-
45		oveq1	$$⊢x=y{+}_s{1}_s\to x{+}_s{1}_s=\left(y{+}_s{1}_s\right){+}_s{1}_s$$
46	45	oveq2d	Could not format ( x = ( y +s 1s ) -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) with typecode |-
47	46	oveq2d	Could not format ( x = ( y +s 1s ) -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) with typecode |-
48	44 47	eqeq12d	Could not format ( x = ( y +s 1s ) -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) with typecode |-
49	48	imbi2d	Could not format ( x = ( y +s 1s ) -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) ) with typecode |-
50		oveq2	Could not format ( x = N -> ( 2s ^su x ) = ( 2s ^su N ) ) : No typesetting found for |- ( x = N -> ( 2s ^su x ) = ( 2s ^su N ) ) with typecode |-
51	50	oveq2d	Could not format ( x = N -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su N ) ) ) : No typesetting found for |- ( x = N -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su N ) ) ) with typecode |-
52	51	sneqd	Could not format ( x = N -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su N ) ) } ) : No typesetting found for |- ( x = N -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su N ) ) } ) with typecode |-
53	50	oveq2d	Could not format ( x = N -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su N ) ) ) : No typesetting found for |- ( x = N -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su N ) ) ) with typecode |-
54	53	sneqd	Could not format ( x = N -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su N ) ) } ) : No typesetting found for |- ( x = N -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su N ) ) } ) with typecode |-
55	52 54	oveq12d	Could not format ( x = N -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) ) : No typesetting found for |- ( x = N -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) ) with typecode |-
56		oveq1	$$⊢x=N\to x{+}_s{1}_s=N{+}_s{1}_s$$
57	56	oveq2d	Could not format ( x = N -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( N +s 1s ) ) ) : No typesetting found for |- ( x = N -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( N +s 1s ) ) ) with typecode |-
58	57	oveq2d	Could not format ( x = N -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) : No typesetting found for |- ( x = N -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) with typecode |-
59	55 58	eqeq12d	Could not format ( x = N -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( x = N -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) ) with typecode |-
60	59	imbi2d	Could not format ( x = N -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) ) ) : No typesetting found for |- ( x = N -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) ) ) with typecode |-
61	1	divs1d	$$⊢\phi \to A{/}_{\mathrm{su}}{1}_s=A$$
62	61	sneqd	$$⊢\phi \to \left\{A{/}_{\mathrm{su}}{1}_s\right\}=\left\{A\right\}$$
63	2	divs1d	$$⊢\phi \to B{/}_{\mathrm{su}}{1}_s=B$$
64	63	sneqd	$$⊢\phi \to \left\{B{/}_{\mathrm{su}}{1}_s\right\}=\left\{B\right\}$$
65	62 64	oveq12d	$$⊢\phi \to \left\{A{/}_{\mathrm{su}}{1}_s\right\}{|}_s\left\{B{/}_{\mathrm{su}}{1}_s\right\}=\left\{A\right\}{|}_s\left\{B\right\}$$
66		eqid	$$⊢\left\{A\right\}{|}_s\left\{B\right\}=\left\{A\right\}{|}_s\left\{B\right\}$$
67	1 2 4 5 66	halfcut	Could not format ( ph -> ( { A } |s { B } ) = ( ( A +s B ) /su 2s ) ) : No typesetting found for |- ( ph -> ( { A } |s { B } ) = ( ( A +s B ) /su 2s ) ) with typecode |-
68	65 67	eqtrd	Could not format ( ph -> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) ) : No typesetting found for |- ( ph -> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) ) with typecode |-
69	1	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge \phi \right)\to A\in \mathrm{No}$$
70		peano2n0s	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
71		expscl	Could not format ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) e. No ) with typecode |-
72	7 70 71	sylancr	Could not format ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) e. No ) : No typesetting found for |- ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) e. No ) with typecode |-
73	72	adantr	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) e. No ) with typecode |-
74		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
75		expsne0	Could not format ( ( 2s e. No /\ 2s =/= 0s /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) =/= 0s ) : No typesetting found for |- ( ( 2s e. No /\ 2s =/= 0s /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) =/= 0s ) with typecode |-
76	7 74 75	mp3an12	Could not format ( ( y +s 1s ) e. NN0_s -> ( 2s ^su ( y +s 1s ) ) =/= 0s ) : No typesetting found for |- ( ( y +s 1s ) e. NN0_s -> ( 2s ^su ( y +s 1s ) ) =/= 0s ) with typecode |-
77	70 76	syl	Could not format ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) =/= 0s ) : No typesetting found for |- ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) =/= 0s ) with typecode |-
78	77	adantr	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) =/= 0s ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) =/= 0s ) with typecode |-
79	69 73 78	divscld	Could not format ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) e. No ) with typecode |-
80	79	3adant3	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) e. No ) with typecode |-
81	2	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge \phi \right)\to B\in \mathrm{No}$$
82	81 73 78	divscld	Could not format ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) e. No ) with typecode |-
83	82	3adant3	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) e. No ) with typecode |-
84	69 73 78	divscan1d	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) ) = A ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) ) = A ) with typecode |-
85	4	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge \phi \right)\to A{<}_{s}B$$
86	84 85	eqbrtrd	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) ) ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) )
87		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
88		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
89	87 88	ax-mp	Could not format 0s
90		expsgt0	Could not format ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s /\ 0s 0s 0s
91	7 89 90	mp3an13	Could not format ( ( y +s 1s ) e. NN0_s -> 0s 0s
92	70 91	syl	Could not format ( y e. NN0_s -> 0s 0s
93	92	adantr	Could not format ( ( y e. NN0_s /\ ph ) -> 0s 0s
94	79 81 73 93	ltmuldivsd	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) ) ( A /su ( 2s ^su ( y +s 1s ) ) ) ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) ) ( A /su ( 2s ^su ( y +s 1s ) ) )
95	86 94	mpbid	Could not format ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) ( A /su ( 2s ^su ( y +s 1s ) ) )
96	95	3adant3	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) ( A /su ( 2s ^su ( y +s 1s ) ) )
97		expsp1	Could not format ( ( 2s e. No /\ y e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) ) : No typesetting found for |- ( ( 2s e. No /\ y e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) ) with typecode |-
98	7 97	mpan	Could not format ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) ) : No typesetting found for |- ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) ) with typecode |-
99	98	adantr	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) ) with typecode |-
100	99	oveq2d	Could not format ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) = ( A /su ( ( 2s ^su y ) x.s 2s ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) = ( A /su ( ( 2s ^su y ) x.s 2s ) ) ) with typecode |-
101		expscl	Could not format ( ( 2s e. No /\ y e. NN0_s ) -> ( 2s ^su y ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ y e. NN0_s ) -> ( 2s ^su y ) e. No ) with typecode |-
102	7 101	mpan	Could not format ( y e. NN0_s -> ( 2s ^su y ) e. No ) : No typesetting found for |- ( y e. NN0_s -> ( 2s ^su y ) e. No ) with typecode |-
103	102	adantr	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s ^su y ) e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s ^su y ) e. No ) with typecode |-
104	7	a1i	Could not format ( ( y e. NN0_s /\ ph ) -> 2s e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> 2s e. No ) with typecode |-
105		expsne0	Could not format ( ( 2s e. No /\ 2s =/= 0s /\ y e. NN0_s ) -> ( 2s ^su y ) =/= 0s ) : No typesetting found for |- ( ( 2s e. No /\ 2s =/= 0s /\ y e. NN0_s ) -> ( 2s ^su y ) =/= 0s ) with typecode |-
106	7 74 105	mp3an12	Could not format ( y e. NN0_s -> ( 2s ^su y ) =/= 0s ) : No typesetting found for |- ( y e. NN0_s -> ( 2s ^su y ) =/= 0s ) with typecode |-
107	106	adantr	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s ^su y ) =/= 0s ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s ^su y ) =/= 0s ) with typecode |-
108	74	a1i	Could not format ( ( y e. NN0_s /\ ph ) -> 2s =/= 0s ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> 2s =/= 0s ) with typecode |-
109	69 103 104 107 108	divdivs1d	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( A /su ( 2s ^su y ) ) /su 2s ) = ( A /su ( ( 2s ^su y ) x.s 2s ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( A /su ( 2s ^su y ) ) /su 2s ) = ( A /su ( ( 2s ^su y ) x.s 2s ) ) ) with typecode |-
110	100 109	eqtr4d	Could not format ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) = ( ( A /su ( 2s ^su y ) ) /su 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) = ( ( A /su ( 2s ^su y ) ) /su 2s ) ) with typecode |-
111	110	oveq2d	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) = ( 2s x.s ( ( A /su ( 2s ^su y ) ) /su 2s ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) = ( 2s x.s ( ( A /su ( 2s ^su y ) ) /su 2s ) ) ) with typecode |-
112	69 103 107	divscld	Could not format ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su y ) ) e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su y ) ) e. No ) with typecode |-
113	112 104 108	divscan2d	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( ( A /su ( 2s ^su y ) ) /su 2s ) ) = ( A /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( ( A /su ( 2s ^su y ) ) /su 2s ) ) = ( A /su ( 2s ^su y ) ) ) with typecode |-
114	111 113	eqtrd	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) = ( A /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) = ( A /su ( 2s ^su y ) ) ) with typecode |-
115	114	sneqd	Could not format ( ( y e. NN0_s /\ ph ) -> { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } = { ( A /su ( 2s ^su y ) ) } ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } = { ( A /su ( 2s ^su y ) ) } ) with typecode |-
116	99	oveq2d	Could not format ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) = ( B /su ( ( 2s ^su y ) x.s 2s ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) = ( B /su ( ( 2s ^su y ) x.s 2s ) ) ) with typecode |-
117	81 103 104 107 108	divdivs1d	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( B /su ( 2s ^su y ) ) /su 2s ) = ( B /su ( ( 2s ^su y ) x.s 2s ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( B /su ( 2s ^su y ) ) /su 2s ) = ( B /su ( ( 2s ^su y ) x.s 2s ) ) ) with typecode |-
118	116 117	eqtr4d	Could not format ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) = ( ( B /su ( 2s ^su y ) ) /su 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) = ( ( B /su ( 2s ^su y ) ) /su 2s ) ) with typecode |-
119	118	oveq2d	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) = ( 2s x.s ( ( B /su ( 2s ^su y ) ) /su 2s ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) = ( 2s x.s ( ( B /su ( 2s ^su y ) ) /su 2s ) ) ) with typecode |-
120	81 103 107	divscld	Could not format ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su y ) ) e. No ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su y ) ) e. No ) with typecode |-
121	120 104 108	divscan2d	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( ( B /su ( 2s ^su y ) ) /su 2s ) ) = ( B /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( ( B /su ( 2s ^su y ) ) /su 2s ) ) = ( B /su ( 2s ^su y ) ) ) with typecode |-
122	119 121	eqtrd	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) = ( B /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) = ( B /su ( 2s ^su y ) ) ) with typecode |-
123	122	sneqd	Could not format ( ( y e. NN0_s /\ ph ) -> { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } = { ( B /su ( 2s ^su y ) ) } ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } = { ( B /su ( 2s ^su y ) ) } ) with typecode |-
124	115 123	oveq12d	Could not format ( ( y e. NN0_s /\ ph ) -> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) ) with typecode |-
125	124	eqcomd	Could not format ( ( y e. NN0_s /\ ph ) -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) ) with typecode |-
126	69 81 73 78	divsdird	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) ) with typecode |-
127	125 126	eqeq12d	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) <-> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) <-> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) ) ) with typecode |-
128	127	biimp3a	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) ) with typecode |-
129		eqid	Could not format ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) : No typesetting found for |- ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) with typecode |-
130	80 83 96 128 129	halfcut	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) ) with typecode |-
131	126	oveq1d	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) ) with typecode |-
132	131	3adant3	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) ) with typecode |-
133	130 132	eqtr4d	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) ) with typecode |-
134		expsp1	Could not format ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) : No typesetting found for |- ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) with typecode |-
135	7 70 134	sylancr	Could not format ( y e. NN0_s -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) : No typesetting found for |- ( y e. NN0_s -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) with typecode |-
136	135	adantr	Could not format ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) with typecode |-
137	136	oveq2d	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( A +s B ) /su ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( A +s B ) /su ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) ) with typecode |-
138	69 81	addscld	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge \phi \right)\to A{+}_{s}B\in \mathrm{No}$$
139	138 73 104 78 108	divdivs1d	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( A +s B ) /su ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( A +s B ) /su ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) ) with typecode |-
140	137 139	eqtr4d	Could not format ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) ) with typecode |-
141	140	3adant3	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) ) with typecode |-
142	133 141	eqtr4d	Could not format ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) with typecode |-
143	142	3exp	Could not format ( y e. NN0_s -> ( ph -> ( ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) ) : No typesetting found for |- ( y e. NN0_s -> ( ph -> ( ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) ) with typecode |-
144	143	a2d	Could not format ( y e. NN0_s -> ( ( ph -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ph -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) ) : No typesetting found for |- ( y e. NN0_s -> ( ( ph -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ph -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) ) with typecode |-
145	27 38 49 60 68 144	n0sind	Could not format ( N e. NN0_s -> ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( N e. NN0_s -> ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) ) with typecode |-
146	3 145	mpcom	Could not format ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) : No typesetting found for |- ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) with typecode |-