Theorem 2timesltsq

Description: Two times an integer greater than 2 is less than the square of the integer. (Contributed by AV, 6-Apr-2026)

	Ref	Expression
Assertion	2timesltsq	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2A<A^2$$

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2	1	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2\in ℝ$$
3		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in \mathbb{Z}$$
4	3	zred	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in ℝ$$
5		eluz3nn	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in \mathbb{N}$$
6	5	nngt0d	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 0<A$$
7	4 6	jca	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to \left(A\in ℝ\wedge 0<A\right)$$
8		eluzle	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 3\le A$$
9		df-3	$$⊢3=2+1$$
10	9	breq1i	$$⊢3\le A\leftrightarrow 2+1\le A$$
11		2z	$$⊢2\in \mathbb{Z}$$
12	11	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2\in \mathbb{Z}$$
13	12 3	zltp1led	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to \left(2<A\leftrightarrow 2+1\le A\right)$$
14	13	biimprd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to \left(2+1\le A\to 2<A\right)$$
15	10 14	biimtrid	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to \left(3\le A\to 2<A\right)$$
16	8 15	mpd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2<A$$
17		ltmul1a	$$⊢\left(\left(2\in ℝ\wedge A\in ℝ\wedge \left(A\in ℝ\wedge 0<A\right)\right)\wedge 2<A\right)\to 2A<AA$$
18	2 4 7 16 17	syl31anc	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2A<AA$$
19	3	zcnd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in ℂ$$
20	19	sqvald	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A^2=AA$$
21	18 20	breqtrrd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2A<A^2$$