Theorem sbgoldbaltlem1

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

	Ref	Expression
Assertion	sbgoldbaltlem1	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) )

Proof

Step	Hyp	Ref	Expression
1		prmnn	⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℕ )
2		nneoALTV	⊢ ( 𝑄 ∈ ℕ → ( 𝑄 ∈ Even ↔ ¬ 𝑄 ∈ Odd ) )
3	2	bicomd	⊢ ( 𝑄 ∈ ℕ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 ∈ Even ) )
4	1 3	syl	⊢ ( 𝑄 ∈ ℙ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 ∈ Even ) )
5		evenprm2	⊢ ( 𝑄 ∈ ℙ → ( 𝑄 ∈ Even ↔ 𝑄 = 2 ) )
6	4 5	bitrd	⊢ ( 𝑄 ∈ ℙ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 = 2 ) )
7	6	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 = 2 ) )
8		oveq2	⊢ ( 𝑄 = 2 → ( 𝑃 + 𝑄 ) = ( 𝑃 + 2 ) )
9	8	eqeq2d	⊢ ( 𝑄 = 2 → ( 𝑁 = ( 𝑃 + 𝑄 ) ↔ 𝑁 = ( 𝑃 + 2 ) ) )
10	9	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( 𝑁 = ( 𝑃 + 𝑄 ) ↔ 𝑁 = ( 𝑃 + 2 ) ) )
11	10	3anbi3d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) ↔ ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 2 ) ) ) )
12		breq2	⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( 4 < 𝑁 ↔ 4 < ( 𝑃 + 2 ) ) )
13		eleq1	⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( 𝑁 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) )
14	12 13	anbi12d	⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( ( 4 < 𝑁 ∧ 𝑁 ∈ Even ) ↔ ( 4 < ( 𝑃 + 2 ) ∧ ( 𝑃 + 2 ) ∈ Even ) ) )
15		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
16		2evenALTV	⊢ 2 ∈ Even
17		evensumeven	⊢ ( ( 𝑃 ∈ ℤ ∧ 2 ∈ Even ) → ( 𝑃 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) )
18	15 16 17	sylancl	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) )
19		evenprm2	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ 𝑃 = 2 ) )
20		oveq1	⊢ ( 𝑃 = 2 → ( 𝑃 + 2 ) = ( 2 + 2 ) )
21		2p2e4	⊢ ( 2 + 2 ) = 4
22	20 21	eqtrdi	⊢ ( 𝑃 = 2 → ( 𝑃 + 2 ) = 4 )
23	22	breq2d	⊢ ( 𝑃 = 2 → ( 4 < ( 𝑃 + 2 ) ↔ 4 < 4 ) )
24		4re	⊢ 4 ∈ ℝ
25	24	ltnri	⊢ ¬ 4 < 4
26	25	pm2.21i	⊢ ( 4 < 4 → 𝑄 ∈ Odd )
27	23 26	biimtrdi	⊢ ( 𝑃 = 2 → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) )
28	19 27	biimtrdi	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) ) )
29	18 28	sylbird	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 + 2 ) ∈ Even → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) ) )
30	29	com13	⊢ ( 4 < ( 𝑃 + 2 ) → ( ( 𝑃 + 2 ) ∈ Even → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) )
31	30	imp	⊢ ( ( 4 < ( 𝑃 + 2 ) ∧ ( 𝑃 + 2 ) ∈ Even ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) )
32	14 31	biimtrdi	⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( ( 4 < 𝑁 ∧ 𝑁 ∈ Even ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) )
33	32	expd	⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( 4 < 𝑁 → ( 𝑁 ∈ Even → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) ) )
34	33	com13	⊢ ( 𝑁 ∈ Even → ( 4 < 𝑁 → ( 𝑁 = ( 𝑃 + 2 ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) ) )
35	34	3imp	⊢ ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 2 ) ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) )
36	35	com12	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 2 ) ) → 𝑄 ∈ Odd ) )
37	36	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 2 ) ) → 𝑄 ∈ Odd ) )
38	11 37	sylbid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) )
39	38	ex	⊢ ( 𝑃 ∈ ℙ → ( 𝑄 = 2 → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) )
40	39	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑄 = 2 → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) )
41	7 40	sylbid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ¬ 𝑄 ∈ Odd → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) )
42		ax-1	⊢ ( 𝑄 ∈ Odd → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) )
43	41 42	pm2.61d2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) )