Proof of Theorem divgcdcoprmex
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . 5
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → 𝐵 ∈
ℤ) |
2 | 1 | anim2i 620 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 ∈ ℤ ∧ 𝐵 ∈
ℤ)) |
3 | | zeqzmulgcd 15946 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
∃𝑎 ∈ ℤ
𝐴 = (𝑎 · (𝐴 gcd 𝐵))) |
4 | 2, 3 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → ∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵))) |
5 | 4 | 3adant3 1133 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵))) |
6 | | zeqzmulgcd 15946 |
. . . . 5
⊢ ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ) →
∃𝑏 ∈ ℤ
𝐵 = (𝑏 · (𝐵 gcd 𝐴))) |
7 | 6 | adantlr 715 |
. . . 4
⊢ (((𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝐴 ∈ ℤ) → ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) |
8 | 7 | ancoms 462 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) |
9 | 8 | 3adant3 1133 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) |
10 | | reeanv 3269 |
. . 3
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) ↔ (∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) |
11 | | zcn 12060 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) |
12 | 11 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → 𝑎 ∈ ℂ) |
13 | | gcdcl 15942 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈
ℕ0) |
14 | 2, 13 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 gcd 𝐵) ∈
ℕ0) |
15 | 14 | nn0cnd 12031 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 gcd 𝐵) ∈ ℂ) |
16 | 15 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ∈ ℂ) |
17 | 16 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℂ) |
18 | 12, 17 | mulcomd 10733 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → (𝑎 · (𝐴 gcd 𝐵)) = ((𝐴 gcd 𝐵) · 𝑎)) |
19 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝑀 = (𝐴 gcd 𝐵)) |
20 | 19 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) = 𝑀) |
21 | 20 | oveq1d 7179 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ((𝐴 gcd 𝐵) · 𝑎) = (𝑀 · 𝑎)) |
22 | 21 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → ((𝐴 gcd 𝐵) · 𝑎) = (𝑀 · 𝑎)) |
23 | 18, 22 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎)) |
24 | 23 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ (𝐵 ∈
ℤ ∧ 𝐵 ≠ 0)
∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎)) |
25 | | eqeq1 2742 |
. . . . . . . . . 10
⊢ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) → (𝐴 = (𝑀 · 𝑎) ↔ (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎))) |
26 | 25 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → (𝐴 = (𝑀 · 𝑎) ↔ (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎))) |
27 | 26 | adantl 485 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ (𝐵 ∈
ℤ ∧ 𝐵 ≠ 0)
∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → (𝐴 = (𝑀 · 𝑎) ↔ (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎))) |
28 | 24, 27 | mpbird 260 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ (𝐵 ∈
ℤ ∧ 𝐵 ≠ 0)
∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → 𝐴 = (𝑀 · 𝑎)) |
29 | | simpr 488 |
. . . . . . . 8
⊢ ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) |
30 | 2 | ancomd 465 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐵 ∈ ℤ ∧ 𝐴 ∈
ℤ)) |
31 | | gcdcom 15949 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐵 gcd 𝐴) = (𝐴 gcd 𝐵)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐵 gcd 𝐴) = (𝐴 gcd 𝐵)) |
33 | 32 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐵 gcd 𝐴) = (𝐴 gcd 𝐵)) |
34 | 33 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝑏 · (𝐵 gcd 𝐴)) = (𝑏 · (𝐴 gcd 𝐵))) |
35 | 34 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐵 gcd 𝐴)) = (𝑏 · (𝐴 gcd 𝐵))) |
36 | | zcn 12060 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) |
37 | 36 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℂ) |
38 | 14 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ∈
ℕ0) |
39 | 38 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ∈
ℕ0) |
40 | 39 | nn0cnd 12031 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℂ) |
41 | 37, 40 | mulcomd 10733 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐴 gcd 𝐵)) = ((𝐴 gcd 𝐵) · 𝑏)) |
42 | 20 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) = 𝑀) |
43 | 42 | oveq1d 7179 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → ((𝐴 gcd 𝐵) · 𝑏) = (𝑀 · 𝑏)) |
44 | 35, 41, 43 | 3eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐵 gcd 𝐴)) = (𝑀 · 𝑏)) |
45 | 44 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐵 gcd 𝐴)) = (𝑀 · 𝑏)) |
46 | 29, 45 | sylan9eqr 2795 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ (𝐵 ∈
ℤ ∧ 𝐵 ≠ 0)
∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → 𝐵 = (𝑀 · 𝑏)) |
47 | | zcn 12060 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
48 | 47 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝐴 ∈ ℂ) |
49 | 48 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝐴 ∈ ℂ) |
50 | 12 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑎 ∈ ℂ) |
51 | | simp1 1137 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝐴 ∈ ℤ) |
52 | 1 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝐵 ∈ ℤ) |
53 | 51, 52 | gcdcld 15944 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ∈
ℕ0) |
54 | 53 | nn0cnd 12031 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ∈ ℂ) |
55 | 54 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℂ) |
56 | | gcdeq0 15953 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
57 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐵 = 0) |
58 | 56, 57 | syl6bi 256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 → 𝐵 = 0)) |
59 | 58 | necon3d 2955 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≠ 0 → (𝐴 gcd 𝐵) ≠ 0)) |
60 | 59 | impr 458 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 gcd 𝐵) ≠ 0) |
61 | 60 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ≠ 0) |
62 | 61 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ≠ 0) |
63 | 49, 50, 55, 62 | divmul3d 11521 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ↔ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)))) |
64 | 63 | bicomd 226 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ↔ (𝐴 / (𝐴 gcd 𝐵)) = 𝑎)) |
65 | | zcn 12060 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) |
66 | 65 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → 𝐵 ∈
ℂ) |
67 | 66 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝐵 ∈ ℂ) |
68 | 67 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝐵 ∈ ℂ) |
69 | 36 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℂ) |
70 | 68, 69, 55, 62 | divmul3d 11521 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐵 / (𝐴 gcd 𝐵)) = 𝑏 ↔ 𝐵 = (𝑏 · (𝐴 gcd 𝐵)))) |
71 | 2 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) |
72 | | gcdcom 15949 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴)) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴)) |
74 | 73 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴)) |
75 | 74 | oveq2d 7180 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐴 gcd 𝐵)) = (𝑏 · (𝐵 gcd 𝐴))) |
76 | 75 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐵 = (𝑏 · (𝐴 gcd 𝐵)) ↔ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) |
77 | 70, 76 | bitr2d 283 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐵 = (𝑏 · (𝐵 gcd 𝐴)) ↔ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏)) |
78 | 64, 77 | anbi12d 634 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) ↔ ((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏))) |
79 | | 3anass 1096 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ↔ (𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0))) |
80 | 79 | biimpri 231 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) |
81 | 80 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) |
82 | | divgcdcoprm0 16099 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1) |
84 | | oveq12 7173 |
. . . . . . . . . . . 12
⊢ (((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = (𝑎 gcd 𝑏)) |
85 | 84 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏) → (((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ↔ (𝑎 gcd 𝑏) = 1)) |
86 | 83, 85 | syl5ibcom 248 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏) → (𝑎 gcd 𝑏) = 1)) |
87 | 86 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏) → (𝑎 gcd 𝑏) = 1)) |
88 | 78, 87 | sylbid 243 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → (𝑎 gcd 𝑏) = 1)) |
89 | 88 | imp 410 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ (𝐵 ∈
ℤ ∧ 𝐵 ≠ 0)
∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → (𝑎 gcd 𝑏) = 1) |
90 | 28, 46, 89 | 3jca 1129 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ (𝐵 ∈
ℤ ∧ 𝐵 ≠ 0)
∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1)) |
91 | 90 | ex 416 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1))) |
92 | 91 | reximdva 3183 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1))) |
93 | 92 | reximdva 3183 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1))) |
94 | 10, 93 | syl5bir 246 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ((∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1))) |
95 | 5, 9, 94 | mp2and 699 |
1
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1)) |