nprmdvdsfacm1lem1

		Ref	Expression
	Assertion	nprmdvdsfacm1lem1	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N ∥ A 2 A$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		eluzelz	$⊢ N \in ℤ_{\geq 6} \to N \in ℤ$
3		dvdsmul2	$⊢ (2 \in ℤ \land N \in ℤ) \to N ∥ 2 \cdot N$
4	1 2 3	sylancr	$⊢ N \in ℤ_{\geq 6} \to N ∥ 2 \cdot N$
5	4	3ad2ant1	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N ∥ 2 \cdot N$
6		elfzoelz	$⊢ A \in (2 ..^N) \to A \in ℤ$
7	6	zcnd	$⊢ A \in (2 ..^N) \to A \in ℂ$
8		2cnd	$⊢ A \in (2 ..^N) \to 2 \in ℂ$
9	7 8 7	mul12d	$⊢ A \in (2 ..^N) \to A 2 A = 2 A A$
10	9	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A 2 A = 2 A A$
11		simp3	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N = A^{2}$
12	7	sqvald	$⊢ A \in (2 ..^N) \to A^{2} = A A$
13	12	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A^{2} = A A$
14	11 13	eqtr2d	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A A = N$
15	14	oveq2d	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A A = 2 \cdot N$
16	10 15	eqtrd	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A 2 A = 2 \cdot N$
17	5 16	breqtrrd	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N ∥ A 2 A$

Metamath Proof Explorer