nprmdvdsfacm1lem3

		Ref	Expression
	Assertion	nprmdvdsfacm1lem3	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A < N - 1$

Step	Hyp	Ref	Expression
1		3z	$⊢ 3 \in ℤ$
2	1	a1i	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 3 \in ℤ$
3		elfzoelz	$⊢ A \in (2 ..^N) \to A \in ℤ$
4	3	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A \in ℤ$
5		nprmdvdsfacm1lem2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 3 \leq A$
6		eluz2	$⊢ A \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land A \in ℤ \land 3 \leq A)$
7	2 4 5 6	syl3anbrc	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A \in ℤ_{\geq 3}$
8		2timesltsqm1	$⊢ A \in ℤ_{\geq 3} \to 2 A < A^{2} - 1$
9	7 8	syl	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A < A^{2} - 1$
10		oveq1	$⊢ N = A^{2} \to N - 1 = A^{2} - 1$
11	10	breq2d	$⊢ N = A^{2} \to (2 A < N - 1 \leftrightarrow 2 A < A^{2} - 1)$
12	11	3ad2ant3	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to (2 A < N - 1 \leftrightarrow 2 A < A^{2} - 1)$
13	9 12	mpbird	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A < N - 1$

Metamath Proof Explorer