Step | Hyp | Ref
| Expression |
1 | | oddz 45897 |
. . . . 5
โข (๐ โ Odd โ ๐ โ
โค) |
2 | 1 | zred 12614 |
. . . 4
โข (๐ โ Odd โ ๐ โ
โ) |
3 | | 10re 12644 |
. . . . 5
โข ;10 โ โ |
4 | | 2nn0 12437 |
. . . . . . 7
โข 2 โ
โ0 |
5 | | 7nn 12252 |
. . . . . . 7
โข 7 โ
โ |
6 | 4, 5 | decnncl 12645 |
. . . . . 6
โข ;27 โ โ |
7 | 6 | nnnn0i 12428 |
. . . . 5
โข ;27 โ
โ0 |
8 | | reexpcl 13991 |
. . . . 5
โข ((;10 โ โ โง ;27 โ โ0) โ
(;10โ;27) โ โ) |
9 | 3, 7, 8 | mp2an 691 |
. . . 4
โข (;10โ;27) โ โ |
10 | | lelttric 11269 |
. . . 4
โข ((๐ โ โ โง (;10โ;27) โ โ) โ (๐ โค (;10โ;27) โจ (;10โ;27) < ๐)) |
11 | 2, 9, 10 | sylancl 587 |
. . 3
โข (๐ โ Odd โ (๐ โค (;10โ;27) โจ (;10โ;27) < ๐)) |
12 | | tgoldbachlt 46082 |
. . . . 5
โข
โ๐ โ
โ ((8 ยท (;10โ;30)) < ๐ โง โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd )) |
13 | | breq2 5114 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (7 < ๐ โ 7 < ๐)) |
14 | | breq1 5113 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ < ๐ โ ๐ < ๐)) |
15 | 13, 14 | anbi12d 632 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((7 < ๐ โง ๐ < ๐) โ (7 < ๐ โง ๐ < ๐))) |
16 | | eleq1w 2821 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ GoldbachOdd โ ๐ โ GoldbachOdd )) |
17 | 15, 16 | imbi12d 345 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ) โ ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ))) |
18 | 17 | rspcv 3580 |
. . . . . . . . . 10
โข (๐ โ Odd โ
(โ๐ โ Odd ((7
< ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ) โ ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ))) |
19 | 9 | recni 11176 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (;10โ;27) โ โ |
20 | 19 | mulid2i 11167 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (1
ยท (;10โ;27)) = (;10โ;27) |
21 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 1 โ
โ |
22 | | 8re 12256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 8 โ
โ |
23 | 21, 22 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (1 โ
โ โง 8 โ โ) |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ Odd โง ๐ โ โ) โ (1
โ โ โง 8 โ โ)) |
25 | | 0le1 11685 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 0 โค
1 |
26 | | 1lt8 12358 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 1 <
8 |
27 | 25, 26 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (0 โค 1
โง 1 < 8) |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ Odd โง ๐ โ โ) โ (0 โค
1 โง 1 < 8)) |
29 | | 3nn 12239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข 3 โ
โ |
30 | 29 | decnncl2 12649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ;30 โ โ |
31 | 30 | nnnn0i 12428 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ;30 โ
โ0 |
32 | | reexpcl 13991 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((;10 โ โ โง ;30 โ โ0) โ
(;10โ;30) โ โ) |
33 | 3, 31, 32 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (;10โ;30) โ โ |
34 | 9, 33 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((;10โ;27) โ โ โง (;10โ;30) โ โ) |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ Odd โง ๐ โ โ) โ ((;10โ;27) โ โ โง (;10โ;30) โ โ)) |
36 | | 10nn0 12643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ;10 โ
โ0 |
37 | 36, 7 | nn0expcli 14001 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (;10โ;27) โ โ0 |
38 | 37 | nn0ge0i 12447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 0 โค
(;10โ;27) |
39 | 6 | nnzi 12534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ;27 โ โค |
40 | 30 | nnzi 12534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ;30 โ โค |
41 | 3, 39, 40 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (;10 โ โ โง ;27 โ โค โง ;30 โ โค) |
42 | | 1lt10 12764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข 1 <
;10 |
43 | | 3nn0 12438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข 3 โ
โ0 |
44 | | 7nn0 12442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข 7 โ
โ0 |
45 | | 0nn0 12435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข 0 โ
โ0 |
46 | | 7lt10 12758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข 7 <
;10 |
47 | | 2lt3 12332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข 2 <
3 |
48 | 4, 43, 44, 45, 46, 47 | decltc 12654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ;27 < ;30 |
49 | 42, 48 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (1 <
;10 โง ;27 < ;30) |
50 | | ltexp2a 14078 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((;10 โ โ โง ;27 โ โค โง ;30 โ โค) โง (1 < ;10 โง ;27 < ;30)) โ (;10โ;27) < (;10โ;30)) |
51 | 41, 49, 50 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (;10โ;27) < (;10โ;30) |
52 | 38, 51 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (0 โค
(;10โ;27) โง (;10โ;27) < (;10โ;30)) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ Odd โง ๐ โ โ) โ (0 โค
(;10โ;27) โง (;10โ;27) < (;10โ;30))) |
54 | | ltmul12a 12018 |
. . . . . . . . . . . . . . . . . . . . . . 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 838 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ Odd โง ๐ โ โ) โ (1
ยท (;10โ;27)) < (8 ยท (;10โ;30))) |
56 | 20, 55 | eqbrtrrid 5146 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ Odd โง ๐ โ โ) โ (;10โ;27) < (8 ยท (;10โ;30))) |
57 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ Odd โง ๐ โ โ) โ (;10โ;27) โ โ) |
58 | 22, 33 | remulcli 11178 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (8
ยท (;10โ;30)) โ โ |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ Odd โง ๐ โ โ) โ (8
ยท (;10โ;30)) โ โ) |
60 | | nnre 12167 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
61 | 60 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ Odd โง ๐ โ โ) โ ๐ โ
โ) |
62 | | lttr 11238 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((;10โ;27) โ โ โง (8 ยท (;10โ;30)) โ โ โง ๐ โ โ) โ (((;10โ;27) < (8 ยท (;10โ;30)) โง (8 ยท (;10โ;30)) < ๐) โ (;10โ;27) < ๐)) |
63 | 57, 59, 61, 62 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ Odd โง ๐ โ โ) โ (((;10โ;27) < (8 ยท (;10โ;30)) โง (8 ยท (;10โ;30)) < ๐) โ (;10โ;27) < ๐)) |
64 | 56, 63 | mpand 694 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ Odd โง ๐ โ โ) โ ((8
ยท (;10โ;30)) < ๐ โ (;10โ;27) < ๐)) |
65 | 64 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ Odd โง ๐ โ โ) โง (8
ยท (;10โ;30)) < ๐) โ (;10โ;27) < ๐) |
66 | 2 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ Odd โง ๐ โ โ) โ ๐ โ
โ) |
67 | 66, 57, 61 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ Odd โง ๐ โ โ) โ (๐ โ โ โง (;10โ;27) โ โ โง ๐ โ โ)) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ Odd โง ๐ โ โ) โง (8
ยท (;10โ;30)) < ๐) โ (๐ โ โ โง (;10โ;27) โ โ โง ๐ โ โ)) |
69 | | lelttr 11252 |
. . . . . . . . . . . . . . . . . . . 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 693 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ Odd โง ๐ โ โ) โง (8
ยท (;10โ;30)) < ๐) โ (๐ โค (;10โ;27) โ ๐ < ๐)) |
72 | 71 | imp 408 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ Odd โง ๐ โ โ) โง (8
ยท (;10โ;30)) < ๐) โง ๐ โค (;10โ;27)) โ ๐ < ๐) |
73 | 72 | anim1i 616 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โ Odd
โง ๐ โ โ)
โง (8 ยท (;10โ;30)) < ๐) โง ๐ โค (;10โ;27)) โง 7 < ๐) โ (๐ < ๐ โง 7 < ๐)) |
74 | 73 | ancomd 463 |
. . . . . . . . . . . . . . 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 414 |
. . . . . . . . . . . . 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 436 |
. . . . . . . . . . 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 420 |
. . . . . 6
โข ((๐ โ โ โง ((8
ยท (;10โ;30)) < ๐ โง โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ))) โ (๐ โค (;10โ;27) โ (๐ โ Odd โ (7 < ๐ โ ๐ โ GoldbachOdd )))) |
85 | 84 | rexlimiva 3145 |
. . . . 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 46078 |
. . . . 5
โข
โ๐ โ
โ (๐ โค (;10โ;27) โง โ๐ โ Odd (๐ < ๐ โ ๐ โ GoldbachOdd )) |
88 | | breq2 5114 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ < ๐ โ ๐ < ๐)) |
89 | 88, 16 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ < ๐ โ ๐ โ GoldbachOdd ) โ (๐ < ๐ โ ๐ โ GoldbachOdd ))) |
90 | 89 | rspcv 3580 |
. . . . . . . . 9
โข (๐ โ Odd โ
(โ๐ โ Odd
(๐ < ๐ โ ๐ โ GoldbachOdd ) โ (๐ < ๐ โ ๐ โ GoldbachOdd ))) |
91 | | lelttr 11252 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง (;10โ;27) โ โ โง ๐ โ โ) โ ((๐ โค (;10โ;27) โง (;10โ;27) < ๐) โ ๐ < ๐)) |
92 | 61, 57, 66, 91 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ Odd โง ๐ โ โ) โ ((๐ โค (;10โ;27) โง (;10โ;27) < ๐) โ ๐ < ๐)) |
93 | 92 | expcomd 418 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ Odd โง ๐ โ โ) โ ((;10โ;27) < ๐ โ (๐ โค (;10โ;27) โ ๐ < ๐))) |
94 | 93 | ex 414 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ Odd โ (๐ โ โ โ ((;10โ;27) < ๐ โ (๐ โค (;10โ;27) โ ๐ < ๐)))) |
95 | 94 | com23 86 |
. . . . . . . . . . . . . . . 16
โข (๐ โ Odd โ ((;10โ;27) < ๐ โ (๐ โ โ โ (๐ โค (;10โ;27) โ ๐ < ๐)))) |
96 | 95 | imp43 429 |
. . . . . . . . . . . . . . 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 414 |
. . . . . . . . . . . 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 414 |
. . . . . . . . . 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 456 |
. . . . . 6
โข ((๐ โ โ โง (๐ โค (;10โ;27) โง โ๐ โ Odd (๐ < ๐ โ ๐ โ GoldbachOdd ))) โ ((;10โ;27) < ๐ โ (๐ โ Odd โ (7 < ๐ โ ๐ โ GoldbachOdd )))) |
107 | 106 | rexlimiva 3145 |
. . . . 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 856 |
. . 3
โข ((๐ โค (;10โ;27) โจ (;10โ;27) < ๐) โ (๐ โ Odd โ (7 < ๐ โ ๐ โ GoldbachOdd ))) |
110 | 11, 109 | mpcom 38 |
. 2
โข (๐ โ Odd โ (7 < ๐ โ ๐ โ GoldbachOdd )) |
111 | 110 | rgen 3067 |
1
โข
โ๐ โ Odd
(7 < ๐ โ ๐ โ GoldbachOdd
) |