Metamath Proof Explorer


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