Metamath Proof Explorer

Theorem nndivsub

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

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

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↔AC<BC
7 1 2 5 6 syl3an ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→A<B↔AC<BC
8 nnsub ⊢AC∈ℕ∧BC∈ℕ→AC<BC↔BC−AC∈ℕ
9 7 8 sylan9bb ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧AC∈ℕ∧BC∈ℕ→A<B↔BC−AC∈ℕ
10 9 biimpd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧AC∈ℕ∧BC∈ℕ→A<B→BC−AC∈ℕ
11 10 exp32 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→AC∈ℕ→BC∈ℕ→A<B→BC−AC∈ℕ
12 11 com34 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→AC∈ℕ→A<B→BC∈ℕ→BC−AC∈ℕ
13 12 imp32 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧AC∈ℕ∧A<B→BC∈ℕ→BC−AC∈ℕ
14 nnaddcl ⊢BC−AC∈ℕ∧AC∈ℕ→BC-AC+AC∈ℕ
15 14 expcom ⊢AC∈ℕ→BC−AC∈ℕ→BC-AC+AC∈ℕ
16 nnsscn ⊢ℕ⊆ℂ
17 nnne0 ⊢C∈ℕ→C≠0
18 divcl ⊢A∈ℂ∧C∈ℂ∧C≠0→AC∈ℂ
19 16 17 18 nnssi2 ⊢A∈ℕ∧C∈ℕ→AC∈ℂ
20 divcl ⊢B∈ℂ∧C∈ℂ∧C≠0→BC∈ℂ
21 16 17 20 nnssi2 ⊢B∈ℕ∧C∈ℕ→BC∈ℂ
22 19 21 anim12i ⊢A∈ℕ∧C∈ℕ∧B∈ℕ∧C∈ℕ→AC∈ℂ∧BC∈ℂ
23 22 3impdir ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→AC∈ℂ∧BC∈ℂ
24 npcan ⊢BC∈ℂ∧AC∈ℂ→BC-AC+AC=BC
25 24 ancoms ⊢AC∈ℂ∧BC∈ℂ→BC-AC+AC=BC
26 23 25 syl ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→BC-AC+AC=BC
27 26 eleq1d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→BC-AC+AC∈ℕ↔BC∈ℕ
28 27 biimpd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→BC-AC+AC∈ℕ→BC∈ℕ
29 15 28 sylan9r ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧AC∈ℕ→BC−AC∈ℕ→BC∈ℕ
30 29 adantrr ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧AC∈ℕ∧A<B→BC−AC∈ℕ→BC∈ℕ
31 13 30 impbid ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧AC∈ℕ∧A<B→BC∈ℕ↔BC−AC∈ℕ
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−AC=BC−AC
40 33 35 38 39 syl3anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→B−AC=BC−AC
41 40 eleq1d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→B−AC∈ℕ↔BC−AC∈ℕ
42 41 adantr ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧AC∈ℕ∧A<B→B−AC∈ℕ↔BC−AC∈ℕ
43 31 42 bitr4d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧AC∈ℕ∧A<B→BC∈ℕ↔B−AC∈ℕ