Proof of Theorem divalglem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | divalglem2.4 | . . . 4
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} | 
| 2 | 1 | ssrab3 4081 | . . 3
⊢ 𝑆 ⊆
ℕ0 | 
| 3 |  | nn0uz 12921 | . . 3
⊢
ℕ0 = (ℤ≥‘0) | 
| 4 | 2, 3 | sseqtri 4031 | . 2
⊢ 𝑆 ⊆
(ℤ≥‘0) | 
| 5 |  | divalglem0.1 | . . . . . 6
⊢ 𝑁 ∈ ℤ | 
| 6 |  | divalglem0.2 | . . . . . . . . 9
⊢ 𝐷 ∈ ℤ | 
| 7 |  | zmulcl 12668 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑁 · 𝐷) ∈ ℤ) | 
| 8 | 5, 6, 7 | mp2an 692 | . . . . . . . 8
⊢ (𝑁 · 𝐷) ∈ ℤ | 
| 9 |  | nn0abscl 15352 | . . . . . . . 8
⊢ ((𝑁 · 𝐷) ∈ ℤ → (abs‘(𝑁 · 𝐷)) ∈
ℕ0) | 
| 10 | 8, 9 | ax-mp 5 | . . . . . . 7
⊢
(abs‘(𝑁
· 𝐷)) ∈
ℕ0 | 
| 11 | 10 | nn0zi 12644 | . . . . . 6
⊢
(abs‘(𝑁
· 𝐷)) ∈
ℤ | 
| 12 |  | zaddcl 12659 | . . . . . 6
⊢ ((𝑁 ∈ ℤ ∧
(abs‘(𝑁 ·
𝐷)) ∈ ℤ) →
(𝑁 + (abs‘(𝑁 · 𝐷))) ∈ ℤ) | 
| 13 | 5, 11, 12 | mp2an 692 | . . . . 5
⊢ (𝑁 + (abs‘(𝑁 · 𝐷))) ∈ ℤ | 
| 14 |  | divalglem1.3 | . . . . . 6
⊢ 𝐷 ≠ 0 | 
| 15 | 5, 6, 14 | divalglem1 16432 | . . . . 5
⊢ 0 ≤
(𝑁 + (abs‘(𝑁 · 𝐷))) | 
| 16 |  | elnn0z 12628 | . . . . 5
⊢ ((𝑁 + (abs‘(𝑁 · 𝐷))) ∈ ℕ0 ↔
((𝑁 + (abs‘(𝑁 · 𝐷))) ∈ ℤ ∧ 0 ≤ (𝑁 + (abs‘(𝑁 · 𝐷))))) | 
| 17 | 13, 15, 16 | mpbir2an 711 | . . . 4
⊢ (𝑁 + (abs‘(𝑁 · 𝐷))) ∈
ℕ0 | 
| 18 |  | iddvds 16308 | . . . . . . . 8
⊢ (𝐷 ∈ ℤ → 𝐷 ∥ 𝐷) | 
| 19 |  | dvdsabsb 16314 | . . . . . . . . 9
⊢ ((𝐷 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐷 ∥ 𝐷 ↔ 𝐷 ∥ (abs‘𝐷))) | 
| 20 | 19 | anidms 566 | . . . . . . . 8
⊢ (𝐷 ∈ ℤ → (𝐷 ∥ 𝐷 ↔ 𝐷 ∥ (abs‘𝐷))) | 
| 21 | 18, 20 | mpbid 232 | . . . . . . 7
⊢ (𝐷 ∈ ℤ → 𝐷 ∥ (abs‘𝐷)) | 
| 22 | 6, 21 | ax-mp 5 | . . . . . 6
⊢ 𝐷 ∥ (abs‘𝐷) | 
| 23 |  | nn0abscl 15352 | . . . . . . . . 9
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∈
ℕ0) | 
| 24 | 5, 23 | ax-mp 5 | . . . . . . . 8
⊢
(abs‘𝑁) ∈
ℕ0 | 
| 25 | 24 | nn0negzi 12658 | . . . . . . 7
⊢
-(abs‘𝑁)
∈ ℤ | 
| 26 |  | nn0abscl 15352 | . . . . . . . . 9
⊢ (𝐷 ∈ ℤ →
(abs‘𝐷) ∈
ℕ0) | 
| 27 | 6, 26 | ax-mp 5 | . . . . . . . 8
⊢
(abs‘𝐷) ∈
ℕ0 | 
| 28 | 27 | nn0zi 12644 | . . . . . . 7
⊢
(abs‘𝐷) ∈
ℤ | 
| 29 |  | dvdsmultr2 16336 | . . . . . . 7
⊢ ((𝐷 ∈ ℤ ∧
-(abs‘𝑁) ∈
ℤ ∧ (abs‘𝐷)
∈ ℤ) → (𝐷
∥ (abs‘𝐷)
→ 𝐷 ∥
(-(abs‘𝑁) ·
(abs‘𝐷)))) | 
| 30 | 6, 25, 28, 29 | mp3an 1462 | . . . . . 6
⊢ (𝐷 ∥ (abs‘𝐷) → 𝐷 ∥ (-(abs‘𝑁) · (abs‘𝐷))) | 
| 31 | 22, 30 | ax-mp 5 | . . . . 5
⊢ 𝐷 ∥ (-(abs‘𝑁) · (abs‘𝐷)) | 
| 32 |  | zcn 12620 | . . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 33 | 5, 32 | ax-mp 5 | . . . . . . . 8
⊢ 𝑁 ∈ ℂ | 
| 34 |  | zcn 12620 | . . . . . . . . 9
⊢ (𝐷 ∈ ℤ → 𝐷 ∈
ℂ) | 
| 35 | 6, 34 | ax-mp 5 | . . . . . . . 8
⊢ 𝐷 ∈ ℂ | 
| 36 | 33, 35 | absmuli 15444 | . . . . . . 7
⊢
(abs‘(𝑁
· 𝐷)) =
((abs‘𝑁) ·
(abs‘𝐷)) | 
| 37 | 36 | negeqi 11502 | . . . . . 6
⊢
-(abs‘(𝑁
· 𝐷)) =
-((abs‘𝑁) ·
(abs‘𝐷)) | 
| 38 |  | df-neg 11496 | . . . . . . 7
⊢
-(abs‘(𝑁
· 𝐷)) = (0 −
(abs‘(𝑁 ·
𝐷))) | 
| 39 | 33 | subidi 11581 | . . . . . . . 8
⊢ (𝑁 − 𝑁) = 0 | 
| 40 | 39 | oveq1i 7442 | . . . . . . 7
⊢ ((𝑁 − 𝑁) − (abs‘(𝑁 · 𝐷))) = (0 − (abs‘(𝑁 · 𝐷))) | 
| 41 | 10 | nn0cni 12540 | . . . . . . . 8
⊢
(abs‘(𝑁
· 𝐷)) ∈
ℂ | 
| 42 |  | subsub4 11543 | . . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(abs‘(𝑁 ·
𝐷)) ∈ ℂ) →
((𝑁 − 𝑁) − (abs‘(𝑁 · 𝐷))) = (𝑁 − (𝑁 + (abs‘(𝑁 · 𝐷))))) | 
| 43 | 33, 33, 41, 42 | mp3an 1462 | . . . . . . 7
⊢ ((𝑁 − 𝑁) − (abs‘(𝑁 · 𝐷))) = (𝑁 − (𝑁 + (abs‘(𝑁 · 𝐷)))) | 
| 44 | 38, 40, 43 | 3eqtr2ri 2771 | . . . . . 6
⊢ (𝑁 − (𝑁 + (abs‘(𝑁 · 𝐷)))) = -(abs‘(𝑁 · 𝐷)) | 
| 45 | 33 | abscli 15435 | . . . . . . . 8
⊢
(abs‘𝑁) ∈
ℝ | 
| 46 | 45 | recni 11276 | . . . . . . 7
⊢
(abs‘𝑁) ∈
ℂ | 
| 47 | 35 | abscli 15435 | . . . . . . . 8
⊢
(abs‘𝐷) ∈
ℝ | 
| 48 | 47 | recni 11276 | . . . . . . 7
⊢
(abs‘𝐷) ∈
ℂ | 
| 49 | 46, 48 | mulneg1i 11710 | . . . . . 6
⊢
(-(abs‘𝑁)
· (abs‘𝐷)) =
-((abs‘𝑁) ·
(abs‘𝐷)) | 
| 50 | 37, 44, 49 | 3eqtr4i 2774 | . . . . 5
⊢ (𝑁 − (𝑁 + (abs‘(𝑁 · 𝐷)))) = (-(abs‘𝑁) · (abs‘𝐷)) | 
| 51 | 31, 50 | breqtrri 5169 | . . . 4
⊢ 𝐷 ∥ (𝑁 − (𝑁 + (abs‘(𝑁 · 𝐷)))) | 
| 52 |  | oveq2 7440 | . . . . . 6
⊢ (𝑟 = (𝑁 + (abs‘(𝑁 · 𝐷))) → (𝑁 − 𝑟) = (𝑁 − (𝑁 + (abs‘(𝑁 · 𝐷))))) | 
| 53 | 52 | breq2d 5154 | . . . . 5
⊢ (𝑟 = (𝑁 + (abs‘(𝑁 · 𝐷))) → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − (𝑁 + (abs‘(𝑁 · 𝐷)))))) | 
| 54 | 53, 1 | elrab2 3694 | . . . 4
⊢ ((𝑁 + (abs‘(𝑁 · 𝐷))) ∈ 𝑆 ↔ ((𝑁 + (abs‘(𝑁 · 𝐷))) ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − (𝑁 + (abs‘(𝑁 · 𝐷)))))) | 
| 55 | 17, 51, 54 | mpbir2an 711 | . . 3
⊢ (𝑁 + (abs‘(𝑁 · 𝐷))) ∈ 𝑆 | 
| 56 | 55 | ne0ii 4343 | . 2
⊢ 𝑆 ≠ ∅ | 
| 57 |  | infssuzcl 12975 | . 2
⊢ ((𝑆 ⊆
(ℤ≥‘0) ∧ 𝑆 ≠ ∅) → inf(𝑆, ℝ, < ) ∈ 𝑆) | 
| 58 | 4, 56, 57 | mp2an 692 | 1
⊢ inf(𝑆, ℝ, < ) ∈ 𝑆 |