| Step | Hyp | Ref
| Expression |
| 1 | | ax-hgprmladder 47801 |
. 2
⊢
∃𝑑 ∈
(ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |
| 2 | | 1nn0 12542 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
| 3 | | 1nn 12277 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
| 4 | 2, 3 | decnncl 12753 |
. . . . . . . . 9
⊢ ;11 ∈ ℕ |
| 5 | 4 | nnzi 12641 |
. . . . . . . 8
⊢ ;11 ∈ ℤ |
| 6 | | 8nn0 12549 |
. . . . . . . . . . 11
⊢ 8 ∈
ℕ0 |
| 7 | | 8nn 12361 |
. . . . . . . . . . 11
⊢ 8 ∈
ℕ |
| 8 | 6, 7 | decnncl 12753 |
. . . . . . . . . 10
⊢ ;88 ∈ ℕ |
| 9 | | 10nn 12749 |
. . . . . . . . . . 11
⊢ ;10 ∈ ℕ |
| 10 | | 2nn0 12543 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
| 11 | | 9nn 12364 |
. . . . . . . . . . . . 13
⊢ 9 ∈
ℕ |
| 12 | 10, 11 | decnncl 12753 |
. . . . . . . . . . . 12
⊢ ;29 ∈ ℕ |
| 13 | 12 | nnnn0i 12534 |
. . . . . . . . . . 11
⊢ ;29 ∈
ℕ0 |
| 14 | | nnexpcl 14115 |
. . . . . . . . . . 11
⊢ ((;10 ∈ ℕ ∧ ;29 ∈ ℕ0) →
(;10↑;29) ∈ ℕ) |
| 15 | 9, 13, 14 | mp2an 692 |
. . . . . . . . . 10
⊢ (;10↑;29) ∈ ℕ |
| 16 | 8, 15 | nnmulcli 12291 |
. . . . . . . . 9
⊢ (;88 · (;10↑;29)) ∈ ℕ |
| 17 | 16 | nnzi 12641 |
. . . . . . . 8
⊢ (;88 · (;10↑;29)) ∈ ℤ |
| 18 | | 1re 11261 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
| 19 | 8 | nnrei 12275 |
. . . . . . . . . . 11
⊢ ;88 ∈ ℝ |
| 20 | 18, 19 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ ∧ ;88 ∈
ℝ) |
| 21 | | 0le1 11786 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
| 22 | | 1lt10 12872 |
. . . . . . . . . . . 12
⊢ 1 <
;10 |
| 23 | 7, 6, 2, 22 | declti 12771 |
. . . . . . . . . . 11
⊢ 1 <
;88 |
| 24 | 21, 23 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (0 ≤ 1
∧ 1 < ;88) |
| 25 | | nnexpcl 14115 |
. . . . . . . . . . . . 13
⊢ ((;10 ∈ ℕ ∧ 1 ∈
ℕ0) → (;10↑1) ∈ ℕ) |
| 26 | 9, 2, 25 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (;10↑1) ∈
ℕ |
| 27 | 26 | nnrei 12275 |
. . . . . . . . . . 11
⊢ (;10↑1) ∈
ℝ |
| 28 | 15 | nnrei 12275 |
. . . . . . . . . . 11
⊢ (;10↑;29) ∈ ℝ |
| 29 | 27, 28 | pm3.2i 470 |
. . . . . . . . . 10
⊢ ((;10↑1) ∈ ℝ ∧ (;10↑;29) ∈ ℝ) |
| 30 | | 0re 11263 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
| 31 | | 10re 12752 |
. . . . . . . . . . . . 13
⊢ ;10 ∈ ℝ |
| 32 | | 10pos 12750 |
. . . . . . . . . . . . 13
⊢ 0 <
;10 |
| 33 | 30, 31, 32 | ltleii 11384 |
. . . . . . . . . . . 12
⊢ 0 ≤
;10 |
| 34 | 9 | nncni 12276 |
. . . . . . . . . . . . 13
⊢ ;10 ∈ ℂ |
| 35 | | exp1 14108 |
. . . . . . . . . . . . 13
⊢ (;10 ∈ ℂ → (;10↑1) = ;10) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (;10↑1) = ;10 |
| 37 | 33, 36 | breqtrri 5170 |
. . . . . . . . . . 11
⊢ 0 ≤
(;10↑1) |
| 38 | | 1z 12647 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
| 39 | 12 | nnzi 12641 |
. . . . . . . . . . . . 13
⊢ ;29 ∈ ℤ |
| 40 | 31, 38, 39 | 3pm3.2i 1340 |
. . . . . . . . . . . 12
⊢ (;10 ∈ ℝ ∧ 1 ∈
ℤ ∧ ;29 ∈
ℤ) |
| 41 | | 2nn 12339 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
| 42 | | 9nn0 12550 |
. . . . . . . . . . . . . 14
⊢ 9 ∈
ℕ0 |
| 43 | 41, 42, 2, 22 | declti 12771 |
. . . . . . . . . . . . 13
⊢ 1 <
;29 |
| 44 | 22, 43 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (1 <
;10 ∧ 1 < ;29) |
| 45 | | ltexp2a 14206 |
. . . . . . . . . . . 12
⊢ (((;10 ∈ ℝ ∧ 1 ∈
ℤ ∧ ;29 ∈ ℤ)
∧ (1 < ;10 ∧ 1 <
;29)) → (;10↑1) < (;10↑;29)) |
| 46 | 40, 44, 45 | mp2an 692 |
. . . . . . . . . . 11
⊢ (;10↑1) < (;10↑;29) |
| 47 | 37, 46 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (0 ≤
(;10↑1) ∧ (;10↑1) < (;10↑;29)) |
| 48 | | ltmul12a 12123 |
. . . . . . . . . 10
⊢ ((((1
∈ ℝ ∧ ;88 ∈
ℝ) ∧ (0 ≤ 1 ∧ 1 < ;88)) ∧ (((;10↑1) ∈ ℝ ∧ (;10↑;29) ∈ ℝ) ∧ (0 ≤ (;10↑1) ∧ (;10↑1) < (;10↑;29)))) → (1 · (;10↑1)) < (;88 · (;10↑;29))) |
| 49 | 20, 24, 29, 47, 48 | mp4an 693 |
. . . . . . . . 9
⊢ (1
· (;10↑1)) < (;88 · (;10↑;29)) |
| 50 | 26 | nnzi 12641 |
. . . . . . . . . . . 12
⊢ (;10↑1) ∈
ℤ |
| 51 | | zmulcl 12666 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ (;10↑1)
∈ ℤ) → (1 · (;10↑1)) ∈ ℤ) |
| 52 | 38, 50, 51 | mp2an 692 |
. . . . . . . . . . 11
⊢ (1
· (;10↑1)) ∈
ℤ |
| 53 | | zltp1le 12667 |
. . . . . . . . . . 11
⊢ (((1
· (;10↑1)) ∈
ℤ ∧ (;88 · (;10↑;29)) ∈ ℤ) → ((1 · (;10↑1)) < (;88 · (;10↑;29)) ↔ ((1 · (;10↑1)) + 1) ≤ (;88 · (;10↑;29)))) |
| 54 | 52, 17, 53 | mp2an 692 |
. . . . . . . . . 10
⊢ ((1
· (;10↑1)) < (;88 · (;10↑;29)) ↔ ((1 · (;10↑1)) + 1) ≤ (;88 · (;10↑;29))) |
| 55 | | 1t10e1p1e11 47322 |
. . . . . . . . . . . 12
⊢ ;11 = ((1 · (;10↑1)) + 1) |
| 56 | 55 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ ((1
· (;10↑1)) + 1) =
;11 |
| 57 | 56 | breq1i 5150 |
. . . . . . . . . 10
⊢ (((1
· (;10↑1)) + 1) ≤
(;88 · (;10↑;29)) ↔ ;11 ≤ (;88 · (;10↑;29))) |
| 58 | 54, 57 | bitri 275 |
. . . . . . . . 9
⊢ ((1
· (;10↑1)) < (;88 · (;10↑;29)) ↔ ;11 ≤ (;88 · (;10↑;29))) |
| 59 | 49, 58 | mpbi 230 |
. . . . . . . 8
⊢ ;11 ≤ (;88 · (;10↑;29)) |
| 60 | | eluz2 12884 |
. . . . . . . 8
⊢ ((;88 · (;10↑;29)) ∈ (ℤ≥‘;11) ↔ (;11 ∈ ℤ ∧ (;88 · (;10↑;29)) ∈ ℤ ∧ ;11 ≤ (;88 · (;10↑;29)))) |
| 61 | 5, 17, 59, 60 | mpbir3an 1342 |
. . . . . . 7
⊢ (;88 · (;10↑;29)) ∈ (ℤ≥‘;11) |
| 62 | 61 | a1i 11 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → (;88 · (;10↑;29)) ∈ (ℤ≥‘;11)) |
| 63 | | 4nn 12349 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ |
| 64 | 2, 7 | decnncl 12753 |
. . . . . . . . . . . 12
⊢ ;18 ∈ ℕ |
| 65 | 64 | nnnn0i 12534 |
. . . . . . . . . . 11
⊢ ;18 ∈
ℕ0 |
| 66 | | nnexpcl 14115 |
. . . . . . . . . . 11
⊢ ((;10 ∈ ℕ ∧ ;18 ∈ ℕ0) →
(;10↑;18) ∈ ℕ) |
| 67 | 9, 65, 66 | mp2an 692 |
. . . . . . . . . 10
⊢ (;10↑;18) ∈ ℕ |
| 68 | 63, 67 | nnmulcli 12291 |
. . . . . . . . 9
⊢ (4
· (;10↑;18)) ∈ ℕ |
| 69 | 68 | nnzi 12641 |
. . . . . . . 8
⊢ (4
· (;10↑;18)) ∈ ℤ |
| 70 | | 4re 12350 |
. . . . . . . . . . 11
⊢ 4 ∈
ℝ |
| 71 | 18, 70 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ ∧ 4 ∈ ℝ) |
| 72 | | 1lt4 12442 |
. . . . . . . . . . 11
⊢ 1 <
4 |
| 73 | 21, 72 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (0 ≤ 1
∧ 1 < 4) |
| 74 | 67 | nnrei 12275 |
. . . . . . . . . . 11
⊢ (;10↑;18) ∈ ℝ |
| 75 | 27, 74 | pm3.2i 470 |
. . . . . . . . . 10
⊢ ((;10↑1) ∈ ℝ ∧ (;10↑;18) ∈ ℝ) |
| 76 | 64 | nnzi 12641 |
. . . . . . . . . . . . 13
⊢ ;18 ∈ ℤ |
| 77 | 31, 38, 76 | 3pm3.2i 1340 |
. . . . . . . . . . . 12
⊢ (;10 ∈ ℝ ∧ 1 ∈
ℤ ∧ ;18 ∈
ℤ) |
| 78 | 3, 6, 2, 22 | declti 12771 |
. . . . . . . . . . . . 13
⊢ 1 <
;18 |
| 79 | 22, 78 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (1 <
;10 ∧ 1 < ;18) |
| 80 | | ltexp2a 14206 |
. . . . . . . . . . . 12
⊢ (((;10 ∈ ℝ ∧ 1 ∈
ℤ ∧ ;18 ∈ ℤ)
∧ (1 < ;10 ∧ 1 <
;18)) → (;10↑1) < (;10↑;18)) |
| 81 | 77, 79, 80 | mp2an 692 |
. . . . . . . . . . 11
⊢ (;10↑1) < (;10↑;18) |
| 82 | 37, 81 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (0 ≤
(;10↑1) ∧ (;10↑1) < (;10↑;18)) |
| 83 | | ltmul12a 12123 |
. . . . . . . . . 10
⊢ ((((1
∈ ℝ ∧ 4 ∈ ℝ) ∧ (0 ≤ 1 ∧ 1 < 4)) ∧
(((;10↑1) ∈ ℝ
∧ (;10↑;18) ∈ ℝ) ∧ (0 ≤ (;10↑1) ∧ (;10↑1) < (;10↑;18)))) → (1 · (;10↑1)) < (4 · (;10↑;18))) |
| 84 | 71, 73, 75, 82, 83 | mp4an 693 |
. . . . . . . . 9
⊢ (1
· (;10↑1)) < (4
· (;10↑;18)) |
| 85 | | 4z 12651 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℤ |
| 86 | 67 | nnzi 12641 |
. . . . . . . . . . . 12
⊢ (;10↑;18) ∈ ℤ |
| 87 | | zmulcl 12666 |
. . . . . . . . . . . 12
⊢ ((4
∈ ℤ ∧ (;10↑;18) ∈ ℤ) → (4 · (;10↑;18)) ∈ ℤ) |
| 88 | 85, 86, 87 | mp2an 692 |
. . . . . . . . . . 11
⊢ (4
· (;10↑;18)) ∈ ℤ |
| 89 | | zltp1le 12667 |
. . . . . . . . . . 11
⊢ (((1
· (;10↑1)) ∈
ℤ ∧ (4 · (;10↑;18)) ∈ ℤ) → ((1 · (;10↑1)) < (4 · (;10↑;18)) ↔ ((1 · (;10↑1)) + 1) ≤ (4 · (;10↑;18)))) |
| 90 | 52, 88, 89 | mp2an 692 |
. . . . . . . . . 10
⊢ ((1
· (;10↑1)) < (4
· (;10↑;18)) ↔ ((1 · (;10↑1)) + 1) ≤ (4 ·
(;10↑;18))) |
| 91 | 56 | breq1i 5150 |
. . . . . . . . . 10
⊢ (((1
· (;10↑1)) + 1) ≤
(4 · (;10↑;18)) ↔ ;11 ≤ (4 · (;10↑;18))) |
| 92 | 90, 91 | bitri 275 |
. . . . . . . . 9
⊢ ((1
· (;10↑1)) < (4
· (;10↑;18)) ↔ ;11 ≤ (4 · (;10↑;18))) |
| 93 | 84, 92 | mpbi 230 |
. . . . . . . 8
⊢ ;11 ≤ (4 · (;10↑;18)) |
| 94 | | eluz2 12884 |
. . . . . . . 8
⊢ ((4
· (;10↑;18)) ∈
(ℤ≥‘;11)
↔ (;11 ∈ ℤ ∧
(4 · (;10↑;18)) ∈ ℤ ∧ ;11 ≤ (4 · (;10↑;18)))) |
| 95 | 5, 69, 93, 94 | mpbir3an 1342 |
. . . . . . 7
⊢ (4
· (;10↑;18)) ∈
(ℤ≥‘;11) |
| 96 | 95 | a1i 11 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → (4 · (;10↑;18)) ∈ (ℤ≥‘;11)) |
| 97 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ Even ∧ (4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 𝑛 ∈ Even ) |
| 98 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ Even ∧ (4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 4 < 𝑛) |
| 99 | | evenz 47617 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℤ) |
| 100 | 99 | zred 12722 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℝ) |
| 101 | 68 | nnrei 12275 |
. . . . . . . . . . . . 13
⊢ (4
· (;10↑;18)) ∈ ℝ |
| 102 | | ltle 11349 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℝ ∧ (4
· (;10↑;18)) ∈ ℝ) → (𝑛 < (4 · (;10↑;18)) → 𝑛 ≤ (4 · (;10↑;18)))) |
| 103 | 100, 101,
102 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ Even → (𝑛 < (4 · (;10↑;18)) → 𝑛 ≤ (4 · (;10↑;18)))) |
| 104 | 103 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Even → (4 <
𝑛 → (𝑛 < (4 · (;10↑;18)) → 𝑛 ≤ (4 · (;10↑;18))))) |
| 105 | 104 | imp32 418 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ Even ∧ (4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 𝑛 ≤ (4 · (;10↑;18))) |
| 106 | | ax-bgbltosilva 47797 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 ≤ (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven ) |
| 107 | 97, 98, 105, 106 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑛 ∈ Even ∧ (4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 𝑛 ∈ GoldbachEven ) |
| 108 | 107 | ex 412 |
. . . . . . . 8
⊢ (𝑛 ∈ Even → ((4 <
𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven )) |
| 109 | 108 | a1i 11 |
. . . . . . 7
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → (𝑛 ∈ Even → ((4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven ))) |
| 110 | 109 | ralrimiv 3145 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven )) |
| 111 | | simpl 482 |
. . . . . . 7
⊢ ((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) → 𝑑 ∈
(ℤ≥‘3)) |
| 112 | 111 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → 𝑑 ∈
(ℤ≥‘3)) |
| 113 | | simpr 484 |
. . . . . . 7
⊢ ((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) → 𝑓 ∈ (RePart‘𝑑)) |
| 114 | 113 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → 𝑓 ∈ (RePart‘𝑑)) |
| 115 | | simpr 484 |
. . . . . . 7
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |
| 116 | 115 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |
| 117 | | simpl1 1192 |
. . . . . . 7
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → (𝑓‘0) = 7) |
| 118 | 117 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → (𝑓‘0) = 7) |
| 119 | | simpl2 1193 |
. . . . . . 7
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → (𝑓‘1) = ;13) |
| 120 | 119 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → (𝑓‘1) = ;13) |
| 121 | 6, 11 | decnncl 12753 |
. . . . . . . . . . . . 13
⊢ ;89 ∈ ℕ |
| 122 | 121 | nnrei 12275 |
. . . . . . . . . . . 12
⊢ ;89 ∈ ℝ |
| 123 | 15 | nngt0i 12305 |
. . . . . . . . . . . . 13
⊢ 0 <
(;10↑;29) |
| 124 | 28, 123 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ ((;10↑;29) ∈ ℝ ∧ 0 < (;10↑;29)) |
| 125 | 19, 122, 124 | 3pm3.2i 1340 |
. . . . . . . . . . 11
⊢ (;88 ∈ ℝ ∧ ;89 ∈ ℝ ∧ ((;10↑;29) ∈ ℝ ∧ 0 < (;10↑;29))) |
| 126 | | 8lt9 12465 |
. . . . . . . . . . . 12
⊢ 8 <
9 |
| 127 | 6, 6, 11, 126 | declt 12761 |
. . . . . . . . . . 11
⊢ ;88 < ;89 |
| 128 | | ltmul1a 12116 |
. . . . . . . . . . 11
⊢ (((;88 ∈ ℝ ∧ ;89 ∈ ℝ ∧ ((;10↑;29) ∈ ℝ ∧ 0 < (;10↑;29))) ∧ ;88 < ;89) → (;88 · (;10↑;29)) < (;89 · (;10↑;29))) |
| 129 | 125, 127,
128 | mp2an 692 |
. . . . . . . . . 10
⊢ (;88 · (;10↑;29)) < (;89 · (;10↑;29)) |
| 130 | | breq2 5147 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑑) = (;89 · (;10↑;29)) → ((;88 · (;10↑;29)) < (𝑓‘𝑑) ↔ (;88 · (;10↑;29)) < (;89 · (;10↑;29)))) |
| 131 | 129, 130 | mpbiri 258 |
. . . . . . . . 9
⊢ ((𝑓‘𝑑) = (;89 · (;10↑;29)) → (;88 · (;10↑;29)) < (𝑓‘𝑑)) |
| 132 | 131 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) → (;88 · (;10↑;29)) < (𝑓‘𝑑)) |
| 133 | 132 | adantr 480 |
. . . . . . 7
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → (;88 · (;10↑;29)) < (𝑓‘𝑑)) |
| 134 | 133 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → (;88 · (;10↑;29)) < (𝑓‘𝑑)) |
| 135 | 121, 15 | nnmulcli 12291 |
. . . . . . . . . . 11
⊢ (;89 · (;10↑;29)) ∈ ℕ |
| 136 | 135 | nnrei 12275 |
. . . . . . . . . 10
⊢ (;89 · (;10↑;29)) ∈ ℝ |
| 137 | | eleq1 2829 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑑) = (;89 · (;10↑;29)) → ((𝑓‘𝑑) ∈ ℝ ↔ (;89 · (;10↑;29)) ∈ ℝ)) |
| 138 | 136, 137 | mpbiri 258 |
. . . . . . . . 9
⊢ ((𝑓‘𝑑) = (;89 · (;10↑;29)) → (𝑓‘𝑑) ∈ ℝ) |
| 139 | 138 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) → (𝑓‘𝑑) ∈ ℝ) |
| 140 | 139 | adantr 480 |
. . . . . . 7
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → (𝑓‘𝑑) ∈ ℝ) |
| 141 | 140 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → (𝑓‘𝑑) ∈ ℝ) |
| 142 | 62, 96, 110, 112, 114, 116, 118, 120, 134, 141 | bgoldbtbnd 47796 |
. . . . 5
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29)))) → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd )) |
| 143 | 142 | exp31 419 |
. . . 4
⊢ ((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) → ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd )))) |
| 144 | 143 | rexlimivv 3201 |
. . 3
⊢
(∃𝑑 ∈
(ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
| 145 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (7 < 𝑛 ↔ 7 < 𝑁)) |
| 146 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑛 < (;88 · (;10↑;29)) ↔ 𝑁 < (;88 · (;10↑;29)))) |
| 147 | 145, 146 | anbi12d 632 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) ↔ (7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))))) |
| 148 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd )) |
| 149 | 147, 148 | imbi12d 344 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ) ↔ ((7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd ))) |
| 150 | 149 | rspcv 3618 |
. . . . 5
⊢ (𝑁 ∈ Odd →
(∀𝑛 ∈ Odd ((7
< 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ) → ((7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd ))) |
| 151 | 150 | com23 86 |
. . . 4
⊢ (𝑁 ∈ Odd → ((7 <
𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → (∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ) → 𝑁 ∈ GoldbachOdd
))) |
| 152 | 151 | 3impib 1117 |
. . 3
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → (∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ) → 𝑁 ∈ GoldbachOdd
)) |
| 153 | 144, 152 | sylcom 30 |
. 2
⊢
(∃𝑑 ∈
(ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd )) |
| 154 | 1, 153 | ax-mp 5 |
1
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd ) |