| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-9 12336 | . . 3
⊢ 9 = (8 +
1) | 
| 2 |  | 8even 47700 | . . . 4
⊢ 8 ∈
Even | 
| 3 |  | evenp1odd 47627 | . . . 4
⊢ (8 ∈
Even → (8 + 1) ∈ Odd ) | 
| 4 | 2, 3 | ax-mp 5 | . . 3
⊢ (8 + 1)
∈ Odd | 
| 5 | 1, 4 | eqeltri 2837 | . 2
⊢ 9 ∈
Odd | 
| 6 |  | 3prm 16731 | . . 3
⊢ 3 ∈
ℙ | 
| 7 |  | 3odd 47695 | . . . . . 6
⊢ 3 ∈
Odd | 
| 8 | 7, 7, 7 | 3pm3.2i 1340 | . . . . 5
⊢ (3 ∈
Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd ) | 
| 9 |  | gbpart9 47756 | . . . . 5
⊢ 9 = ((3 +
3) + 3) | 
| 10 | 8, 9 | pm3.2i 470 | . . . 4
⊢ ((3
∈ Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd ) ∧ 9 = ((3 + 3) +
3)) | 
| 11 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑟 = 3 → (𝑟 ∈ Odd ↔ 3 ∈ Odd
)) | 
| 12 | 11 | 3anbi3d 1444 | . . . . . 6
⊢ (𝑟 = 3 → ((3 ∈ Odd ∧
3 ∈ Odd ∧ 𝑟 ∈
Odd ) ↔ (3 ∈ Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd
))) | 
| 13 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑟 = 3 → ((3 + 3) + 𝑟) = ((3 + 3) +
3)) | 
| 14 | 13 | eqeq2d 2748 | . . . . . 6
⊢ (𝑟 = 3 → (9 = ((3 + 3) +
𝑟) ↔ 9 = ((3 + 3) +
3))) | 
| 15 | 12, 14 | anbi12d 632 | . . . . 5
⊢ (𝑟 = 3 → (((3 ∈ Odd
∧ 3 ∈ Odd ∧ 𝑟
∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟)) ↔ ((3 ∈ Odd ∧ 3 ∈ Odd
∧ 3 ∈ Odd ) ∧ 9 = ((3 + 3) + 3)))) | 
| 16 | 15 | rspcev 3622 | . . . 4
⊢ ((3
∈ ℙ ∧ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 3 ∈ Odd )
∧ 9 = ((3 + 3) + 3))) → ∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 3 ∈
Odd ∧ 𝑟 ∈ Odd )
∧ 9 = ((3 + 3) + 𝑟))) | 
| 17 | 6, 10, 16 | mp2an 692 | . . 3
⊢
∃𝑟 ∈
ℙ ((3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟)) | 
| 18 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑝 = 3 → (𝑝 ∈ Odd ↔ 3 ∈ Odd
)) | 
| 19 | 18 | 3anbi1d 1442 | . . . . . 6
⊢ (𝑝 = 3 → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (3 ∈ Odd ∧
𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ))) | 
| 20 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑝 = 3 → (𝑝 + 𝑞) = (3 + 𝑞)) | 
| 21 | 20 | oveq1d 7446 | . . . . . . 7
⊢ (𝑝 = 3 → ((𝑝 + 𝑞) + 𝑟) = ((3 + 𝑞) + 𝑟)) | 
| 22 | 21 | eqeq2d 2748 | . . . . . 6
⊢ (𝑝 = 3 → (9 = ((𝑝 + 𝑞) + 𝑟) ↔ 9 = ((3 + 𝑞) + 𝑟))) | 
| 23 | 19, 22 | anbi12d 632 | . . . . 5
⊢ (𝑝 = 3 → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 +
𝑞) + 𝑟)))) | 
| 24 | 23 | rexbidv 3179 | . . . 4
⊢ (𝑝 = 3 → (∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((𝑝 + 𝑞) + 𝑟)) ↔ ∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((3 +
𝑞) + 𝑟)))) | 
| 25 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑞 = 3 → (𝑞 ∈ Odd ↔ 3 ∈ Odd
)) | 
| 26 | 25 | 3anbi2d 1443 | . . . . . 6
⊢ (𝑞 = 3 → ((3 ∈ Odd ∧
𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (3 ∈
Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ))) | 
| 27 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑞 = 3 → (3 + 𝑞) = (3 + 3)) | 
| 28 | 27 | oveq1d 7446 | . . . . . . 7
⊢ (𝑞 = 3 → ((3 + 𝑞) + 𝑟) = ((3 + 3) + 𝑟)) | 
| 29 | 28 | eqeq2d 2748 | . . . . . 6
⊢ (𝑞 = 3 → (9 = ((3 + 𝑞) + 𝑟) ↔ 9 = ((3 + 3) + 𝑟))) | 
| 30 | 26, 29 | anbi12d 632 | . . . . 5
⊢ (𝑞 = 3 → (((3 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 9 =
((3 + 𝑞) + 𝑟)) ↔ ((3 ∈ Odd ∧ 3
∈ Odd ∧ 𝑟 ∈
Odd ) ∧ 9 = ((3 + 3) + 𝑟)))) | 
| 31 | 30 | rexbidv 3179 | . . . 4
⊢ (𝑞 = 3 → (∃𝑟 ∈ ℙ ((3 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 9 =
((3 + 𝑞) + 𝑟)) ↔ ∃𝑟 ∈ ℙ ((3 ∈ Odd
∧ 3 ∈ Odd ∧ 𝑟
∈ Odd ) ∧ 9 = ((3 + 3) + 𝑟)))) | 
| 32 | 24, 31 | rspc2ev 3635 | . . 3
⊢ ((3
∈ ℙ ∧ 3 ∈ ℙ ∧ ∃𝑟 ∈ ℙ ((3 ∈ Odd ∧ 3 ∈
Odd ∧ 𝑟 ∈ Odd )
∧ 9 = ((3 + 3) + 𝑟)))
→ ∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 9 =
((𝑝 + 𝑞) + 𝑟))) | 
| 33 | 6, 6, 17, 32 | mp3an 1463 | . 2
⊢
∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 9 =
((𝑝 + 𝑞) + 𝑟)) | 
| 34 |  | isgbo 47740 | . 2
⊢ (9 ∈
GoldbachOdd ↔ (9 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 9 = ((𝑝 + 𝑞) + 𝑟)))) | 
| 35 | 5, 33, 34 | mpbir2an 711 | 1
⊢ 9 ∈
GoldbachOdd |