Metamath Proof Explorer

Theorem divalglem2

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

Ref Expression
Hypotheses divalglem0.1 
|- N e. ZZ
divalglem0.2 
|- D e. ZZ
divalglem1.3 
|- D =/= 0
divalglem2.4 
|- S = { r e. NN0 | D || ( N - r ) }
Assertion divalglem2 
|- inf ( S , RR , < ) e. S

Proof

Step Hyp Ref Expression
1 divalglem0.1 
 |-  N e. ZZ
2 divalglem0.2 
 |-  D e. ZZ
3 divalglem1.3 
 |-  D =/= 0
4 divalglem2.4 
 |-  S = { r e. NN0 | D || ( N - r ) }
5 4 ssrab3 
 |-  S C_ NN0
6 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
7 5 6 sseqtri 
 |-  S C_ ( ZZ>= ` 0 )
8 zmulcl 
 |-  ( ( N e. ZZ /\ D e. ZZ ) -> ( N x. D ) e. ZZ )
9 1 2 8 mp2an 
 |-  ( N x. D ) e. ZZ
10 nn0abscl 
 |-  ( ( N x. D ) e. ZZ -> ( abs ` ( N x. D ) ) e. NN0 )
11 9 10 ax-mp 
 |-  ( abs ` ( N x. D ) ) e. NN0
12 11 nn0zi 
 |-  ( abs ` ( N x. D ) ) e. ZZ
13 zaddcl 
 |-  ( ( N e. ZZ /\ ( abs ` ( N x. D ) ) e. ZZ ) -> ( N + ( abs ` ( N x. D ) ) ) e. ZZ )
14 1 12 13 mp2an 
 |-  ( N + ( abs ` ( N x. D ) ) ) e. ZZ
15 1 2 3 divalglem1 
 |-  0 <_ ( N + ( abs ` ( N x. D ) ) )
16 elnn0z 
 |-  ( ( N + ( abs ` ( N x. D ) ) ) e. NN0 <-> ( ( N + ( abs ` ( N x. D ) ) ) e. ZZ /\ 0 <_ ( N + ( abs ` ( N x. D ) ) ) ) )
17 14 15 16 mpbir2an 
 |-  ( N + ( abs ` ( N x. D ) ) ) e. NN0
18 iddvds 
 |-  ( D e. ZZ -> D || D )
19 dvdsabsb 
 |-  ( ( D e. ZZ /\ D e. ZZ ) -> ( D || D <-> D || ( abs ` D ) ) )
20 19 anidms 
 |-  ( D e. ZZ -> ( D || D <-> D || ( abs ` D ) ) )
21 18 20 mpbid 
 |-  ( D e. ZZ -> D || ( abs ` D ) )
22 2 21 ax-mp 
 |-  D || ( abs ` D )
23 nn0abscl 
 |-  ( N e. ZZ -> ( abs ` N ) e. NN0 )
24 1 23 ax-mp 
 |-  ( abs ` N ) e. NN0
25 24 nn0negzi 
 |-  -u ( abs ` N ) e. ZZ
26 nn0abscl 
 |-  ( D e. ZZ -> ( abs ` D ) e. NN0 )
27 2 26 ax-mp 
 |-  ( abs ` D ) e. NN0
28 27 nn0zi 
 |-  ( abs ` D ) e. ZZ
29 dvdsmultr2 
 |-  ( ( D e. ZZ /\ -u ( abs ` N ) e. ZZ /\ ( abs ` D ) e. ZZ ) -> ( D || ( abs ` D ) -> D || ( -u ( abs ` N ) x. ( abs ` D ) ) ) )
30 2 25 28 29 mp3an 
 |-  ( D || ( abs ` D ) -> D || ( -u ( abs ` N ) x. ( abs ` D ) ) )
31 22 30 ax-mp 
 |-  D || ( -u ( abs ` N ) x. ( abs ` D ) )
32 zcn 
 |-  ( N e. ZZ -> N e. CC )
33 1 32 ax-mp 
 |-  N e. CC
34 zcn 
 |-  ( D e. ZZ -> D e. CC )
35 2 34 ax-mp 
 |-  D e. CC
36 33 35 absmuli 
 |-  ( abs ` ( N x. D ) ) = ( ( abs ` N ) x. ( abs ` D ) )
37 36 negeqi 
 |-  -u ( abs ` ( N x. D ) ) = -u ( ( abs ` N ) x. ( abs ` D ) )
38 df-neg 
 |-  -u ( abs ` ( N x. D ) ) = ( 0 - ( abs ` ( N x. D ) ) )
39 33 subidi 
 |-  ( N - N ) = 0
40 39 oveq1i 
 |-  ( ( N - N ) - ( abs ` ( N x. D ) ) ) = ( 0 - ( abs ` ( N x. D ) ) )
41 11 nn0cni 
 |-  ( abs ` ( N x. D ) ) e. CC
42 subsub4 
 |-  ( ( N e. CC /\ N e. CC /\ ( abs ` ( N x. D ) ) e. CC ) -> ( ( N - N ) - ( abs ` ( N x. D ) ) ) = ( N - ( N + ( abs ` ( N x. D ) ) ) ) )
43 33 33 41 42 mp3an 
 |-  ( ( N - N ) - ( abs ` ( N x. D ) ) ) = ( N - ( N + ( abs ` ( N x. D ) ) ) )
44 38 40 43 3eqtr2ri 
 |-  ( N - ( N + ( abs ` ( N x. D ) ) ) ) = -u ( abs ` ( N x. D ) )
45 33 abscli 
 |-  ( abs ` N ) e. RR
46 45 recni 
 |-  ( abs ` N ) e. CC
47 35 abscli 
 |-  ( abs ` D ) e. RR
48 47 recni 
 |-  ( abs ` D ) e. CC
49 46 48 mulneg1i 
 |-  ( -u ( abs ` N ) x. ( abs ` D ) ) = -u ( ( abs ` N ) x. ( abs ` D ) )
50 37 44 49 3eqtr4i 
 |-  ( N - ( N + ( abs ` ( N x. D ) ) ) ) = ( -u ( abs ` N ) x. ( abs ` D ) )
51 31 50 breqtrri 
 |-  D || ( N - ( N + ( abs ` ( N x. D ) ) ) )
52 oveq2 
 |-  ( r = ( N + ( abs ` ( N x. D ) ) ) -> ( N - r ) = ( N - ( N + ( abs ` ( N x. D ) ) ) ) )
53 52 breq2d 
 |-  ( r = ( N + ( abs ` ( N x. D ) ) ) -> ( D || ( N - r ) <-> D || ( N - ( N + ( abs ` ( N x. D ) ) ) ) ) )
54 53 4 elrab2 
 |-  ( ( N + ( abs ` ( N x. D ) ) ) e. S <-> ( ( N + ( abs ` ( N x. D ) ) ) e. NN0 /\ D || ( N - ( N + ( abs ` ( N x. D ) ) ) ) ) )
55 17 51 54 mpbir2an 
 |-  ( N + ( abs ` ( N x. D ) ) ) e. S
56 55 ne0ii 
 |-  S =/= (/)
57 infssuzcl 
 |-  ( ( S C_ ( ZZ>= ` 0 ) /\ S =/= (/) ) -> inf ( S , RR , < ) e. S )
58 7 56 57 mp2an 
 |-  inf ( S , RR , < ) e. S