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

Metamath Proof Explorer

Theorem dvdsexpad

Description: Deduction associated with dvdsexpim . (Contributed by SN, 21-Aug-2024)

Ref Expression
Hypotheses dvdsexpad.1 ⊢ φ → A ∈ ℤ
dvdsexpad.2 ⊢ φ → B ∈ ℤ
dvdsexpad.3 ⊢ φ → N ∈ ℕ 0
dvdsexpad.5 ⊢ φ → A ∥ B
Assertion dvdsexpad ⊢ φ → A N ∥ B N

Proof

Step Hyp Ref Expression
1 dvdsexpad.1 ⊢ φ → A ∈ ℤ
2 dvdsexpad.2 ⊢ φ → B ∈ ℤ
3 dvdsexpad.3 ⊢ φ → N ∈ ℕ 0
4 dvdsexpad.5 ⊢ φ → A ∥ B
5 dvdsexpim ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A ∥ B → A N ∥ B N
6 1 2 3 5 syl3anc ⊢ φ → A ∥ B → A N ∥ B N
7 4 6 mpd ⊢ φ → A N ∥ B N