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 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltdvdsabdvdsc.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltdvdsabdvdsc.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltdvdsabdvdsc.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
fltdvdsabdvdsc.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
Assertion fltdvdsabdvdsc ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∥ 𝐶 )

Proof

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