Step | Hyp | Ref
| Expression |
1 | | simplr 525 |
. . . 4
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → 𝐶 ∈ ℤ) |
2 | | dvdszrcl 11754 |
. . . . . 6
⊢ (𝐴 ∥ (𝐵 · 𝐶) → (𝐴 ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ)) |
3 | 2 | adantl 275 |
. . . . 5
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → (𝐴 ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ)) |
4 | 3 | simpld 111 |
. . . 4
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → 𝐴 ∈ ℤ) |
5 | | bezout 11966 |
. . . 4
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
(𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦))) |
6 | 1, 4, 5 | syl2anc 409 |
. . 3
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦))) |
7 | 4 | adantr 274 |
. . . . . . 7
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∈ ℤ) |
8 | | simplll 528 |
. . . . . . . 8
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐵 ∈ ℤ) |
9 | | simpllr 529 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐶 ∈ ℤ) |
10 | | simprl 526 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈ ℤ) |
11 | 9, 10 | zmulcld 9340 |
. . . . . . . 8
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐶 · 𝑥) ∈ ℤ) |
12 | 8, 11 | zmulcld 9340 |
. . . . . . 7
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐶 · 𝑥)) ∈ ℤ) |
13 | | simprr 527 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℤ) |
14 | 7, 13 | zmulcld 9340 |
. . . . . . . 8
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐴 · 𝑦) ∈ ℤ) |
15 | 8, 14 | zmulcld 9340 |
. . . . . . 7
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐴 · 𝑦)) ∈ ℤ) |
16 | | simplr 525 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · 𝐶)) |
17 | 8, 9 | zmulcld 9340 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · 𝐶) ∈ ℤ) |
18 | | dvdsmultr1 11793 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) → 𝐴 ∥ ((𝐵 · 𝐶) · 𝑥))) |
19 | 7, 17, 10, 18 | syl3anc 1233 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐴 ∥ (𝐵 · 𝐶) → 𝐴 ∥ ((𝐵 · 𝐶) · 𝑥))) |
20 | 16, 19 | mpd 13 |
. . . . . . . 8
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ ((𝐵 · 𝐶) · 𝑥)) |
21 | 8 | zcnd 9335 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐵 ∈ ℂ) |
22 | 9 | zcnd 9335 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐶 ∈ ℂ) |
23 | 10 | zcnd 9335 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈ ℂ) |
24 | 21, 22, 23 | mulassd 7943 |
. . . . . . . 8
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝐵 · 𝐶) · 𝑥) = (𝐵 · (𝐶 · 𝑥))) |
25 | 20, 24 | breqtrd 4015 |
. . . . . . 7
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · (𝐶 · 𝑥))) |
26 | 8, 13 | zmulcld 9340 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · 𝑦) ∈ ℤ) |
27 | | dvdsmul1 11775 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 · 𝑦) ∈ ℤ) → 𝐴 ∥ (𝐴 · (𝐵 · 𝑦))) |
28 | 7, 26, 27 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐴 · (𝐵 · 𝑦))) |
29 | 7 | zcnd 9335 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∈ ℂ) |
30 | 13 | zcnd 9335 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℂ) |
31 | 21, 29, 30 | mul12d 8071 |
. . . . . . . 8
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐴 · 𝑦)) = (𝐴 · (𝐵 · 𝑦))) |
32 | 28, 31 | breqtrrd 4017 |
. . . . . . 7
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · (𝐴 · 𝑦))) |
33 | | dvds2add 11787 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 · (𝐶 · 𝑥)) ∈ ℤ ∧ (𝐵 · (𝐴 · 𝑦)) ∈ ℤ) → ((𝐴 ∥ (𝐵 · (𝐶 · 𝑥)) ∧ 𝐴 ∥ (𝐵 · (𝐴 · 𝑦))) → 𝐴 ∥ ((𝐵 · (𝐶 · 𝑥)) + (𝐵 · (𝐴 · 𝑦))))) |
34 | 33 | imp 123 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 · (𝐶 · 𝑥)) ∈ ℤ ∧ (𝐵 · (𝐴 · 𝑦)) ∈ ℤ) ∧ (𝐴 ∥ (𝐵 · (𝐶 · 𝑥)) ∧ 𝐴 ∥ (𝐵 · (𝐴 · 𝑦)))) → 𝐴 ∥ ((𝐵 · (𝐶 · 𝑥)) + (𝐵 · (𝐴 · 𝑦)))) |
35 | 7, 12, 15, 25, 32, 34 | syl32anc 1241 |
. . . . . 6
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ ((𝐵 · (𝐶 · 𝑥)) + (𝐵 · (𝐴 · 𝑦)))) |
36 | 11 | zcnd 9335 |
. . . . . . 7
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐶 · 𝑥) ∈ ℂ) |
37 | 14 | zcnd 9335 |
. . . . . . 7
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐴 · 𝑦) ∈ ℂ) |
38 | 21, 36, 37 | adddid 7944 |
. . . . . 6
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦))) = ((𝐵 · (𝐶 · 𝑥)) + (𝐵 · (𝐴 · 𝑦)))) |
39 | 35, 38 | breqtrrd 4017 |
. . . . 5
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦)))) |
40 | | oveq2 5861 |
. . . . . 6
⊢ ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → (𝐵 · (𝐶 gcd 𝐴)) = (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦)))) |
41 | 40 | breq2d 4001 |
. . . . 5
⊢ ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → (𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)) ↔ 𝐴 ∥ (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦))))) |
42 | 39, 41 | syl5ibrcom 156 |
. . . 4
⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))) |
43 | 42 | rexlimdvva 2595 |
. . 3
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))) |
44 | 6, 43 | mpd 13 |
. 2
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) |
45 | | dvdszrcl 11754 |
. . . . 5
⊢ (𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)) → (𝐴 ∈ ℤ ∧ (𝐵 · (𝐶 gcd 𝐴)) ∈ ℤ)) |
46 | 45 | adantl 275 |
. . . 4
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐴 ∈ ℤ ∧ (𝐵 · (𝐶 gcd 𝐴)) ∈ ℤ)) |
47 | 46 | simpld 111 |
. . 3
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐴 ∈ ℤ) |
48 | 46 | simprd 113 |
. . 3
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐵 · (𝐶 gcd 𝐴)) ∈ ℤ) |
49 | | zmulcl 9265 |
. . . 4
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ) |
50 | 49 | adantr 274 |
. . 3
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐵 · 𝐶) ∈ ℤ) |
51 | | simpr 109 |
. . 3
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) |
52 | | simplr 525 |
. . . . . 6
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐶 ∈ ℤ) |
53 | | gcddvds 11918 |
. . . . . 6
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐶 gcd 𝐴) ∥ 𝐶 ∧ (𝐶 gcd 𝐴) ∥ 𝐴)) |
54 | 52, 47, 53 | syl2anc 409 |
. . . . 5
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → ((𝐶 gcd 𝐴) ∥ 𝐶 ∧ (𝐶 gcd 𝐴) ∥ 𝐴)) |
55 | 54 | simpld 111 |
. . . 4
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∥ 𝐶) |
56 | 52, 47 | gcdcld 11923 |
. . . . . 6
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∈
ℕ0) |
57 | 56 | nn0zd 9332 |
. . . . 5
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∈ ℤ) |
58 | | simpll 524 |
. . . . 5
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐵 ∈ ℤ) |
59 | | dvdscmul 11780 |
. . . . 5
⊢ (((𝐶 gcd 𝐴) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐶 gcd 𝐴) ∥ 𝐶 → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶))) |
60 | 57, 52, 58, 59 | syl3anc 1233 |
. . . 4
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → ((𝐶 gcd 𝐴) ∥ 𝐶 → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶))) |
61 | 55, 60 | mpd 13 |
. . 3
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶)) |
62 | | dvdstr 11790 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 · (𝐶 gcd 𝐴)) ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ) → ((𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)) ∧ (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶)) → 𝐴 ∥ (𝐵 · 𝐶))) |
63 | 62 | imp 123 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 · (𝐶 gcd 𝐴)) ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ) ∧ (𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)) ∧ (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶))) → 𝐴 ∥ (𝐵 · 𝐶)) |
64 | 47, 48, 50, 51, 61, 63 | syl32anc 1241 |
. 2
⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐴 ∥ (𝐵 · 𝐶)) |
65 | 44, 64 | impbida 591 |
1
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))) |