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 ⊢ r = 3 → 2 + 2 + r = 2 + 2 + 3
6 5 rspceeqv ⊢ 3 ∈ ℙ ∧ 7 = 2 + 2 + 3 → ∃ r ∈ ℙ 7 = 2 + 2 + r
7 3 4 6 mp2an ⊢ ∃ r ∈ ℙ 7 = 2 + 2 + r
8 oveq1 ⊢ p = 2 → p + q = 2 + q
9 8 oveq1d ⊢ p = 2 → p + q + r = 2 + q + r
10 9 eqeq2d ⊢ p = 2 → 7 = p + q + r ↔ 7 = 2 + q + r
11 10 rexbidv ⊢ p = 2 → ∃ r ∈ ℙ 7 = p + q + r ↔ ∃ r ∈ ℙ 7 = 2 + q + r
12 oveq2 ⊢ q = 2 → 2 + q = 2 + 2
13 12 oveq1d ⊢ q = 2 → 2 + q + r = 2 + 2 + r
14 13 eqeq2d ⊢ q = 2 → 7 = 2 + q + r ↔ 7 = 2 + 2 + r
15 14 rexbidv ⊢ q = 2 → ∃ r ∈ ℙ 7 = 2 + q + r ↔ ∃ r ∈ ℙ 7 = 2 + 2 + r
16 11 15 rspc2ev ⊢ 2 ∈ ℙ ∧ 2 ∈ ℙ ∧ ∃ r ∈ ℙ 7 = 2 + 2 + r → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ 7 = p + q + r
17 2 2 7 16 mp3an ⊢ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ 7 = p + q + r
18 isgbow ⊢ 7 ∈ GoldbachOddW ↔ 7 ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ 7 = p + q + r
19 1 17 18 mpbir2an ⊢ 7 ∈ GoldbachOddW