Theorem 2timesltsqm1

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

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

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2	1	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2\in ℝ$$
3		eluzelre	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in ℝ$$
4	2 3	remulcld	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2A\in ℝ$$
5		peano2rem	$$⊢A\in ℝ\to A-1\in ℝ$$
6	3 5	syl	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A-1\in ℝ$$
7	6 3	remulcld	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to \left(A-1\right)A\in ℝ$$
8		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in \mathbb{Z}$$
9		zsqcl	$$⊢A\in \mathbb{Z}\to A^2\in \mathbb{Z}$$
10	8 9	syl	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A^2\in \mathbb{Z}$$
11	10	zred	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A^2\in ℝ$$
12		peano2rem	$$⊢A^2\in ℝ\to A^2-1\in ℝ$$
13	11 12	syl	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A^2-1\in ℝ$$
14		2p1e3	$$⊢2+1=3$$
15		eluzle	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 3\le A$$
16	14 15	eqbrtrid	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2+1\le A$$
17		1red	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 1\in ℝ$$
18		leaddsub	$$⊢\left(2\in ℝ\wedge 1\in ℝ\wedge A\in ℝ\right)\to \left(2+1\le A\leftrightarrow 2\le A-1\right)$$
19	1 17 3 18	mp3an2i	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to \left(2+1\le A\leftrightarrow 2\le A-1\right)$$
20	16 19	mpbid	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2\le A-1$$
21		eluz3nn	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in \mathbb{N}$$
22	21	nnrpd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in {ℝ}^{+}$$
23	2 6 22	lemul1d	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to \left(2\le A-1\leftrightarrow 2A\le \left(A-1\right)A\right)$$
24	20 23	mpbid	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2A\le \left(A-1\right)A$$
25		eluzelcn	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in ℂ$$
26	25 25	mulsubfacd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to AA-A=\left(A-1\right)A$$
27	25	sqvald	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A^2=AA$$
28	27	eqcomd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to AA=A^2$$
29	28	oveq1d	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to AA-A=A^2-A$$
30		eluz2	$$⊢A\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(3\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge 3\le A\right)$$
31		df-3	$$⊢3=2+1$$
32	31	breq1i	$$⊢3\le A\leftrightarrow 2+1\le A$$
33		2z	$$⊢2\in \mathbb{Z}$$
34	33	a1i	$$⊢A\in \mathbb{Z}\to 2\in \mathbb{Z}$$
35		id	$$⊢A\in \mathbb{Z}\to A\in \mathbb{Z}$$
36	34 35	zltp1led	$$⊢A\in \mathbb{Z}\to \left(2<A\leftrightarrow 2+1\le A\right)$$
37	32 36	bitr4id	$$⊢A\in \mathbb{Z}\to \left(3\le A\leftrightarrow 2<A\right)$$
38		1red	$$⊢\left(A\in \mathbb{Z}\wedge 2<A\right)\to 1\in ℝ$$
39	1	a1i	$$⊢\left(A\in \mathbb{Z}\wedge 2<A\right)\to 2\in ℝ$$
40		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
41	40	adantr	$$⊢\left(A\in \mathbb{Z}\wedge 2<A\right)\to A\in ℝ$$
42		1lt2	$$⊢1<2$$
43	42	a1i	$$⊢\left(A\in \mathbb{Z}\wedge 2<A\right)\to 1<2$$
44		simpr	$$⊢\left(A\in \mathbb{Z}\wedge 2<A\right)\to 2<A$$
45	38 39 41 43 44	lttrd	$$⊢\left(A\in \mathbb{Z}\wedge 2<A\right)\to 1<A$$
46	45	ex	$$⊢A\in \mathbb{Z}\to \left(2<A\to 1<A\right)$$
47	37 46	sylbid	$$⊢A\in \mathbb{Z}\to \left(3\le A\to 1<A\right)$$
48	47	a1i	$$⊢3\in \mathbb{Z}\to \left(A\in \mathbb{Z}\to \left(3\le A\to 1<A\right)\right)$$
49	48	3imp	$$⊢\left(3\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge 3\le A\right)\to 1<A$$
50	30 49	sylbi	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 1<A$$
51	17 3 11 50	ltsub2dd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A^2-A<A^2-1$$
52	29 51	eqbrtrd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to AA-A<A^2-1$$
53	26 52	eqbrtrrd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to \left(A-1\right)A<A^2-1$$
54	4 7 13 24 53	lelttrd	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to 2A<A^2-1$$