Metamath Proof Explorer

Theorem nndivsub

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

Ref Expression
Assertion nndivsub ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 / 𝐶 ) ∈ ℕ ∧ 𝐴 < 𝐵 ) ) → ( ( 𝐵 / 𝐶 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) / 𝐶 ) ∈ ℕ ) )

Proof

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