Proof of Theorem evengpop3
Step | Hyp | Ref
| Expression |
1 | | 3odd 44833 |
. . . . . . 7
⊢ 3 ∈
Odd |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘9) → 3 ∈ Odd ) |
3 | 2 | anim1i 618 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (3 ∈ Odd ∧
𝑁 ∈ Even
)) |
4 | 3 | ancomd 465 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 ∈ Even ∧ 3 ∈ Odd
)) |
5 | | emoo 44829 |
. . . 4
⊢ ((𝑁 ∈ Even ∧ 3 ∈ Odd
) → (𝑁 − 3)
∈ Odd ) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 − 3) ∈ Odd ) |
7 | | breq2 5057 |
. . . . 5
⊢ (𝑚 = (𝑁 − 3) → (5 < 𝑚 ↔ 5 < (𝑁 − 3))) |
8 | | eleq1 2825 |
. . . . 5
⊢ (𝑚 = (𝑁 − 3) → (𝑚 ∈ GoldbachOddW ↔ (𝑁 − 3) ∈ GoldbachOddW
)) |
9 | 7, 8 | imbi12d 348 |
. . . 4
⊢ (𝑚 = (𝑁 − 3) → ((5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ↔ (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOddW
))) |
10 | 9 | adantl 485 |
. . 3
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ 𝑚 = (𝑁 − 3)) → ((5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ↔ (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOddW
))) |
11 | 6, 10 | rspcdv 3529 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOddW
))) |
12 | | eluz2 12444 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘9) ↔ (9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤
𝑁)) |
13 | | 5p3e8 11987 |
. . . . . . . 8
⊢ (5 + 3) =
8 |
14 | | 8p1e9 11980 |
. . . . . . . . 9
⊢ (8 + 1) =
9 |
15 | | 9cn 11930 |
. . . . . . . . . 10
⊢ 9 ∈
ℂ |
16 | | ax-1cn 10787 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
17 | | 8cn 11927 |
. . . . . . . . . 10
⊢ 8 ∈
ℂ |
18 | 15, 16, 17 | subadd2i 11166 |
. . . . . . . . 9
⊢ ((9
− 1) = 8 ↔ (8 + 1) = 9) |
19 | 14, 18 | mpbir 234 |
. . . . . . . 8
⊢ (9
− 1) = 8 |
20 | 13, 19 | eqtr4i 2768 |
. . . . . . 7
⊢ (5 + 3) =
(9 − 1) |
21 | | zlem1lt 12229 |
. . . . . . . 8
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ) → (9 ≤ 𝑁 ↔ (9 − 1) < 𝑁)) |
22 | 21 | biimp3a 1471 |
. . . . . . 7
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → (9 − 1) < 𝑁) |
23 | 20, 22 | eqbrtrid 5088 |
. . . . . 6
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → (5 + 3) < 𝑁) |
24 | | 5re 11917 |
. . . . . . . . . 10
⊢ 5 ∈
ℝ |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 5 ∈
ℝ) |
26 | | 3re 11910 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 3 ∈
ℝ) |
28 | | zre 12180 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
29 | 25, 27, 28 | 3jca 1130 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (5 ∈
ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
30 | 29 | 3ad2ant2 1136 |
. . . . . . 7
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → (5 ∈ ℝ ∧ 3 ∈
ℝ ∧ 𝑁 ∈
ℝ)) |
31 | | ltaddsub 11306 |
. . . . . . 7
⊢ ((5
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((5 + 3) < 𝑁 ↔ 5 < (𝑁 − 3))) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → ((5 + 3) < 𝑁 ↔ 5 < (𝑁 − 3))) |
33 | 23, 32 | mpbid 235 |
. . . . 5
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → 5 < (𝑁 − 3)) |
34 | 12, 33 | sylbi 220 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘9) → 5 < (𝑁 − 3)) |
35 | 34 | adantr 484 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → 5 < (𝑁 − 3)) |
36 | | simpr 488 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) →
(𝑁 − 3) ∈
GoldbachOddW ) |
37 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑜 = (𝑁 − 3) → (𝑜 + 3) = ((𝑁 − 3) + 3)) |
38 | 37 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑜 = (𝑁 − 3) → (𝑁 = (𝑜 + 3) ↔ 𝑁 = ((𝑁 − 3) + 3))) |
39 | 38 | adantl 485 |
. . . . 5
⊢ ((((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) ∧
𝑜 = (𝑁 − 3)) → (𝑁 = (𝑜 + 3) ↔ 𝑁 = ((𝑁 − 3) + 3))) |
40 | | eluzelcn 12450 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘9) → 𝑁 ∈ ℂ) |
41 | | 3cn 11911 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
42 | 41 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘9) → 3 ∈ ℂ) |
43 | 40, 42 | jca 515 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘9) → (𝑁 ∈ ℂ ∧ 3 ∈
ℂ)) |
44 | 43 | adantr 484 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 ∈ ℂ ∧ 3 ∈
ℂ)) |
45 | 44 | adantr 484 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) →
(𝑁 ∈ ℂ ∧ 3
∈ ℂ)) |
46 | | npcan 11087 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 3 ∈
ℂ) → ((𝑁 −
3) + 3) = 𝑁) |
47 | 46 | eqcomd 2743 |
. . . . . 6
⊢ ((𝑁 ∈ ℂ ∧ 3 ∈
ℂ) → 𝑁 = ((𝑁 − 3) +
3)) |
48 | 45, 47 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) →
𝑁 = ((𝑁 − 3) + 3)) |
49 | 36, 39, 48 | rspcedvd 3540 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) →
∃𝑜 ∈
GoldbachOddW 𝑁 = (𝑜 + 3)) |
50 | 49 | ex 416 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ((𝑁 − 3) ∈ GoldbachOddW →
∃𝑜 ∈
GoldbachOddW 𝑁 = (𝑜 + 3))) |
51 | 35, 50 | embantd 59 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ((5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOddW
) → ∃𝑜 ∈
GoldbachOddW 𝑁 = (𝑜 + 3))) |
52 | 11, 51 | syldc 48 |
1
⊢
(∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) →
((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3))) |