This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbgoldbaltlem2

Description: Lemma 2 for sbgoldbalt : If an even number greater than 4 is the sum of two primes, the primes must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020)

		Ref	Expression
	Assertion	sbgoldbaltlem2	$⊢ (P \in ℙ \land Q \in ℙ) \to ((N \in Even \land 4 < N \land N = P + Q) \to (P \in Odd \land Q \in Odd))$

Proof

Step	Hyp	Ref	Expression
1		prmz	$⊢ P \in ℙ \to P \in ℤ$
2	1	zcnd	$⊢ P \in ℙ \to P \in ℂ$
3		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
4	3	zcnd	$⊢ Q \in ℙ \to Q \in ℂ$
5		addcom	$⊢ (P \in ℂ \land Q \in ℂ) \to P + Q = Q + P$
6	2 4 5	syl2anr	$⊢ (Q \in ℙ \land P \in ℙ) \to P + Q = Q + P$
7	6	eqeq2d	$⊢ (Q \in ℙ \land P \in ℙ) \to (N = P + Q \leftrightarrow N = Q + P)$
8	7	3anbi3d	$⊢ (Q \in ℙ \land P \in ℙ) \to ((N \in Even \land 4 < N \land N = P + Q) \leftrightarrow (N \in Even \land 4 < N \land N = Q + P))$
9		sbgoldbaltlem1	$⊢ (Q \in ℙ \land P \in ℙ) \to ((N \in Even \land 4 < N \land N = Q + P) \to P \in Odd)$
10	8 9	sylbid	$⊢ (Q \in ℙ \land P \in ℙ) \to ((N \in Even \land 4 < N \land N = P + Q) \to P \in Odd)$
11	10	ancoms	$⊢ (P \in ℙ \land Q \in ℙ) \to ((N \in Even \land 4 < N \land N = P + Q) \to P \in Odd)$
12		sbgoldbaltlem1	$⊢ (P \in ℙ \land Q \in ℙ) \to ((N \in Even \land 4 < N \land N = P + Q) \to Q \in Odd)$
13	11 12	jcad	$⊢ (P \in ℙ \land Q \in ℙ) \to ((N \in Even \land 4 < N \land N = P + Q) \to (P \in Odd \land Q \in Odd))$