Metamath Proof Explorer

Theorem divalglem10

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011) (Proof shortened by AV, 2-Oct-2020)

Ref Expression
Hypotheses divalglem8.1 
|- N e. ZZ
divalglem8.2 
|- D e. ZZ
divalglem8.3 
|- D =/= 0
divalglem8.4 
|- S = { r e. NN0 | D || ( N - r ) }
Assertion divalglem10 
|- E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) )

Proof

Step Hyp Ref Expression
1 divalglem8.1 
 |-  N e. ZZ
2 divalglem8.2 
 |-  D e. ZZ
3 divalglem8.3 
 |-  D =/= 0
4 divalglem8.4 
 |-  S = { r e. NN0 | D || ( N - r ) }
5 eqid 
 |-  inf ( S , RR , < ) = inf ( S , RR , < )
6 1 2 3 4 5 divalglem9 
 |-  E! x e. S x < ( abs ` D )
7 elnn0z 
 |-  ( x e. NN0 <-> ( x e. ZZ /\ 0 <_ x ) )
8 7 anbi2i 
 |-  ( ( x < ( abs ` D ) /\ x e. NN0 ) <-> ( x < ( abs ` D ) /\ ( x e. ZZ /\ 0 <_ x ) ) )
9 an12 
 |-  ( ( x < ( abs ` D ) /\ ( x e. ZZ /\ 0 <_ x ) ) <-> ( x e. ZZ /\ ( x < ( abs ` D ) /\ 0 <_ x ) ) )
10 ancom 
 |-  ( ( x < ( abs ` D ) /\ 0 <_ x ) <-> ( 0 <_ x /\ x < ( abs ` D ) ) )
11 10 anbi2i 
 |-  ( ( x e. ZZ /\ ( x < ( abs ` D ) /\ 0 <_ x ) ) <-> ( x e. ZZ /\ ( 0 <_ x /\ x < ( abs ` D ) ) ) )
12 9 11 bitri 
 |-  ( ( x < ( abs ` D ) /\ ( x e. ZZ /\ 0 <_ x ) ) <-> ( x e. ZZ /\ ( 0 <_ x /\ x < ( abs ` D ) ) ) )
13 8 12 bitri 
 |-  ( ( x < ( abs ` D ) /\ x e. NN0 ) <-> ( x e. ZZ /\ ( 0 <_ x /\ x < ( abs ` D ) ) ) )
14 13 anbi1i 
 |-  ( ( ( x < ( abs ` D ) /\ x e. NN0 ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) <-> ( ( x e. ZZ /\ ( 0 <_ x /\ x < ( abs ` D ) ) ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) )
15 anass 
 |-  ( ( ( x e. ZZ /\ ( 0 <_ x /\ x < ( abs ` D ) ) ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) <-> ( x e. ZZ /\ ( ( 0 <_ x /\ x < ( abs ` D ) ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) ) )
16 14 15 bitri 
 |-  ( ( ( x < ( abs ` D ) /\ x e. NN0 ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) <-> ( x e. ZZ /\ ( ( 0 <_ x /\ x < ( abs ` D ) ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) ) )
17 oveq2 
 |-  ( r = x -> ( ( q x. D ) + r ) = ( ( q x. D ) + x ) )
18 17 eqeq2d 
 |-  ( r = x -> ( N = ( ( q x. D ) + r ) <-> N = ( ( q x. D ) + x ) ) )
19 18 rexbidv 
 |-  ( r = x -> ( E. q e. ZZ N = ( ( q x. D ) + r ) <-> E. q e. ZZ N = ( ( q x. D ) + x ) ) )
20 1 2 3 4 divalglem4 
 |-  S = { r e. NN0 | E. q e. ZZ N = ( ( q x. D ) + r ) }
21 19 20 elrab2 
 |-  ( x e. S <-> ( x e. NN0 /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) )
22 21 anbi2i 
 |-  ( ( x < ( abs ` D ) /\ x e. S ) <-> ( x < ( abs ` D ) /\ ( x e. NN0 /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) ) )
23 ancom 
 |-  ( ( x e. S /\ x < ( abs ` D ) ) <-> ( x < ( abs ` D ) /\ x e. S ) )
24 anass 
 |-  ( ( ( x < ( abs ` D ) /\ x e. NN0 ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) <-> ( x < ( abs ` D ) /\ ( x e. NN0 /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) ) )
25 22 23 24 3bitr4i 
 |-  ( ( x e. S /\ x < ( abs ` D ) ) <-> ( ( x < ( abs ` D ) /\ x e. NN0 ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) )
26 df-3an 
 |-  ( ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) <-> ( ( 0 <_ x /\ x < ( abs ` D ) ) /\ N = ( ( q x. D ) + x ) ) )
27 26 rexbii 
 |-  ( E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) <-> E. q e. ZZ ( ( 0 <_ x /\ x < ( abs ` D ) ) /\ N = ( ( q x. D ) + x ) ) )
28 r19.42v 
 |-  ( E. q e. ZZ ( ( 0 <_ x /\ x < ( abs ` D ) ) /\ N = ( ( q x. D ) + x ) ) <-> ( ( 0 <_ x /\ x < ( abs ` D ) ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) )
29 27 28 bitri 
 |-  ( E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) <-> ( ( 0 <_ x /\ x < ( abs ` D ) ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) )
30 29 anbi2i 
 |-  ( ( x e. ZZ /\ E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) ) <-> ( x e. ZZ /\ ( ( 0 <_ x /\ x < ( abs ` D ) ) /\ E. q e. ZZ N = ( ( q x. D ) + x ) ) ) )
31 16 25 30 3bitr4i 
 |-  ( ( x e. S /\ x < ( abs ` D ) ) <-> ( x e. ZZ /\ E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) ) )
32 31 eubii 
 |-  ( E! x ( x e. S /\ x < ( abs ` D ) ) <-> E! x ( x e. ZZ /\ E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) ) )
33 df-reu 
 |-  ( E! x e. S x < ( abs ` D ) <-> E! x ( x e. S /\ x < ( abs ` D ) ) )
34 df-reu 
 |-  ( E! x e. ZZ E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) <-> E! x ( x e. ZZ /\ E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) ) )
35 32 33 34 3bitr4i 
 |-  ( E! x e. S x < ( abs ` D ) <-> E! x e. ZZ E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) )
36 6 35 mpbi 
 |-  E! x e. ZZ E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) )
37 breq2 
 |-  ( x = r -> ( 0 <_ x <-> 0 <_ r ) )
38 breq1 
 |-  ( x = r -> ( x < ( abs ` D ) <-> r < ( abs ` D ) ) )
39 oveq2 
 |-  ( x = r -> ( ( q x. D ) + x ) = ( ( q x. D ) + r ) )
40 39 eqeq2d 
 |-  ( x = r -> ( N = ( ( q x. D ) + x ) <-> N = ( ( q x. D ) + r ) ) )
41 37 38 40 3anbi123d 
 |-  ( x = r -> ( ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) <-> ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) ) )
42 41 rexbidv 
 |-  ( x = r -> ( E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) <-> E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) ) )
43 42 cbvreuvw 
 |-  ( E! x e. ZZ E. q e. ZZ ( 0 <_ x /\ x < ( abs ` D ) /\ N = ( ( q x. D ) + x ) ) <-> E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) )
44 36 43 mpbi 
 |-  E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) )