Proof of Theorem jm2.19
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rmyeq0 42970 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0)) | 
| 2 | 1 | 3adant2 1131 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0)) | 
| 3 |  | 0dvds 16315 | . . . . . 6
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ 𝑁 = 0)) | 
| 4 | 3 | 3ad2ant3 1135 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ 𝑁 ↔ 𝑁 = 0)) | 
| 5 |  | frmy 42931 | . . . . . . . 8
⊢ 
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ | 
| 6 | 5 | fovcl 7562 | . . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) | 
| 7 | 6 | 3adant2 1131 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) | 
| 8 |  | 0dvds 16315 | . . . . . 6
⊢ ((𝐴 Yrm 𝑁) ∈ ℤ → (0
∥ (𝐴 Yrm
𝑁) ↔ (𝐴 Yrm 𝑁) = 0)) | 
| 9 | 7, 8 | syl 17 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑁) = 0)) | 
| 10 | 2, 4, 9 | 3bitr4d 311 | . . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ 𝑁 ↔ 0 ∥ (𝐴 Yrm 𝑁))) | 
| 11 | 10 | adantr 480 | . . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (0 ∥ 𝑁 ↔ 0 ∥ (𝐴 Yrm 𝑁))) | 
| 12 |  | simpr 484 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → 𝑀 = 0) | 
| 13 | 12 | breq1d 5152 | . . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑀 ∥ 𝑁 ↔ 0 ∥ 𝑁)) | 
| 14 | 12 | oveq2d 7448 | . . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐴 Yrm 𝑀) = (𝐴 Yrm 0)) | 
| 15 |  | simpl1 1191 | . . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → 𝐴 ∈
(ℤ≥‘2)) | 
| 16 |  | rmy0 42946 | . . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) | 
| 17 | 15, 16 | syl 17 | . . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐴 Yrm 0) = 0) | 
| 18 | 14, 17 | eqtrd 2776 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐴 Yrm 𝑀) = 0) | 
| 19 | 18 | breq1d 5152 | . . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ 0 ∥ (𝐴 Yrm 𝑁))) | 
| 20 | 11, 13, 19 | 3bitr4d 311 | . 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁))) | 
| 21 | 5 | fovcl 7562 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ) | 
| 22 | 21 | 3adant3 1132 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ) | 
| 23 |  | dvds0 16310 | . . . . . . . 8
⊢ ((𝐴 Yrm 𝑀) ∈ ℤ → (𝐴 Yrm 𝑀) ∥ 0) | 
| 24 | 22, 23 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∥ 0) | 
| 25 | 16 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 0) = 0) | 
| 26 | 24, 25 | breqtrrd 5170 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 0)) | 
| 27 |  | oveq2 7440 | . . . . . . 7
⊢ ((𝑁 mod (abs‘𝑀)) = 0 → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) = (𝐴 Yrm 0)) | 
| 28 | 27 | breq2d 5154 | . . . . . 6
⊢ ((𝑁 mod (abs‘𝑀)) = 0 → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 0))) | 
| 29 | 26, 28 | syl5ibrcom 247 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 mod (abs‘𝑀)) = 0 → (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))))) | 
| 30 | 29 | adantr 480 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 mod (abs‘𝑀)) = 0 → (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))))) | 
| 31 |  | zre 12619 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 32 | 31 | 3ad2ant3 1135 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ) | 
| 33 | 32 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑁 ∈ ℝ) | 
| 34 |  | zcn 12620 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) | 
| 35 | 34 | 3ad2ant2 1134 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℂ) | 
| 36 | 35 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑀 ∈ ℂ) | 
| 37 |  | simplr 768 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑀 ≠ 0) | 
| 38 | 36, 37 | absrpcld 15488 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘𝑀) ∈
ℝ+) | 
| 39 |  | modlt 13921 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧
(abs‘𝑀) ∈
ℝ+) → (𝑁 mod (abs‘𝑀)) < (abs‘𝑀)) | 
| 40 | 33, 38, 39 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) < (abs‘𝑀)) | 
| 41 |  | simpll1 1212 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝐴 ∈
(ℤ≥‘2)) | 
| 42 |  | simpll3 1214 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑁 ∈ ℤ) | 
| 43 |  | simpll2 1213 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑀 ∈ ℤ) | 
| 44 |  | nnabscl 15365 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℕ) | 
| 45 | 43, 37, 44 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘𝑀) ∈
ℕ) | 
| 46 | 42, 45 | zmodcld 13933 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈
ℕ0) | 
| 47 |  | nn0abscl 15352 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ →
(abs‘𝑀) ∈
ℕ0) | 
| 48 | 47 | 3ad2ant2 1134 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘𝑀) ∈
ℕ0) | 
| 49 | 48 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘𝑀) ∈
ℕ0) | 
| 50 |  | ltrmynn0 42965 | . . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑁 mod (abs‘𝑀)) ∈ ℕ0 ∧
(abs‘𝑀) ∈
ℕ0) → ((𝑁 mod (abs‘𝑀)) < (abs‘𝑀) ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) < (𝐴 Yrm (abs‘𝑀)))) | 
| 51 | 41, 46, 49, 50 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((𝑁 mod (abs‘𝑀)) < (abs‘𝑀) ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) < (𝐴 Yrm (abs‘𝑀)))) | 
| 52 | 40, 51 | mpbid 232 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) < (𝐴 Yrm (abs‘𝑀))) | 
| 53 | 46 | nn0zd 12641 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℤ) | 
| 54 |  | rmyabs 42975 | . . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑁 mod (abs‘𝑀)) ∈ ℤ) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) = (𝐴 Yrm (abs‘(𝑁 mod (abs‘𝑀))))) | 
| 55 | 41, 53, 54 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) = (𝐴 Yrm (abs‘(𝑁 mod (abs‘𝑀))))) | 
| 56 | 33, 38 | modcld 13916 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℝ) | 
| 57 |  | modge0 13920 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧
(abs‘𝑀) ∈
ℝ+) → 0 ≤ (𝑁 mod (abs‘𝑀))) | 
| 58 | 33, 38, 57 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 0 ≤ (𝑁 mod (abs‘𝑀))) | 
| 59 | 56, 58 | absidd 15462 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝑁 mod (abs‘𝑀))) = (𝑁 mod (abs‘𝑀))) | 
| 60 | 59 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm (abs‘(𝑁 mod (abs‘𝑀)))) = (𝐴 Yrm (𝑁 mod (abs‘𝑀)))) | 
| 61 | 55, 60 | eqtrd 2776 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) = (𝐴 Yrm (𝑁 mod (abs‘𝑀)))) | 
| 62 |  | rmyabs 42975 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (abs‘(𝐴 Yrm 𝑀)) = (𝐴 Yrm (abs‘𝑀))) | 
| 63 | 41, 43, 62 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm 𝑀)) = (𝐴 Yrm (abs‘𝑀))) | 
| 64 | 52, 61, 63 | 3brtr4d 5174 | . . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) < (abs‘(𝐴 Yrm 𝑀))) | 
| 65 | 5 | fovcl 7562 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑁 mod (abs‘𝑀)) ∈ ℤ) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ∈ ℤ) | 
| 66 | 41, 53, 65 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ∈ ℤ) | 
| 67 |  | nn0abscl 15352 | . . . . . . . . . . 11
⊢ ((𝐴 Yrm (𝑁 mod (abs‘𝑀))) ∈ ℤ →
(abs‘(𝐴
Yrm (𝑁 mod
(abs‘𝑀)))) ∈
ℕ0) | 
| 68 | 66, 67 | syl 17 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) ∈
ℕ0) | 
| 69 | 68 | nn0red 12590 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) ∈
ℝ) | 
| 70 | 22 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm 𝑀) ∈ ℤ) | 
| 71 |  | nn0abscl 15352 | . . . . . . . . . . 11
⊢ ((𝐴 Yrm 𝑀) ∈ ℤ →
(abs‘(𝐴
Yrm 𝑀)) ∈
ℕ0) | 
| 72 | 70, 71 | syl 17 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm 𝑀)) ∈
ℕ0) | 
| 73 | 72 | nn0red 12590 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm 𝑀)) ∈
ℝ) | 
| 74 | 69, 73 | ltnled 11409 | . . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) < (abs‘(𝐴 Yrm 𝑀)) ↔ ¬
(abs‘(𝐴
Yrm 𝑀)) ≤
(abs‘(𝐴
Yrm (𝑁 mod
(abs‘𝑀)))))) | 
| 75 | 64, 74 | mpbid 232 | . . . . . . 7
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ¬ (abs‘(𝐴 Yrm 𝑀)) ≤ (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀))))) | 
| 76 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) ≠ 0) | 
| 77 |  | rmyeq0 42970 | . . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑁 mod (abs‘𝑀)) ∈ ℤ) → ((𝑁 mod (abs‘𝑀)) = 0 ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) = 0)) | 
| 78 | 41, 53, 77 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((𝑁 mod (abs‘𝑀)) = 0 ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) = 0)) | 
| 79 | 78 | necon3bid 2984 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((𝑁 mod (abs‘𝑀)) ≠ 0 ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ≠ 0)) | 
| 80 | 76, 79 | mpbid 232 | . . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ≠ 0) | 
| 81 |  | dvdsleabs2 16350 | . . . . . . . 8
⊢ (((𝐴 Yrm 𝑀) ∈ ℤ ∧ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ∈ ℤ ∧ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) → (abs‘(𝐴 Yrm 𝑀)) ≤ (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))))) | 
| 82 | 70, 66, 80, 81 | syl3anc 1372 | . . . . . . 7
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) → (abs‘(𝐴 Yrm 𝑀)) ≤ (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))))) | 
| 83 | 75, 82 | mtod 198 | . . . . . 6
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ¬ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀)))) | 
| 84 | 83 | ex 412 | . . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 mod (abs‘𝑀)) ≠ 0 → ¬ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))))) | 
| 85 | 84 | necon4ad 2958 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) → (𝑁 mod (abs‘𝑀)) = 0)) | 
| 86 | 30, 85 | impbid 212 | . . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 mod (abs‘𝑀)) = 0 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))))) | 
| 87 |  | simpl2 1192 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑀 ∈ ℤ) | 
| 88 |  | simpl3 1193 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑁 ∈ ℤ) | 
| 89 |  | simpr 484 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑀 ≠ 0) | 
| 90 |  | dvdsabsmod0 43004 | . . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝑁 mod (abs‘𝑀)) = 0)) | 
| 91 | 87, 88, 89, 90 | syl3anc 1372 | . . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝑁 mod (abs‘𝑀)) = 0)) | 
| 92 |  | simpl1 1191 | . . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝐴 ∈
(ℤ≥‘2)) | 
| 93 | 32 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑁 ∈ ℝ) | 
| 94 |  | zre 12619 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) | 
| 95 | 94 | 3ad2ant2 1134 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℝ) | 
| 96 | 95 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑀 ∈ ℝ) | 
| 97 |  | modabsdifz 43003 | . . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≠ 0) → ((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ) | 
| 98 | 93, 96, 89, 97 | syl3anc 1372 | . . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ) | 
| 99 | 98 | znegcld 12726 | . . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → -((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ) | 
| 100 |  | jm2.19lem4 43009 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ -((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀))))) | 
| 101 | 92, 87, 88, 99, 100 | syl121anc 1376 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀))))) | 
| 102 | 32 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℂ) | 
| 103 | 102 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑁 ∈ ℂ) | 
| 104 | 35 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑀 ∈ ℂ) | 
| 105 | 104, 89 | absrpcld 15488 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℝ+) | 
| 106 | 93, 105 | modcld 13916 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℝ) | 
| 107 | 106 | recnd 11290 | . . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℂ) | 
| 108 | 103, 107 | subcld 11621 | . . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 − (𝑁 mod (abs‘𝑀))) ∈ ℂ) | 
| 109 | 108, 104,
89 | divcld 12044 | . . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℂ) | 
| 110 | 109, 104 | mulneg1d 11717 | . . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀) = -(((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) | 
| 111 | 110 | oveq2d 7448 | . . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) = (𝑁 + -(((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀))) | 
| 112 | 109, 104 | mulcld 11282 | . . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀) ∈ ℂ) | 
| 113 | 103, 112 | negsubd 11627 | . . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 + -(((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) = (𝑁 − (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀))) | 
| 114 | 108, 104,
89 | divcan1d 12045 | . . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀) = (𝑁 − (𝑁 mod (abs‘𝑀)))) | 
| 115 | 114 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 − (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) = (𝑁 − (𝑁 − (𝑁 mod (abs‘𝑀))))) | 
| 116 | 103, 107 | nncand 11626 | . . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 − (𝑁 − (𝑁 mod (abs‘𝑀)))) = (𝑁 mod (abs‘𝑀))) | 
| 117 | 115, 116 | eqtrd 2776 | . . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 − (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) = (𝑁 mod (abs‘𝑀))) | 
| 118 | 111, 113,
117 | 3eqtrrd 2781 | . . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 mod (abs‘𝑀)) = (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀))) | 
| 119 | 118 | oveq2d 7448 | . . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) = (𝐴 Yrm (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)))) | 
| 120 | 119 | breq2d 5154 | . . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀))))) | 
| 121 | 101, 120 | bitr4d 282 | . . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))))) | 
| 122 | 86, 91, 121 | 3bitr4d 311 | . 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁))) | 
| 123 | 20, 122 | pm2.61dane 3028 | 1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁))) |