Metamath Proof Explorer

Theorem nndivtr

Description: Transitive property of divisibility: if A divides B and B divides C , then A divides C . Typically, C would be an integer, although the theorem holds for complex C . (Contributed by NM, 3-May-2005)

Ref Expression
Assertion nndivtr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ ∧ B A ∈ ℕ ∧ C B ∈ ℕ → C A ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnmulcl ⊢ B A ∈ ℕ ∧ C B ∈ ℕ → B A ⁢ C B ∈ ℕ
2 nncn ⊢ B ∈ ℕ → B ∈ ℂ
3 2 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → B ∈ ℂ
4 simp3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → C ∈ ℂ
5 nncn ⊢ A ∈ ℕ → A ∈ ℂ
6 nnne0 ⊢ A ∈ ℕ → A ≠ 0
7 5 6 jca ⊢ A ∈ ℕ → A ∈ ℂ ∧ A ≠ 0
8 7 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → A ∈ ℂ ∧ A ≠ 0
9 nnne0 ⊢ B ∈ ℕ → B ≠ 0
10 2 9 jca ⊢ B ∈ ℕ → B ∈ ℂ ∧ B ≠ 0
11 10 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → B ∈ ℂ ∧ B ≠ 0
12 divmul24 ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → B A ⁢ C B = B B ⁢ C A
13 3 4 8 11 12 syl22anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → B A ⁢ C B = B B ⁢ C A
14 2 9 dividd ⊢ B ∈ ℕ → B B = 1
15 14 oveq1d ⊢ B ∈ ℕ → B B ⁢ C A = 1 ⁢ C A
16 15 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → B B ⁢ C A = 1 ⁢ C A
17 divcl ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → C A ∈ ℂ
18 17 3expb ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → C A ∈ ℂ
19 7 18 sylan2 ⊢ C ∈ ℂ ∧ A ∈ ℕ → C A ∈ ℂ
20 19 ancoms ⊢ A ∈ ℕ ∧ C ∈ ℂ → C A ∈ ℂ
21 20 mullidd ⊢ A ∈ ℕ ∧ C ∈ ℂ → 1 ⁢ C A = C A
22 21 3adant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → 1 ⁢ C A = C A
23 13 16 22 3eqtrd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → B A ⁢ C B = C A
24 23 eleq1d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → B A ⁢ C B ∈ ℕ ↔ C A ∈ ℕ
25 1 24 imbitrid ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ → B A ∈ ℕ ∧ C B ∈ ℕ → C A ∈ ℕ
26 25 imp ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℂ ∧ B A ∈ ℕ ∧ C B ∈ ℕ → C A ∈ ℕ