Proof of Theorem evengpoap3
Step | Hyp | Ref
| Expression |
1 | | 3odd 40155 |
. . . . . . . 8
⊢ 3 ∈
Odd |
2 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 3 ∈ Odd ) |
3 | 2 | anim1i 590 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (3 ∈ Odd ∧ 𝑁 ∈ Even )) |
4 | 3 | ancomd 466 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (𝑁 ∈ Even ∧
3 ∈ Odd )) |
5 | | emoo 40151 |
. . . . 5
⊢ ((𝑁 ∈ Even ∧ 3 ∈ Odd
) → (𝑁 − 3)
∈ Odd ) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (𝑁 − 3) ∈
Odd ) |
7 | | breq2 4587 |
. . . . . 6
⊢ (𝑚 = (𝑁 − 3) → (7 < 𝑚 ↔ 7 < (𝑁 − 3))) |
8 | | eleq1 2676 |
. . . . . 6
⊢ (𝑚 = (𝑁 − 3) → (𝑚 ∈ GoldbachOddALTV ↔ (𝑁 − 3) ∈
GoldbachOddALTV )) |
9 | 7, 8 | imbi12d 333 |
. . . . 5
⊢ (𝑚 = (𝑁 − 3) → ((7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ↔ (7 <
(𝑁 − 3) → (𝑁 − 3) ∈
GoldbachOddALTV ))) |
10 | 9 | adantl 481 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ) ∧
𝑚 = (𝑁 − 3)) → ((7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) ↔ (7 <
(𝑁 − 3) → (𝑁 − 3) ∈
GoldbachOddALTV ))) |
11 | 6, 10 | rspcdv 3285 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) →
(7 < (𝑁 − 3)
→ (𝑁 − 3) ∈
GoldbachOddALTV ))) |
12 | | eluz2 11569 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘;12)
↔ (;12 ∈ ℤ ∧
𝑁 ∈ ℤ ∧
;12 ≤ 𝑁)) |
13 | | 7p3e10 11479 |
. . . . . . . . . . 11
⊢ (7 + 3) =
;10 |
14 | | 1nn0 11185 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
15 | | 0nn0 11184 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
16 | | 2nn 11062 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
17 | | 2pos 10989 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
18 | 14, 15, 16, 17 | declt 11406 |
. . . . . . . . . . 11
⊢ ;10 < ;12 |
19 | 13, 18 | eqbrtri 4604 |
. . . . . . . . . 10
⊢ (7 + 3)
< ;12 |
20 | | 7re 10980 |
. . . . . . . . . . . 12
⊢ 7 ∈
ℝ |
21 | | 3re 10971 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℝ |
22 | 20, 21 | readdcli 9932 |
. . . . . . . . . . 11
⊢ (7 + 3)
∈ ℝ |
23 | | 2nn0 11186 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
24 | 14, 23 | deccl 11388 |
. . . . . . . . . . . 12
⊢ ;12 ∈
ℕ0 |
25 | 24 | nn0rei 11180 |
. . . . . . . . . . 11
⊢ ;12 ∈ ℝ |
26 | | zre 11258 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
27 | | ltletr 10008 |
. . . . . . . . . . 11
⊢ (((7 + 3)
∈ ℝ ∧ ;12 ∈
ℝ ∧ 𝑁 ∈
ℝ) → (((7 + 3) < ;12
∧ ;12 ≤ 𝑁) → (7 + 3) < 𝑁)) |
28 | 22, 25, 26, 27 | mp3an12i 1420 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (((7 + 3)
< ;12 ∧ ;12 ≤ 𝑁) → (7 + 3) < 𝑁)) |
29 | 19, 28 | mpani 708 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (;12 ≤ 𝑁 → (7 + 3) < 𝑁)) |
30 | 29 | imp 444 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → (7 + 3) < 𝑁) |
31 | 30 | 3adant1 1072 |
. . . . . . 7
⊢ ((;12 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → (7 + 3) < 𝑁) |
32 | 20 | a1i 11 |
. . . . . . . 8
⊢ ((;12 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → 7 ∈ ℝ) |
33 | 21 | a1i 11 |
. . . . . . . 8
⊢ ((;12 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → 3 ∈ ℝ) |
34 | 26 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((;12 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → 𝑁 ∈ ℝ) |
35 | 32, 33, 34 | ltaddsubd 10506 |
. . . . . . 7
⊢ ((;12 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → ((7 + 3) < 𝑁 ↔ 7 < (𝑁 − 3))) |
36 | 31, 35 | mpbid 221 |
. . . . . 6
⊢ ((;12 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ;12 ≤ 𝑁) → 7 < (𝑁 − 3)) |
37 | 12, 36 | sylbi 206 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 7 < (𝑁 −
3)) |
38 | 37 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ 7 < (𝑁 −
3)) |
39 | | simpr 476 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ) ∧
(𝑁 − 3) ∈
GoldbachOddALTV ) → (𝑁
− 3) ∈ GoldbachOddALTV ) |
40 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑜 = (𝑁 − 3) → (𝑜 + 3) = ((𝑁 − 3) + 3)) |
41 | 40 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑜 = (𝑁 − 3) → (𝑁 = (𝑜 + 3) ↔ 𝑁 = ((𝑁 − 3) + 3))) |
42 | 41 | adantl 481 |
. . . . . 6
⊢ ((((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ) ∧
(𝑁 − 3) ∈
GoldbachOddALTV ) ∧ 𝑜 =
(𝑁 − 3)) →
(𝑁 = (𝑜 + 3) ↔ 𝑁 = ((𝑁 − 3) + 3))) |
43 | | eluzelcn 11575 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ 𝑁 ∈
ℂ) |
44 | | 3cn 10972 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
45 | 43, 44 | jctir 559 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘;12)
→ (𝑁 ∈ ℂ
∧ 3 ∈ ℂ)) |
46 | 45 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (𝑁 ∈ ℂ
∧ 3 ∈ ℂ)) |
47 | 46 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ) ∧
(𝑁 − 3) ∈
GoldbachOddALTV ) → (𝑁
∈ ℂ ∧ 3 ∈ ℂ)) |
48 | | npcan 10169 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 3 ∈
ℂ) → ((𝑁 −
3) + 3) = 𝑁) |
49 | 48 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 3 ∈
ℂ) → 𝑁 = ((𝑁 − 3) +
3)) |
50 | 47, 49 | syl 17 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ) ∧
(𝑁 − 3) ∈
GoldbachOddALTV ) → 𝑁
= ((𝑁 − 3) +
3)) |
51 | 39, 42, 50 | rspcedvd 3289 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even ) ∧
(𝑁 − 3) ∈
GoldbachOddALTV ) → ∃𝑜 ∈ GoldbachOddALTV 𝑁 = (𝑜 + 3)) |
52 | 51 | ex 449 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ ((𝑁 − 3)
∈ GoldbachOddALTV → ∃𝑜 ∈ GoldbachOddALTV 𝑁 = (𝑜 + 3))) |
53 | 38, 52 | embantd 57 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ ((7 < (𝑁 −
3) → (𝑁 − 3)
∈ GoldbachOddALTV ) → ∃𝑜 ∈ GoldbachOddALTV 𝑁 = (𝑜 + 3))) |
54 | 11, 53 | syld 46 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ (∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) →
∃𝑜 ∈
GoldbachOddALTV 𝑁 = (𝑜 + 3))) |
55 | 54 | com12 32 |
1
⊢
(∀𝑚 ∈
Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) →
((𝑁 ∈
(ℤ≥‘;12)
∧ 𝑁 ∈ Even )
→ ∃𝑜 ∈
GoldbachOddALTV 𝑁 = (𝑜 + 3))) |