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

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1 a1i 
 |-  ( A e. ( ZZ>= ` 3 ) -> 2 e. RR )
3 eluzelre 
 |-  ( A e. ( ZZ>= ` 3 ) -> A e. RR )
4 2 3 remulcld 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( 2 x. A ) e. RR )
5 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
6 3 5 syl 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( A - 1 ) e. RR )
7 6 3 remulcld 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( ( A - 1 ) x. A ) e. RR )
8 eluzelz 
 |-  ( A e. ( ZZ>= ` 3 ) -> A e. ZZ )
9 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
10 8 9 syl 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( A ^ 2 ) e. ZZ )
11 10 zred 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( A ^ 2 ) e. RR )
12 peano2rem 
 |-  ( ( A ^ 2 ) e. RR -> ( ( A ^ 2 ) - 1 ) e. RR )
13 11 12 syl 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( ( A ^ 2 ) - 1 ) e. RR )
14 2p1e3 
 |-  ( 2 + 1 ) = 3
15 eluzle 
 |-  ( A e. ( ZZ>= ` 3 ) -> 3 <_ A )
16 14 15 eqbrtrid 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( 2 + 1 ) <_ A )
17 1red 
 |-  ( A e. ( ZZ>= ` 3 ) -> 1 e. RR )
18 leaddsub 
 |-  ( ( 2 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 2 + 1 ) <_ A <-> 2 <_ ( A - 1 ) ) )
19 1 17 3 18 mp3an2i 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( ( 2 + 1 ) <_ A <-> 2 <_ ( A - 1 ) ) )
20 16 19 mpbid 
 |-  ( A e. ( ZZ>= ` 3 ) -> 2 <_ ( A - 1 ) )
21 eluz3nn 
 |-  ( A e. ( ZZ>= ` 3 ) -> A e. NN )
22 21 nnrpd 
 |-  ( A e. ( ZZ>= ` 3 ) -> A e. RR+ )
23 2 6 22 lemul1d 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( 2 <_ ( A - 1 ) <-> ( 2 x. A ) <_ ( ( A - 1 ) x. A ) ) )
24 20 23 mpbid 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( 2 x. A ) <_ ( ( A - 1 ) x. A ) )
25 eluzelcn 
 |-  ( A e. ( ZZ>= ` 3 ) -> A e. CC )
26 25 25 mulsubfacd 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( ( A x. A ) - A ) = ( ( A - 1 ) x. A ) )
27 25 sqvald 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( A ^ 2 ) = ( A x. A ) )
28 27 eqcomd 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( A x. A ) = ( A ^ 2 ) )
29 28 oveq1d 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( ( A x. A ) - A ) = ( ( A ^ 2 ) - A ) )
30 eluz2 
 |-  ( A e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ A e. ZZ /\ 3 <_ A ) )
31 df-3 
 |-  3 = ( 2 + 1 )
32 31 breq1i 
 |-  ( 3 <_ A <-> ( 2 + 1 ) <_ A )
33 2z 
 |-  2 e. ZZ
34 33 a1i 
 |-  ( A e. ZZ -> 2 e. ZZ )
35 id 
 |-  ( A e. ZZ -> A e. ZZ )
36 34 35 zltp1led 
 |-  ( A e. ZZ -> ( 2 < A <-> ( 2 + 1 ) <_ A ) )
37 32 36 bitr4id 
 |-  ( A e. ZZ -> ( 3 <_ A <-> 2 < A ) )
38 1red 
 |-  ( ( A e. ZZ /\ 2 < A ) -> 1 e. RR )
39 1 a1i 
 |-  ( ( A e. ZZ /\ 2 < A ) -> 2 e. RR )
40 zre 
 |-  ( A e. ZZ -> A e. RR )
41 40 adantr 
 |-  ( ( A e. ZZ /\ 2 < A ) -> A e. RR )
42 1lt2 
 |-  1 < 2
43 42 a1i 
 |-  ( ( A e. ZZ /\ 2 < A ) -> 1 < 2 )
44 simpr 
 |-  ( ( A e. ZZ /\ 2 < A ) -> 2 < A )
45 38 39 41 43 44 lttrd 
 |-  ( ( A e. ZZ /\ 2 < A ) -> 1 < A )
46 45 ex 
 |-  ( A e. ZZ -> ( 2 < A -> 1 < A ) )
47 37 46 sylbid 
 |-  ( A e. ZZ -> ( 3 <_ A -> 1 < A ) )
48 47 a1i 
 |-  ( 3 e. ZZ -> ( A e. ZZ -> ( 3 <_ A -> 1 < A ) ) )
49 48 3imp 
 |-  ( ( 3 e. ZZ /\ A e. ZZ /\ 3 <_ A ) -> 1 < A )
50 30 49 sylbi 
 |-  ( A e. ( ZZ>= ` 3 ) -> 1 < A )
51 17 3 11 50 ltsub2dd 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( ( A ^ 2 ) - A ) < ( ( A ^ 2 ) - 1 ) )
52 29 51 eqbrtrd 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( ( A x. A ) - A ) < ( ( A ^ 2 ) - 1 ) )
53 26 52 eqbrtrrd 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( ( A - 1 ) x. A ) < ( ( A ^ 2 ) - 1 ) )
54 4 7 13 24 53 lelttrd 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( 2 x. A ) < ( ( A ^ 2 ) - 1 ) )