| Step | Hyp | Ref
| Expression |
| 1 | | isgbe 47738 |
. 2
⊢ (𝑍 ∈ GoldbachEven ↔
(𝑍 ∈ Even ∧
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞)))) |
| 2 | | oddprmuzge3 47703 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℙ ∧ 𝑝 ∈ Odd ) → 𝑝 ∈
(ℤ≥‘3)) |
| 3 | 2 | ancoms 458 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ Odd ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
(ℤ≥‘3)) |
| 4 | | oddprmuzge3 47703 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧ 𝑞 ∈ Odd ) → 𝑞 ∈
(ℤ≥‘3)) |
| 5 | 4 | ancoms 458 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ Odd ∧ 𝑞 ∈ ℙ) → 𝑞 ∈
(ℤ≥‘3)) |
| 6 | | eluz2 12884 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 3 ≤
𝑝)) |
| 7 | | eluz2 12884 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 3 ≤
𝑞)) |
| 8 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 ∈ ℤ → 𝑞 ∈
ℝ) |
| 9 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 ∈ ℤ → 𝑝 ∈
ℝ) |
| 10 | | 3re 12346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 3 ∈
ℝ |
| 11 | 10, 10 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (3 ∈
ℝ ∧ 3 ∈ ℝ) |
| 12 | | pm3.22 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝑝 ∈ ℝ ∧ 𝑞 ∈
ℝ)) |
| 13 | | le2add 11745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((3
∈ ℝ ∧ 3 ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ)) → ((3 ≤ 𝑝 ∧ 3 ≤ 𝑞) → (3 + 3) ≤ (𝑝 + 𝑞))) |
| 14 | 11, 12, 13 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((3 ≤
𝑝 ∧ 3 ≤ 𝑞) → (3 + 3) ≤ (𝑝 + 𝑞))) |
| 15 | 14 | ancomsd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((3 ≤
𝑞 ∧ 3 ≤ 𝑝) → (3 + 3) ≤ (𝑝 + 𝑞))) |
| 16 | | 3p3e6 12418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (3 + 3) =
6 |
| 17 | 16 | breq1i 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((3 + 3)
≤ (𝑝 + 𝑞) ↔ 6 ≤ (𝑝 + 𝑞)) |
| 18 | | 5lt6 12447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 5 <
6 |
| 19 | | 5re 12353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 5 ∈
ℝ |
| 20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → 5 ∈
ℝ) |
| 21 | | 6re 12356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 6 ∈
ℝ |
| 22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → 6 ∈
ℝ) |
| 23 | | readdcl 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ) → (𝑝 + 𝑞) ∈ ℝ) |
| 24 | 23 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝑝 + 𝑞) ∈ ℝ) |
| 25 | | ltletr 11353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((5
∈ ℝ ∧ 6 ∈ ℝ ∧ (𝑝 + 𝑞) ∈ ℝ) → ((5 < 6 ∧ 6
≤ (𝑝 + 𝑞)) → 5 < (𝑝 + 𝑞))) |
| 26 | 20, 22, 24, 25 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((5 <
6 ∧ 6 ≤ (𝑝 + 𝑞)) → 5 < (𝑝 + 𝑞))) |
| 27 | 18, 26 | mpani 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (6 ≤
(𝑝 + 𝑞) → 5 < (𝑝 + 𝑞))) |
| 28 | 17, 27 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((3 + 3)
≤ (𝑝 + 𝑞) → 5 < (𝑝 + 𝑞))) |
| 29 | 15, 28 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((3 ≤
𝑞 ∧ 3 ≤ 𝑝) → 5 < (𝑝 + 𝑞))) |
| 30 | 8, 9, 29 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑞 ∈ ℤ ∧ 𝑝 ∈ ℤ) → ((3 ≤
𝑞 ∧ 3 ≤ 𝑝) → 5 < (𝑝 + 𝑞))) |
| 31 | 30 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ ℤ → (𝑝 ∈ ℤ → ((3 ≤
𝑞 ∧ 3 ≤ 𝑝) → 5 < (𝑝 + 𝑞)))) |
| 32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((3
∈ ℤ ∧ 𝑞
∈ ℤ) → (𝑝
∈ ℤ → ((3 ≤ 𝑞 ∧ 3 ≤ 𝑝) → 5 < (𝑝 + 𝑞)))) |
| 33 | 32 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((3
∈ ℤ ∧ 𝑞
∈ ℤ) → ((3 ≤ 𝑞 ∧ 3 ≤ 𝑝) → (𝑝 ∈ ℤ → 5 < (𝑝 + 𝑞)))) |
| 34 | 33 | exp4b 430 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3 ∈
ℤ → (𝑞 ∈
ℤ → (3 ≤ 𝑞
→ (3 ≤ 𝑝 →
(𝑝 ∈ ℤ → 5
< (𝑝 + 𝑞)))))) |
| 35 | 34 | 3imp 1111 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℤ ∧ 𝑞
∈ ℤ ∧ 3 ≤ 𝑞) → (3 ≤ 𝑝 → (𝑝 ∈ ℤ → 5 < (𝑝 + 𝑞)))) |
| 36 | 35 | com13 88 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℤ → (3 ≤
𝑝 → ((3 ∈ ℤ
∧ 𝑞 ∈ ℤ
∧ 3 ≤ 𝑞) → 5
< (𝑝 + 𝑞)))) |
| 37 | 36 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℤ ∧ 3 ≤
𝑝) → ((3 ∈
ℤ ∧ 𝑞 ∈
ℤ ∧ 3 ≤ 𝑞)
→ 5 < (𝑝 + 𝑞))) |
| 38 | 37 | 3adant1 1131 |
. . . . . . . . . . . . . . 15
⊢ ((3
∈ ℤ ∧ 𝑝
∈ ℤ ∧ 3 ≤ 𝑝) → ((3 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 3 ≤
𝑞) → 5 < (𝑝 + 𝑞))) |
| 39 | 7, 38 | biimtrid 242 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑝
∈ ℤ ∧ 3 ≤ 𝑝) → (𝑞 ∈ (ℤ≥‘3)
→ 5 < (𝑝 + 𝑞))) |
| 40 | 6, 39 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
(ℤ≥‘3) → (𝑞 ∈ (ℤ≥‘3)
→ 5 < (𝑝 + 𝑞))) |
| 41 | 40 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
(ℤ≥‘3) ∧ 𝑞 ∈ (ℤ≥‘3))
→ 5 < (𝑝 + 𝑞)) |
| 42 | 3, 5, 41 | syl2an 596 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ Odd ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ Odd ∧ 𝑞 ∈ ℙ)) → 5 <
(𝑝 + 𝑞)) |
| 43 | 42 | an4s 660 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) → 5 <
(𝑝 + 𝑞)) |
| 44 | 43 | ex 412 |
. . . . . . . . 9
⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) → ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → 5 <
(𝑝 + 𝑞))) |
| 45 | 44 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞)) → ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → 5 < (𝑝 + 𝑞))) |
| 46 | 45 | impcom 407 |
. . . . . . 7
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞))) → 5 < (𝑝 + 𝑞)) |
| 47 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑍 = (𝑝 + 𝑞) → (5 < 𝑍 ↔ 5 < (𝑝 + 𝑞))) |
| 48 | 47 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞)) → (5 < 𝑍 ↔ 5 < (𝑝 + 𝑞))) |
| 49 | 48 | adantl 481 |
. . . . . . 7
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞))) → (5 < 𝑍 ↔ 5 < (𝑝 + 𝑞))) |
| 50 | 46, 49 | mpbird 257 |
. . . . . 6
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞))) → 5 < 𝑍) |
| 51 | 50 | ex 412 |
. . . . 5
⊢ ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞)) → 5 < 𝑍)) |
| 52 | 51 | a1i 11 |
. . . 4
⊢ (𝑍 ∈ Even → ((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞)) → 5 < 𝑍))) |
| 53 | 52 | rexlimdvv 3212 |
. . 3
⊢ (𝑍 ∈ Even →
(∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞)) → 5 < 𝑍)) |
| 54 | 53 | imp 406 |
. 2
⊢ ((𝑍 ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞))) → 5 < 𝑍) |
| 55 | 1, 54 | sylbi 217 |
1
⊢ (𝑍 ∈ GoldbachEven → 5
< 𝑍) |