Metamath Proof Explorer

Theorem fltdvdsabdvdsc

Description: Any factor of both A and B also divides C . This establishes the validity of fltabcoprmex . (Contributed by SN, 21-Aug-2024)

Ref Expression
Hypotheses fltdvdsabdvdsc.a ⊢ φ → A ∈ ℕ
fltdvdsabdvdsc.b ⊢ φ → B ∈ ℕ
fltdvdsabdvdsc.c ⊢ φ → C ∈ ℕ
fltdvdsabdvdsc.n ⊢ φ → N ∈ ℕ
fltdvdsabdvdsc.1 ⊢ φ → A N + B N = C N
Assertion fltdvdsabdvdsc ⊢ φ → A gcd B ∥ C

Proof

Step Hyp Ref Expression
1 fltdvdsabdvdsc.a ⊢ φ → A ∈ ℕ
2 fltdvdsabdvdsc.b ⊢ φ → B ∈ ℕ
3 fltdvdsabdvdsc.c ⊢ φ → C ∈ ℕ
4 fltdvdsabdvdsc.n ⊢ φ → N ∈ ℕ
5 fltdvdsabdvdsc.1 ⊢ φ → A N + B N = C N
6 gcdnncl ⊢ A ∈ ℕ ∧ B ∈ ℕ → A gcd B ∈ ℕ
7 1 2 6 syl2anc ⊢ φ → A gcd B ∈ ℕ
8 4 nnnn0d ⊢ φ → N ∈ ℕ 0
9 7 8 nnexpcld ⊢ φ → A gcd B N ∈ ℕ
10 9 nnzd ⊢ φ → A gcd B N ∈ ℤ
11 1 8 nnexpcld ⊢ φ → A N ∈ ℕ
12 11 nnzd ⊢ φ → A N ∈ ℤ
13 2 8 nnexpcld ⊢ φ → B N ∈ ℕ
14 13 nnzd ⊢ φ → B N ∈ ℤ
15 7 nnzd ⊢ φ → A gcd B ∈ ℤ
16 1 nnzd ⊢ φ → A ∈ ℤ
17 2 nnzd ⊢ φ → B ∈ ℤ
18 gcddvds ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B
19 16 17 18 syl2anc ⊢ φ → A gcd B ∥ A ∧ A gcd B ∥ B
20 19 simpld ⊢ φ → A gcd B ∥ A
21 15 16 8 20 dvdsexpad ⊢ φ → A gcd B N ∥ A N
22 19 simprd ⊢ φ → A gcd B ∥ B
23 15 17 8 22 dvdsexpad ⊢ φ → A gcd B N ∥ B N
24 10 12 14 21 23 dvds2addd ⊢ φ → A gcd B N ∥ A N + B N
25 24 5 breqtrd ⊢ φ → A gcd B N ∥ C N
26 dvdsexpnn ⊢ A gcd B ∈ ℕ ∧ C ∈ ℕ ∧ N ∈ ℕ → A gcd B ∥ C ↔ A gcd B N ∥ C N
27 7 3 4 26 syl3anc ⊢ φ → A gcd B ∥ C ↔ A gcd B N ∥ C N
28 25 27 mpbird ⊢ φ → A gcd B ∥ C