Theorem nprmdvdsfacm1lem1

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

	Ref	Expression
Assertion	nprmdvdsfacm1lem1	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 ∥ ( 𝐴 · ( 2 · 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ℤ )
3		dvdsmul2	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 2 · 𝑁 ) )
4	1 2 3	sylancr	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∥ ( 2 · 𝑁 ) )
5	4	3ad2ant1	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 ∥ ( 2 · 𝑁 ) )
6		elfzoelz	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ℤ )
7	6	zcnd	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ℂ )
8		2cnd	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 2 ∈ ℂ )
9	7 8 7	mul12d	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 · ( 2 · 𝐴 ) ) = ( 2 · ( 𝐴 · 𝐴 ) ) )
10	9	3ad2ant2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 𝐴 · ( 2 · 𝐴 ) ) = ( 2 · ( 𝐴 · 𝐴 ) ) )
11		simp3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 = ( 𝐴 ↑ 2 ) )
12	7	sqvald	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
13	12	3ad2ant2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
14	11 13	eqtr2d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 𝐴 · 𝐴 ) = 𝑁 )
15	14	oveq2d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · ( 𝐴 · 𝐴 ) ) = ( 2 · 𝑁 ) )
16	10 15	eqtrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 𝐴 · ( 2 · 𝐴 ) ) = ( 2 · 𝑁 ) )
17	5 16	breqtrrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 ∥ ( 𝐴 · ( 2 · 𝐴 ) ) )