Step | Hyp | Ref
| Expression |
1 | | 8nn0 12441 |
. . . 4
โข 8 โ
โ0 |
2 | | 8nn 12253 |
. . . 4
โข 8 โ
โ |
3 | 1, 2 | decnncl 12643 |
. . 3
โข ;88 โ โ |
4 | | 10nn 12639 |
. . . 4
โข ;10 โ โ |
5 | | 2nn0 12435 |
. . . . 5
โข 2 โ
โ0 |
6 | | 9nn0 12442 |
. . . . 5
โข 9 โ
โ0 |
7 | 5, 6 | deccl 12638 |
. . . 4
โข ;29 โ
โ0 |
8 | | nnexpcl 13986 |
. . . 4
โข ((;10 โ โ โง ;29 โ โ0) โ
(;10โ;29) โ โ) |
9 | 4, 7, 8 | mp2an 691 |
. . 3
โข (;10โ;29) โ โ |
10 | 3, 9 | nnmulcli 12183 |
. 2
โข (;88 ยท (;10โ;29)) โ โ |
11 | | id 22 |
. . 3
โข ((;88 ยท (;10โ;29)) โ โ โ (;88 ยท (;10โ;29)) โ โ) |
12 | | breq2 5110 |
. . . . 5
โข (๐ = (;88 ยท (;10โ;29)) โ ((8 ยท (;10โ;30)) < ๐ โ (8 ยท (;10โ;30)) < (;88 ยท (;10โ;29)))) |
13 | | breq2 5110 |
. . . . . . . 8
โข (๐ = (;88 ยท (;10โ;29)) โ (๐ < ๐ โ ๐ < (;88 ยท (;10โ;29)))) |
14 | 13 | anbi2d 630 |
. . . . . . 7
โข (๐ = (;88 ยท (;10โ;29)) โ ((7 < ๐ โง ๐ < ๐) โ (7 < ๐ โง ๐ < (;88 ยท (;10โ;29))))) |
15 | 14 | imbi1d 342 |
. . . . . 6
โข (๐ = (;88 ยท (;10โ;29)) โ (((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ) โ ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd ))) |
16 | 15 | ralbidv 3171 |
. . . . 5
โข (๐ = (;88 ยท (;10โ;29)) โ (โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ) โ โ๐ โ Odd ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd ))) |
17 | 12, 16 | anbi12d 632 |
. . . 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 483 |
. . 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 768 |
. . . . . . 7
โข ((((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โง (7 < ๐ โง ๐ < (;88 ยท (;10โ;29)))) โ ๐ โ Odd ) |
20 | | simprl 770 |
. . . . . . 7
โข ((((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โง (7 < ๐ โง ๐ < (;88 ยท (;10โ;29)))) โ 7 < ๐) |
21 | | simprr 772 |
. . . . . . 7
โข ((((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โง (7 < ๐ โง ๐ < (;88 ยท (;10โ;29)))) โ ๐ < (;88 ยท (;10โ;29))) |
22 | | tgblthelfgott 46093 |
. . . . . . 7
โข ((๐ โ Odd โง 7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd ) |
23 | 19, 20, 21, 22 | syl3anc 1372 |
. . . . . 6
โข ((((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โง (7 < ๐ โง ๐ < (;88 ยท (;10โ;29)))) โ ๐ โ GoldbachOdd ) |
24 | 23 | ex 414 |
. . . . 5
โข (((;88 ยท (;10โ;29)) โ โ โง ๐ โ Odd ) โ ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd )) |
25 | 24 | ralrimiva 3140 |
. . . 4
โข ((;88 ยท (;10โ;29)) โ โ โ โ๐ โ Odd ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd )) |
26 | 2, 9 | nnmulcli 12183 |
. . . . . . 7
โข (8
ยท (;10โ;29)) โ โ |
27 | 26 | nngt0i 12197 |
. . . . . 6
โข 0 < (8
ยท (;10โ;29)) |
28 | 26 | nnrei 12167 |
. . . . . . 7
โข (8
ยท (;10โ;29)) โ โ |
29 | | 3nn0 12436 |
. . . . . . . . . . 11
โข 3 โ
โ0 |
30 | | 0nn0 12433 |
. . . . . . . . . . 11
โข 0 โ
โ0 |
31 | 29, 30 | deccl 12638 |
. . . . . . . . . 10
โข ;30 โ
โ0 |
32 | | nnexpcl 13986 |
. . . . . . . . . 10
โข ((;10 โ โ โง ;30 โ โ0) โ
(;10โ;30) โ โ) |
33 | 4, 31, 32 | mp2an 691 |
. . . . . . . . 9
โข (;10โ;30) โ โ |
34 | 2, 33 | nnmulcli 12183 |
. . . . . . . 8
โข (8
ยท (;10โ;30)) โ โ |
35 | 34 | nnrei 12167 |
. . . . . . 7
โข (8
ยท (;10โ;30)) โ โ |
36 | 28, 35 | ltaddposi 11709 |
. . . . . 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 12626 |
. . . . . . 7
โข ;88 = ((;10 ยท 8) + 8) |
39 | 38 | oveq1i 7368 |
. . . . . 6
โข (;88 ยท (;10โ;29)) = (((;10 ยท 8) + 8) ยท (;10โ;29)) |
40 | 4, 2 | nnmulcli 12183 |
. . . . . . . 8
โข (;10 ยท 8) โ
โ |
41 | 40 | nncni 12168 |
. . . . . . 7
โข (;10 ยท 8) โ
โ |
42 | | 8cn 12255 |
. . . . . . 7
โข 8 โ
โ |
43 | 9 | nncni 12168 |
. . . . . . 7
โข (;10โ;29) โ โ |
44 | 41, 42, 43 | adddiri 11173 |
. . . . . 6
โข (((;10 ยท 8) + 8) ยท (;10โ;29)) = (((;10 ยท 8) ยท (;10โ;29)) + (8 ยท (;10โ;29))) |
45 | 41, 43 | mulcomi 11168 |
. . . . . . . . 9
โข ((;10 ยท 8) ยท (;10โ;29)) = ((;10โ;29) ยท (;10 ยท 8)) |
46 | 4 | nncni 12168 |
. . . . . . . . . 10
โข ;10 โ โ |
47 | 43, 46, 42 | mulassi 11171 |
. . . . . . . . 9
โข (((;10โ;29) ยท ;10) ยท 8) = ((;10โ;29) ยท (;10 ยท 8)) |
48 | | nncn 12166 |
. . . . . . . . . . . . 13
โข (;10 โ โ โ ;10 โ โ) |
49 | 7 | a1i 11 |
. . . . . . . . . . . . 13
โข (;10 โ โ โ ;29 โ
โ0) |
50 | 48, 49 | expp1d 14058 |
. . . . . . . . . . . 12
โข (;10 โ โ โ (;10โ(;29 + 1)) = ((;10โ;29) ยท ;10)) |
51 | 4, 50 | ax-mp 5 |
. . . . . . . . . . 11
โข (;10โ(;29 + 1)) = ((;10โ;29) ยท ;10) |
52 | 51 | eqcomi 2742 |
. . . . . . . . . 10
โข ((;10โ;29) ยท ;10) = (;10โ(;29 + 1)) |
53 | 52 | oveq1i 7368 |
. . . . . . . . 9
โข (((;10โ;29) ยท ;10) ยท 8) = ((;10โ(;29 + 1)) ยท 8) |
54 | 45, 47, 53 | 3eqtr2i 2767 |
. . . . . . . 8
โข ((;10 ยท 8) ยท (;10โ;29)) = ((;10โ(;29 + 1)) ยท 8) |
55 | 54 | oveq1i 7368 |
. . . . . . 7
โข (((;10 ยท 8) ยท (;10โ;29)) + (8 ยท (;10โ;29))) = (((;10โ(;29 + 1)) ยท 8) + (8 ยท (;10โ;29))) |
56 | | 2p1e3 12300 |
. . . . . . . . . . 11
โข (2 + 1) =
3 |
57 | | eqid 2733 |
. . . . . . . . . . 11
โข ;29 = ;29 |
58 | 5, 56, 57 | decsucc 12664 |
. . . . . . . . . 10
โข (;29 + 1) = ;30 |
59 | 58 | oveq2i 7369 |
. . . . . . . . 9
โข (;10โ(;29 + 1)) = (;10โ;30) |
60 | 59 | oveq1i 7368 |
. . . . . . . 8
โข ((;10โ(;29 + 1)) ยท 8) = ((;10โ;30) ยท 8) |
61 | 60 | oveq1i 7368 |
. . . . . . 7
โข (((;10โ(;29 + 1)) ยท 8) + (8 ยท (;10โ;29))) = (((;10โ;30) ยท 8) + (8 ยท (;10โ;29))) |
62 | 33 | nncni 12168 |
. . . . . . . 8
โข (;10โ;30) โ โ |
63 | | mulcom 11142 |
. . . . . . . . 9
โข (((;10โ;30) โ โ โง 8 โ โ) โ
((;10โ;30) ยท 8) = (8 ยท (;10โ;30))) |
64 | 63 | oveq1d 7373 |
. . . . . . . 8
โข (((;10โ;30) โ โ โง 8 โ โ) โ
(((;10โ;30) ยท 8) + (8 ยท (;10โ;29))) = ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29)))) |
65 | 62, 42, 64 | mp2an 691 |
. . . . . . 7
โข (((;10โ;30) ยท 8) + (8 ยท (;10โ;29))) = ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29))) |
66 | 55, 61, 65 | 3eqtri 2765 |
. . . . . 6
โข (((;10 ยท 8) ยท (;10โ;29)) + (8 ยท (;10โ;29))) = ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29))) |
67 | 39, 44, 66 | 3eqtri 2765 |
. . . . 5
โข (;88 ยท (;10โ;29)) = ((8 ยท (;10โ;30)) + (8 ยท (;10โ;29))) |
68 | 37, 67 | breqtrri 5133 |
. . . 4
โข (8
ยท (;10โ;30)) < (;88 ยท (;10โ;29)) |
69 | 25, 68 | jctil 521 |
. . 3
โข ((;88 ยท (;10โ;29)) โ โ โ ((8 ยท (;10โ;30)) < (;88 ยท (;10โ;29)) โง โ๐ โ Odd ((7 < ๐ โง ๐ < (;88 ยท (;10โ;29))) โ ๐ โ GoldbachOdd ))) |
70 | 11, 18, 69 | rspcedvd 3582 |
. 2
โข ((;88 ยท (;10โ;29)) โ โ โ โ๐ โ โ ((8 ยท (;10โ;30)) < ๐ โง โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd ))) |
71 | 10, 70 | ax-mp 5 |
1
โข
โ๐ โ
โ ((8 ยท (;10โ;30)) < ๐ โง โ๐ โ Odd ((7 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachOdd )) |