Metamath Proof Explorer

Theorem eucliddivs

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

Ref Expression
Assertion eucliddivs ( ( 𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕs ) → ∃ 𝑝 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝐴 = ( ( 𝐵 ·s 𝑝 ) +s 𝑞 ) ∧ 𝑞 <s 𝐵 ) )

Proof

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