Metamath Proof Explorer

Theorem nprmdvdsfacm1lem1

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

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

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 eluzelz 
 |-  ( N e. ( ZZ>= ` 6 ) -> N e. ZZ )
3 dvdsmul2 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> N || ( 2 x. N ) )
4 1 2 3 sylancr 
 |-  ( N e. ( ZZ>= ` 6 ) -> N || ( 2 x. N ) )
5 4 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> N || ( 2 x. N ) )
6 elfzoelz 
 |-  ( A e. ( 2 ..^ N ) -> A e. ZZ )
7 6 zcnd 
 |-  ( A e. ( 2 ..^ N ) -> A e. CC )
8 2cnd 
 |-  ( A e. ( 2 ..^ N ) -> 2 e. CC )
9 7 8 7 mul12d 
 |-  ( A e. ( 2 ..^ N ) -> ( A x. ( 2 x. A ) ) = ( 2 x. ( A x. A ) ) )
10 9 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( A x. ( 2 x. A ) ) = ( 2 x. ( A x. A ) ) )
11 simp3 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> N = ( A ^ 2 ) )
12 7 sqvald 
 |-  ( A e. ( 2 ..^ N ) -> ( A ^ 2 ) = ( A x. A ) )
13 12 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( A ^ 2 ) = ( A x. A ) )
14 11 13 eqtr2d 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( A x. A ) = N )
15 14 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( 2 x. ( A x. A ) ) = ( 2 x. N ) )
16 10 15 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> ( A x. ( 2 x. A ) ) = ( 2 x. N ) )
17 5 16 breqtrrd 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> N || ( A x. ( 2 x. A ) ) )