ltdifltdiv

Description: If the dividend of a division is less than the difference between a real number and the divisor, the floor function of the division plus 1 is less than the division of the real number by the divisor. (Contributed by Alexander van der Vekens, 14-Apr-2018)

		Ref	Expression
	Assertion	ltdifltdiv	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (A < C - B \to ⌊\frac{A}{B}⌋ + 1 < \frac{C}{B})$

Proof

Step	Hyp	Ref	Expression
1		refldivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℝ$
2		peano2re	$⊢ ⌊\frac{A}{B}⌋ \in ℝ \to ⌊\frac{A}{B}⌋ + 1 \in ℝ$
3	1 2	syl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ + 1 \in ℝ$
4	3	3adant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to ⌊\frac{A}{B}⌋ + 1 \in ℝ$
5	4	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to ⌊\frac{A}{B}⌋ + 1 \in ℝ$
6		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
7		peano2re	$⊢ \frac{A}{B} \in ℝ \to (\frac{A}{B}) + 1 \in ℝ$
8	6 7	syl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (\frac{A}{B}) + 1 \in ℝ$
9	8	3adant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (\frac{A}{B}) + 1 \in ℝ$
10	9	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to (\frac{A}{B}) + 1 \in ℝ$
11		rerpdivcl	$⊢ (C \in ℝ \land B \in ℝ^{+}) \to \frac{C}{B} \in ℝ$
12	11	ancoms	$⊢ (B \in ℝ^{+} \land C \in ℝ) \to \frac{C}{B} \in ℝ$
13	12	3adant1	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to \frac{C}{B} \in ℝ$
14	13	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to \frac{C}{B} \in ℝ$
15	1	3adant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to ⌊\frac{A}{B}⌋ \in ℝ$
16	15	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to ⌊\frac{A}{B}⌋ \in ℝ$
17	6	3adant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to \frac{A}{B} \in ℝ$
18	17	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to \frac{A}{B} \in ℝ$
19		1red	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to 1 \in ℝ$
20		3simpa	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (A \in ℝ \land B \in ℝ^{+})$
21	20	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to (A \in ℝ \land B \in ℝ^{+})$
22		fldivle	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \leq \frac{A}{B}$
23	21 22	syl	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to ⌊\frac{A}{B}⌋ \leq \frac{A}{B}$
24	16 18 19 23	leadd1dd	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to ⌊\frac{A}{B}⌋ + 1 \leq (\frac{A}{B}) + 1$
25		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
26		ltaddsub	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A + B < C \leftrightarrow A < C - B)$
27	25 26	syl3an2	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (A + B < C \leftrightarrow A < C - B)$
28	27	biimpar	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to A + B < C$
29		recn	$⊢ \frac{A}{B} \in ℝ \to \frac{A}{B} \in ℂ$
30	6 29	syl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℂ$
31	30	3adant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to \frac{A}{B} \in ℂ$
32		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
33	32	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to B \in ℂ$
34		1cnd	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to 1 \in ℂ$
35		recn	$⊢ A \in ℝ \to A \in ℂ$
36	35	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to A \in ℂ$
37		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
38	37	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to B \neq 0$
39	36 33 38	divcan1d	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (\frac{A}{B}) B = A$
40	32	mulid2d	$⊢ B \in ℝ^{+} \to 1 B = B$
41	40	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to 1 B = B$
42	39 41	oveq12d	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (\frac{A}{B}) B + 1 B = A + B$
43	31 33 34 42	joinlmuladdmuld	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to ((\frac{A}{B}) + 1) B = A + B$
44		recn	$⊢ C \in ℝ \to C \in ℂ$
45	44	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to C \in ℂ$
46	45 33 38	divcan1d	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (\frac{C}{B}) B = C$
47	43 46	breq12d	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (((\frac{A}{B}) + 1) B < (\frac{C}{B}) B \leftrightarrow A + B < C)$
48	47	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to (((\frac{A}{B}) + 1) B < (\frac{C}{B}) B \leftrightarrow A + B < C)$
49	28 48	mpbird	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to ((\frac{A}{B}) + 1) B < (\frac{C}{B}) B$
50	17 7	syl	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (\frac{A}{B}) + 1 \in ℝ$
51		simp2	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to B \in ℝ^{+}$
52	50 13 51	ltmul1d	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to ((\frac{A}{B}) + 1 < \frac{C}{B} \leftrightarrow ((\frac{A}{B}) + 1) B < (\frac{C}{B}) B)$
53	52	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to ((\frac{A}{B}) + 1 < \frac{C}{B} \leftrightarrow ((\frac{A}{B}) + 1) B < (\frac{C}{B}) B)$
54	49 53	mpbird	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to (\frac{A}{B}) + 1 < \frac{C}{B}$
55	5 10 14 24 54	lelttrd	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \land A < C - B) \to ⌊\frac{A}{B}⌋ + 1 < \frac{C}{B}$
56	55	ex	$⊢ (A \in ℝ \land B \in ℝ^{+} \land C \in ℝ) \to (A < C - B \to ⌊\frac{A}{B}⌋ + 1 < \frac{C}{B})$

Metamath Proof Explorer

Theorem ltdifltdiv

Proof