This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( numer ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∧ ( denom ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )

Proof

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