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∈ℤ
divalglem0.2 ⊢D∈ℤ
divalglem1.3 ⊢D≠0
divalglem2.4 ⊢S=r∈ℕ0|D∥N−r
Assertion divalglem2 ⊢supSℝ<∈S

Proof

Step Hyp Ref Expression
1 divalglem0.1 ⊢N∈ℤ
2 divalglem0.2 ⊢D∈ℤ
3 divalglem1.3 ⊢D≠0
4 divalglem2.4 ⊢S=r∈ℕ0|D∥N−r
5 4 ssrab3 ⊢S⊆ℕ0
6 nn0uz ⊢ℕ0=ℤ≥0
7 5 6 sseqtri ⊢S⊆ℤ≥0
8 zmulcl ⊢N∈ℤ∧D∈ℤ→N⁢D∈ℤ
9 1 2 8 mp2an ⊢N⁢D∈ℤ
10 nn0abscl ⊢N⁢D∈ℤ→N⁢D∈ℕ0
11 9 10 ax-mp ⊢N⁢D∈ℕ0
12 11 nn0zi ⊢N⁢D∈ℤ
13 zaddcl ⊢N∈ℤ∧N⁢D∈ℤ→N+N⁢D∈ℤ
14 1 12 13 mp2an ⊢N+N⁢D∈ℤ
15 1 2 3 divalglem1 ⊢0≤N+N⁢D
16 elnn0z ⊢N+N⁢D∈ℕ0↔N+N⁢D∈ℤ∧0≤N+N⁢D
17 14 15 16 mpbir2an ⊢N+N⁢D∈ℕ0
18 iddvds ⊢D∈ℤ→D∥D
19 dvdsabsb ⊢D∈ℤ∧D∈ℤ→D∥D↔D∥D
20 19 anidms ⊢D∈ℤ→D∥D↔D∥D
21 18 20 mpbid ⊢D∈ℤ→D∥D
22 2 21 ax-mp ⊢D∥D
23 nn0abscl ⊢N∈ℤ→N∈ℕ0
24 1 23 ax-mp ⊢N∈ℕ0
25 24 nn0negzi ⊢−N∈ℤ
26 nn0abscl ⊢D∈ℤ→D∈ℕ0
27 2 26 ax-mp ⊢D∈ℕ0
28 27 nn0zi ⊢D∈ℤ
29 dvdsmultr2 ⊢D∈ℤ∧−N∈ℤ∧D∈ℤ→D∥D→D∥−N⁢D
30 2 25 28 29 mp3an ⊢D∥D→D∥−N⁢D
31 22 30 ax-mp ⊢D∥−N⁢D
32 zcn ⊢N∈ℤ→N∈ℂ
33 1 32 ax-mp ⊢N∈ℂ
34 zcn ⊢D∈ℤ→D∈ℂ
35 2 34 ax-mp ⊢D∈ℂ
36 33 35 absmuli ⊢N⁢D=N⁢D
37 36 negeqi ⊢−N⁢D=−N⁢D
38 df-neg ⊢−N⁢D=0−N⁢D
39 33 subidi ⊢N−N=0
40 39 oveq1i ⊢N-N-N⁢D=0−N⁢D
41 11 nn0cni ⊢N⁢D∈ℂ
42 subsub4 ⊢N∈ℂ∧N∈ℂ∧N⁢D∈ℂ→N-N-N⁢D=N−N+N⁢D
43 33 33 41 42 mp3an ⊢N-N-N⁢D=N−N+N⁢D
44 38 40 43 3eqtr2ri ⊢N−N+N⁢D=−N⁢D
45 33 abscli ⊢N∈ℝ
46 45 recni ⊢N∈ℂ
47 35 abscli ⊢D∈ℝ
48 47 recni ⊢D∈ℂ
49 46 48 mulneg1i ⊢−N⁢D=−N⁢D
50 37 44 49 3eqtr4i ⊢N−N+N⁢D=−N⁢D
51 31 50 breqtrri ⊢D∥N−N+N⁢D
52 oveq2 ⊢r=N+N⁢D→N−r=N−N+N⁢D
53 52 breq2d ⊢r=N+N⁢D→D∥N−r↔D∥N−N+N⁢D
54 53 4 elrab2 ⊢N+N⁢D∈S↔N+N⁢D∈ℕ0∧D∥N−N+N⁢D
55 17 51 54 mpbir2an ⊢N+N⁢D∈S
56 55 ne0ii ⊢S≠∅
57 infssuzcl ⊢S⊆ℤ≥0∧S≠∅→supSℝ<∈S
58 7 56 57 mp2an ⊢supSℝ<∈S