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		2sno	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		1sno	$$⊢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		divs1	$$⊢A\in \mathrm{No}\to A{/}_{\mathrm{su}}{1}_s=A$$
62	1 61	syl	$$⊢\phi \to A{/}_{\mathrm{su}}{1}_s=A$$
63	62	sneqd	$$⊢\phi \to \left\{A{/}_{\mathrm{su}}{1}_s\right\}=\left\{A\right\}$$
64		divs1	$$⊢B\in \mathrm{No}\to B{/}_{\mathrm{su}}{1}_s=B$$
65	2 64	syl	$$⊢\phi \to B{/}_{\mathrm{su}}{1}_s=B$$
66	65	sneqd	$$⊢\phi \to \left\{B{/}_{\mathrm{su}}{1}_s\right\}=\left\{B\right\}$$
67	63 66	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\}$$
68		eqid	$$⊢\left\{A\right\}{|}_s\left\{B\right\}=\left\{A\right\}{|}_s\left\{B\right\}$$
69	1 2 4 5 68	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 |-
70	67 69	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 |-
71	1	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge \phi \right)\to A\in \mathrm{No}$$
72		peano2n0s	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
73		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 |-
74	7 72 73	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 |-
75	74	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 |-
76		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
77		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 |-
78	7 76 77	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 |-
79	72 78	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 |-
80	79	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 |-
81	71 75 80	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 |-
82	81	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 |-
83	2	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge \phi \right)\to B\in \mathrm{No}$$
84	83 75 80	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 |-
85	84	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 |-
86	71 75 80	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 |-
87	4	adantl	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge \phi \right)\to A{<}_{s}B$$
88	86 87	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 ) ) )
89		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
90		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
91	89 90	ax-mp	Could not format 0s
92		expsgt0	Could not format ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s /\ 0s 0s 0s
93	7 91 92	mp3an13	Could not format ( ( y +s 1s ) e. NN0_s -> 0s 0s
94	72 93	syl	Could not format ( y e. NN0_s -> 0s 0s
95	94	adantr	Could not format ( ( y e. NN0_s /\ ph ) -> 0s 0s
96	81 83 75 95	sltmuldivd	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 ) ) )
97	88 96	mpbid	Could not format ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) ( A /su ( 2s ^su ( y +s 1s ) ) )
98	97	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 ) ) )
99		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 |-
100	7 99	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 |-
101	100	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 |-
102	101	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 |-
103		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 |-
104	7 103	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 |-
105	104	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 |-
106	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 |-
107		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 |-
108	7 76 107	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 |-
109	108	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 |-
110	76	a1i	Could not format ( ( y e. NN0_s /\ ph ) -> 2s =/= 0s ) : No typesetting found for |- ( ( y e. NN0_s /\ ph ) -> 2s =/= 0s ) with typecode |-
111	71 105 106 109 110	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 |-
112	102 111	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 |-
113	112	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 |-
114	71 105 109	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 |-
115	114 106 110	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 |-
116	113 115	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 |-
117	116	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 |-
118	101	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 |-
119	83 105 106 109 110	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 |-
120	118 119	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 |-
121	120	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 |-
122	83 105 109	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 |-
123	122 106 110	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 |-
124	121 123	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 |-
125	124	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 |-
126	117 125	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 |-
127	126	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 |-
128	71 83 75 80	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 |-
129	127 128	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 |-
130	129	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 |-
131		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 |-
132	82 85 98 130 131	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 |-
133	128	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 |-
134	133	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 |-
135	132 134	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 |-
136		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 |-
137	7 72 136	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 |-
138	137	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 |-
139	138	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 |-
140	71 83	addscld	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge \phi \right)\to A{+}_{s}B\in \mathrm{No}$$
141	140 75 106 80 110	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 |-
142	139 141	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 |-
143	142	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 |-
144	135 143	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 |-
145	144	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 |-
146	145	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 |-
147	27 38 49 60 70 146	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 |-
148	3 147	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 |-