Metamath Proof Explorer

Theorem nprmdvdsfacm1lem3

Description: Lemma 3 for nprmdvdsfacm1 . (Contributed by AV, 7-Apr-2026)

Ref Expression
Assertion nprmdvdsfacm1lem3 
|- ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( 2 x. A ) < ( N - 1 ) )

Proof

Step Hyp Ref Expression
1 3z 
 |-  3 e. ZZ
2 1 a1i 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> 3 e. ZZ )
3 elfzoelz 
 |-  ( A e. ( 2 ..^ N ) -> A e. ZZ )
4 3 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> A e. ZZ )
5 nprmdvdsfacm1lem2 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> 3 <_ A )
6 eluz2 
 |-  ( A e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ A e. ZZ /\ 3 <_ A ) )
7 2 4 5 6 syl3anbrc 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> A e. ( ZZ>= ` 3 ) )
8 2timesltsqm1 
 |-  ( A e. ( ZZ>= ` 3 ) -> ( 2 x. A ) < ( ( A ^ 2 ) - 1 ) )
9 7 8 syl 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( 2 x. A ) < ( ( A ^ 2 ) - 1 ) )
10 oveq1 
 |-  ( N = ( A ^ 2 ) -> ( N - 1 ) = ( ( A ^ 2 ) - 1 ) )
11 10 breq2d 
 |-  ( N = ( A ^ 2 ) -> ( ( 2 x. A ) < ( N - 1 ) <-> ( 2 x. A ) < ( ( A ^ 2 ) - 1 ) ) )
12 11 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( ( 2 x. A ) < ( N - 1 ) <-> ( 2 x. A ) < ( ( A ^ 2 ) - 1 ) ) )
13 9 12 mpbird 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( 2 x. A ) < ( N - 1 ) )