Proof of Theorem nndivsub
Step | Hyp | Ref
| Expression |
1 | | nnre 11726 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
2 | | nnre 11726 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
3 | | nnre 11726 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℕ → 𝐶 ∈
ℝ) |
4 | | nngt0 11750 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℕ → 0 <
𝐶) |
5 | 3, 4 | jca 515 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℕ → (𝐶 ∈ ℝ ∧ 0 <
𝐶)) |
6 | | ltdiv1 11585 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) |
7 | 1, 2, 5, 6 | syl3an 1161 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) |
8 | | nnsub 11763 |
. . . . . . . 8
⊢ (((𝐴 / 𝐶) ∈ ℕ ∧ (𝐵 / 𝐶) ∈ ℕ) → ((𝐴 / 𝐶) < (𝐵 / 𝐶) ↔ ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)) |
9 | 7, 8 | sylan9bb 513 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ (𝐵 / 𝐶) ∈ ℕ)) → (𝐴 < 𝐵 ↔ ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)) |
10 | 9 | biimpd 232 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ (𝐵 / 𝐶) ∈ ℕ)) → (𝐴 < 𝐵 → ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)) |
11 | 10 | exp32 424 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 / 𝐶) ∈ ℕ → ((𝐵 / 𝐶) ∈ ℕ → (𝐴 < 𝐵 → ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)))) |
12 | 11 | com34 91 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 / 𝐶) ∈ ℕ → (𝐴 < 𝐵 → ((𝐵 / 𝐶) ∈ ℕ → ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)))) |
13 | 12 | imp32 422 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ → ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)) |
14 | | nnaddcl 11742 |
. . . . . 6
⊢ ((((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ ∧ (𝐴 / 𝐶) ∈ ℕ) → (((𝐵 / 𝐶) − (𝐴 / 𝐶)) + (𝐴 / 𝐶)) ∈ ℕ) |
15 | 14 | expcom 417 |
. . . . 5
⊢ ((𝐴 / 𝐶) ∈ ℕ → (((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ → (((𝐵 / 𝐶) − (𝐴 / 𝐶)) + (𝐴 / 𝐶)) ∈ ℕ)) |
16 | | nnsscn 11724 |
. . . . . . . . . . 11
⊢ ℕ
⊆ ℂ |
17 | | nnne0 11753 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℕ → 𝐶 ≠ 0) |
18 | | divcl 11385 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → (𝐴 / 𝐶) ∈ ℂ) |
19 | 16, 17, 18 | nnssi2 34290 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 / 𝐶) ∈ ℂ) |
20 | | divcl 11385 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → (𝐵 / 𝐶) ∈ ℂ) |
21 | 16, 17, 20 | nnssi2 34290 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵 / 𝐶) ∈ ℂ) |
22 | 19, 21 | anim12i 616 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ (𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ)) → ((𝐴 / 𝐶) ∈ ℂ ∧ (𝐵 / 𝐶) ∈ ℂ)) |
23 | 22 | 3impdir 1352 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 / 𝐶) ∈ ℂ ∧ (𝐵 / 𝐶) ∈ ℂ)) |
24 | | npcan 10976 |
. . . . . . . . 9
⊢ (((𝐵 / 𝐶) ∈ ℂ ∧ (𝐴 / 𝐶) ∈ ℂ) → (((𝐵 / 𝐶) − (𝐴 / 𝐶)) + (𝐴 / 𝐶)) = (𝐵 / 𝐶)) |
25 | 24 | ancoms 462 |
. . . . . . . 8
⊢ (((𝐴 / 𝐶) ∈ ℂ ∧ (𝐵 / 𝐶) ∈ ℂ) → (((𝐵 / 𝐶) − (𝐴 / 𝐶)) + (𝐴 / 𝐶)) = (𝐵 / 𝐶)) |
26 | 23, 25 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐵 / 𝐶) − (𝐴 / 𝐶)) + (𝐴 / 𝐶)) = (𝐵 / 𝐶)) |
27 | 26 | eleq1d 2818 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((((𝐵 / 𝐶) − (𝐴 / 𝐶)) + (𝐴 / 𝐶)) ∈ ℕ ↔ (𝐵 / 𝐶) ∈ ℕ)) |
28 | 27 | biimpd 232 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((((𝐵 / 𝐶) − (𝐴 / 𝐶)) + (𝐴 / 𝐶)) ∈ ℕ → (𝐵 / 𝐶) ∈ ℕ)) |
29 | 15, 28 | sylan9r 512 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ (𝐴 / 𝐶) ∈ ℕ) → (((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ → (𝐵 / 𝐶) ∈ ℕ)) |
30 | 29 | adantrr 717 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → (((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ → (𝐵 / 𝐶) ∈ ℕ)) |
31 | 13, 30 | impbid 215 |
. 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)) |
32 | | nncn 11727 |
. . . . . 6
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
33 | 32 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈
ℂ) |
34 | | nncn 11727 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
35 | 34 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈
ℂ) |
36 | | nncn 11727 |
. . . . . . 7
⊢ (𝐶 ∈ ℕ → 𝐶 ∈
ℂ) |
37 | 36, 17 | jca 515 |
. . . . . 6
⊢ (𝐶 ∈ ℕ → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
38 | 37 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
39 | | divsubdir 11415 |
. . . . 5
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐵 − 𝐴) / 𝐶) = ((𝐵 / 𝐶) − (𝐴 / 𝐶))) |
40 | 33, 35, 38, 39 | syl3anc 1372 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐵 − 𝐴) / 𝐶) = ((𝐵 / 𝐶) − (𝐴 / 𝐶))) |
41 | 40 | eleq1d 2818 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐵 − 𝐴) / 𝐶) ∈ ℕ ↔ ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)) |
42 | 41 | adantr 484 |
. 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → (((𝐵 − 𝐴) / 𝐶) ∈ ℕ ↔ ((𝐵 / 𝐶) − (𝐴 / 𝐶)) ∈ ℕ)) |
43 | 31, 42 | bitr4d 285 |
1
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ)) |