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 e. ( ZZ>= ` 3 ) -> ( 2 x. A ) < ( A ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2re	|- 2 e. RR
2	1	a1i	|- ( A e. ( ZZ>= ` 3 ) -> 2 e. RR )
3		eluzelz	|- ( A e. ( ZZ>= ` 3 ) -> A e. ZZ )
4	3	zred	|- ( A e. ( ZZ>= ` 3 ) -> A e. RR )
5		eluz3nn	|- ( A e. ( ZZ>= ` 3 ) -> A e. NN )
6	5	nngt0d	|- ( A e. ( ZZ>= ` 3 ) -> 0 < A )
7	4 6	jca	|- ( A e. ( ZZ>= ` 3 ) -> ( A e. RR /\ 0 < A ) )
8		eluzle	|- ( A e. ( ZZ>= ` 3 ) -> 3 <_ A )
9		df-3	|- 3 = ( 2 + 1 )
10	9	breq1i	|- ( 3 <_ A <-> ( 2 + 1 ) <_ A )
11		2z	|- 2 e. ZZ
12	11	a1i	|- ( A e. ( ZZ>= ` 3 ) -> 2 e. ZZ )
13	12 3	zltp1led	|- ( A e. ( ZZ>= ` 3 ) -> ( 2 < A <-> ( 2 + 1 ) <_ A ) )
14	13	biimprd	|- ( A e. ( ZZ>= ` 3 ) -> ( ( 2 + 1 ) <_ A -> 2 < A ) )
15	10 14	biimtrid	|- ( A e. ( ZZ>= ` 3 ) -> ( 3 <_ A -> 2 < A ) )
16	8 15	mpd	|- ( A e. ( ZZ>= ` 3 ) -> 2 < A )
17		ltmul1a	|- ( ( ( 2 e. RR /\ A e. RR /\ ( A e. RR /\ 0 < A ) ) /\ 2 < A ) -> ( 2 x. A ) < ( A x. A ) )
18	2 4 7 16 17	syl31anc	|- ( A e. ( ZZ>= ` 3 ) -> ( 2 x. A ) < ( A x. A ) )
19	3	zcnd	|- ( A e. ( ZZ>= ` 3 ) -> A e. CC )
20	19	sqvald	|- ( A e. ( ZZ>= ` 3 ) -> ( A ^ 2 ) = ( A x. A ) )
21	18 20	breqtrrd	|- ( A e. ( ZZ>= ` 3 ) -> ( 2 x. A ) < ( A ^ 2 ) )