Theorem 8gbe

Description: 8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020)

	Ref	Expression
Assertion	8gbe	⊢ 8 ∈ GoldbachEven

Proof

Step	Hyp	Ref	Expression
1		8even	⊢ 8 ∈ Even
2		5prm	⊢ 5 ∈ ℙ
3		3prm	⊢ 3 ∈ ℙ
4		5odd	⊢ 5 ∈ Odd
5		3odd	⊢ 3 ∈ Odd
6		5p3e8	⊢ ( 5 + 3 ) = 8
7	6	eqcomi	⊢ 8 = ( 5 + 3 )
8	4 5 7	3pm3.2i	⊢ ( 5 ∈ Odd ∧ 3 ∈ Odd ∧ 8 = ( 5 + 3 ) )
9		eleq1	⊢ ( 𝑝 = 5 → ( 𝑝 ∈ Odd ↔ 5 ∈ Odd ) )
10		biidd	⊢ ( 𝑝 = 5 → ( 𝑞 ∈ Odd ↔ 𝑞 ∈ Odd ) )
11		oveq1	⊢ ( 𝑝 = 5 → ( 𝑝 + 𝑞 ) = ( 5 + 𝑞 ) )
12	11	eqeq2d	⊢ ( 𝑝 = 5 → ( 8 = ( 𝑝 + 𝑞 ) ↔ 8 = ( 5 + 𝑞 ) ) )
13	9 10 12	3anbi123d	⊢ ( 𝑝 = 5 → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 𝑝 + 𝑞 ) ) ↔ ( 5 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 5 + 𝑞 ) ) ) )
14		biidd	⊢ ( 𝑞 = 3 → ( 5 ∈ Odd ↔ 5 ∈ Odd ) )
15		eleq1	⊢ ( 𝑞 = 3 → ( 𝑞 ∈ Odd ↔ 3 ∈ Odd ) )
16		oveq2	⊢ ( 𝑞 = 3 → ( 5 + 𝑞 ) = ( 5 + 3 ) )
17	16	eqeq2d	⊢ ( 𝑞 = 3 → ( 8 = ( 5 + 𝑞 ) ↔ 8 = ( 5 + 3 ) ) )
18	14 15 17	3anbi123d	⊢ ( 𝑞 = 3 → ( ( 5 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 5 + 𝑞 ) ) ↔ ( 5 ∈ Odd ∧ 3 ∈ Odd ∧ 8 = ( 5 + 3 ) ) ) )
19	13 18	rspc2ev	⊢ ( ( 5 ∈ ℙ ∧ 3 ∈ ℙ ∧ ( 5 ∈ Odd ∧ 3 ∈ Odd ∧ 8 = ( 5 + 3 ) ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 𝑝 + 𝑞 ) ) )
20	2 3 8 19	mp3an	⊢ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 𝑝 + 𝑞 ) )
21		isgbe	⊢ ( 8 ∈ GoldbachEven ↔ ( 8 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 𝑝 + 𝑞 ) ) ) )
22	1 20 21	mpbir2an	⊢ 8 ∈ GoldbachEven