Step |
Hyp |
Ref |
Expression |
1 |
|
0z |
⊢ 0 ∈ ℤ |
2 |
|
dvds0 |
⊢ ( 0 ∈ ℤ → 0 ∥ 0 ) |
3 |
1 2
|
ax-mp |
⊢ 0 ∥ 0 |
4 |
|
breq2 |
⊢ ( 𝑀 = 0 → ( 0 ∥ 𝑀 ↔ 0 ∥ 0 ) ) |
5 |
|
breq2 |
⊢ ( 𝑁 = 0 → ( 0 ∥ 𝑁 ↔ 0 ∥ 0 ) ) |
6 |
4 5
|
bi2anan9 |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 0 ∥ 𝑀 ∧ 0 ∥ 𝑁 ) ↔ ( 0 ∥ 0 ∧ 0 ∥ 0 ) ) ) |
7 |
|
anidm |
⊢ ( ( 0 ∥ 0 ∧ 0 ∥ 0 ) ↔ 0 ∥ 0 ) |
8 |
6 7
|
bitrdi |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 0 ∥ 𝑀 ∧ 0 ∥ 𝑁 ) ↔ 0 ∥ 0 ) ) |
9 |
3 8
|
mpbiri |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 0 ∥ 𝑀 ∧ 0 ∥ 𝑁 ) ) |
10 |
|
oveq12 |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = ( 0 gcd 0 ) ) |
11 |
|
gcd0val |
⊢ ( 0 gcd 0 ) = 0 |
12 |
10 11
|
eqtrdi |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = 0 ) |
13 |
12
|
breq1d |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ↔ 0 ∥ 𝑀 ) ) |
14 |
12
|
breq1d |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ↔ 0 ∥ 𝑁 ) ) |
15 |
13 14
|
anbi12d |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ↔ ( 0 ∥ 𝑀 ∧ 0 ∥ 𝑁 ) ) ) |
16 |
9 15
|
mpbird |
⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ) |
17 |
16
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ) |
18 |
|
eqid |
⊢ { 𝑛 ∈ ℤ ∣ ∀ 𝑧 ∈ { 𝑀 , 𝑁 } 𝑛 ∥ 𝑧 } = { 𝑛 ∈ ℤ ∣ ∀ 𝑧 ∈ { 𝑀 , 𝑁 } 𝑛 ∥ 𝑧 } |
19 |
|
eqid |
⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } = { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } |
20 |
18 19
|
gcdcllem3 |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∈ ℕ ∧ ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑀 ∧ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑁 ) ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) ) ) |
21 |
20
|
simp2d |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑀 ∧ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑁 ) ) |
22 |
|
gcdn0val |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) |
23 |
22
|
breq1d |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ↔ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑀 ) ) |
24 |
22
|
breq1d |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ↔ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑁 ) ) |
25 |
23 24
|
anbi12d |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ↔ ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑀 ∧ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑁 ) ) ) |
26 |
21 25
|
mpbird |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ) |
27 |
17 26
|
pm2.61dan |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ) |