Step | Hyp | Ref
| Expression |
1 | | 8nn0 12491 |
. . . 4
โข 8 โ
โ0 |
2 | | 8nn 12303 |
. . . 4
โข 8 โ
โ |
3 | 1, 2 | decnncl 12693 |
. . 3
โข ;88 โ โ |
4 | | 10nn 12689 |
. . . 4
โข ;10 โ โ |
5 | | 2nn0 12485 |
. . . . 5
โข 2 โ
โ0 |
6 | | 9nn0 12492 |
. . . . 5
โข 9 โ
โ0 |
7 | 5, 6 | deccl 12688 |
. . . 4
โข ;29 โ
โ0 |
8 | | nnexpcl 14036 |
. . . 4
โข ((;10 โ โ โง ;29 โ โ0) โ
(;10โ;29) โ โ) |
9 | 4, 7, 8 | mp2an 690 |
. . 3
โข (;10โ;29) โ โ |
10 | 3, 9 | nnmulcli 12233 |
. 2
โข (;88 ยท (;10โ;29)) โ โ |
11 | | id 22 |
. . 3
โข ((;88 ยท (;10โ;29)) โ โ โ (;88 ยท (;10โ;29)) โ โ) |
12 | | breq2 5151 |
. . . . 5
โข (๐ = (;88 ยท (;10โ;29)) โ ((8 ยท (;10โ;30)) < ๐ โ (8 ยท (;10โ;30)) < (;88 ยท (;10โ;29)))) |
13 | | breq2 5151 |
. . . . . . . 8
โข (๐ = (;88 ยท (;10โ;29)) โ (๐ < ๐ โ ๐ < (;88 ยท (;10โ;29)))) |
14 | 13 | anbi2d 629 |
. . . . . . 7
โข (๐ = (;88 ยท (;10โ;29)) โ ((7 < ๐ โง ๐ < ๐) โ (7 < ๐ โง ๐ < (;88 ยท (;10โ;29))))) |
15 | 14 | imbi1d 341 |
. . . . . 6
โข (๐ = (;88 ยท (;10โ;29)) โ (((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ) โ ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd ))) |
16 | 15 | ralbidv 3177 |
. . . . 5
โข (๐ = (;88 ยท (;10โ;29)) โ (โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ) โ โ๐ โ Odd ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd ))) |
17 | 12, 16 | anbi12d 631 |
. . . 4
โข (๐ = (;88 ยท (;10โ;29)) โ (((8 ยท (;10โ;30)) < ๐ โง โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd )) โ ((8 ยท
(;10โ;30)) < (;88 ยท (;10โ;29)) โง โ๐ โ Odd ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd )))) |
18 | 17 | adantl 482 |
. . 3
โข (((;88 ยท (;10โ;29)) โ โ โง ๐ = (;88 ยท (;10โ;29))) โ (((8 ยท (;10โ;30)) < ๐ โง โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd )) โ ((8 ยท
(;10โ;30)) < (;88 ยท (;10โ;29)) โง โ๐ โ Odd ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd )))) |
19 | | simplr 767 |
. . . . . . 7
โข ((((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โง (7 < ๐ โง ๐ < (;88 ยท (;10โ;29)))) โ ๐ โ Odd ) |
20 | | simprl 769 |
. . . . . . 7
โข ((((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โง (7 < ๐ โง ๐ < (;88 ยท (;10โ;29)))) โ 7 < ๐) |
21 | | simprr 771 |
. . . . . . 7
โข ((((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โง (7 < ๐ โง ๐ < (;88 ยท (;10โ;29)))) โ ๐ < (;88 ยท (;10โ;29))) |
22 | | tgblthelfgott 46469 |
. . . . . . 7
โข ((๐ โ Odd โง 7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd ) |
23 | 19, 20, 21, 22 | syl3anc 1371 |
. . . . . 6
โข ((((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โง (7 < ๐ โง ๐ < (;88 ยท (;10โ;29)))) โ ๐ โ GoldbachOdd ) |
24 | 23 | ex 413 |
. . . . 5
โข (((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โ ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd )) |
25 | 24 | ralrimiva 3146 |
. . . 4
โข ((;88 ยท (;10โ;29)) โ โ โ โ๐ โ Odd ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd )) |
26 | 2, 9 | nnmulcli 12233 |
. . . . . . 7
โข (8
ยท (;10โ;29)) โ โ |
27 | 26 | nngt0i 12247 |
. . . . . 6
โข 0 < (8
ยท (;10โ;29)) |
28 | 26 | nnrei 12217 |
. . . . . . 7
โข (8
ยท (;10โ;29)) โ โ |
29 | | 3nn0 12486 |
. . . . . . . . . . 11
โข 3 โ
โ0 |
30 | | 0nn0 12483 |
. . . . . . . . . . 11
โข 0 โ
โ0 |
31 | 29, 30 | deccl 12688 |
. . . . . . . . . 10
โข ;30 โ
โ0 |
32 | | nnexpcl 14036 |
. . . . . . . . . 10
โข ((;10 โ โ โง ;30 โ โ0) โ
(;10โ;30) โ โ) |
33 | 4, 31, 32 | mp2an 690 |
. . . . . . . . 9
โข (;10โ;30) โ โ |
34 | 2, 33 | nnmulcli 12233 |
. . . . . . . 8
โข (8
ยท (;10โ;30)) โ โ |
35 | 34 | nnrei 12217 |
. . . . . . 7
โข (8
ยท (;10โ;30)) โ โ |
36 | 28, 35 | ltaddposi 11759 |
. . . . . 6
โข (0 <
(8 ยท (;10โ;29)) โ (8 ยท (;10โ;30)) < ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29)))) |
37 | 27, 36 | mpbi 229 |
. . . . 5
โข (8
ยท (;10โ;30)) < ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29))) |
38 | | dfdec10 12676 |
. . . . . . 7
โข ;88 = ((;10 ยท 8) + 8) |
39 | 38 | oveq1i 7415 |
. . . . . 6
โข (;88 ยท (;10โ;29)) = (((;10 ยท 8) + 8) ยท (;10โ;29)) |
40 | 4, 2 | nnmulcli 12233 |
. . . . . . . 8
โข (;10 ยท 8) โ
โ |
41 | 40 | nncni 12218 |
. . . . . . 7
โข (;10 ยท 8) โ
โ |
42 | | 8cn 12305 |
. . . . . . 7
โข 8 โ
โ |
43 | 9 | nncni 12218 |
. . . . . . 7
โข (;10โ;29) โ โ |
44 | 41, 42, 43 | adddiri 11223 |
. . . . . 6
โข (((;10 ยท 8) + 8) ยท (;10โ;29)) = (((;10 ยท 8) ยท (;10โ;29)) + (8 ยท (;10โ;29))) |
45 | 41, 43 | mulcomi 11218 |
. . . . . . . . 9
โข ((;10 ยท 8) ยท (;10โ;29)) = ((;10โ;29) ยท (;10 ยท 8)) |
46 | 4 | nncni 12218 |
. . . . . . . . . 10
โข ;10 โ โ |
47 | 43, 46, 42 | mulassi 11221 |
. . . . . . . . 9
โข (((;10โ;29) ยท ;10) ยท 8) = ((;10โ;29) ยท (;10 ยท 8)) |
48 | | nncn 12216 |
. . . . . . . . . . . . 13
โข (;10 โ โ โ ;10 โ โ) |
49 | 7 | a1i 11 |
. . . . . . . . . . . . 13
โข (;10 โ โ โ ;29 โ
โ0) |
50 | 48, 49 | expp1d 14108 |
. . . . . . . . . . . 12
โข (;10 โ โ โ (;10โ(;29 + 1)) = ((;10โ;29) ยท ;10)) |
51 | 4, 50 | ax-mp 5 |
. . . . . . . . . . 11
โข (;10โ(;29 + 1)) = ((;10โ;29) ยท ;10) |
52 | 51 | eqcomi 2741 |
. . . . . . . . . 10
โข ((;10โ;29) ยท ;10) = (;10โ(;29 + 1)) |
53 | 52 | oveq1i 7415 |
. . . . . . . . 9
โข (((;10โ;29) ยท ;10) ยท 8) = ((;10โ(;29 + 1)) ยท 8) |
54 | 45, 47, 53 | 3eqtr2i 2766 |
. . . . . . . 8
โข ((;10 ยท 8) ยท (;10โ;29)) = ((;10โ(;29 + 1)) ยท 8) |
55 | 54 | oveq1i 7415 |
. . . . . . 7
โข (((;10 ยท 8) ยท (;10โ;29)) + (8 ยท (;10โ;29))) = (((;10โ(;29 + 1)) ยท 8) + (8 ยท (;10โ;29))) |
56 | | 2p1e3 12350 |
. . . . . . . . . . 11
โข (2 + 1) =
3 |
57 | | eqid 2732 |
. . . . . . . . . . 11
โข ;29 = ;29 |
58 | 5, 56, 57 | decsucc 12714 |
. . . . . . . . . 10
โข (;29 + 1) = ;30 |
59 | 58 | oveq2i 7416 |
. . . . . . . . 9
โข (;10โ(;29 + 1)) = (;10โ;30) |
60 | 59 | oveq1i 7415 |
. . . . . . . 8
โข ((;10โ(;29 + 1)) ยท 8) = ((;10โ;30) ยท 8) |
61 | 60 | oveq1i 7415 |
. . . . . . 7
โข (((;10โ(;29 + 1)) ยท 8) + (8 ยท (;10โ;29))) = (((;10โ;30) ยท 8) + (8 ยท (;10โ;29))) |
62 | 33 | nncni 12218 |
. . . . . . . 8
โข (;10โ;30) โ โ |
63 | | mulcom 11192 |
. . . . . . . . 9
โข (((;10โ;30) โ โ โง 8 โ โ) โ
((;10โ;30) ยท 8) = (8 ยท (;10โ;30))) |
64 | 63 | oveq1d 7420 |
. . . . . . . 8
โข (((;10โ;30) โ โ โง 8 โ โ) โ
(((;10โ;30) ยท 8) + (8 ยท (;10โ;29))) = ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29)))) |
65 | 62, 42, 64 | mp2an 690 |
. . . . . . 7
โข (((;10โ;30) ยท 8) + (8 ยท (;10โ;29))) = ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29))) |
66 | 55, 61, 65 | 3eqtri 2764 |
. . . . . 6
โข (((;10 ยท 8) ยท (;10โ;29)) + (8 ยท (;10โ;29))) = ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29))) |
67 | 39, 44, 66 | 3eqtri 2764 |
. . . . 5
โข (;88 ยท (;10โ;29)) = ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29))) |
68 | 37, 67 | breqtrri 5174 |
. . . 4
โข (8
ยท (;10โ;30)) < (;88 ยท (;10โ;29)) |
69 | 25, 68 | jctil 520 |
. . 3
โข ((;88 ยท (;10โ;29)) โ โ โ ((8 ยท (;10โ;30)) < (;88 ยท (;10โ;29)) โง โ๐ โ Odd ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd ))) |
70 | 11, 18, 69 | rspcedvd 3614 |
. 2
โข ((;88 ยท (;10โ;29)) โ โ โ โ๐ โ โ ((8 ยท (;10โ;30)) < ๐ โง โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ))) |
71 | 10, 70 | ax-mp 5 |
1
โข
โ๐ โ
โ ((8 ยท (;10โ;30)) < ๐ โง โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd )) |