Step | Hyp | Ref
| Expression |
1 | | oddz 44501 |
. . . 4
⊢ (𝑚 ∈ Odd → 𝑚 ∈
ℤ) |
2 | | 5nn 11745 |
. . . . . . . 8
⊢ 5 ∈
ℕ |
3 | 2 | nnzi 12030 |
. . . . . . 7
⊢ 5 ∈
ℤ |
4 | | zltp1le 12056 |
. . . . . . 7
⊢ ((5
∈ ℤ ∧ 𝑚
∈ ℤ) → (5 < 𝑚 ↔ (5 + 1) ≤ 𝑚)) |
5 | 3, 4 | mpan 690 |
. . . . . 6
⊢ (𝑚 ∈ ℤ → (5 <
𝑚 ↔ (5 + 1) ≤ 𝑚)) |
6 | | 5p1e6 11806 |
. . . . . . . . 9
⊢ (5 + 1) =
6 |
7 | 6 | breq1i 5032 |
. . . . . . . 8
⊢ ((5 + 1)
≤ 𝑚 ↔ 6 ≤ 𝑚) |
8 | | 6re 11749 |
. . . . . . . . . 10
⊢ 6 ∈
ℝ |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℤ → 6 ∈
ℝ) |
10 | | zre 12009 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℝ) |
11 | 9, 10 | leloed 10806 |
. . . . . . . 8
⊢ (𝑚 ∈ ℤ → (6 ≤
𝑚 ↔ (6 < 𝑚 ∨ 6 = 𝑚))) |
12 | 7, 11 | syl5bb 286 |
. . . . . . 7
⊢ (𝑚 ∈ ℤ → ((5 + 1)
≤ 𝑚 ↔ (6 < 𝑚 ∨ 6 = 𝑚))) |
13 | | 6nn 11748 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℕ |
14 | 13 | nnzi 12030 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℤ |
15 | | zltp1le 12056 |
. . . . . . . . . . . 12
⊢ ((6
∈ ℤ ∧ 𝑚
∈ ℤ) → (6 < 𝑚 ↔ (6 + 1) ≤ 𝑚)) |
16 | 14, 15 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℤ → (6 <
𝑚 ↔ (6 + 1) ≤ 𝑚)) |
17 | | 6p1e7 11807 |
. . . . . . . . . . . . . 14
⊢ (6 + 1) =
7 |
18 | 17 | breq1i 5032 |
. . . . . . . . . . . . 13
⊢ ((6 + 1)
≤ 𝑚 ↔ 7 ≤ 𝑚) |
19 | | 7re 11752 |
. . . . . . . . . . . . . . 15
⊢ 7 ∈
ℝ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℤ → 7 ∈
ℝ) |
21 | 20, 10 | leloed 10806 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℤ → (7 ≤
𝑚 ↔ (7 < 𝑚 ∨ 7 = 𝑚))) |
22 | 18, 21 | syl5bb 286 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℤ → ((6 + 1)
≤ 𝑚 ↔ (7 < 𝑚 ∨ 7 = 𝑚))) |
23 | | simpr 489 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → 𝑚 ∈ Odd ) |
24 | | 3odd 44578 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
Odd |
25 | 23, 24 | jctir 525 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (𝑚 ∈ Odd ∧ 3 ∈ Odd
)) |
26 | | omoeALTV 44555 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ Odd ∧ 3 ∈ Odd )
→ (𝑚 − 3) ∈
Even ) |
27 | | breq2 5029 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑚 − 3) → (4 < 𝑛 ↔ 4 < (𝑚 − 3))) |
28 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑚 − 3) → (𝑛 ∈ GoldbachEven ↔ (𝑚 − 3) ∈ GoldbachEven
)) |
29 | 27, 28 | imbi12d 349 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑚 − 3) → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ (4 < (𝑚 − 3) → (𝑚 − 3) ∈ GoldbachEven
))) |
30 | 29 | rspcv 3534 |
. . . . . . . . . . . . . . . . . . 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 11813 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 + 3) =
7 |
33 | 32 | eqcomi 2768 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 7 = (4 +
3) |
34 | 33 | breq1i 5032 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (7 <
𝑚 ↔ (4 + 3) < 𝑚) |
35 | | 4re 11743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 4 ∈
ℝ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℤ → 4 ∈
ℝ) |
37 | | 3re 11739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 ∈
ℝ |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℤ → 3 ∈
ℝ) |
39 | | ltaddsub 11137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((4
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((4 + 3) < 𝑚 ↔ 4 < (𝑚 − 3))) |
40 | 39 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((4
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((4 + 3) < 𝑚 → 4 < (𝑚 − 3))) |
41 | 36, 38, 10, 40 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℤ → ((4 + 3)
< 𝑚 → 4 < (𝑚 − 3))) |
42 | 34, 41 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℤ → (7 <
𝑚 → 4 < (𝑚 − 3))) |
43 | 42 | impcom 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((7 <
𝑚 ∧ 𝑚 ∈ ℤ) → 4 < (𝑚 − 3)) |
44 | 43 | adantr 485 |
. . . . . . . . . . . . . . . . . . 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 44621 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 − 3) ∈ GoldbachEven
↔ ((𝑚 − 3)
∈ Even ∧ ∃𝑝
∈ ℙ ∃𝑞
∈ ℙ (𝑝 ∈
Odd ∧ 𝑞 ∈ Odd
∧ (𝑚 − 3) =
(𝑝 + 𝑞)))) |
48 | | 3prm 16075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 3 ∈
ℙ |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑚 ∈ ℤ → 3 ∈
ℙ) |
50 | | zcn 12010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℂ) |
51 | | 3cn 11740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 3 ∈
ℂ |
52 | 50, 51 | jctir 525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 ∈ ℤ → (𝑚 ∈ ℂ ∧ 3 ∈
ℂ)) |
53 | | npcan 10918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑚 ∈ ℂ ∧ 3 ∈
ℂ) → ((𝑚 −
3) + 3) = 𝑚) |
54 | 53 | eqcomd 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑚 ∈ ℂ ∧ 3 ∈
ℂ) → 𝑚 = ((𝑚 − 3) +
3)) |
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑚 ∈ ℤ → 𝑚 = ((𝑚 − 3) + 3)) |
56 | | oveq2 7151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (3 =
𝑟 → ((𝑚 − 3) + 3) = ((𝑚 − 3) + 𝑟)) |
57 | 56 | eqcoms 2767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑟 = 3 → ((𝑚 − 3) + 3) = ((𝑚 − 3) + 𝑟)) |
58 | 55, 57 | sylan9eq 2814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑚 ∈ ℤ ∧ 𝑟 = 3) → 𝑚 = ((𝑚 − 3) + 𝑟)) |
59 | 49, 58 | rspcedeq2vd 3546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 ∈ ℤ →
∃𝑟 ∈ ℙ
𝑚 = ((𝑚 − 3) + 𝑟)) |
60 | | oveq1 7150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑚 − 3) = (𝑝 + 𝑞) → ((𝑚 − 3) + 𝑟) = ((𝑝 + 𝑞) + 𝑟)) |
61 | 60 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑚 − 3) = (𝑝 + 𝑞) → (𝑚 = ((𝑚 − 3) + 𝑟) ↔ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
62 | 61 | rexbidv 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑚 − 3) = (𝑝 + 𝑞) → (∃𝑟 ∈ ℙ 𝑚 = ((𝑚 − 3) + 𝑟) ↔ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
63 | 59, 62 | syl5ib 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 − 3) = (𝑝 + 𝑞) → (𝑚 ∈ ℤ → ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
64 | 63 | 3ad2ant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 3196 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((7
< 𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) ∧ 𝑝 ∈ ℙ) →
(∃𝑞 ∈ ℙ
(𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
68 | 67 | reximdva 3196 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
69 | 68, 23 | jctild 530 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → (𝑚 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟)))) |
70 | | isgbow 44622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ GoldbachOddW ↔
(𝑚 ∈ Odd ∧
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
∃𝑟 ∈ ℙ
𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
71 | 69, 70 | syl6ibr 255 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞)) → 𝑚 ∈ GoldbachOddW )) |
72 | 71 | adantld 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (((𝑚 − 3) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑚 − 3) = (𝑝 + 𝑞))) → 𝑚 ∈ GoldbachOddW )) |
73 | 47, 72 | syl5bi 245 |
. . . . . . . . . . . . . . . . . 18
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → ((𝑚 − 3) ∈ GoldbachEven → 𝑚 ∈ GoldbachOddW
)) |
74 | 31, 46, 73 | 3syld 60 |
. . . . . . . . . . . . . . . . 17
⊢ (((7 <
𝑚 ∧ 𝑚 ∈ ℤ) ∧ 𝑚 ∈ Odd ) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑚 ∈ GoldbachOddW
)) |
75 | 74 | ex 417 |
. . . . . . . . . . . . . . . 16
⊢ ((7 <
𝑚 ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ Odd → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑚 ∈ GoldbachOddW
))) |
76 | 75 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((7 <
𝑚 ∧ 𝑚 ∈ ℤ) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
))) |
77 | 76 | ex 417 |
. . . . . . . . . . . . . 14
⊢ (7 <
𝑚 → (𝑚 ∈ ℤ →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
78 | | 7gbow 44642 |
. . . . . . . . . . . . . . . . . 18
⊢ 7 ∈
GoldbachOddW |
79 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . 18
⊢ (7 =
𝑚 → (7 ∈
GoldbachOddW ↔ 𝑚
∈ GoldbachOddW )) |
80 | 78, 79 | mpbii 236 |
. . . . . . . . . . . . . . . . 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 855 |
. . . . . . . . . . . . 13
⊢ ((7 <
𝑚 ∨ 7 = 𝑚) → (𝑚 ∈ ℤ → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
85 | 84 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℤ → ((7 <
𝑚 ∨ 7 = 𝑚) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
86 | 22, 85 | sylbid 243 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℤ → ((6 + 1)
≤ 𝑚 →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
87 | 16, 86 | sylbid 243 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℤ → (6 <
𝑚 → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
88 | 87 | com12 32 |
. . . . . . . . 9
⊢ (6 <
𝑚 → (𝑚 ∈ ℤ →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
89 | | eleq1 2838 |
. . . . . . . . . . . 12
⊢ (6 =
𝑚 → (6 ∈ Odd
↔ 𝑚 ∈ Odd
)) |
90 | | 6even 44581 |
. . . . . . . . . . . . 13
⊢ 6 ∈
Even |
91 | | evennodd 44513 |
. . . . . . . . . . . . . 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 | syl6bir 257 |
. . . . . . . . . . 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 855 |
. . . . . . . 8
⊢ ((6 <
𝑚 ∨ 6 = 𝑚) → (𝑚 ∈ ℤ → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
98 | 97 | com12 32 |
. . . . . . 7
⊢ (𝑚 ∈ ℤ → ((6 <
𝑚 ∨ 6 = 𝑚) → (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → (𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
99 | 12, 98 | sylbid 243 |
. . . . . 6
⊢ (𝑚 ∈ ℤ → ((5 + 1)
≤ 𝑚 →
(∀𝑛 ∈ Even (4
< 𝑛 → 𝑛 ∈ GoldbachEven ) →
(𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW
)))) |
100 | 5, 99 | sylbid 243 |
. . . . 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 412 |
. 2
⊢
((∀𝑛 ∈
Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ∧
𝑚 ∈ Odd ) → (5
< 𝑚 → 𝑚 ∈ GoldbachOddW
)) |
104 | 103 | ralrimiva 3111 |
1
⊢
(∀𝑛 ∈
Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) →
∀𝑚 ∈ Odd (5
< 𝑚 → 𝑚 ∈ GoldbachOddW
)) |