Proof of Theorem evengpop3
Step | Hyp | Ref
| Expression |
1 | | 3odd 40155 |
. . . . . . . 8
⊢ 3 ∈
Odd |
2 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘9) → 3 ∈ Odd ) |
3 | 2 | anim1i 590 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (3 ∈ Odd ∧
𝑁 ∈ Even
)) |
4 | 3 | ancomd 466 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 ∈ Even ∧ 3 ∈ Odd
)) |
5 | | emoo 40151 |
. . . . 5
⊢ ((𝑁 ∈ Even ∧ 3 ∈ Odd
) → (𝑁 − 3)
∈ Odd ) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 − 3) ∈ Odd ) |
7 | | breq2 4587 |
. . . . . 6
⊢ (𝑚 = (𝑁 − 3) → (5 < 𝑚 ↔ 5 < (𝑁 − 3))) |
8 | | eleq1 2676 |
. . . . . 6
⊢ (𝑚 = (𝑁 − 3) → (𝑚 ∈ GoldbachOdd ↔ (𝑁 − 3) ∈ GoldbachOdd
)) |
9 | 7, 8 | imbi12d 333 |
. . . . 5
⊢ (𝑚 = (𝑁 − 3) → ((5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ↔ (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOdd
))) |
10 | 9 | adantl 481 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ 𝑚 = (𝑁 − 3)) → ((5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ↔ (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOdd
))) |
11 | 6, 10 | rspcdv 3285 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOdd
))) |
12 | | eluz2 11569 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘9) ↔ (9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤
𝑁)) |
13 | | 5p3e8 11043 |
. . . . . . . . 9
⊢ (5 + 3) =
8 |
14 | | 8p1e9 11035 |
. . . . . . . . . 10
⊢ (8 + 1) =
9 |
15 | | 9cn 10985 |
. . . . . . . . . . 11
⊢ 9 ∈
ℂ |
16 | | ax-1cn 9873 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
17 | | 8cn 10983 |
. . . . . . . . . . 11
⊢ 8 ∈
ℂ |
18 | 15, 16, 17 | subadd2i 10248 |
. . . . . . . . . 10
⊢ ((9
− 1) = 8 ↔ (8 + 1) = 9) |
19 | 14, 18 | mpbir 220 |
. . . . . . . . 9
⊢ (9
− 1) = 8 |
20 | 13, 19 | eqtr4i 2635 |
. . . . . . . 8
⊢ (5 + 3) =
(9 − 1) |
21 | | zlem1lt 11306 |
. . . . . . . . 9
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ) → (9 ≤ 𝑁 ↔ (9 − 1) < 𝑁)) |
22 | 21 | biimp3a 1424 |
. . . . . . . 8
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → (9 − 1) < 𝑁) |
23 | 20, 22 | syl5eqbr 4618 |
. . . . . . 7
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → (5 + 3) < 𝑁) |
24 | | 5re 10976 |
. . . . . . . . . . 11
⊢ 5 ∈
ℝ |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 5 ∈
ℝ) |
26 | | 3re 10971 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 3 ∈
ℝ) |
28 | | zre 11258 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
29 | 25, 27, 28 | 3jca 1235 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (5 ∈
ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
30 | 29 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → (5 ∈ ℝ ∧ 3 ∈
ℝ ∧ 𝑁 ∈
ℝ)) |
31 | | ltaddsub 10381 |
. . . . . . . 8
⊢ ((5
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((5 + 3) < 𝑁 ↔ 5 < (𝑁 − 3))) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → ((5 + 3) < 𝑁 ↔ 5 < (𝑁 − 3))) |
33 | 23, 32 | mpbid 221 |
. . . . . 6
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 9 ≤ 𝑁) → 5 < (𝑁 − 3)) |
34 | 12, 33 | sylbi 206 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘9) → 5 < (𝑁 − 3)) |
35 | 34 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → 5 < (𝑁 − 3)) |
36 | | simpr 476 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOdd ) →
(𝑁 − 3) ∈
GoldbachOdd ) |
37 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑜 = (𝑁 − 3) → (𝑜 + 3) = ((𝑁 − 3) + 3)) |
38 | 37 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑜 = (𝑁 − 3) → (𝑁 = (𝑜 + 3) ↔ 𝑁 = ((𝑁 − 3) + 3))) |
39 | 38 | adantl 481 |
. . . . . 6
⊢ ((((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOdd ) ∧ 𝑜 = (𝑁 − 3)) → (𝑁 = (𝑜 + 3) ↔ 𝑁 = ((𝑁 − 3) + 3))) |
40 | | eluzelcn 11575 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘9) → 𝑁 ∈ ℂ) |
41 | | 3cn 10972 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
42 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘9) → 3 ∈ ℂ) |
43 | 40, 42 | jca 553 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘9) → (𝑁 ∈ ℂ ∧ 3 ∈
ℂ)) |
44 | 43 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 ∈ ℂ ∧ 3 ∈
ℂ)) |
45 | 44 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOdd ) →
(𝑁 ∈ ℂ ∧ 3
∈ ℂ)) |
46 | | npcan 10169 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 3 ∈
ℂ) → ((𝑁 −
3) + 3) = 𝑁) |
47 | 46 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 3 ∈
ℂ) → 𝑁 = ((𝑁 − 3) +
3)) |
48 | 45, 47 | syl 17 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOdd ) →
𝑁 = ((𝑁 − 3) + 3)) |
49 | 36, 39, 48 | rspcedvd 3289 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOdd ) →
∃𝑜 ∈ GoldbachOdd
𝑁 = (𝑜 + 3)) |
50 | 49 | ex 449 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ((𝑁 − 3) ∈ GoldbachOdd →
∃𝑜 ∈ GoldbachOdd
𝑁 = (𝑜 + 3))) |
51 | 35, 50 | embantd 57 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ((5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOdd )
→ ∃𝑜 ∈
GoldbachOdd 𝑁 = (𝑜 + 3))) |
52 | 11, 51 | syld 46 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ∃𝑜 ∈ GoldbachOdd 𝑁 = (𝑜 + 3))) |
53 | 52 | com12 32 |
1
⊢
(∀𝑚 ∈
Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) →
((𝑁 ∈
(ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOdd 𝑁 = (𝑜 + 3))) |