| Step | Hyp | Ref
| Expression |
| 1 | | oddz 47618 |
. . . . 5
⊢ (𝑛 ∈ Odd → 𝑛 ∈
ℤ) |
| 2 | 1 | zred 12722 |
. . . 4
⊢ (𝑛 ∈ Odd → 𝑛 ∈
ℝ) |
| 3 | | 10re 12752 |
. . . . 5
⊢ ;10 ∈ ℝ |
| 4 | | 2nn0 12543 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
| 5 | | 7nn 12358 |
. . . . . . 7
⊢ 7 ∈
ℕ |
| 6 | 4, 5 | decnncl 12753 |
. . . . . 6
⊢ ;27 ∈ ℕ |
| 7 | 6 | nnnn0i 12534 |
. . . . 5
⊢ ;27 ∈
ℕ0 |
| 8 | | reexpcl 14119 |
. . . . 5
⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ0) →
(;10↑;27) ∈ ℝ) |
| 9 | 3, 7, 8 | mp2an 692 |
. . . 4
⊢ (;10↑;27) ∈ ℝ |
| 10 | | lelttric 11368 |
. . . 4
⊢ ((𝑛 ∈ ℝ ∧ (;10↑;27) ∈ ℝ) → (𝑛 ≤ (;10↑;27) ∨ (;10↑;27) < 𝑛)) |
| 11 | 2, 9, 10 | sylancl 586 |
. . 3
⊢ (𝑛 ∈ Odd → (𝑛 ≤ (;10↑;27) ∨ (;10↑;27) < 𝑛)) |
| 12 | | tgoldbachlt 47803 |
. . . . 5
⊢
∃𝑚 ∈
ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑜 ∈ Odd ((7 < 𝑜 ∧ 𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd )) |
| 13 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (𝑜 = 𝑛 → (7 < 𝑜 ↔ 7 < 𝑛)) |
| 14 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑜 = 𝑛 → (𝑜 < 𝑚 ↔ 𝑛 < 𝑚)) |
| 15 | 13, 14 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑜 = 𝑛 → ((7 < 𝑜 ∧ 𝑜 < 𝑚) ↔ (7 < 𝑛 ∧ 𝑛 < 𝑚))) |
| 16 | | eleq1w 2824 |
. . . . . . . . . . . 12
⊢ (𝑜 = 𝑛 → (𝑜 ∈ GoldbachOdd ↔ 𝑛 ∈ GoldbachOdd )) |
| 17 | 15, 16 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑜 = 𝑛 → (((7 < 𝑜 ∧ 𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ) ↔ ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))) |
| 18 | 17 | rspcv 3618 |
. . . . . . . . . 10
⊢ (𝑛 ∈ Odd →
(∀𝑜 ∈ Odd ((7
< 𝑜 ∧ 𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ) → ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))) |
| 19 | 9 | recni 11275 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (;10↑;27) ∈ ℂ |
| 20 | 19 | mullidi 11266 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
· (;10↑;27)) = (;10↑;27) |
| 21 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℝ |
| 22 | | 8re 12362 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 8 ∈
ℝ |
| 23 | 21, 22 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ∈
ℝ ∧ 8 ∈ ℝ) |
| 24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (1
∈ ℝ ∧ 8 ∈ ℝ)) |
| 25 | | 0le1 11786 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ≤
1 |
| 26 | | 1lt8 12464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 <
8 |
| 27 | 25, 26 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ≤ 1
∧ 1 < 8) |
| 28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (0 ≤
1 ∧ 1 < 8)) |
| 29 | | 3nn 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 3 ∈
ℕ |
| 30 | 29 | decnncl2 12757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ;30 ∈ ℕ |
| 31 | 30 | nnnn0i 12534 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ;30 ∈
ℕ0 |
| 32 | | reexpcl 14119 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((;10 ∈ ℝ ∧ ;30 ∈ ℕ0) →
(;10↑;30) ∈ ℝ) |
| 33 | 3, 31, 32 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (;10↑;30) ∈ ℝ |
| 34 | 9, 33 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((;10↑;27) ∈ ℝ ∧ (;10↑;30) ∈ ℝ) |
| 35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → ((;10↑;27) ∈ ℝ ∧ (;10↑;30) ∈ ℝ)) |
| 36 | | 10nn0 12751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ;10 ∈
ℕ0 |
| 37 | 36, 7 | nn0expcli 14129 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (;10↑;27) ∈ ℕ0 |
| 38 | 37 | nn0ge0i 12553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ≤
(;10↑;27) |
| 39 | 6 | nnzi 12641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ;27 ∈ ℤ |
| 40 | 30 | nnzi 12641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ;30 ∈ ℤ |
| 41 | 3, 39, 40 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (;10 ∈ ℝ ∧ ;27 ∈ ℤ ∧ ;30 ∈ ℤ) |
| 42 | | 1lt10 12872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 1 <
;10 |
| 43 | | 3nn0 12544 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 3 ∈
ℕ0 |
| 44 | | 7nn0 12548 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 7 ∈
ℕ0 |
| 45 | | 0nn0 12541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
ℕ0 |
| 46 | | 7lt10 12866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 7 <
;10 |
| 47 | | 2lt3 12438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 <
3 |
| 48 | 4, 43, 44, 45, 46, 47 | decltc 12762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ;27 < ;30 |
| 49 | 42, 48 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 <
;10 ∧ ;27 < ;30) |
| 50 | | ltexp2a 14206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((;10 ∈ ℝ ∧ ;27 ∈ ℤ ∧ ;30 ∈ ℤ) ∧ (1 < ;10 ∧ ;27 < ;30)) → (;10↑;27) < (;10↑;30)) |
| 51 | 41, 49, 50 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (;10↑;27) < (;10↑;30) |
| 52 | 38, 51 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ≤
(;10↑;27) ∧ (;10↑;27) < (;10↑;30)) |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (0 ≤
(;10↑;27) ∧ (;10↑;27) < (;10↑;30))) |
| 54 | | ltmul12a 12123 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((1
∈ ℝ ∧ 8 ∈ ℝ) ∧ (0 ≤ 1 ∧ 1 < 8)) ∧
(((;10↑;27) ∈ ℝ ∧ (;10↑;30) ∈ ℝ) ∧ (0 ≤ (;10↑;27) ∧ (;10↑;27) < (;10↑;30)))) → (1 · (;10↑;27)) < (8 · (;10↑;30))) |
| 55 | 24, 28, 35, 53, 54 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (1
· (;10↑;27)) < (8 · (;10↑;30))) |
| 56 | 20, 55 | eqbrtrrid 5179 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (;10↑;27) < (8 · (;10↑;30))) |
| 57 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (;10↑;27) ∈ ℝ) |
| 58 | 22, 33 | remulcli 11277 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (8
· (;10↑;30)) ∈ ℝ |
| 59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (8
· (;10↑;30)) ∈ ℝ) |
| 60 | | nnre 12273 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
| 61 | 60 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → 𝑚 ∈
ℝ) |
| 62 | | lttr 11337 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((;10↑;27) ∈ ℝ ∧ (8 · (;10↑;30)) ∈ ℝ ∧ 𝑚 ∈ ℝ) → (((;10↑;27) < (8 · (;10↑;30)) ∧ (8 · (;10↑;30)) < 𝑚) → (;10↑;27) < 𝑚)) |
| 63 | 57, 59, 61, 62 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (((;10↑;27) < (8 · (;10↑;30)) ∧ (8 · (;10↑;30)) < 𝑚) → (;10↑;27) < 𝑚)) |
| 64 | 56, 63 | mpand 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → ((8
· (;10↑;30)) < 𝑚 → (;10↑;27) < 𝑚)) |
| 65 | 64 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8
· (;10↑;30)) < 𝑚) → (;10↑;27) < 𝑚) |
| 66 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → 𝑛 ∈
ℝ) |
| 67 | 66, 57, 61 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (𝑛 ∈ ℝ ∧ (;10↑;27) ∈ ℝ ∧ 𝑚 ∈ ℝ)) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8
· (;10↑;30)) < 𝑚) → (𝑛 ∈ ℝ ∧ (;10↑;27) ∈ ℝ ∧ 𝑚 ∈ ℝ)) |
| 69 | | lelttr 11351 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℝ ∧ (;10↑;27) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑛 ≤ (;10↑;27) ∧ (;10↑;27) < 𝑚) → 𝑛 < 𝑚)) |
| 70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8
· (;10↑;30)) < 𝑚) → ((𝑛 ≤ (;10↑;27) ∧ (;10↑;27) < 𝑚) → 𝑛 < 𝑚)) |
| 71 | 65, 70 | mpan2d 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8
· (;10↑;30)) < 𝑚) → (𝑛 ≤ (;10↑;27) → 𝑛 < 𝑚)) |
| 72 | 71 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8
· (;10↑;30)) < 𝑚) ∧ 𝑛 ≤ (;10↑;27)) → 𝑛 < 𝑚) |
| 73 | 72 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑛 ∈ Odd
∧ 𝑚 ∈ ℕ)
∧ (8 · (;10↑;30)) < 𝑚) ∧ 𝑛 ≤ (;10↑;27)) ∧ 7 < 𝑛) → (𝑛 < 𝑚 ∧ 7 < 𝑛)) |
| 74 | 73 | ancomd 461 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑛 ∈ Odd
∧ 𝑚 ∈ ℕ)
∧ (8 · (;10↑;30)) < 𝑚) ∧ 𝑛 ≤ (;10↑;27)) ∧ 7 < 𝑛) → (7 < 𝑛 ∧ 𝑛 < 𝑚)) |
| 75 | | pm2.27 42 |
. . . . . . . . . . . . . . 15
⊢ ((7 <
𝑛 ∧ 𝑛 < 𝑚) → (((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd
)) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑛 ∈ Odd
∧ 𝑚 ∈ ℕ)
∧ (8 · (;10↑;30)) < 𝑚) ∧ 𝑛 ≤ (;10↑;27)) ∧ 7 < 𝑛) → (((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd
)) |
| 77 | 76 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8
· (;10↑;30)) < 𝑚) ∧ 𝑛 ≤ (;10↑;27)) → (7 < 𝑛 → (((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd
))) |
| 78 | 77 | com23 86 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8
· (;10↑;30)) < 𝑚) ∧ 𝑛 ≤ (;10↑;27)) → (((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
| 79 | 78 | exp41 434 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Odd → (𝑚 ∈ ℕ → ((8
· (;10↑;30)) < 𝑚 → (𝑛 ≤ (;10↑;27) → (((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))))) |
| 80 | 79 | com25 99 |
. . . . . . . . . 10
⊢ (𝑛 ∈ Odd → (((7 <
𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) → ((8 ·
(;10↑;30)) < 𝑚 → (𝑛 ≤ (;10↑;27) → (𝑚 ∈ ℕ → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))))) |
| 81 | 18, 80 | syld 47 |
. . . . . . . . 9
⊢ (𝑛 ∈ Odd →
(∀𝑜 ∈ Odd ((7
< 𝑜 ∧ 𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ) → ((8 ·
(;10↑;30)) < 𝑚 → (𝑛 ≤ (;10↑;27) → (𝑚 ∈ ℕ → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))))) |
| 82 | 81 | com15 101 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ →
(∀𝑜 ∈ Odd ((7
< 𝑜 ∧ 𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ) → ((8 ·
(;10↑;30)) < 𝑚 → (𝑛 ≤ (;10↑;27) → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))))) |
| 83 | 82 | com23 86 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ → ((8
· (;10↑;30)) < 𝑚 → (∀𝑜 ∈ Odd ((7 < 𝑜 ∧ 𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ) → (𝑛 ≤ (;10↑;27) → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))))) |
| 84 | 83 | imp32 418 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ ∧ ((8
· (;10↑;30)) < 𝑚 ∧ ∀𝑜 ∈ Odd ((7 < 𝑜 ∧ 𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ))) → (𝑛 ≤ (;10↑;27) → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))) |
| 85 | 84 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑚 ∈
ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑜 ∈ Odd ((7 < 𝑜 ∧ 𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd )) → (𝑛 ≤ (;10↑;27) → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))) |
| 86 | 12, 85 | ax-mp 5 |
. . . 4
⊢ (𝑛 ≤ (;10↑;27) → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
| 87 | | tgoldbachgtALTV 47799 |
. . . . 5
⊢
∃𝑚 ∈
ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑜 ∈ Odd (𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd )) |
| 88 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑜 = 𝑛 → (𝑚 < 𝑜 ↔ 𝑚 < 𝑛)) |
| 89 | 88, 16 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑜 = 𝑛 → ((𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) ↔ (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
| 90 | 89 | rspcv 3618 |
. . . . . . . . 9
⊢ (𝑛 ∈ Odd →
(∀𝑜 ∈ Odd
(𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) → (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
| 91 | | lelttr 11351 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ ℝ ∧ (;10↑;27) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑚 ≤ (;10↑;27) ∧ (;10↑;27) < 𝑛) → 𝑚 < 𝑛)) |
| 92 | 61, 57, 66, 91 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → ((𝑚 ≤ (;10↑;27) ∧ (;10↑;27) < 𝑛) → 𝑚 < 𝑛)) |
| 93 | 92 | expcomd 416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → ((;10↑;27) < 𝑛 → (𝑚 ≤ (;10↑;27) → 𝑚 < 𝑛))) |
| 94 | 93 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ Odd → (𝑚 ∈ ℕ → ((;10↑;27) < 𝑛 → (𝑚 ≤ (;10↑;27) → 𝑚 < 𝑛)))) |
| 95 | 94 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ Odd → ((;10↑;27) < 𝑛 → (𝑚 ∈ ℕ → (𝑚 ≤ (;10↑;27) → 𝑚 < 𝑛)))) |
| 96 | 95 | imp43 427 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ Odd ∧ (;10↑;27) < 𝑛) ∧ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27))) → 𝑚 < 𝑛) |
| 97 | | pm2.27 42 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 < 𝑛 → ((𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd
)) |
| 98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ Odd ∧ (;10↑;27) < 𝑛) ∧ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27))) → ((𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd
)) |
| 99 | 98 | a1dd 50 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ Odd ∧ (;10↑;27) < 𝑛) ∧ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27))) → ((𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
| 100 | 99 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ Odd ∧ (;10↑;27) < 𝑛) → ((𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27)) → ((𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))) |
| 101 | 100 | com23 86 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ Odd ∧ (;10↑;27) < 𝑛) → ((𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ((𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27)) → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))) |
| 102 | 101 | ex 412 |
. . . . . . . . . 10
⊢ (𝑛 ∈ Odd → ((;10↑;27) < 𝑛 → ((𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ((𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27)) → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))))) |
| 103 | 102 | com23 86 |
. . . . . . . . 9
⊢ (𝑛 ∈ Odd → ((𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ((;10↑;27) < 𝑛 → ((𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27)) → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))))) |
| 104 | 90, 103 | syld 47 |
. . . . . . . 8
⊢ (𝑛 ∈ Odd →
(∀𝑜 ∈ Odd
(𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) → ((;10↑;27) < 𝑛 → ((𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27)) → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))))) |
| 105 | 104 | com14 96 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧ 𝑚 ≤ (;10↑;27)) → (∀𝑜 ∈ Odd (𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) → ((;10↑;27) < 𝑛 → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))))) |
| 106 | 105 | impr 454 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 ≤ (;10↑;27) ∧ ∀𝑜 ∈ Odd (𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ))) → ((;10↑;27) < 𝑛 → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))) |
| 107 | 106 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑚 ∈
ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑜 ∈ Odd (𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd )) → ((;10↑;27) < 𝑛 → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )))) |
| 108 | 87, 107 | ax-mp 5 |
. . . 4
⊢ ((;10↑;27) < 𝑛 → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
| 109 | 86, 108 | jaoi 858 |
. . 3
⊢ ((𝑛 ≤ (;10↑;27) ∨ (;10↑;27) < 𝑛) → (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ))) |
| 110 | 11, 109 | mpcom 38 |
. 2
⊢ (𝑛 ∈ Odd → (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )) |
| 111 | 110 | rgen 3063 |
1
⊢
∀𝑛 ∈ Odd
(7 < 𝑛 → 𝑛 ∈ GoldbachOdd
) |