| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oddz 47618 | . . . 4
⊢ (𝑚 ∈ Odd → 𝑚 ∈
ℤ) | 
| 2 |  | 5nn 12352 | . . . . . . . 8
⊢ 5 ∈
ℕ | 
| 3 | 2 | nnzi 12641 | . . . . . . 7
⊢ 5 ∈
ℤ | 
| 4 |  | zltp1le 12667 | . . . . . . 7
⊢ ((5
∈ ℤ ∧ 𝑚
∈ ℤ) → (5 < 𝑚 ↔ (5 + 1) ≤ 𝑚)) | 
| 5 | 3, 4 | mpan 690 | . . . . . 6
⊢ (𝑚 ∈ ℤ → (5 <
𝑚 ↔ (5 + 1) ≤ 𝑚)) | 
| 6 |  | 5p1e6 12413 | . . . . . . . . 9
⊢ (5 + 1) =
6 | 
| 7 | 6 | breq1i 5150 | . . . . . . . 8
⊢ ((5 + 1)
≤ 𝑚 ↔ 6 ≤ 𝑚) | 
| 8 |  | 6re 12356 | . . . . . . . . . 10
⊢ 6 ∈
ℝ | 
| 9 | 8 | a1i 11 | . . . . . . . . 9
⊢ (𝑚 ∈ ℤ → 6 ∈
ℝ) | 
| 10 |  | zre 12617 | . . . . . . . . 9
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℝ) | 
| 11 | 9, 10 | leloed 11404 | . . . . . . . 8
⊢ (𝑚 ∈ ℤ → (6 ≤
𝑚 ↔ (6 < 𝑚 ∨ 6 = 𝑚))) | 
| 12 | 7, 11 | bitrid 283 | . . . . . . 7
⊢ (𝑚 ∈ ℤ → ((5 + 1)
≤ 𝑚 ↔ (6 < 𝑚 ∨ 6 = 𝑚))) | 
| 13 |  | 6nn 12355 | . . . . . . . . . . . . 13
⊢ 6 ∈
ℕ | 
| 14 | 13 | nnzi 12641 | . . . . . . . . . . . 12
⊢ 6 ∈
ℤ | 
| 15 |  | zltp1le 12667 | . . . . . . . . . . . 12
⊢ ((6
∈ ℤ ∧ 𝑚
∈ ℤ) → (6 < 𝑚 ↔ (6 + 1) ≤ 𝑚)) | 
| 16 | 14, 15 | mpan 690 | . . . . . . . . . . 11
⊢ (𝑚 ∈ ℤ → (6 <
𝑚 ↔ (6 + 1) ≤ 𝑚)) | 
| 17 |  | 6p1e7 12414 | . . . . . . . . . . . . . 14
⊢ (6 + 1) =
7 | 
| 18 | 17 | breq1i 5150 | . . . . . . . . . . . . 13
⊢ ((6 + 1)
≤ 𝑚 ↔ 7 ≤ 𝑚) | 
| 19 |  | 7re 12359 | . . . . . . . . . . . . . . 15
⊢ 7 ∈
ℝ | 
| 20 | 19 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℤ → 7 ∈
ℝ) | 
| 21 | 20, 10 | leloed 11404 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℤ → (7 ≤
𝑚 ↔ (7 < 𝑚 ∨ 7 = 𝑚))) | 
| 22 | 18, 21 | bitrid 283 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℤ → ((6 + 1)
≤ 𝑚 ↔ (7 < 𝑚 ∨ 7 = 𝑚))) | 
| 23 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → 𝑚 ∈ Odd ) | 
| 24 |  | 3odd 47695 | . . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
Odd | 
| 25 | 23, 24 | jctir 520 | . . . . . . . . . . . . . . . . . . 19
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (𝑚 ∈ Odd ∧ 3 ∈ Odd
)) | 
| 26 |  | omoeALTV 47672 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ Odd ∧ 3 ∈ Odd )
→ (𝑚 − 3) ∈
Even ) | 
| 27 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑚 − 3) → (4 < 𝑛 ↔ 4 < (𝑚 − 3))) | 
| 28 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑚 − 3) → (𝑛 ∈ GoldbachEven ↔ (𝑚 − 3) ∈ GoldbachEven
)) | 
| 29 | 27, 28 | imbi12d 344 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑚 − 3) → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ (4 < (𝑚 − 3) → (𝑚 − 3) ∈ GoldbachEven
))) | 
| 30 | 29 | rspcv 3618 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 − 3) ∈ Even →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) → (4
< (𝑚 − 3) →
(𝑚 − 3) ∈
GoldbachEven ))) | 
| 31 | 25, 26, 30 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (4 < (𝑚 − 3) → (𝑚 − 3) ∈ GoldbachEven
))) | 
| 32 |  | 4p3e7 12420 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 + 3) =
7 | 
| 33 | 32 | eqcomi 2746 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 7 = (4 +
3) | 
| 34 | 33 | breq1i 5150 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (7 <
𝑚 ↔ (4 + 3) < 𝑚) | 
| 35 |  | 4re 12350 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 4 ∈
ℝ | 
| 36 | 35 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℤ → 4 ∈
ℝ) | 
| 37 |  | 3re 12346 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 ∈
ℝ | 
| 38 | 37 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℤ → 3 ∈
ℝ) | 
| 39 |  | ltaddsub 11737 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((4
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((4 + 3) < 𝑚 ↔ 4 < (𝑚 − 3))) | 
| 40 | 39 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((4
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((4 + 3) < 𝑚 → 4 < (𝑚 − 3))) | 
| 41 | 36, 38, 10, 40 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℤ → ((4 + 3)
< 𝑚 → 4 < (𝑚 − 3))) | 
| 42 | 34, 41 | biimtrid 242 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℤ → (7 <
𝑚 → 4 < (𝑚 − 3))) | 
| 43 | 42 | impcom 407 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((7 <
𝑚 ∧ 𝑚 ∈ ℤ) → 4 < (𝑚 − 3)) | 
| 44 | 43 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → 4 < (𝑚 − 3)) | 
| 45 |  | pm2.27 42 | . . . . . . . . . . . . . . . . . . 19
⊢ (4 <
(𝑚 − 3) → ((4
< (𝑚 − 3) →
(𝑚 − 3) ∈
GoldbachEven ) → (𝑚
− 3) ∈ GoldbachEven )) | 
| 46 | 44, 45 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → ((4 < (𝑚 − 3) → (𝑚 − 3) ∈ GoldbachEven
) → (𝑚 − 3)
∈ GoldbachEven )) | 
| 47 |  | isgbe 47738 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 − 3) ∈ GoldbachEven
↔ ((𝑚 − 3)
∈ Even ∧ ∃𝑝
∈ ℙ ∃𝑞
∈ ℙ (𝑝 ∈
Odd ∧ 𝑞 ∈ Odd
∧ (𝑚 − 3) =
(𝑝 + 𝑞)))) | 
| 48 |  | 3prm 16731 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 3 ∈
ℙ | 
| 49 | 48 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑚 ∈ ℤ → 3 ∈
ℙ) | 
| 50 |  | zcn 12618 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℂ) | 
| 51 |  | 3cn 12347 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 3 ∈
ℂ | 
| 52 | 50, 51 | jctir 520 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 ∈ ℤ → (𝑚 ∈ ℂ ∧ 3 ∈
ℂ)) | 
| 53 |  | npcan 11517 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑚 ∈ ℂ ∧ 3 ∈
ℂ) → ((𝑚 −
3) + 3) = 𝑚) | 
| 54 | 53 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑚 ∈ ℂ ∧ 3 ∈
ℂ) → 𝑚 = ((𝑚 − 3) +
3)) | 
| 55 | 52, 54 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑚 ∈ ℤ → 𝑚 = ((𝑚 − 3) + 3)) | 
| 56 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (3 =
𝑟 → ((𝑚 − 3) + 3) = ((𝑚 − 3) + 𝑟)) | 
| 57 | 56 | eqcoms 2745 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑟 = 3 → ((𝑚 − 3) + 3) = ((𝑚 − 3) + 𝑟)) | 
| 58 | 55, 57 | sylan9eq 2797 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑚 ∈ ℤ ∧ 𝑟 = 3) → 𝑚 = ((𝑚 − 3) + 𝑟)) | 
| 59 | 49, 58 | rspcedeq2vd 3630 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 ∈ ℤ →
∃𝑟 ∈ ℙ
𝑚 = ((𝑚 − 3) + 𝑟)) | 
| 60 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑚 − 3) = (𝑝 + 𝑞) → ((𝑚 − 3) + 𝑟) = ((𝑝 + 𝑞) + 𝑟)) | 
| 61 | 60 | eqeq2d 2748 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑚 − 3) = (𝑝 + 𝑞) → (𝑚 = ((𝑚 − 3) + 𝑟) ↔ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 62 | 61 | rexbidv 3179 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑚 − 3) = (𝑝 + 𝑞) → (∃𝑟 ∈ ℙ 𝑚 = ((𝑚 − 3) + 𝑟) ↔ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 63 | 59, 62 | imbitrid 244 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 − 3) = (𝑝 + 𝑞) → (𝑚 ∈ ℤ → ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 64 | 63 | 3ad2ant3 1136 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → (𝑚 ∈ ℤ → ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 65 | 64 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℤ → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 66 | 65 | ad4antlr 733 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((((7
< 𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 67 | 66 | reximdva 3168 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((7
< 𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) ∧ 𝑝 ∈ ℙ) →
(∃𝑞 ∈ ℙ
(𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 68 | 67 | reximdva 3168 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 69 | 68, 23 | jctild 525 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → (𝑚 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟)))) | 
| 70 |  | isgbow 47739 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ GoldbachOddW ↔
(𝑚 ∈ Odd ∧
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
∃𝑟 ∈ ℙ
𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 71 | 69, 70 | imbitrrdi 252 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → 𝑚 ∈ GoldbachOddW )) | 
| 72 | 71 | adantld 490 | . . . . . . . . . . . . . . . . . . 19
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (((𝑚 − 3) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞))) → 𝑚 ∈ GoldbachOddW )) | 
| 73 | 47, 72 | biimtrid 242 | . . . . . . . . . . . . . . . . . 18
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → ((𝑚 − 3) ∈ GoldbachEven → 𝑚 ∈ GoldbachOddW
)) | 
| 74 | 31, 46, 73 | 3syld 60 | . . . . . . . . . . . . . . . . 17
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑚 ∈ GoldbachOddW
)) | 
| 75 | 74 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ ((7 <
𝑚 ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ Odd → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑚 ∈ GoldbachOddW
))) | 
| 76 | 75 | com23 86 | . . . . . . . . . . . . . . 15
⊢ ((7 <
𝑚 ∧ 𝑚 ∈ ℤ) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
))) | 
| 77 | 76 | ex 412 | . . . . . . . . . . . . . 14
⊢ (7 <
𝑚 → (𝑚 ∈ ℤ →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 78 |  | 7gbow 47759 | . . . . . . . . . . . . . . . . . 18
⊢ 7 ∈
GoldbachOddW | 
| 79 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . 18
⊢ (7 =
𝑚 → (7 ∈
GoldbachOddW ↔ 𝑚
∈ GoldbachOddW )) | 
| 80 | 78, 79 | mpbii 233 | . . . . . . . . . . . . . . . . 17
⊢ (7 =
𝑚 → 𝑚 ∈ GoldbachOddW ) | 
| 81 | 80 | a1d 25 | . . . . . . . . . . . . . . . 16
⊢ (7 =
𝑚 → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)) | 
| 82 | 81 | a1d 25 | . . . . . . . . . . . . . . 15
⊢ (7 =
𝑚 → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
))) | 
| 83 | 82 | a1d 25 | . . . . . . . . . . . . . 14
⊢ (7 =
𝑚 → (𝑚 ∈ ℤ →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 84 | 77, 83 | jaoi 858 | . . . . . . . . . . . . 13
⊢ ((7 <
𝑚 ∨ 7 = 𝑚) → (𝑚 ∈ ℤ → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 85 | 84 | com12 32 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℤ → ((7 <
𝑚 ∨ 7 = 𝑚) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 86 | 22, 85 | sylbid 240 | . . . . . . . . . . 11
⊢ (𝑚 ∈ ℤ → ((6 + 1)
≤ 𝑚 →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 87 | 16, 86 | sylbid 240 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℤ → (6 <
𝑚 → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 88 | 87 | com12 32 | . . . . . . . . 9
⊢ (6 <
𝑚 → (𝑚 ∈ ℤ →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 89 |  | eleq1 2829 | . . . . . . . . . . . 12
⊢ (6 =
𝑚 → (6 ∈ Odd
↔ 𝑚 ∈ Odd
)) | 
| 90 |  | 6even 47698 | . . . . . . . . . . . . 13
⊢ 6 ∈
Even | 
| 91 |  | evennodd 47630 | . . . . . . . . . . . . . 14
⊢ (6 ∈
Even → ¬ 6 ∈ Odd ) | 
| 92 | 91 | pm2.21d 121 | . . . . . . . . . . . . 13
⊢ (6 ∈
Even → (6 ∈ Odd → 𝑚 ∈ GoldbachOddW )) | 
| 93 | 90, 92 | ax-mp 5 | . . . . . . . . . . . 12
⊢ (6 ∈
Odd → 𝑚 ∈
GoldbachOddW ) | 
| 94 | 89, 93 | biimtrrdi 254 | . . . . . . . . . . 11
⊢ (6 =
𝑚 → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)) | 
| 95 | 94 | a1d 25 | . . . . . . . . . 10
⊢ (6 =
𝑚 → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
))) | 
| 96 | 95 | a1d 25 | . . . . . . . . 9
⊢ (6 =
𝑚 → (𝑚 ∈ ℤ →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 97 | 88, 96 | jaoi 858 | . . . . . . . 8
⊢ ((6 <
𝑚 ∨ 6 = 𝑚) → (𝑚 ∈ ℤ → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 98 | 97 | com12 32 | . . . . . . 7
⊢ (𝑚 ∈ ℤ → ((6 <
𝑚 ∨ 6 = 𝑚) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 99 | 12, 98 | sylbid 240 | . . . . . 6
⊢ (𝑚 ∈ ℤ → ((5 + 1)
≤ 𝑚 →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 100 | 5, 99 | sylbid 240 | . . . . 5
⊢ (𝑚 ∈ ℤ → (5 <
𝑚 → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) | 
| 101 | 100 | com24 95 | . . . 4
⊢ (𝑚 ∈ ℤ → (𝑚 ∈ Odd →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) → (5
< 𝑚 → 𝑚 ∈ GoldbachOddW
)))) | 
| 102 | 1, 101 | mpcom 38 | . . 3
⊢ (𝑚 ∈ Odd →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) → (5
< 𝑚 → 𝑚 ∈ GoldbachOddW
))) | 
| 103 | 102 | impcom 407 | . 2
⊢
((∀𝑛 ∈
Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ∧
𝑚 ∈ Odd ) → (5
< 𝑚 → 𝑚 ∈ GoldbachOddW
)) | 
| 104 | 103 | ralrimiva 3146 | 1
⊢
(∀𝑛 ∈
Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) →
∀𝑚 ∈ Odd (5
< 𝑚 → 𝑚 ∈ GoldbachOddW
)) |