divgcdcoprm0 - Intuitionistic Logic Explorer

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

Theorem divgcdcoprm0 12269

Description: Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021.)

**Assertion**
Ref	Expression
divgcdcoprm0	⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)

Proof of Theorem divgcdcoprm0 Dummy variables 𝑎 𝑏 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gcddvds 12130	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
2	1	3adant3 1019	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
3		gcdcl 12133	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
4	3	nn0zd 9446	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ)
5		simpl 109	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ)
6	4, 5	jca 306	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ))
7	6	3adant3 1019	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ))
8		divides 11954	. . . . 5 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ∃𝑎 ∈ ℤ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴))
9	7, 8	syl 14	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ∃𝑎 ∈ ℤ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴))
10		simpr 110	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℤ)
11	4, 10	jca 306	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ))
12	11	3adant3 1019	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ))
13		divides 11954	. . . . 5 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ∃𝑏 ∈ ℤ (𝑏 · (𝐴 gcd 𝐵)) = 𝐵))
14	12, 13	syl 14	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ∃𝑏 ∈ ℤ (𝑏 · (𝐴 gcd 𝐵)) = 𝐵))
15	9, 14	anbi12d 473	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵) ↔ (∃𝑎 ∈ ℤ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴 ∧ ∃𝑏 ∈ ℤ (𝑏 · (𝐴 gcd 𝐵)) = 𝐵)))
16		bezout 12178	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)))
17	16	3adant3 1019	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)))
18		oveq1 5929	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝑎 · (𝐴 gcd 𝐵)) · 𝑚) = (𝐴 · 𝑚))
19		oveq1 5929	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑏 · (𝐴 gcd 𝐵)) · 𝑛) = (𝐵 · 𝑛))
20	18, 19	oveqan12rd 5942	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴) → (((𝑎 · (𝐴 gcd 𝐵)) · 𝑚) + ((𝑏 · (𝐴 gcd 𝐵)) · 𝑛)) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)))
21	20	eqeq2d 2208	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴) → ((𝐴 gcd 𝐵) = (((𝑎 · (𝐴 gcd 𝐵)) · 𝑚) + ((𝑏 · (𝐴 gcd 𝐵)) · 𝑛)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛))))
22	21	bicomd 141	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) ↔ (𝐴 gcd 𝐵) = (((𝑎 · (𝐴 gcd 𝐵)) · 𝑚) + ((𝑏 · (𝐴 gcd 𝐵)) · 𝑛))))
23		simpl 109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑎 ∈ ℤ)
24	23	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑎 ∈ ℂ)
25	24	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℂ)
26	3	nn0cnd 9304	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℂ)
27	26	3adant3 1019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℂ)
28	27	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝐴 gcd 𝐵) ∈ ℂ)
29		simpl 109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∈ ℤ)
30	29	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∈ ℂ)
31	30	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑚 ∈ ℂ)
32	25, 28, 31	mul32d 8179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑎 · (𝐴 gcd 𝐵)) · 𝑚) = ((𝑎 · 𝑚) · (𝐴 gcd 𝐵)))
33		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
34	33	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℂ)
35	34	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℂ)
36		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
37	36	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℂ)
38	37	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑛 ∈ ℂ)
39	35, 28, 38	mul32d 8179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑏 · (𝐴 gcd 𝐵)) · 𝑛) = ((𝑏 · 𝑛) · (𝐴 gcd 𝐵)))
40	32, 39	oveq12d 5940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑎 · (𝐴 gcd 𝐵)) · 𝑚) + ((𝑏 · (𝐴 gcd 𝐵)) · 𝑛)) = (((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))))
41	40	eqeq2d 2208	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝐴 gcd 𝐵) = (((𝑎 · (𝐴 gcd 𝐵)) · 𝑚) + ((𝑏 · (𝐴 gcd 𝐵)) · 𝑛)) ↔ (𝐴 gcd 𝐵) = (((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵)))))
42	23	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
43	29	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑚 ∈ ℤ)
44	42, 43	zmulcld 9454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 · 𝑚) ∈ ℤ)
45	4	3adant3 1019	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℤ)
46	45	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝐴 gcd 𝐵) ∈ ℤ)
47	44, 46	zmulcld 9454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) ∈ ℤ)
48	33	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
49	36	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑛 ∈ ℤ)
50	48, 49	zmulcld 9454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑏 · 𝑛) ∈ ℤ)
51	3	3adant3 1019	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ₀)
52	51	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝐴 gcd 𝐵) ∈ ℕ₀)
53	52	nn0zd 9446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝐴 gcd 𝐵) ∈ ℤ)
54	50, 53	zmulcld 9454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑏 · 𝑛) · (𝐴 gcd 𝐵)) ∈ ℤ)
55	47, 54	zaddcld 9452	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) ∈ ℤ)
56	55	zcnd 9449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) ∈ ℂ)
57		gcd2n0cl 12136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ)
58		nncn 8998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → (𝐴 gcd 𝐵) ∈ ℂ)
59		nnap0 9019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → (𝐴 gcd 𝐵) # 0)
60	58, 59	jca 306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0))
61	57, 60	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0))
62	61	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0))
63		div11ap 8727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 gcd 𝐵) ∈ ℂ ∧ (((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) ∈ ℂ ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0)) → (((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) / (𝐴 gcd 𝐵)) ↔ (𝐴 gcd 𝐵) = (((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵)))))
64	28, 56, 62, 63	syl3anc 1249	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) / (𝐴 gcd 𝐵)) ↔ (𝐴 gcd 𝐵) = (((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵)))))
65		dividap 8728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = 1)
66	62, 65	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = 1)
67	47	zcnd 9449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) ∈ ℂ)
68	54	zcnd 9449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑏 · 𝑛) · (𝐴 gcd 𝐵)) ∈ ℂ)
69		divdirap 8724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) ∈ ℂ ∧ ((𝑏 · 𝑛) · (𝐴 gcd 𝐵)) ∈ ℂ ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0)) → ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) / (𝐴 gcd 𝐵)) = ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) / (𝐴 gcd 𝐵)) + (((𝑏 · 𝑛) · (𝐴 gcd 𝐵)) / (𝐴 gcd 𝐵))))
70	67, 68, 62, 69	syl3anc 1249	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) / (𝐴 gcd 𝐵)) = ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) / (𝐴 gcd 𝐵)) + (((𝑏 · 𝑛) · (𝐴 gcd 𝐵)) / (𝐴 gcd 𝐵))))
71	44	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 · 𝑚) ∈ ℂ)
72	51	nn0cnd 9304	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℂ)
73	72	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝐴 gcd 𝐵) ∈ ℂ)
74	62	simprd 114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝐴 gcd 𝐵) # 0)
75	71, 73, 74	divcanap4d 8823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) / (𝐴 gcd 𝐵)) = (𝑎 · 𝑚))
76	50	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑏 · 𝑛) ∈ ℂ)
77	76, 28, 74	divcanap4d 8823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑏 · 𝑛) · (𝐴 gcd 𝐵)) / (𝐴 gcd 𝐵)) = (𝑏 · 𝑛))
78	75, 77	oveq12d 5940	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) / (𝐴 gcd 𝐵)) + (((𝑏 · 𝑛) · (𝐴 gcd 𝐵)) / (𝐴 gcd 𝐵))) = ((𝑎 · 𝑚) + (𝑏 · 𝑛)))
79	70, 78	eqtrd 2229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) / (𝐴 gcd 𝐵)) = ((𝑎 · 𝑚) + (𝑏 · 𝑛)))
80	66, 79	eqeq12d 2211	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((((𝑎 · 𝑚) · (𝐴 gcd 𝐵)) + ((𝑏 · 𝑛) · (𝐴 gcd 𝐵))) / (𝐴 gcd 𝐵)) ↔ 1 = ((𝑎 · 𝑚) + (𝑏 · 𝑛))))
81	41, 64, 80	3bitr2d 216	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝐴 gcd 𝐵) = (((𝑎 · (𝐴 gcd 𝐵)) · 𝑚) + ((𝑏 · (𝐴 gcd 𝐵)) · 𝑛)) ↔ 1 = ((𝑎 · 𝑚) + (𝑏 · 𝑛))))
82	22, 81	sylan9bbr 463	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) ↔ 1 = ((𝑎 · 𝑚) + (𝑏 · 𝑛))))
83		eqcom 2198	. . . . . . . . . . . . . . . . . 18 ⊢ (1 = ((𝑎 · 𝑚) + (𝑏 · 𝑛)) ↔ ((𝑎 · 𝑚) + (𝑏 · 𝑛)) = 1)
84		simpr 110	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ))
85	84	anim1i 340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)))
86	85	ancomd 267	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)))
87		bezoutr1 12200	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (((𝑎 · 𝑚) + (𝑏 · 𝑛)) = 1 → (𝑎 gcd 𝑏) = 1))
88	86, 87	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑎 · 𝑚) + (𝑏 · 𝑛)) = 1 → (𝑎 gcd 𝑏) = 1))
89	88	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → (((𝑎 · 𝑚) + (𝑏 · 𝑛)) = 1 → (𝑎 gcd 𝑏) = 1))
90	83, 89	biimtrid 152	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → (1 = ((𝑎 · 𝑚) + (𝑏 · 𝑛)) → (𝑎 gcd 𝑏) = 1))
91		simpll1 1038	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐴 ∈ ℤ)
92	91	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐴 ∈ ℂ)
93		divmulap3 8704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0)) → ((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ↔ 𝐴 = (𝑎 · (𝐴 gcd 𝐵))))
94	92, 25, 62, 93	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝐴 / (𝐴 gcd 𝐵)) = 𝑎 ↔ 𝐴 = (𝑎 · (𝐴 gcd 𝐵))))
95		eqcom 2198	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝐴 / (𝐴 gcd 𝐵)) ↔ (𝐴 / (𝐴 gcd 𝐵)) = 𝑎)
96		eqcom 2198	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 ↔ 𝐴 = (𝑎 · (𝐴 gcd 𝐵)))
97	94, 95, 96	3bitr4g 223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 = (𝐴 / (𝐴 gcd 𝐵)) ↔ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴))
98	97	biimprd 158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → 𝑎 = (𝐴 / (𝐴 gcd 𝐵))))
99	98	a1d 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → 𝑎 = (𝐴 / (𝐴 gcd 𝐵)))))
100	99	imp32 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → 𝑎 = (𝐴 / (𝐴 gcd 𝐵)))
101		simp2 1000	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℤ)
102	101	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
103	102	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐵 ∈ ℂ)
104		divmulap3 8704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0)) → ((𝐵 / (𝐴 gcd 𝐵)) = 𝑏 ↔ 𝐵 = (𝑏 · (𝐴 gcd 𝐵))))
105	103, 35, 62, 104	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝐵 / (𝐴 gcd 𝐵)) = 𝑏 ↔ 𝐵 = (𝑏 · (𝐴 gcd 𝐵))))
106		eqcom 2198	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (𝐵 / (𝐴 gcd 𝐵)) ↔ (𝐵 / (𝐴 gcd 𝐵)) = 𝑏)
107		eqcom 2198	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ↔ 𝐵 = (𝑏 · (𝐴 gcd 𝐵)))
108	105, 106, 107	3bitr4g 223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑏 = (𝐵 / (𝐴 gcd 𝐵)) ↔ (𝑏 · (𝐴 gcd 𝐵)) = 𝐵))
109	108	biimprd 158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → 𝑏 = (𝐵 / (𝐴 gcd 𝐵))))
110	109	a1dd 48	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → 𝑏 = (𝐵 / (𝐴 gcd 𝐵)))))
111	110	imp32 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → 𝑏 = (𝐵 / (𝐴 gcd 𝐵)))
112	100, 111	oveq12d 5940	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → (𝑎 gcd 𝑏) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))))
113	112	eqeq1d 2205	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → ((𝑎 gcd 𝑏) = 1 ↔ ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))
114	90, 113	sylibd 149	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → (1 = ((𝑎 · 𝑚) + (𝑏 · 𝑛)) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))
115	82, 114	sylbid 150	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 ∧ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴)) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))
116	115	exp32 365	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))))
117	116	com34 83	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))))
118	117	com23 78	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))))
119	118	ex 115	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)))))
120	119	com23 78	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) → ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)))))
121	120	rexlimdvva 2622	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑚) + (𝐵 · 𝑛)) → ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)))))
122	17, 121	mpd 13	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))))
123	122	impl 380	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → ((𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)))
124	123	rexlimdva 2614	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑎 ∈ ℤ) → (∃𝑏 ∈ ℤ (𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)))
125	124	com23 78	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑎 ∈ ℤ) → ((𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → (∃𝑏 ∈ ℤ (𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)))
126	125	rexlimdva 2614	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (∃𝑎 ∈ ℤ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴 → (∃𝑏 ∈ ℤ (𝑏 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)))
127	126	impd 254	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((∃𝑎 ∈ ℤ (𝑎 · (𝐴 gcd 𝐵)) = 𝐴 ∧ ∃𝑏 ∈ ℤ (𝑏 · (𝐴 gcd 𝐵)) = 𝐵) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))
128	15, 127	sylbid 150	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))
129	2, 128	mpd 13	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 ≠ wne 2367 ∃wrex 2476 class class class wbr 4033 (class class class)co 5922 ℂcc 7877 0cc0 7879 1c1 7880 + caddc 7882 · cmul 7884 # cap 8608 / cdiv 8699 ℕcn 8990 ℕ₀cn0 9249 ℤcz 9326 ∥ cdvds 11952 gcd cgcd 12120

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-sup 7050 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-fz 10084 df-fzo 10218 df-fl 10360 df-mod 10415 df-seqfrec 10540 df-exp 10631 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-dvds 11953 df-gcd 12121

This theorem is referenced by: divgcdcoprmex 12270

W3C validator