Theorem 6gbe

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

	Ref	Expression
Assertion	6gbe	⊢ 6 ∈ GoldbachEven

Proof

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