Metamath Proof Explorer

Theorem eucliddivs

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

Ref Expression
Assertion eucliddivs 
|- ( ( A e. NN0_s /\ B e. NN_s ) -> E. p e. NN0_s E. q e. NN0_s ( A = ( ( B x.s p ) +s q ) /\ q

Proof

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