Proof of Theorem sbgoldbaltlem1
| Step | Hyp | Ref
| Expression |
| 1 | | prmnn 16711 |
. . . . . 6
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) |
| 2 | | nneoALTV 47659 |
. . . . . . 7
⊢ (𝑄 ∈ ℕ → (𝑄 ∈ Even ↔ ¬ 𝑄 ∈ Odd )) |
| 3 | 2 | bicomd 223 |
. . . . . 6
⊢ (𝑄 ∈ ℕ → (¬
𝑄 ∈ Odd ↔ 𝑄 ∈ Even )) |
| 4 | 1, 3 | syl 17 |
. . . . 5
⊢ (𝑄 ∈ ℙ → (¬
𝑄 ∈ Odd ↔ 𝑄 ∈ Even )) |
| 5 | | evenprm2 47701 |
. . . . 5
⊢ (𝑄 ∈ ℙ → (𝑄 ∈ Even ↔ 𝑄 = 2)) |
| 6 | 4, 5 | bitrd 279 |
. . . 4
⊢ (𝑄 ∈ ℙ → (¬
𝑄 ∈ Odd ↔ 𝑄 = 2)) |
| 7 | 6 | adantl 481 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → (¬
𝑄 ∈ Odd ↔ 𝑄 = 2)) |
| 8 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑄 = 2 → (𝑃 + 𝑄) = (𝑃 + 2)) |
| 9 | 8 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑄 = 2 → (𝑁 = (𝑃 + 𝑄) ↔ 𝑁 = (𝑃 + 2))) |
| 10 | 9 | adantl 481 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 = 2) → (𝑁 = (𝑃 + 𝑄) ↔ 𝑁 = (𝑃 + 2))) |
| 11 | 10 | 3anbi3d 1444 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 = 2) → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) ↔ (𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 2)))) |
| 12 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (𝑁 = (𝑃 + 2) → (4 < 𝑁 ↔ 4 < (𝑃 + 2))) |
| 13 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑁 = (𝑃 + 2) → (𝑁 ∈ Even ↔ (𝑃 + 2) ∈ Even )) |
| 14 | 12, 13 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑁 = (𝑃 + 2) → ((4 < 𝑁 ∧ 𝑁 ∈ Even ) ↔ (4 < (𝑃 + 2) ∧ (𝑃 + 2) ∈ Even ))) |
| 15 | | prmz 16712 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 16 | | 2evenALTV 47679 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
Even |
| 17 | | evensumeven 47694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℤ ∧ 2 ∈
Even ) → (𝑃 ∈
Even ↔ (𝑃 + 2) ∈
Even )) |
| 18 | 15, 16, 17 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ (𝑃 + 2) ∈ Even
)) |
| 19 | | evenprm2 47701 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ 𝑃 = 2)) |
| 20 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 = 2 → (𝑃 + 2) = (2 + 2)) |
| 21 | | 2p2e4 12401 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 + 2) =
4 |
| 22 | 20, 21 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 = 2 → (𝑃 + 2) = 4) |
| 23 | 22 | breq2d 5155 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 = 2 → (4 < (𝑃 + 2) ↔ 4 <
4)) |
| 24 | | 4re 12350 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℝ |
| 25 | 24 | ltnri 11370 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ 4
< 4 |
| 26 | 25 | pm2.21i 119 |
. . . . . . . . . . . . . . . . 17
⊢ (4 < 4
→ 𝑄 ∈ Odd
) |
| 27 | 23, 26 | biimtrdi 253 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 = 2 → (4 < (𝑃 + 2) → 𝑄 ∈ Odd )) |
| 28 | 19, 27 | biimtrdi 253 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even → (4 <
(𝑃 + 2) → 𝑄 ∈ Odd ))) |
| 29 | 18, 28 | sylbird 260 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → ((𝑃 + 2) ∈ Even → (4 <
(𝑃 + 2) → 𝑄 ∈ Odd ))) |
| 30 | 29 | com13 88 |
. . . . . . . . . . . . 13
⊢ (4 <
(𝑃 + 2) → ((𝑃 + 2) ∈ Even → (𝑃 ∈ ℙ → 𝑄 ∈ Odd ))) |
| 31 | 30 | imp 406 |
. . . . . . . . . . . 12
⊢ ((4 <
(𝑃 + 2) ∧ (𝑃 + 2) ∈ Even ) →
(𝑃 ∈ ℙ →
𝑄 ∈ Odd
)) |
| 32 | 14, 31 | biimtrdi 253 |
. . . . . . . . . . 11
⊢ (𝑁 = (𝑃 + 2) → ((4 < 𝑁 ∧ 𝑁 ∈ Even ) → (𝑃 ∈ ℙ → 𝑄 ∈ Odd ))) |
| 33 | 32 | expd 415 |
. . . . . . . . . 10
⊢ (𝑁 = (𝑃 + 2) → (4 < 𝑁 → (𝑁 ∈ Even → (𝑃 ∈ ℙ → 𝑄 ∈ Odd )))) |
| 34 | 33 | com13 88 |
. . . . . . . . 9
⊢ (𝑁 ∈ Even → (4 <
𝑁 → (𝑁 = (𝑃 + 2) → (𝑃 ∈ ℙ → 𝑄 ∈ Odd )))) |
| 35 | 34 | 3imp 1111 |
. . . . . . . 8
⊢ ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 2)) → (𝑃 ∈ ℙ → 𝑄 ∈ Odd )) |
| 36 | 35 | com12 32 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 2)) → 𝑄 ∈ Odd )) |
| 37 | 36 | adantr 480 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 = 2) → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 2)) → 𝑄 ∈ Odd )) |
| 38 | 11, 37 | sylbid 240 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 = 2) → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd )) |
| 39 | 38 | ex 412 |
. . . 4
⊢ (𝑃 ∈ ℙ → (𝑄 = 2 → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd ))) |
| 40 | 39 | adantr 480 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → (𝑄 = 2 → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd ))) |
| 41 | 7, 40 | sylbid 240 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → (¬
𝑄 ∈ Odd → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd ))) |
| 42 | | ax-1 6 |
. 2
⊢ (𝑄 ∈ Odd → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd )) |
| 43 | 41, 42 | pm2.61d2 181 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd )) |