dchrisum0lem1a

		Ref	Expression
	Assertion	dchrisum0lem1a	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to (X \leq \frac{X^{2}}{D} \land ⌊\frac{X^{2}}{D}⌋ \in ℤ_{\geq ⌊X⌋})$

Proof

Step	Hyp	Ref	Expression
1		elfznn	$⊢ D \in (1 \dots ⌊X⌋) \to D \in ℕ$
2	1	adantl	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to D \in ℕ$
3	2	nnred	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to D \in ℝ$
4		simpr	$⊢ (φ \land X \in ℝ^{+}) \to X \in ℝ^{+}$
5	4	rpregt0d	$⊢ (φ \land X \in ℝ^{+}) \to (X \in ℝ \land 0 < X)$
6	5	adantr	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to (X \in ℝ \land 0 < X)$
7	6	simpld	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to X \in ℝ$
8	4	adantr	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to X \in ℝ^{+}$
9	8	rpge0d	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to 0 \leq X$
10	4	rpred	$⊢ (φ \land X \in ℝ^{+}) \to X \in ℝ$
11		fznnfl	$⊢ X \in ℝ \to (D \in (1 \dots ⌊X⌋) \leftrightarrow (D \in ℕ \land D \leq X))$
12	10 11	syl	$⊢ (φ \land X \in ℝ^{+}) \to (D \in (1 \dots ⌊X⌋) \leftrightarrow (D \in ℕ \land D \leq X))$
13	12	simplbda	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to D \leq X$
14	3 7 7 9 13	lemul2ad	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to X D \leq X X$
15		rpcn	$⊢ X \in ℝ^{+} \to X \in ℂ$
16	15	adantl	$⊢ (φ \land X \in ℝ^{+}) \to X \in ℂ$
17	16	sqvald	$⊢ (φ \land X \in ℝ^{+}) \to X^{2} = X X$
18	17	adantr	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to X^{2} = X X$
19	14 18	breqtrrd	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to X D \leq X^{2}$
20		2z	$⊢ 2 \in ℤ$
21		rpexpcl	$⊢ (X \in ℝ^{+} \land 2 \in ℤ) \to X^{2} \in ℝ^{+}$
22	4 20 21	sylancl	$⊢ (φ \land X \in ℝ^{+}) \to X^{2} \in ℝ^{+}$
23	22	rpred	$⊢ (φ \land X \in ℝ^{+}) \to X^{2} \in ℝ$
24	23	adantr	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to X^{2} \in ℝ$
25	2	nnrpd	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to D \in ℝ^{+}$
26	7 24 25	lemuldivd	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to (X D \leq X^{2} \leftrightarrow X \leq \frac{X^{2}}{D})$
27	19 26	mpbid	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to X \leq \frac{X^{2}}{D}$
28		nndivre	$⊢ (X^{2} \in ℝ \land D \in ℕ) \to \frac{X^{2}}{D} \in ℝ$
29	23 1 28	syl2an	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to \frac{X^{2}}{D} \in ℝ$
30		flword2	$⊢ (X \in ℝ \land \frac{X^{2}}{D} \in ℝ \land X \leq \frac{X^{2}}{D}) \to ⌊\frac{X^{2}}{D}⌋ \in ℤ_{\geq ⌊X⌋}$
31	7 29 27 30	syl3anc	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to ⌊\frac{X^{2}}{D}⌋ \in ℤ_{\geq ⌊X⌋}$
32	27 31	jca	$⊢ ((φ \land X \in ℝ^{+}) \land D \in (1 \dots ⌊X⌋)) \to (X \leq \frac{X^{2}}{D} \land ⌊\frac{X^{2}}{D}⌋ \in ℤ_{\geq ⌊X⌋})$

Metamath Proof Explorer

Theorem dchrisum0lem1a

Proof