Metamath Proof Explorer

Theorem nndivsub

Description: Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008)

Ref Expression
Assertion nndivsub ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ ∧ A < B → B C ∈ ℕ ↔ B − A C ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnre ⊢ A ∈ ℕ → A ∈ ℝ
2 nnre ⊢ B ∈ ℕ → B ∈ ℝ
3 nnre ⊢ C ∈ ℕ → C ∈ ℝ
4 nngt0 ⊢ C ∈ ℕ → 0 < C
5 3 4 jca ⊢ C ∈ ℕ → C ∈ ℝ ∧ 0 < C
6 ltdiv1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A C < B C
7 1 2 5 6 syl3an ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A < B ↔ A C < B C
8 nnsub ⊢ A C ∈ ℕ ∧ B C ∈ ℕ → A C < B C ↔ B C − A C ∈ ℕ
9 7 8 sylan9bb ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ ∧ B C ∈ ℕ → A < B ↔ B C − A C ∈ ℕ
10 9 biimpd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ ∧ B C ∈ ℕ → A < B → B C − A C ∈ ℕ
11 10 exp32 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A C ∈ ℕ → B C ∈ ℕ → A < B → B C − A C ∈ ℕ
12 11 com34 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A C ∈ ℕ → A < B → B C ∈ ℕ → B C − A C ∈ ℕ
13 12 imp32 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ ∧ A < B → B C ∈ ℕ → B C − A C ∈ ℕ
14 nnaddcl ⊢ B C − A C ∈ ℕ ∧ A C ∈ ℕ → B C - A C + A C ∈ ℕ
15 14 expcom ⊢ A C ∈ ℕ → B C − A C ∈ ℕ → B C - A C + A C ∈ ℕ
16 nnsscn ⊢ ℕ ⊆ ℂ
17 nnne0 ⊢ C ∈ ℕ → C ≠ 0
18 divcl ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
19 16 17 18 nnssi2 ⊢ A ∈ ℕ ∧ C ∈ ℕ → A C ∈ ℂ
20 divcl ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
21 16 17 20 nnssi2 ⊢ B ∈ ℕ ∧ C ∈ ℕ → B C ∈ ℂ
22 19 21 anim12i ⊢ A ∈ ℕ ∧ C ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A C ∈ ℂ ∧ B C ∈ ℂ
23 22 3impdir ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A C ∈ ℂ ∧ B C ∈ ℂ
24 npcan ⊢ B C ∈ ℂ ∧ A C ∈ ℂ → B C - A C + A C = B C
25 24 ancoms ⊢ A C ∈ ℂ ∧ B C ∈ ℂ → B C - A C + A C = B C
26 23 25 syl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B C - A C + A C = B C
27 26 eleq1d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B C - A C + A C ∈ ℕ ↔ B C ∈ ℕ
28 27 biimpd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B C - A C + A C ∈ ℕ → B C ∈ ℕ
29 15 28 sylan9r ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ → B C − A C ∈ ℕ → B C ∈ ℕ
30 29 adantrr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ ∧ A < B → B C − A C ∈ ℕ → B C ∈ ℕ
31 13 30 impbid ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ ∧ A < B → B C ∈ ℕ ↔ B C − A C ∈ ℕ
32 nncn ⊢ B ∈ ℕ → B ∈ ℂ
33 32 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B ∈ ℂ
34 nncn ⊢ A ∈ ℕ → A ∈ ℂ
35 34 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A ∈ ℂ
36 nncn ⊢ C ∈ ℕ → C ∈ ℂ
37 36 17 jca ⊢ C ∈ ℕ → C ∈ ℂ ∧ C ≠ 0
38 37 3ad2ant3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C ∈ ℂ ∧ C ≠ 0
39 divsubdir ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B − A C = B C − A C
40 33 35 38 39 syl3anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B − A C = B C − A C
41 40 eleq1d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B − A C ∈ ℕ ↔ B C − A C ∈ ℕ
42 41 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ ∧ A < B → B − A C ∈ ℕ ↔ B C − A C ∈ ℕ
43 31 42 bitr4d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A C ∈ ℕ ∧ A < B → B C ∈ ℕ ↔ B − A C ∈ ℕ