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	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐴 ) < ( 𝐴 ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2re	⊢ 2 ∈ ℝ
2	1	a1i	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℝ )
3		eluzelz	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℤ )
4	3	zred	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℝ )
5		eluz3nn	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℕ )
6	5	nngt0d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 0 < 𝐴 )
7	4 6	jca	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
8		eluzle	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝐴 )
9		df-3	⊢ 3 = ( 2 + 1 )
10	9	breq1i	⊢ ( 3 ≤ 𝐴 ↔ ( 2 + 1 ) ≤ 𝐴 )
11		2z	⊢ 2 ∈ ℤ
12	11	a1i	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℤ )
13	12 3	zltp1led	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 < 𝐴 ↔ ( 2 + 1 ) ≤ 𝐴 ) )
14	13	biimprd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 2 + 1 ) ≤ 𝐴 → 2 < 𝐴 ) )
15	10 14	biimtrid	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 3 ≤ 𝐴 → 2 < 𝐴 ) )
16	8 15	mpd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 2 < 𝐴 )
17		ltmul1a	⊢ ( ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) ∧ 2 < 𝐴 ) → ( 2 · 𝐴 ) < ( 𝐴 · 𝐴 ) )
18	2 4 7 16 17	syl31anc	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐴 ) < ( 𝐴 · 𝐴 ) )
19	3	zcnd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℂ )
20	19	sqvald	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
21	18 20	breqtrrd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐴 ) < ( 𝐴 ↑ 2 ) )