| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfra1 3283 | . 2
⊢
Ⅎ𝑛∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) | 
| 2 |  | eqeq1 2740 | . . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 3 | 2 | rexbidv 3178 | . . . . . . 7
⊢ (𝑛 = 𝑚 → (∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 4 | 3 | 2rexbidv 3221 | . . . . . 6
⊢ (𝑛 = 𝑚 → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟))) | 
| 5 | 4 | cbvralvw 3236 | . . . . 5
⊢
(∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ ∀𝑚 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟)) | 
| 6 |  | 6nn 12356 | . . . . . . . . 9
⊢ 6 ∈
ℕ | 
| 7 | 6 | nnzi 12643 | . . . . . . . 8
⊢ 6 ∈
ℤ | 
| 8 | 7 | a1i 11 | . . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → 6 ∈
ℤ) | 
| 9 |  | evenz 47622 | . . . . . . . . 9
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℤ) | 
| 10 |  | 2z 12651 | . . . . . . . . . 10
⊢ 2 ∈
ℤ | 
| 11 | 10 | a1i 11 | . . . . . . . . 9
⊢ (𝑛 ∈ Even → 2 ∈
ℤ) | 
| 12 | 9, 11 | zaddcld 12728 | . . . . . . . 8
⊢ (𝑛 ∈ Even → (𝑛 + 2) ∈
ℤ) | 
| 13 | 12 | adantr 480 | . . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (𝑛 + 2) ∈ ℤ) | 
| 14 |  | 4cn 12352 | . . . . . . . . . 10
⊢ 4 ∈
ℂ | 
| 15 |  | 2cn 12342 | . . . . . . . . . 10
⊢ 2 ∈
ℂ | 
| 16 |  | 4p2e6 12420 | . . . . . . . . . . 11
⊢ (4 + 2) =
6 | 
| 17 | 16 | eqcomi 2745 | . . . . . . . . . 10
⊢ 6 = (4 +
2) | 
| 18 | 14, 15, 17 | mvrraddi 11526 | . . . . . . . . 9
⊢ (6
− 2) = 4 | 
| 19 |  | 2p2e4 12402 | . . . . . . . . . 10
⊢ (2 + 2) =
4 | 
| 20 |  | 2evenALTV 47684 | . . . . . . . . . . 11
⊢ 2 ∈
Even | 
| 21 |  | evenltle 47709 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ Even ∧ 2 ∈ Even
∧ 2 < 𝑛) → (2 +
2) ≤ 𝑛) | 
| 22 | 20, 21 | mp3an2 1450 | . . . . . . . . . 10
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (2 + 2) ≤ 𝑛) | 
| 23 | 19, 22 | eqbrtrrid 5178 | . . . . . . . . 9
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → 4 ≤ 𝑛) | 
| 24 | 18, 23 | eqbrtrid 5177 | . . . . . . . 8
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (6 − 2) ≤
𝑛) | 
| 25 |  | 6re 12357 | . . . . . . . . . . . 12
⊢ 6 ∈
ℝ | 
| 26 | 25 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 6 ∈
ℝ) | 
| 27 |  | 2re 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 28 | 27 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 2 ∈
ℝ) | 
| 29 | 9 | zred 12724 | . . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℝ) | 
| 30 | 26, 28, 29 | 3jca 1128 | . . . . . . . . . 10
⊢ (𝑛 ∈ Even → (6 ∈
ℝ ∧ 2 ∈ ℝ ∧ 𝑛 ∈ ℝ)) | 
| 31 | 30 | adantr 480 | . . . . . . . . 9
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (6 ∈ ℝ ∧
2 ∈ ℝ ∧ 𝑛
∈ ℝ)) | 
| 32 |  | lesubadd 11736 | . . . . . . . . 9
⊢ ((6
∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((6 − 2) ≤
𝑛 ↔ 6 ≤ (𝑛 + 2))) | 
| 33 | 31, 32 | syl 17 | . . . . . . . 8
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → ((6 − 2) ≤
𝑛 ↔ 6 ≤ (𝑛 + 2))) | 
| 34 | 24, 33 | mpbid 232 | . . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → 6 ≤ (𝑛 + 2)) | 
| 35 |  | eluz2 12885 | . . . . . . 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 3178 | . . . . . . . 8
⊢ (𝑚 = (𝑛 + 2) → (∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) | 
| 39 | 38 | 2rexbidv 3221 | . . . . . . 7
⊢ (𝑚 = (𝑛 + 2) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) | 
| 40 | 39 | rspcv 3617 | . . . . . 6
⊢ ((𝑛 + 2) ∈
(ℤ≥‘6) → (∀𝑚 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) | 
| 41 | 36, 40 | syl 17 | . . . . 5
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (∀𝑚 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑚 = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) | 
| 42 | 5, 41 | biimtrid 242 | . . . 4
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟))) | 
| 43 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑝(𝑛 ∈ Even ∧ 2 < 𝑛) | 
| 44 |  | nfre1 3284 | . . . . 5
⊢
Ⅎ𝑝∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) | 
| 45 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑞((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ 𝑝 ∈ ℙ) | 
| 46 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑞ℙ | 
| 47 |  | nfre1 3284 | . . . . . . . 8
⊢
Ⅎ𝑞∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) | 
| 48 | 46, 47 | nfrexw 3312 | . . . . . . 7
⊢
Ⅎ𝑞∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞) | 
| 49 |  | simplrl 776 | . . . . . . . . . . . 12
⊢ ((((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) ∧ 𝑟 ∈ ℙ) → 𝑝 ∈ ℙ) | 
| 50 |  | simplrr 777 | . . . . . . . . . . . 12
⊢ ((((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) ∧ 𝑟 ∈ ℙ) → 𝑞 ∈ ℙ) | 
| 51 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) ∧ 𝑟 ∈ ℙ) → 𝑟 ∈ ℙ) | 
| 52 | 49, 50, 51 | 3jca 1128 | . . . . . . . . . . 11
⊢ ((((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) ∧ 𝑟 ∈ ℙ) → (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ)) | 
| 53 | 52 | adantr 480 | . . . . . . . . . 10
⊢
(((((𝑛 ∈ Even
∧ 2 < 𝑛) ∧
(𝑝 ∈ ℙ ∧
𝑞 ∈ ℙ)) ∧
𝑟 ∈ ℙ) ∧
(𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ)) | 
| 54 |  | simp-4l 782 | . . . . . . . . . 10
⊢
(((((𝑛 ∈ Even
∧ 2 < 𝑛) ∧
(𝑝 ∈ ℙ ∧
𝑞 ∈ ℙ)) ∧
𝑟 ∈ ℙ) ∧
(𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → 𝑛 ∈ Even ) | 
| 55 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝑛 ∈ Even
∧ 2 < 𝑛) ∧
(𝑝 ∈ ℙ ∧
𝑞 ∈ ℙ)) ∧
𝑟 ∈ ℙ) ∧
(𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) | 
| 56 |  | mogoldbblem 47712 | . . . . . . . . . . 11
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ) ∧ 𝑛 ∈ Even ∧ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑦 ∈ ℙ ∃𝑥 ∈ ℙ 𝑛 = (𝑦 + 𝑥)) | 
| 57 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑝 = 𝑦 → (𝑝 + 𝑞) = (𝑦 + 𝑞)) | 
| 58 | 57 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑝 = 𝑦 → (𝑛 = (𝑝 + 𝑞) ↔ 𝑛 = (𝑦 + 𝑞))) | 
| 59 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑞 = 𝑥 → (𝑦 + 𝑞) = (𝑦 + 𝑥)) | 
| 60 | 59 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑞 = 𝑥 → (𝑛 = (𝑦 + 𝑞) ↔ 𝑛 = (𝑦 + 𝑥))) | 
| 61 | 58, 60 | cbvrex2vw 3241 | . . . . . . . . . . 11
⊢
(∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ 𝑛 = (𝑝 + 𝑞) ↔ ∃𝑦 ∈ ℙ ∃𝑥 ∈ ℙ 𝑛 = (𝑦 + 𝑥)) | 
| 62 | 56, 61 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ) ∧ 𝑛 ∈ Even ∧ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) | 
| 63 | 53, 54, 55, 62 | syl3anc 1372 | . . . . . . . . 9
⊢
(((((𝑛 ∈ Even
∧ 2 < 𝑛) ∧
(𝑝 ∈ ℙ ∧
𝑞 ∈ ℙ)) ∧
𝑟 ∈ ℙ) ∧
(𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)) | 
| 64 | 63 | rexlimdva2 3156 | . . . . . . . 8
⊢ (((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ (𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ)) → (∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) | 
| 65 | 64 | expr 456 | . . . . . . 7
⊢ (((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ 𝑝 ∈ ℙ) → (𝑞 ∈ ℙ → (∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) | 
| 66 | 45, 48, 65 | rexlimd 3265 | . . . . . 6
⊢ (((𝑛 ∈ Even ∧ 2 < 𝑛) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) | 
| 67 | 66 | ex 412 | . . . . 5
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (𝑝 ∈ ℙ → (∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) | 
| 68 | 43, 44, 67 | rexlimd 3265 | . . . 4
⊢ ((𝑛 ∈ Even ∧ 2 < 𝑛) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ (𝑛 + 2) = ((𝑝 + 𝑞) + 𝑟) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) | 
| 69 | 42, 68 | syldc 48 | . . 3
⊢
(∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → ((𝑛 ∈ Even ∧ 2 < 𝑛) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) | 
| 70 | 69 | expd 415 | . 2
⊢
(∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → (𝑛 ∈ Even → (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))) | 
| 71 | 1, 70 | ralrimi 3256 | 1
⊢
(∀𝑛 ∈
(ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) |