Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 1 a1i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℝ )
3 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℝ )
4 2 3 remulcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐴 ) ∈ ℝ )
5 peano2rem ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℝ )
6 3 5 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐴 − 1 ) ∈ ℝ )
7 6 3 remulcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝐴 − 1 ) · 𝐴 ) ∈ ℝ )
8 eluzelz ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℤ )
9 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
10 8 9 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
11 10 zred ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
12 peano2rem ⊢ ( ( 𝐴 ↑ 2 ) ∈ ℝ → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ )
13 11 12 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ )
14 2p1e3 ⊢ ( 2 + 1 ) = 3
15 eluzle ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝐴 )
16 14 15 eqbrtrid ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 + 1 ) ≤ 𝐴 )
17 1red ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℝ )
18 leaddsub ⊢ ( ( 2 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 2 + 1 ) ≤ 𝐴 ↔ 2 ≤ ( 𝐴 − 1 ) ) )
19 1 17 3 18 mp3an2i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 2 + 1 ) ≤ 𝐴 ↔ 2 ≤ ( 𝐴 − 1 ) ) )
20 16 19 mpbid ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ ( 𝐴 − 1 ) )
21 eluz3nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℕ )
22 21 nnrpd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℝ+ )
23 2 6 22 lemul1d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 ≤ ( 𝐴 − 1 ) ↔ ( 2 · 𝐴 ) ≤ ( ( 𝐴 − 1 ) · 𝐴 ) ) )
24 20 23 mpbid ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐴 ) ≤ ( ( 𝐴 − 1 ) · 𝐴 ) )
25 eluzelcn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ℂ )
26 25 25 mulsubfacd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝐴 · 𝐴 ) − 𝐴 ) = ( ( 𝐴 − 1 ) · 𝐴 ) )
27 25 sqvald ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
28 27 eqcomd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐴 · 𝐴 ) = ( 𝐴 ↑ 2 ) )
29 28 oveq1d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝐴 · 𝐴 ) − 𝐴 ) = ( ( 𝐴 ↑ 2 ) − 𝐴 ) )
30 eluz2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 3 ≤ 𝐴 ) )
31 df-3 ⊢ 3 = ( 2 + 1 )
32 31 breq1i ⊢ ( 3 ≤ 𝐴 ↔ ( 2 + 1 ) ≤ 𝐴 )
33 2z ⊢ 2 ∈ ℤ
34 33 a1i ⊢ ( 𝐴 ∈ ℤ → 2 ∈ ℤ )
35 id ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℤ )
36 34 35 zltp1led ⊢ ( 𝐴 ∈ ℤ → ( 2 < 𝐴 ↔ ( 2 + 1 ) ≤ 𝐴 ) )
37 32 36 bitr4id ⊢ ( 𝐴 ∈ ℤ → ( 3 ≤ 𝐴 ↔ 2 < 𝐴 ) )
38 1red ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → 1 ∈ ℝ )
39 1 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → 2 ∈ ℝ )
40 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
41 40 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → 𝐴 ∈ ℝ )
42 1lt2 ⊢ 1 < 2
43 42 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → 1 < 2 )
44 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → 2 < 𝐴 )
45 38 39 41 43 44 lttrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → 1 < 𝐴 )
46 45 ex ⊢ ( 𝐴 ∈ ℤ → ( 2 < 𝐴 → 1 < 𝐴 ) )
47 37 46 sylbid ⊢ ( 𝐴 ∈ ℤ → ( 3 ≤ 𝐴 → 1 < 𝐴 ) )
48 47 a1i ⊢ ( 3 ∈ ℤ → ( 𝐴 ∈ ℤ → ( 3 ≤ 𝐴 → 1 < 𝐴 ) ) )
49 48 3imp ⊢ ( ( 3 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 3 ≤ 𝐴 ) → 1 < 𝐴 )
50 30 49 sylbi ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 1 < 𝐴 )
51 17 3 11 50 ltsub2dd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝐴 ↑ 2 ) − 𝐴 ) < ( ( 𝐴 ↑ 2 ) − 1 ) )
52 29 51 eqbrtrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝐴 · 𝐴 ) − 𝐴 ) < ( ( 𝐴 ↑ 2 ) − 1 ) )
53 26 52 eqbrtrrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝐴 − 1 ) · 𝐴 ) < ( ( 𝐴 ↑ 2 ) − 1 ) )
54 4 7 13 24 53 lelttrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐴 ) < ( ( 𝐴 ↑ 2 ) − 1 ) )