Metamath Proof Explorer

Theorem divnumden

Description: Calculate the reduced form of a quotient using gcd . (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion divnumden ⊢A∈ℤ∧B∈ℕ→numer⁡AB=AAgcdB∧denom⁡AB=BAgcdB

Proof

Step Hyp Ref Expression
1 simpl ⊢A∈ℤ∧B∈ℕ→A∈ℤ
2 nnz ⊢B∈ℕ→B∈ℤ
3 2 adantl ⊢A∈ℤ∧B∈ℕ→B∈ℤ
4 nnne0 ⊢B∈ℕ→B≠0
5 4 neneqd ⊢B∈ℕ→¬B=0
6 5 adantl ⊢A∈ℤ∧B∈ℕ→¬B=0
7 6 intnand ⊢A∈ℤ∧B∈ℕ→¬A=0∧B=0
8 gcdn0cl ⊢A∈ℤ∧B∈ℤ∧¬A=0∧B=0→AgcdB∈ℕ
9 1 3 7 8 syl21anc ⊢A∈ℤ∧B∈ℕ→AgcdB∈ℕ
10 gcddvds ⊢A∈ℤ∧B∈ℤ→AgcdB∥A∧AgcdB∥B
11 2 10 sylan2 ⊢A∈ℤ∧B∈ℕ→AgcdB∥A∧AgcdB∥B
12 gcddiv ⊢A∈ℤ∧B∈ℤ∧AgcdB∈ℕ∧AgcdB∥A∧AgcdB∥B→AgcdBAgcdB=AAgcdBgcdBAgcdB
13 1 3 9 11 12 syl31anc ⊢A∈ℤ∧B∈ℕ→AgcdBAgcdB=AAgcdBgcdBAgcdB
14 9 nncnd ⊢A∈ℤ∧B∈ℕ→AgcdB∈ℂ
15 9 nnne0d ⊢A∈ℤ∧B∈ℕ→AgcdB≠0
16 14 15 dividd ⊢A∈ℤ∧B∈ℕ→AgcdBAgcdB=1
17 13 16 eqtr3d ⊢A∈ℤ∧B∈ℕ→AAgcdBgcdBAgcdB=1
18 zcn ⊢A∈ℤ→A∈ℂ
19 18 adantr ⊢A∈ℤ∧B∈ℕ→A∈ℂ
20 nncn ⊢B∈ℕ→B∈ℂ
21 20 adantl ⊢A∈ℤ∧B∈ℕ→B∈ℂ
22 4 adantl ⊢A∈ℤ∧B∈ℕ→B≠0
23 divcan7 ⊢A∈ℂ∧B∈ℂ∧B≠0∧AgcdB∈ℂ∧AgcdB≠0→AAgcdBBAgcdB=AB
24 23 eqcomd ⊢A∈ℂ∧B∈ℂ∧B≠0∧AgcdB∈ℂ∧AgcdB≠0→AB=AAgcdBBAgcdB
25 19 21 22 14 15 24 syl122anc ⊢A∈ℤ∧B∈ℕ→AB=AAgcdBBAgcdB
26 znq ⊢A∈ℤ∧B∈ℕ→AB∈ℚ
27 11 simpld ⊢A∈ℤ∧B∈ℕ→AgcdB∥A
28 gcdcl ⊢A∈ℤ∧B∈ℤ→AgcdB∈ℕ0
29 28 nn0zd ⊢A∈ℤ∧B∈ℤ→AgcdB∈ℤ
30 2 29 sylan2 ⊢A∈ℤ∧B∈ℕ→AgcdB∈ℤ
31 dvdsval2 ⊢AgcdB∈ℤ∧AgcdB≠0∧A∈ℤ→AgcdB∥A↔AAgcdB∈ℤ
32 30 15 1 31 syl3anc ⊢A∈ℤ∧B∈ℕ→AgcdB∥A↔AAgcdB∈ℤ
33 27 32 mpbid ⊢A∈ℤ∧B∈ℕ→AAgcdB∈ℤ
34 11 simprd ⊢A∈ℤ∧B∈ℕ→AgcdB∥B
35 simpr ⊢A∈ℤ∧B∈ℕ→B∈ℕ
36 nndivdvds ⊢B∈ℕ∧AgcdB∈ℕ→AgcdB∥B↔BAgcdB∈ℕ
37 35 9 36 syl2anc ⊢A∈ℤ∧B∈ℕ→AgcdB∥B↔BAgcdB∈ℕ
38 34 37 mpbid ⊢A∈ℤ∧B∈ℕ→BAgcdB∈ℕ
39 qnumdenbi ⊢AB∈ℚ∧AAgcdB∈ℤ∧BAgcdB∈ℕ→AAgcdBgcdBAgcdB=1∧AB=AAgcdBBAgcdB↔numer⁡AB=AAgcdB∧denom⁡AB=BAgcdB
40 26 33 38 39 syl3anc ⊢A∈ℤ∧B∈ℕ→AAgcdBgcdBAgcdB=1∧AB=AAgcdBBAgcdB↔numer⁡AB=AAgcdB∧denom⁡AB=BAgcdB
41 17 25 40 mpbi2and ⊢A∈ℤ∧B∈ℕ→numer⁡AB=AAgcdB∧denom⁡AB=BAgcdB