Step |
Hyp |
Ref |
Expression |
1 |
|
gcdcl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ0 ) |
2 |
1
|
nn0zd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ ) |
3 |
2
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ ) |
4 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → 𝐴 ∈ ℤ ) |
5 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → 𝑋 ∈ ℤ ) |
6 |
4 5
|
zmulcld |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 · 𝑋 ) ∈ ℤ ) |
7 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → 𝐵 ∈ ℤ ) |
8 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → 𝑌 ∈ ℤ ) |
9 |
7 8
|
zmulcld |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐵 · 𝑌 ) ∈ ℤ ) |
10 |
|
gcddvds |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) |
11 |
10
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) |
12 |
11
|
simpld |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ) |
13 |
3 4 5 12
|
dvdsmultr1d |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( 𝐴 · 𝑋 ) ) |
14 |
11
|
simprd |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) |
15 |
3 7 8 14
|
dvdsmultr1d |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( 𝐵 · 𝑌 ) ) |
16 |
3 6 9 13 15
|
dvds2addd |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ) |