Step | Hyp | Ref
| Expression |
1 | | nfra1 3267 |
. 2
⊢
Ⅎ𝑛∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) |
2 | | eqeq1 2740 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
3 | 2 | rexbidv 3175 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
4 | 3 | 2rexbidv 3213 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) |
5 | 4 | cbvralvw 3225 |
. . . . 5
⊢
(∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ ∀𝑚 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟)) |
6 | | 6nn 12242 |
. . . . . . . . 9
⊢ 6 ∈
ℕ |
7 | 6 | nnzi 12527 |
. . . . . . . 8
⊢ 6 ∈
ℤ |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → 6 ∈
ℤ) |
9 | | evenz 45812 |
. . . . . . . . 9
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℤ) |
10 | | 2z 12535 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ Even → 2 ∈
ℤ) |
12 | 9, 11 | zaddcld 12611 |
. . . . . . . 8
⊢ (𝑛 ∈ Even → (𝑛 + 2) ∈
ℤ) |
13 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (𝑛 + 2) ∈ ℤ) |
14 | | 4cn 12238 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
15 | | 2cn 12228 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
16 | | 4p2e6 12306 |
. . . . . . . . . . 11
⊢ (4 + 2) =
6 |
17 | 16 | eqcomi 2745 |
. . . . . . . . . 10
⊢ 6 = (4 +
2) |
18 | 14, 15, 17 | mvrraddi 11418 |
. . . . . . . . 9
⊢ (6
− 2) = 4 |
19 | | 2p2e4 12288 |
. . . . . . . . . 10
⊢ (2 + 2) =
4 |
20 | | 2evenALTV 45874 |
. . . . . . . . . . 11
⊢ 2 ∈
Even |
21 | | evenltle 45899 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ Even ∧ 2 ∈ Even
∧ 2 < 𝑛) → (2 +
2) ≤ 𝑛) |
22 | 20, 21 | mp3an2 1449 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (2 + 2) ≤ 𝑛) |
23 | 19, 22 | eqbrtrrid 5141 |
. . . . . . . . 9
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → 4 ≤ 𝑛) |
24 | 18, 23 | eqbrtrid 5140 |
. . . . . . . 8
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (6 − 2) ≤
𝑛) |
25 | | 6re 12243 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ |
26 | 25 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 6 ∈
ℝ) |
27 | | 2re 12227 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
28 | 27 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 2 ∈
ℝ) |
29 | 9 | zred 12607 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℝ) |
30 | 26, 28, 29 | 3jca 1128 |
. . . . . . . . . 10
⊢ (𝑛 ∈ Even → (6 ∈
ℝ ∧ 2 ∈ ℝ ∧ 𝑛 ∈ ℝ)) |
31 | 30 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (6 ∈ ℝ ∧
2 ∈ ℝ ∧ 𝑛
∈ ℝ)) |
32 | | lesubadd 11627 |
. . . . . . . . 9
⊢ ((6
∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((6 − 2) ≤
𝑛 ↔ 6 ≤ (𝑛 + 2))) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → ((6 − 2) ≤
𝑛 ↔ 6 ≤ (𝑛 + 2))) |
34 | 24, 33 | mpbid 231 |
. . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → 6 ≤ (𝑛 + 2)) |
35 | | eluz2 12769 |
. . . . . . 7
⊢ ((𝑛 + 2) ∈
(ℤ≥‘6) ↔ (6 ∈ ℤ ∧ (𝑛 + 2) ∈ ℤ ∧ 6
≤ (𝑛 +
2))) |
36 | 8, 13, 34, 35 | syl3anbrc 1343 |
. . . . . 6
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (𝑛 + 2) ∈
(ℤ≥‘6)) |
37 | | eqeq1 2740 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 2) → (𝑚 = ((𝑝 + 𝑞) + 𝑟) ↔ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) |
38 | 37 | rexbidv 3175 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 2) → (∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) |
39 | 38 | 2rexbidv 3213 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 2) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) |
40 | 39 | rspcv 3577 |
. . . . . 6
⊢ ((𝑛 + 2) ∈
(ℤ≥‘6) → (∀𝑚 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) |
41 | 36, 40 | syl 17 |
. . . . 5
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (∀𝑚 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) |
42 | 5, 41 | biimtrid 241 |
. . . 4
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) |
43 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑝(𝑛 ∈ Even ∧ 2 < 𝑛) |
44 | | nfre1 3268 |
. . . . 5
⊢
Ⅎ𝑝∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) |
45 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑞((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ 𝑝 ∈ ℙ) |
46 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑞ℙ |
47 | | nfre1 3268 |
. . . . . . . 8
⊢
Ⅎ𝑞∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) |
48 | 46, 47 | nfrexw 3296 |
. . . . . . 7
⊢
Ⅎ𝑞∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) |
49 | | simplrl 775 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) ∧ 𝑟 ∈ ℙ) → 𝑝 ∈ ℙ) |
50 | | simplrr 776 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) ∧ 𝑟 ∈ ℙ) → 𝑞 ∈ ℙ) |
51 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) ∧ 𝑟 ∈ ℙ) → 𝑟 ∈ ℙ) |
52 | 49, 50, 51 | 3jca 1128 |
. . . . . . . . . . 11
⊢ ((((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) ∧ 𝑟 ∈ ℙ) → (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ)) |
53 | 52 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝑛 ∈ Even
∧ 2 < 𝑛) ∧
(𝑝 ∈ ℙ ∧
𝑞 ∈ ℙ)) ∧
𝑟 ∈ ℙ) ∧
(𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ)) |
54 | | simp-4l 781 |
. . . . . . . . . 10
⊢
(((((𝑛 ∈ Even
∧ 2 < 𝑛) ∧
(𝑝 ∈ ℙ ∧
𝑞 ∈ ℙ)) ∧
𝑟 ∈ ℙ) ∧
(𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → 𝑛 ∈ Even ) |
55 | | simpr 485 |
. . . . . . . . . 10
⊢
(((((𝑛 ∈ Even
∧ 2 < 𝑛) ∧
(𝑝 ∈ ℙ ∧
𝑞 ∈ ℙ)) ∧
𝑟 ∈ ℙ) ∧
(𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) |
56 | | mogoldbblem 45902 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ) ∧ 𝑛 ∈ Even ∧ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑦 ∈ ℙ ∃𝑥 ∈ ℙ 𝑛 = (𝑦 + 𝑥)) |
57 | | oveq1 7364 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑦 → (𝑝 + 𝑞) = (𝑦 + 𝑞)) |
58 | 57 | eqeq2d 2747 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑦 → (𝑛 = (𝑝 + 𝑞) ↔ 𝑛 = (𝑦 + 𝑞))) |
59 | | oveq2 7365 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑥 → (𝑦 + 𝑞) = (𝑦 + 𝑥)) |
60 | 59 | eqeq2d 2747 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑥 → (𝑛 = (𝑦 + 𝑞) ↔ 𝑛 = (𝑦 + 𝑥))) |
61 | 58, 60 | cbvrex2vw 3228 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ 𝑛 = (𝑝 + 𝑞) ↔ ∃𝑦 ∈ ℙ ∃𝑥 ∈ ℙ 𝑛 = (𝑦 + 𝑥)) |
62 | 56, 61 | sylibr 233 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ) ∧ 𝑛 ∈ Even ∧ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) |
63 | 53, 54, 55, 62 | syl3anc 1371 |
. . . . . . . . 9
⊢
(((((𝑛 ∈ Even
∧ 2 < 𝑛) ∧
(𝑝 ∈ ℙ ∧
𝑞 ∈ ℙ)) ∧
𝑟 ∈ ℙ) ∧
(𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) |
64 | 63 | rexlimdva2 3154 |
. . . . . . . 8
⊢ (((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) → (∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
65 | 64 | expr 457 |
. . . . . . 7
⊢ (((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ 𝑝 ∈ ℙ) → (𝑞 ∈ ℙ → (∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
66 | 45, 48, 65 | rexlimd 3249 |
. . . . . 6
⊢ (((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
67 | 66 | ex 413 |
. . . . 5
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (𝑝 ∈ ℙ → (∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
68 | 43, 44, 67 | rexlimd 3249 |
. . . 4
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
69 | 42, 68 | syldc 48 |
. . 3
⊢
(∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → ((𝑛 ∈ Even ∧ 2 < 𝑛) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |
70 | 69 | expd 416 |
. 2
⊢
(∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → (𝑛 ∈ Even → (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) |
71 | 1, 70 | ralrimi 3240 |
1
⊢
(∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |