This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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