Theorem 7gbow

Description: 7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020)

	Ref	Expression
Assertion	7gbow	⊢ 7 ∈ GoldbachOddW

Proof

Step	Hyp	Ref	Expression
1		7odd	⊢ 7 ∈ Odd
2		2prm	⊢ 2 ∈ ℙ
3		3prm	⊢ 3 ∈ ℙ
4		gbpart7	⊢ 7 = ( ( 2 + 2 ) + 3 )
5		oveq2	⊢ ( 𝑟 = 3 → ( ( 2 + 2 ) + 𝑟 ) = ( ( 2 + 2 ) + 3 ) )
6	5	rspceeqv	⊢ ( ( 3 ∈ ℙ ∧ 7 = ( ( 2 + 2 ) + 3 ) ) → ∃ 𝑟 ∈ ℙ 7 = ( ( 2 + 2 ) + 𝑟 ) )
7	3 4 6	mp2an	⊢ ∃ 𝑟 ∈ ℙ 7 = ( ( 2 + 2 ) + 𝑟 )
8		oveq1	⊢ ( 𝑝 = 2 → ( 𝑝 + 𝑞 ) = ( 2 + 𝑞 ) )
9	8	oveq1d	⊢ ( 𝑝 = 2 → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( 2 + 𝑞 ) + 𝑟 ) )
10	9	eqeq2d	⊢ ( 𝑝 = 2 → ( 7 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 7 = ( ( 2 + 𝑞 ) + 𝑟 ) ) )
11	10	rexbidv	⊢ ( 𝑝 = 2 → ( ∃ 𝑟 ∈ ℙ 7 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ ℙ 7 = ( ( 2 + 𝑞 ) + 𝑟 ) ) )
12		oveq2	⊢ ( 𝑞 = 2 → ( 2 + 𝑞 ) = ( 2 + 2 ) )
13	12	oveq1d	⊢ ( 𝑞 = 2 → ( ( 2 + 𝑞 ) + 𝑟 ) = ( ( 2 + 2 ) + 𝑟 ) )
14	13	eqeq2d	⊢ ( 𝑞 = 2 → ( 7 = ( ( 2 + 𝑞 ) + 𝑟 ) ↔ 7 = ( ( 2 + 2 ) + 𝑟 ) ) )
15	14	rexbidv	⊢ ( 𝑞 = 2 → ( ∃ 𝑟 ∈ ℙ 7 = ( ( 2 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ ℙ 7 = ( ( 2 + 2 ) + 𝑟 ) ) )
16	11 15	rspc2ev	⊢ ( ( 2 ∈ ℙ ∧ 2 ∈ ℙ ∧ ∃ 𝑟 ∈ ℙ 7 = ( ( 2 + 2 ) + 𝑟 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 7 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
17	2 2 7 16	mp3an	⊢ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 7 = ( ( 𝑝 + 𝑞 ) + 𝑟 )
18		isgbow	⊢ ( 7 ∈ GoldbachOddW ↔ ( 7 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 7 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
19	1 17 18	mpbir2an	⊢ 7 ∈ GoldbachOddW