Step | Hyp | Ref
| Expression |
1 | | quart1.p |
. . 3
โข (๐ โ ๐ = (๐ต โ ((3 / 8) ยท (๐ดโ2)))) |
2 | | quart1.b |
. . . 4
โข (๐ โ ๐ต โ โ) |
3 | | 3cn 12241 |
. . . . . 6
โข 3 โ
โ |
4 | | 8cn 12257 |
. . . . . 6
โข 8 โ
โ |
5 | | 8nn 12255 |
. . . . . . 7
โข 8 โ
โ |
6 | 5 | nnne0i 12200 |
. . . . . 6
โข 8 โ
0 |
7 | 3, 4, 6 | divcli 11904 |
. . . . 5
โข (3 / 8)
โ โ |
8 | | quart1.a |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
9 | 8 | sqcld 14056 |
. . . . 5
โข (๐ โ (๐ดโ2) โ โ) |
10 | | mulcl 11142 |
. . . . 5
โข (((3 / 8)
โ โ โง (๐ดโ2) โ โ) โ ((3 / 8)
ยท (๐ดโ2)) โ
โ) |
11 | 7, 9, 10 | sylancr 588 |
. . . 4
โข (๐ โ ((3 / 8) ยท (๐ดโ2)) โ
โ) |
12 | 2, 11 | subcld 11519 |
. . 3
โข (๐ โ (๐ต โ ((3 / 8) ยท (๐ดโ2))) โ
โ) |
13 | 1, 12 | eqeltrd 2838 |
. 2
โข (๐ โ ๐ โ โ) |
14 | | quart1.q |
. . 3
โข (๐ โ ๐ = ((๐ถ โ ((๐ด ยท ๐ต) / 2)) + ((๐ดโ3) / 8))) |
15 | | quart1.c |
. . . . 5
โข (๐ โ ๐ถ โ โ) |
16 | 8, 2 | mulcld 11182 |
. . . . . 6
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
17 | 16 | halfcld 12405 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ต) / 2) โ โ) |
18 | 15, 17 | subcld 11519 |
. . . 4
โข (๐ โ (๐ถ โ ((๐ด ยท ๐ต) / 2)) โ โ) |
19 | | 3nn0 12438 |
. . . . . 6
โข 3 โ
โ0 |
20 | | expcl 13992 |
. . . . . 6
โข ((๐ด โ โ โง 3 โ
โ0) โ (๐ดโ3) โ โ) |
21 | 8, 19, 20 | sylancl 587 |
. . . . 5
โข (๐ โ (๐ดโ3) โ โ) |
22 | 4 | a1i 11 |
. . . . 5
โข (๐ โ 8 โ
โ) |
23 | 6 | a1i 11 |
. . . . 5
โข (๐ โ 8 โ 0) |
24 | 21, 22, 23 | divcld 11938 |
. . . 4
โข (๐ โ ((๐ดโ3) / 8) โ
โ) |
25 | 18, 24 | addcld 11181 |
. . 3
โข (๐ โ ((๐ถ โ ((๐ด ยท ๐ต) / 2)) + ((๐ดโ3) / 8)) โ
โ) |
26 | 14, 25 | eqeltrd 2838 |
. 2
โข (๐ โ ๐ โ โ) |
27 | | quart1.r |
. . 3
โข (๐ โ ๐
= ((๐ท โ ((๐ถ ยท ๐ด) / 4)) + ((((๐ดโ2) ยท ๐ต) / ;16) โ ((3 / ;;256)
ยท (๐ดโ4))))) |
28 | | quart1.d |
. . . . 5
โข (๐ โ ๐ท โ โ) |
29 | 15, 8 | mulcld 11182 |
. . . . . 6
โข (๐ โ (๐ถ ยท ๐ด) โ โ) |
30 | | 4cn 12245 |
. . . . . . 7
โข 4 โ
โ |
31 | 30 | a1i 11 |
. . . . . 6
โข (๐ โ 4 โ
โ) |
32 | | 4ne0 12268 |
. . . . . . 7
โข 4 โ
0 |
33 | 32 | a1i 11 |
. . . . . 6
โข (๐ โ 4 โ 0) |
34 | 29, 31, 33 | divcld 11938 |
. . . . 5
โข (๐ โ ((๐ถ ยท ๐ด) / 4) โ โ) |
35 | 28, 34 | subcld 11519 |
. . . 4
โข (๐ โ (๐ท โ ((๐ถ ยท ๐ด) / 4)) โ โ) |
36 | 9, 2 | mulcld 11182 |
. . . . . 6
โข (๐ โ ((๐ดโ2) ยท ๐ต) โ โ) |
37 | | 1nn0 12436 |
. . . . . . . . 9
โข 1 โ
โ0 |
38 | | 6nn 12249 |
. . . . . . . . 9
โข 6 โ
โ |
39 | 37, 38 | decnncl 12645 |
. . . . . . . 8
โข ;16 โ โ |
40 | 39 | nncni 12170 |
. . . . . . 7
โข ;16 โ โ |
41 | 40 | a1i 11 |
. . . . . 6
โข (๐ โ ;16 โ โ) |
42 | 39 | nnne0i 12200 |
. . . . . . 7
โข ;16 โ 0 |
43 | 42 | a1i 11 |
. . . . . 6
โข (๐ โ ;16 โ 0) |
44 | 36, 41, 43 | divcld 11938 |
. . . . 5
โข (๐ โ (((๐ดโ2) ยท ๐ต) / ;16) โ โ) |
45 | | 2nn0 12437 |
. . . . . . . . . 10
โข 2 โ
โ0 |
46 | | 5nn0 12440 |
. . . . . . . . . 10
โข 5 โ
โ0 |
47 | 45, 46 | deccl 12640 |
. . . . . . . . 9
โข ;25 โ
โ0 |
48 | 47, 38 | decnncl 12645 |
. . . . . . . 8
โข ;;256 โ โ |
49 | 48 | nncni 12170 |
. . . . . . 7
โข ;;256 โ โ |
50 | 48 | nnne0i 12200 |
. . . . . . 7
โข ;;256 โ 0 |
51 | 3, 49, 50 | divcli 11904 |
. . . . . 6
โข (3 /
;;256) โ โ |
52 | | 4nn0 12439 |
. . . . . . 7
โข 4 โ
โ0 |
53 | | expcl 13992 |
. . . . . . 7
โข ((๐ด โ โ โง 4 โ
โ0) โ (๐ดโ4) โ โ) |
54 | 8, 52, 53 | sylancl 587 |
. . . . . 6
โข (๐ โ (๐ดโ4) โ โ) |
55 | | mulcl 11142 |
. . . . . 6
โข (((3 /
;;256) โ โ โง (๐ดโ4) โ โ) โ ((3 / ;;256) ยท (๐ดโ4)) โ โ) |
56 | 51, 54, 55 | sylancr 588 |
. . . . 5
โข (๐ โ ((3 / ;;256)
ยท (๐ดโ4)) โ
โ) |
57 | 44, 56 | subcld 11519 |
. . . 4
โข (๐ โ ((((๐ดโ2) ยท ๐ต) / ;16) โ ((3 / ;;256)
ยท (๐ดโ4)))
โ โ) |
58 | 35, 57 | addcld 11181 |
. . 3
โข (๐ โ ((๐ท โ ((๐ถ ยท ๐ด) / 4)) + ((((๐ดโ2) ยท ๐ต) / ;16) โ ((3 / ;;256)
ยท (๐ดโ4))))
โ โ) |
59 | 27, 58 | eqeltrd 2838 |
. 2
โข (๐ โ ๐
โ โ) |
60 | 13, 26, 59 | 3jca 1129 |
1
โข (๐ โ (๐ โ โ โง ๐ โ โ โง ๐
โ โ)) |