divgcdcoprmex - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > divgcdcoprmex		GIF version

Theorem divgcdcoprmex 12116

Description: Integers divided by gcd are coprime (see ProofWiki "Integers Divided by GCD are Coprime", 11-Jul-2021, https://proofwiki.org/wiki/Integers_Divided_by_GCD_are_Coprime): Any pair of integers, not both zero, can be reduced to a pair of coprime ones by dividing them by their gcd. (Contributed by AV, 12-Jul-2021.)

**Assertion**
Ref	Expression
divgcdcoprmex	⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1))

Distinct variable groups: 𝐴,𝑎,𝑏 𝐵,𝑎,𝑏 𝑀,𝑎,𝑏

**Proof of Theorem divgcdcoprmex**
Step	Hyp	Ref	Expression
1		simpl 109	. . . . 5 ⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℤ)
2	1	anim2i 342	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
3		zeqzmulgcd 11985	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)))
4	2, 3	syl 14	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → ∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)))
5	4	3adant3 1018	. 2 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)))
6		zeqzmulgcd 11985	. . . . 5 ⊢ ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))
7	6	adantlr 477	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝐴 ∈ ℤ) → ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))
8	7	ancoms 268	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))
9	8	3adant3 1018	. 2 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))
10		reeanv 2657	. . 3 ⊢ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) ↔ (∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))))
11		zcn 9272	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
12	11	adantl 277	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → 𝑎 ∈ ℂ)
13		gcdcl 11981	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
14	2, 13	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 gcd 𝐵) ∈ ℕ₀)
15	14	nn0cnd 9245	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 gcd 𝐵) ∈ ℂ)
16	15	3adant3 1018	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ∈ ℂ)
17	16	adantr 276	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℂ)
18	12, 17	mulcomd 7993	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → (𝑎 · (𝐴 gcd 𝐵)) = ((𝐴 gcd 𝐵) · 𝑎))
19		simp3 1000	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝑀 = (𝐴 gcd 𝐵))
20	19	eqcomd 2193	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) = 𝑀)
21	20	oveq1d 5903	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ((𝐴 gcd 𝐵) · 𝑎) = (𝑀 · 𝑎))
22	21	adantr 276	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → ((𝐴 gcd 𝐵) · 𝑎) = (𝑀 · 𝑎))
23	18, 22	eqtrd 2220	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎))
24	23	ad2antrr 488	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎))
25		eqeq1 2194	. . . . . . . . . 10 ⊢ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) → (𝐴 = (𝑀 · 𝑎) ↔ (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎)))
26	25	adantr 276	. . . . . . . . 9 ⊢ ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → (𝐴 = (𝑀 · 𝑎) ↔ (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎)))
27	26	adantl 277	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → (𝐴 = (𝑀 · 𝑎) ↔ (𝑎 · (𝐴 gcd 𝐵)) = (𝑀 · 𝑎)))
28	24, 27	mpbird 167	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → 𝐴 = (𝑀 · 𝑎))
29		simpr 110	. . . . . . . 8 ⊢ ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))
30	2	ancomd 267	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ))
31		gcdcom 11988	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐵 gcd 𝐴) = (𝐴 gcd 𝐵))
32	30, 31	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐵 gcd 𝐴) = (𝐴 gcd 𝐵))
33	32	3adant3 1018	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐵 gcd 𝐴) = (𝐴 gcd 𝐵))
34	33	oveq2d 5904	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝑏 · (𝐵 gcd 𝐴)) = (𝑏 · (𝐴 gcd 𝐵)))
35	34	adantr 276	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐵 gcd 𝐴)) = (𝑏 · (𝐴 gcd 𝐵)))
36		zcn 9272	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ℤ → 𝑏 ∈ ℂ)
37	36	adantl 277	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℂ)
38	14	3adant3 1018	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ∈ ℕ₀)
39	38	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
40	39	nn0cnd 9245	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℂ)
41	37, 40	mulcomd 7993	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐴 gcd 𝐵)) = ((𝐴 gcd 𝐵) · 𝑏))
42	20	adantr 276	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) = 𝑀)
43	42	oveq1d 5903	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → ((𝐴 gcd 𝐵) · 𝑏) = (𝑀 · 𝑏))
44	35, 41, 43	3eqtrd 2224	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐵 gcd 𝐴)) = (𝑀 · 𝑏))
45	44	adantlr 477	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐵 gcd 𝐴)) = (𝑀 · 𝑏))
46	29, 45	sylan9eqr 2242	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → 𝐵 = (𝑀 · 𝑏))
47		zcn 9272	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
48	47	3ad2ant1 1019	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝐴 ∈ ℂ)
49	48	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝐴 ∈ ℂ)
50	12	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑎 ∈ ℂ)
51		simp1 998	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝐴 ∈ ℤ)
52	1	3ad2ant2 1020	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝐵 ∈ ℤ)
53	51, 52	gcdcld 11983	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ∈ ℕ₀)
54	53	nn0cnd 9245	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ∈ ℂ)
55	54	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℂ)
56		gcdeq0 11992	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
57		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐵 = 0)
58	56, 57	biimtrdi 163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 → 𝐵 = 0))
59	58	necon3d 2401	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≠ 0 → (𝐴 gcd 𝐵) ≠ 0))
60	59	impr 379	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 gcd 𝐵) ≠ 0)
61	60	3adant3 1018	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) ≠ 0)
62	61	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ≠ 0)
63	38	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
64	63	nn0zd 9387	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ)
65		0zd 9279	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 0 ∈ ℤ)
66		zapne 9341	. . . . . . . . . . . . . 14 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝐴 gcd 𝐵) # 0 ↔ (𝐴 gcd 𝐵) ≠ 0))
67	64, 65, 66	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 gcd 𝐵) # 0 ↔ (𝐴 gcd 𝐵) ≠ 0))
68	62, 67	mpbird 167	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) # 0)
69	49, 50, 55, 68	divmulap3d 8796	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ↔ 𝐴 = (𝑎 · (𝐴 gcd 𝐵))))
70	69	bicomd 141	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ↔ (𝐴 / (𝐴 gcd 𝐵)) = 𝑎))
71		zcn 9272	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℂ)
72	71	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
73	72	3ad2ant2 1020	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → 𝐵 ∈ ℂ)
74	73	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝐵 ∈ ℂ)
75	36	adantl 277	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℂ)
76	74, 75, 55, 68	divmulap3d 8796	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐵 / (𝐴 gcd 𝐵)) = 𝑏 ↔ 𝐵 = (𝑏 · (𝐴 gcd 𝐵))))
77	2	3adant3 1018	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
78		gcdcom 11988	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
79	77, 78	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
80	79	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
81	80	oveq2d 5904	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑏 · (𝐴 gcd 𝐵)) = (𝑏 · (𝐵 gcd 𝐴)))
82	81	eqeq2d 2199	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐵 = (𝑏 · (𝐴 gcd 𝐵)) ↔ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))))
83	76, 82	bitr2d 189	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝐵 = (𝑏 · (𝐵 gcd 𝐴)) ↔ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏))
84	70, 83	anbi12d 473	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) ↔ ((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏)))
85		3anass 983	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ↔ (𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)))
86	85	biimpri 133	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0))
87	86	3adant3 1018	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0))
88		divgcdcoprm0 12115	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)
89	87, 88	syl 14	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)
90		oveq12 5897	. . . . . . . . . . . 12 ⊢ (((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = (𝑎 gcd 𝑏))
91	90	eqeq1d 2196	. . . . . . . . . . 11 ⊢ (((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏) → (((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ↔ (𝑎 gcd 𝑏) = 1))
92	89, 91	syl5ibcom 155	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏) → (𝑎 gcd 𝑏) = 1))
93	92	ad2antrr 488	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ∧ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏) → (𝑎 gcd 𝑏) = 1))
94	84, 93	sylbid 150	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → (𝑎 gcd 𝑏) = 1))
95	94	imp 124	. . . . . . 7 ⊢ (((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → (𝑎 gcd 𝑏) = 1)
96	28, 46, 95	3jca 1178	. . . . . 6 ⊢ (((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴)))) → (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1))
97	96	ex 115	. . . . 5 ⊢ ((((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1)))
98	97	reximdva 2589	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) ∧ 𝑎 ∈ ℤ) → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1)))
99	98	reximdva 2589	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1)))
100	10, 99	biimtrrid 153	. 2 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ((∃𝑎 ∈ ℤ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)) ∧ ∃𝑏 ∈ ℤ 𝐵 = (𝑏 · (𝐵 gcd 𝐴))) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1)))
101	5, 9, 100	mp2and 433	1 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 979 = wceq 1363 ∈ wcel 2158 ≠ wne 2357 ∃wrex 2466 class class class wbr 4015 (class class class)co 5888 ℂcc 7823 0cc0 7825 1c1 7826 · cmul 7830 # cap 8552 / cdiv 8643 ℕ₀cn0 9190 ℤcz 9267 gcd cgcd 11957

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-coll 4130 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-iinf 4599 ax-cnex 7916 ax-resscn 7917 ax-1cn 7918 ax-1re 7919 ax-icn 7920 ax-addcl 7921 ax-addrcl 7922 ax-mulcl 7923 ax-mulrcl 7924 ax-addcom 7925 ax-mulcom 7926 ax-addass 7927 ax-mulass 7928 ax-distr 7929 ax-i2m1 7930 ax-0lt1 7931 ax-1rid 7932 ax-0id 7933 ax-rnegex 7934 ax-precex 7935 ax-cnre 7936 ax-pre-ltirr 7937 ax-pre-ltwlin 7938 ax-pre-lttrn 7939 ax-pre-apti 7940 ax-pre-ltadd 7941 ax-pre-mulgt0 7942 ax-pre-mulext 7943 ax-arch 7944 ax-caucvg 7945

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rmo 2473 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-tr 4114 df-id 4305 df-po 4308 df-iso 4309 df-iord 4378 df-on 4380 df-ilim 4381 df-suc 4383 df-iom 4602 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 df-fv 5236 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6155 df-2nd 6156 df-recs 6320 df-frec 6406 df-sup 6997 df-pnf 8008 df-mnf 8009 df-xr 8010 df-ltxr 8011 df-le 8012 df-sub 8144 df-neg 8145 df-reap 8546 df-ap 8553 df-div 8644 df-inn 8934 df-2 8992 df-3 8993 df-4 8994 df-n0 9191 df-z 9268 df-uz 9543 df-q 9634 df-rp 9668 df-fz 10023 df-fzo 10157 df-fl 10284 df-mod 10337 df-seqfrec 10460 df-exp 10534 df-cj 10865 df-re 10866 df-im 10867 df-rsqrt 11021 df-abs 11022 df-dvds 11809 df-gcd 11958

This theorem is referenced by: cncongr1 12117

W3C validator