Theorem eucliddivs

Description: Euclid's division lemma for surreal numbers. (Contributed by Scott Fenton, 8-Nov-2025)

	Ref	Expression
Assertion	eucliddivs	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(A=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢m=0_s\to \left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\leftrightarrow 0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\right)$$
2	1	anbi1d	$$⊢m=0_s\to \left(\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \left(0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
3	2	2rexbidv	$$⊢m=0_s\to \left(\exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
4	3	imbi2d	$$⊢m=0_s\to \left(\left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)\leftrightarrow \left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)\right)$$
5		eqeq1	$$⊢m=a\to \left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\leftrightarrow a=\left(B{\cdot }_{s}p\right){+}_{s}q\right)$$
6	5	anbi1d	$$⊢m=a\to \left(\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \left(a=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
7	6	2rexbidv	$$⊢m=a\to \left(\exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(a=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
8	7	imbi2d	$$⊢m=a\to \left(\left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)\leftrightarrow \left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(a=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)\right)$$
9		eqeq1	$$⊢m=a{+}_s{1}_s\to \left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\leftrightarrow a{+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}q\right)$$
10	9	anbi1d	$$⊢m=a{+}_s{1}_s\to \left(\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \left(a{+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
11	10	2rexbidv	$$⊢m=a{+}_s{1}_s\to \left(\exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
12		oveq2	$$⊢p=r\to B{\cdot }_{s}p=B{\cdot }_{s}r$$
13	12	oveq1d	$$⊢p=r\to \left(B{\cdot }_{s}p\right){+}_{s}q=\left(B{\cdot }_{s}r\right){+}_{s}q$$
14	13	eqeq2d	$$⊢p=r\to \left(a{+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}q\leftrightarrow a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}q\right)$$
15	14	anbi1d	$$⊢p=r\to \left(\left(a{+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
16		oveq2	$$⊢q=s\to \left(B{\cdot }_{s}r\right){+}_{s}q=\left(B{\cdot }_{s}r\right){+}_{s}s$$
17	16	eqeq2d	$$⊢q=s\to \left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}q\leftrightarrow a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\right)$$
18		breq1	$$⊢q=s\to \left(q{<}_{s}B\leftrightarrow s{<}_{s}B\right)$$
19	17 18	anbi12d	$$⊢q=s\to \left(\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
20	15 19	cbvrex2vw	$$⊢\exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)$$
21	11 20	bitrdi	$$⊢m=a{+}_s{1}_s\to \left(\exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
22	21	imbi2d	$$⊢m=a{+}_s{1}_s\to \left(\left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)\leftrightarrow \left(B\in {\mathbb{N}}_s\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)\right)$$
23		eqeq1	$$⊢m=A\to \left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\leftrightarrow A=\left(B{\cdot }_{s}p\right){+}_{s}q\right)$$
24	23	anbi1d	$$⊢m=A\to \left(\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \left(A=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
25	24	2rexbidv	$$⊢m=A\to \left(\exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(A=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
26	25	imbi2d	$$⊢m=A\to \left(\left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(m=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)\leftrightarrow \left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(A=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)\right)$$
27		nnsno	$$⊢B\in {\mathbb{N}}_s\to B\in \mathrm{No}$$
28		muls01	$$⊢B\in \mathrm{No}\to B{\cdot }_s{0}_s=0_s$$
29	27 28	syl	$$⊢B\in {\mathbb{N}}_s\to B{\cdot }_s{0}_s=0_s$$
30	29	oveq1d	$$⊢B\in {\mathbb{N}}_s\to \left(B{\cdot }_s{0}_s\right){+}_s{0}_s=0_s{+}_s{0}_s$$
31		0sno	$$⊢0_s\in \mathrm{No}$$
32		addslid	$$⊢0_s\in \mathrm{No}\to 0_s{+}_s{0}_s=0_s$$
33	31 32	ax-mp	$$⊢0_s{+}_s{0}_s=0_s$$
34	30 33	eqtr2di	$$⊢B\in {\mathbb{N}}_s\to 0_s=\left(B{\cdot }_s{0}_s\right){+}_s{0}_s$$
35		nnsgt0	$$⊢B\in {\mathbb{N}}_s\to 0_s{<}_{s}B$$
36		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
37		oveq2	$$⊢p=0_s\to B{\cdot }_{s}p=B{\cdot }_s{0}_s$$
38	37	oveq1d	$$⊢p=0_s\to \left(B{\cdot }_{s}p\right){+}_{s}q=\left(B{\cdot }_s{0}_s\right){+}_{s}q$$
39	38	eqeq2d	$$⊢p=0_s\to \left(0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\leftrightarrow 0_s=\left(B{\cdot }_s{0}_s\right){+}_{s}q\right)$$
40	39	anbi1d	$$⊢p=0_s\to \left(\left(0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \left(0_s=\left(B{\cdot }_s{0}_s\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
41		oveq2	$$⊢q=0_s\to \left(B{\cdot }_s{0}_s\right){+}_{s}q=\left(B{\cdot }_s{0}_s\right){+}_s{0}_s$$
42	41	eqeq2d	$$⊢q=0_s\to \left(0_s=\left(B{\cdot }_s{0}_s\right){+}_{s}q\leftrightarrow 0_s=\left(B{\cdot }_s{0}_s\right){+}_s{0}_s\right)$$
43		breq1	$$⊢q=0_s\to \left(q{<}_{s}B\leftrightarrow 0_s{<}_{s}B\right)$$
44	42 43	anbi12d	$$⊢q=0_s\to \left(\left(0_s=\left(B{\cdot }_s{0}_s\right){+}_{s}q\wedge q{<}_{s}B\right)\leftrightarrow \left(0_s=\left(B{\cdot }_s{0}_s\right){+}_s{0}_s\wedge 0_s{<}_{s}B\right)\right)$$
45	40 44	rspc2ev	$$⊢\left(0_s\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s\in {\mathbb{N}}_{\mathrm{0s}}\wedge \left(0_s=\left(B{\cdot }_s{0}_s\right){+}_s{0}_s\wedge 0_s{<}_{s}B\right)\right)\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)$$
46	36 36 45	mp3an12	$$⊢\left(0_s=\left(B{\cdot }_s{0}_s\right){+}_s{0}_s\wedge 0_s{<}_{s}B\right)\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)$$
47	34 35 46	syl2anc	$$⊢B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(0_s=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)$$
48		simprr	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to q\in {\mathbb{N}}_{\mathrm{0s}}$$
49		simplr	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B\in {\mathbb{N}}_s$$
50		nnm1n0s	$$⊢B\in {\mathbb{N}}_s\to B{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
51	49 50	syl	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
52		n0sleltp1	$$⊢\left(q\in {\mathbb{N}}_{\mathrm{0s}}\wedge B{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(q{\le }_s\left(B{-}_s{1}_s\right)\leftrightarrow q{<}_s\left(\left(B{-}_s{1}_s\right){+}_s{1}_s\right)\right)$$
53	48 51 52	syl2anc	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(q{\le }_s\left(B{-}_s{1}_s\right)\leftrightarrow q{<}_s\left(\left(B{-}_s{1}_s\right){+}_s{1}_s\right)\right)$$
54	48	n0snod	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to q\in \mathrm{No}$$
55	51	n0snod	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B{-}_s{1}_s\in \mathrm{No}$$
56		sleloe	$$⊢\left(q\in \mathrm{No}\wedge B{-}_s{1}_s\in \mathrm{No}\right)\to \left(q{\le }_s\left(B{-}_s{1}_s\right)\leftrightarrow \left(q{<}_s\left(B{-}_s{1}_s\right)\vee q=B{-}_s{1}_s\right)\right)$$
57	54 55 56	syl2anc	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(q{\le }_s\left(B{-}_s{1}_s\right)\leftrightarrow \left(q{<}_s\left(B{-}_s{1}_s\right)\vee q=B{-}_s{1}_s\right)\right)$$
58	49	nnsnod	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B\in \mathrm{No}$$
59		1sno	$$⊢1_s\in \mathrm{No}$$
60		npcans	$$⊢\left(B\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(B{-}_s{1}_s\right){+}_s{1}_s=B$$
61	58 59 60	sylancl	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(B{-}_s{1}_s\right){+}_s{1}_s=B$$
62	61	breq2d	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(q{<}_s\left(\left(B{-}_s{1}_s\right){+}_s{1}_s\right)\leftrightarrow q{<}_{s}B\right)$$
63	53 57 62	3bitr3rd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(q{<}_{s}B\leftrightarrow \left(q{<}_s\left(B{-}_s{1}_s\right)\vee q=B{-}_s{1}_s\right)\right)$$
64		simplrl	$$⊢\left(\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\wedge q{<}_s\left(B{-}_s{1}_s\right)\right)\to p\in {\mathbb{N}}_{\mathrm{0s}}$$
65		simplrr	$$⊢\left(\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\wedge q{<}_s\left(B{-}_s{1}_s\right)\right)\to q\in {\mathbb{N}}_{\mathrm{0s}}$$
66		peano2n0s	$$⊢q\in {\mathbb{N}}_{\mathrm{0s}}\to q{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
67	65 66	syl	$$⊢\left(\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\wedge q{<}_s\left(B{-}_s{1}_s\right)\right)\to q{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
68	49	nnn0sd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B\in {\mathbb{N}}_{\mathrm{0s}}$$
69		simprl	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to p\in {\mathbb{N}}_{\mathrm{0s}}$$
70		n0mulscl	$$⊢\left(B\in {\mathbb{N}}_{\mathrm{0s}}\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\to B{\cdot }_{s}p\in {\mathbb{N}}_{\mathrm{0s}}$$
71	68 69 70	syl2anc	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B{\cdot }_{s}p\in {\mathbb{N}}_{\mathrm{0s}}$$
72	71	n0snod	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B{\cdot }_{s}p\in \mathrm{No}$$
73	59	a1i	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to 1_s\in \mathrm{No}$$
74	72 54 73	addsassd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_s\left(q{+}_s{1}_s\right)$$
75	74	adantr	$$⊢\left(\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\wedge q{<}_s\left(B{-}_s{1}_s\right)\right)\to \left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_s\left(q{+}_s{1}_s\right)$$
76	54 73 58	sltaddsubd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(\left(q{+}_s{1}_s\right){<}_{s}B\leftrightarrow q{<}_s\left(B{-}_s{1}_s\right)\right)$$
77	76	biimpar	$$⊢\left(\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\wedge q{<}_s\left(B{-}_s{1}_s\right)\right)\to \left(q{+}_s{1}_s\right){<}_{s}B$$
78		oveq2	$$⊢r=p\to B{\cdot }_{s}r=B{\cdot }_{s}p$$
79	78	oveq1d	$$⊢r=p\to \left(B{\cdot }_{s}r\right){+}_{s}s=\left(B{\cdot }_{s}p\right){+}_{s}s$$
80	79	eqeq2d	$$⊢r=p\to \left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\leftrightarrow \left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}s\right)$$
81	80	anbi1d	$$⊢r=p\to \left(\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\leftrightarrow \left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
82		oveq2	$$⊢s=q{+}_s{1}_s\to \left(B{\cdot }_{s}p\right){+}_{s}s=\left(B{\cdot }_{s}p\right){+}_s\left(q{+}_s{1}_s\right)$$
83	82	eqeq2d	$$⊢s=q{+}_s{1}_s\to \left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}s\leftrightarrow \left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_s\left(q{+}_s{1}_s\right)\right)$$
84		breq1	$$⊢s=q{+}_s{1}_s\to \left(s{<}_{s}B\leftrightarrow \left(q{+}_s{1}_s\right){<}_{s}B\right)$$
85	83 84	anbi12d	$$⊢s=q{+}_s{1}_s\to \left(\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_{s}s\wedge s{<}_{s}B\right)\leftrightarrow \left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_s\left(q{+}_s{1}_s\right)\wedge \left(q{+}_s{1}_s\right){<}_{s}B\right)\right)$$
86	81 85	rspc2ev	$$⊢\left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\wedge \left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_s\left(q{+}_s{1}_s\right)\wedge \left(q{+}_s{1}_s\right){<}_{s}B\right)\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)$$
87	64 67 75 77 86	syl112anc	$$⊢\left(\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\wedge q{<}_s\left(B{-}_s{1}_s\right)\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)$$
88	87	ex	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(q{<}_s\left(B{-}_s{1}_s\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
89		peano2n0s	$$⊢p\in {\mathbb{N}}_{\mathrm{0s}}\to p{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
90	69 89	syl	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to p{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
91	58	mulsridd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B{\cdot }_s{1}_s=B$$
92	91	oveq2d	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(B{\cdot }_{s}p\right){+}_s\left(B{\cdot }_s{1}_s\right)=\left(B{\cdot }_{s}p\right){+}_{s}B$$
93	69	n0snod	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to p\in \mathrm{No}$$
94	58 93 73	addsdid	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B{\cdot }_s\left(p{+}_s{1}_s\right)=\left(B{\cdot }_{s}p\right){+}_s\left(B{\cdot }_s{1}_s\right)$$
95	61	oveq2d	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(B{\cdot }_{s}p\right){+}_s\left(\left(B{-}_s{1}_s\right){+}_s{1}_s\right)=\left(B{\cdot }_{s}p\right){+}_{s}B$$
96	92 94 95	3eqtr4rd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(B{\cdot }_{s}p\right){+}_s\left(\left(B{-}_s{1}_s\right){+}_s{1}_s\right)=B{\cdot }_s\left(p{+}_s{1}_s\right)$$
97	72 55 73	addsassd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}p\right){+}_s\left(\left(B{-}_s{1}_s\right){+}_s{1}_s\right)$$
98		peano2no	$$⊢p\in \mathrm{No}\to p{+}_s{1}_s\in \mathrm{No}$$
99	93 98	syl	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to p{+}_s{1}_s\in \mathrm{No}$$
100	58 99	mulscld	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to B{\cdot }_s\left(p{+}_s{1}_s\right)\in \mathrm{No}$$
101	100	addsridd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_s{0}_s=B{\cdot }_s\left(p{+}_s{1}_s\right)$$
102	96 97 101	3eqtr4d	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_s{0}_s$$
103	49 35	syl	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to 0_s{<}_{s}B$$
104		oveq2	$$⊢r=p{+}_s{1}_s\to B{\cdot }_{s}r=B{\cdot }_s\left(p{+}_s{1}_s\right)$$
105	104	oveq1d	$$⊢r=p{+}_s{1}_s\to \left(B{\cdot }_{s}r\right){+}_{s}s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_{s}s$$
106	105	eqeq2d	$$⊢r=p{+}_s{1}_s\to \left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\leftrightarrow \left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_{s}s\right)$$
107	106	anbi1d	$$⊢r=p{+}_s{1}_s\to \left(\left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\leftrightarrow \left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
108		oveq2	$$⊢s=0_s\to \left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_{s}s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_s{0}_s$$
109	108	eqeq2d	$$⊢s=0_s\to \left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_{s}s\leftrightarrow \left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_s{0}_s\right)$$
110		breq1	$$⊢s=0_s\to \left(s{<}_{s}B\leftrightarrow 0_s{<}_{s}B\right)$$
111	109 110	anbi12d	$$⊢s=0_s\to \left(\left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_{s}s\wedge s{<}_{s}B\right)\leftrightarrow \left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_s{0}_s\wedge 0_s{<}_{s}B\right)\right)$$
112	107 111	rspc2ev	$$⊢\left(p{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s\in {\mathbb{N}}_{\mathrm{0s}}\wedge \left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_s{0}_s\wedge 0_s{<}_{s}B\right)\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)$$
113	36 112	mp3an2	$$⊢\left(p{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\wedge \left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_s\left(p{+}_s{1}_s\right)\right){+}_s{0}_s\wedge 0_s{<}_{s}B\right)\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)$$
114	90 102 103 113	syl12anc	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)$$
115		oveq2	$$⊢q=B{-}_s{1}_s\to \left(B{\cdot }_{s}p\right){+}_{s}q=\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)$$
116	115	oveq1d	$$⊢q=B{-}_s{1}_s\to \left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s$$
117	116	eqeq1d	$$⊢q=B{-}_s{1}_s\to \left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\leftrightarrow \left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\right)$$
118	117	anbi1d	$$⊢q=B{-}_s{1}_s\to \left(\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\leftrightarrow \left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
119	118	2rexbidv	$$⊢q=B{-}_s{1}_s\to \left(\exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\leftrightarrow \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_s\left(B{-}_s{1}_s\right)\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
120	114 119	syl5ibrcom	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(q=B{-}_s{1}_s\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
121	88 120	jaod	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(\left(q{<}_s\left(B{-}_s{1}_s\right)\vee q=B{-}_s{1}_s\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
122	63 121	sylbid	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(q{<}_{s}B\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
123		oveq1	$$⊢a=\left(B{\cdot }_{s}p\right){+}_{s}q\to a{+}_s{1}_s=\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s$$
124	123	eqeq1d	$$⊢a=\left(B{\cdot }_{s}p\right){+}_{s}q\to \left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\leftrightarrow \left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\right)$$
125	124	anbi1d	$$⊢a=\left(B{\cdot }_{s}p\right){+}_{s}q\to \left(\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\leftrightarrow \left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
126	125	2rexbidv	$$⊢a=\left(B{\cdot }_{s}p\right){+}_{s}q\to \left(\exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\leftrightarrow \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
127	126	imbi2d	$$⊢a=\left(B{\cdot }_{s}p\right){+}_{s}q\to \left(\left(q{<}_{s}B\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)\leftrightarrow \left(q{<}_{s}B\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(\left(\left(B{\cdot }_{s}p\right){+}_{s}q\right){+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)\right)$$
128	122 127	syl5ibrcom	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(a=\left(B{\cdot }_{s}p\right){+}_{s}q\to \left(q{<}_{s}B\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)\right)$$
129	128	impd	$$⊢\left(\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\wedge \left(p\in {\mathbb{N}}_{\mathrm{0s}}\wedge q\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \left(\left(a=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
130	129	rexlimdvva	$$⊢\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\to \left(\exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(a=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)$$
131	130	ex	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(B\in {\mathbb{N}}_s\to \left(\exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(a=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)\right)$$
132	131	a2d	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(a=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)\to \left(B\in {\mathbb{N}}_s\to \exists r\in {\mathbb{N}}_{\mathrm{0s}}\exists s\in {\mathbb{N}}_{\mathrm{0s}}\left(a{+}_s{1}_s=\left(B{\cdot }_{s}r\right){+}_{s}s\wedge s{<}_{s}B\right)\right)\right)$$
133	4 8 22 26 47 132	n0sind	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(B\in {\mathbb{N}}_s\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(A=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)\right)$$
134	133	imp	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_s\right)\to \exists p\in {\mathbb{N}}_{\mathrm{0s}}\exists q\in {\mathbb{N}}_{\mathrm{0s}}\left(A=\left(B{\cdot }_{s}p\right){+}_{s}q\wedge q{<}_{s}B\right)$$