Step | Hyp | Ref
| Expression |
1 | | 4sq.m |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ
(โคโฅโ2)) |
2 | | eluz2nn 12816 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
4 | 3 | nnred 12175 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
5 | 4 | resqcld 14037 |
. . . . . . . . . 10
โข (๐ โ (๐โ2) โ โ) |
6 | 5 | rehalfcld 12407 |
. . . . . . . . 9
โข (๐ โ ((๐โ2) / 2) โ
โ) |
7 | 6 | rehalfcld 12407 |
. . . . . . . 8
โข (๐ โ (((๐โ2) / 2) / 2) โ
โ) |
8 | 7 | recnd 11190 |
. . . . . . 7
โข (๐ โ (((๐โ2) / 2) / 2) โ
โ) |
9 | | 4sq.a |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โค) |
10 | | 4sq.e |
. . . . . . . . . . . 12
โข ๐ธ = (((๐ด + (๐ / 2)) mod ๐) โ (๐ / 2)) |
11 | 9, 3, 10 | 4sqlem5 16821 |
. . . . . . . . . . 11
โข (๐ โ (๐ธ โ โค โง ((๐ด โ ๐ธ) / ๐) โ โค)) |
12 | 11 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ ๐ธ โ โค) |
13 | | zsqcl 14041 |
. . . . . . . . . 10
โข (๐ธ โ โค โ (๐ธโ2) โ
โค) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ธโ2) โ โค) |
15 | 14 | zred 12614 |
. . . . . . . 8
โข (๐ โ (๐ธโ2) โ โ) |
16 | 15 | recnd 11190 |
. . . . . . 7
โข (๐ โ (๐ธโ2) โ โ) |
17 | | 4sq.b |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โค) |
18 | | 4sq.f |
. . . . . . . . . . . 12
โข ๐น = (((๐ต + (๐ / 2)) mod ๐) โ (๐ / 2)) |
19 | 17, 3, 18 | 4sqlem5 16821 |
. . . . . . . . . . 11
โข (๐ โ (๐น โ โค โง ((๐ต โ ๐น) / ๐) โ โค)) |
20 | 19 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ ๐น โ โค) |
21 | | zsqcl 14041 |
. . . . . . . . . 10
โข (๐น โ โค โ (๐นโ2) โ
โค) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐นโ2) โ โค) |
23 | 22 | zred 12614 |
. . . . . . . 8
โข (๐ โ (๐นโ2) โ โ) |
24 | 23 | recnd 11190 |
. . . . . . 7
โข (๐ โ (๐นโ2) โ โ) |
25 | 8, 8, 16, 24 | addsub4d 11566 |
. . . . . 6
โข (๐ โ (((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2)) โ ((๐ธโ2) + (๐นโ2))) = (((((๐โ2) / 2) / 2) โ (๐ธโ2)) + ((((๐โ2) / 2) / 2) โ
(๐นโ2)))) |
26 | 6 | recnd 11190 |
. . . . . . . 8
โข (๐ โ ((๐โ2) / 2) โ
โ) |
27 | 26 | 2halvesd 12406 |
. . . . . . 7
โข (๐ โ ((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2)) = ((๐โ2) / 2)) |
28 | 27 | oveq1d 7377 |
. . . . . 6
โข (๐ โ (((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2)) โ ((๐ธโ2) + (๐นโ2))) = (((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2)))) |
29 | 25, 28 | eqtr3d 2779 |
. . . . 5
โข (๐ โ (((((๐โ2) / 2) / 2) โ (๐ธโ2)) + ((((๐โ2) / 2) / 2) โ
(๐นโ2))) = (((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2)))) |
30 | 29 | adantr 482 |
. . . 4
โข ((๐ โง ๐
= ๐) โ (((((๐โ2) / 2) / 2) โ (๐ธโ2)) + ((((๐โ2) / 2) / 2) โ
(๐นโ2))) = (((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2)))) |
31 | 5 | recnd 11190 |
. . . . . . . . . 10
โข (๐ โ (๐โ2) โ โ) |
32 | 31 | 2halvesd 12406 |
. . . . . . . . 9
โข (๐ โ (((๐โ2) / 2) + ((๐โ2) / 2)) = (๐โ2)) |
33 | 32 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐
= ๐) โ (((๐โ2) / 2) + ((๐โ2) / 2)) = (๐โ2)) |
34 | 4 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
35 | 34 | sqvald 14055 |
. . . . . . . . . 10
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
36 | 35 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐
= ๐) โ (๐โ2) = (๐ ยท ๐)) |
37 | | 4sq.r |
. . . . . . . . . . 11
โข ๐
= ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) |
38 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โง ๐
= ๐) โ ๐
= ๐) |
39 | 37, 38 | eqtr3id 2791 |
. . . . . . . . . 10
โข ((๐ โง ๐
= ๐) โ ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) = ๐) |
40 | 39 | oveq1d 7377 |
. . . . . . . . 9
โข ((๐ โง ๐
= ๐) โ (((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) ยท ๐) = (๐ ยท ๐)) |
41 | 15, 23 | readdcld 11191 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ โ) |
42 | | 4sq.c |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ถ โ โค) |
43 | | 4sq.g |
. . . . . . . . . . . . . . . . . 18
โข ๐บ = (((๐ถ + (๐ / 2)) mod ๐) โ (๐ / 2)) |
44 | 42, 3, 43 | 4sqlem5 16821 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐บ โ โค โง ((๐ถ โ ๐บ) / ๐) โ โค)) |
45 | 44 | simpld 496 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐บ โ โค) |
46 | | zsqcl 14041 |
. . . . . . . . . . . . . . . 16
โข (๐บ โ โค โ (๐บโ2) โ
โค) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐บโ2) โ โค) |
48 | 47 | zred 12614 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐บโ2) โ โ) |
49 | | 4sq.d |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ท โ โค) |
50 | | 4sq.h |
. . . . . . . . . . . . . . . . . 18
โข ๐ป = (((๐ท + (๐ / 2)) mod ๐) โ (๐ / 2)) |
51 | 49, 3, 50 | 4sqlem5 16821 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ป โ โค โง ((๐ท โ ๐ป) / ๐) โ โค)) |
52 | 51 | simpld 496 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ป โ โค) |
53 | | zsqcl 14041 |
. . . . . . . . . . . . . . . 16
โข (๐ป โ โค โ (๐ปโ2) โ
โค) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ปโ2) โ โค) |
55 | 54 | zred 12614 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ปโ2) โ โ) |
56 | 48, 55 | readdcld 11191 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐บโ2) + (๐ปโ2)) โ โ) |
57 | 41, 56 | readdcld 11191 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ โ) |
58 | 57 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ โ) |
59 | 3 | nnne0d 12210 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ 0) |
60 | 58, 34, 59 | divcan1d 11939 |
. . . . . . . . . 10
โข (๐ โ (((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) ยท ๐) = (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) |
61 | 60 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐
= ๐) โ (((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) ยท ๐) = (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) |
62 | 36, 40, 61 | 3eqtr2rd 2784 |
. . . . . . . 8
โข ((๐ โง ๐
= ๐) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) = (๐โ2)) |
63 | 33, 62 | oveq12d 7380 |
. . . . . . 7
โข ((๐ โง ๐
= ๐) โ ((((๐โ2) / 2) + ((๐โ2) / 2)) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) = ((๐โ2) โ (๐โ2))) |
64 | 41 | recnd 11190 |
. . . . . . . . 9
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ โ) |
65 | 56 | recnd 11190 |
. . . . . . . . 9
โข (๐ โ ((๐บโ2) + (๐ปโ2)) โ โ) |
66 | 26, 26, 64, 65 | addsub4d 11566 |
. . . . . . . 8
โข (๐ โ ((((๐โ2) / 2) + ((๐โ2) / 2)) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) = ((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) + (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))))) |
67 | 66 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐
= ๐) โ ((((๐โ2) / 2) + ((๐โ2) / 2)) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) = ((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) + (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))))) |
68 | 31 | subidd 11507 |
. . . . . . . 8
โข (๐ โ ((๐โ2) โ (๐โ2)) = 0) |
69 | 68 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐
= ๐) โ ((๐โ2) โ (๐โ2)) = 0) |
70 | 63, 67, 69 | 3eqtr3d 2785 |
. . . . . 6
โข ((๐ โง ๐
= ๐) โ ((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) + (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2)))) = 0) |
71 | 6, 41 | resubcld 11590 |
. . . . . . . 8
โข (๐ โ (((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) โ โ) |
72 | 9, 3, 10 | 4sqlem7 16823 |
. . . . . . . . . . 11
โข (๐ โ (๐ธโ2) โค (((๐โ2) / 2) / 2)) |
73 | 17, 3, 18 | 4sqlem7 16823 |
. . . . . . . . . . 11
โข (๐ โ (๐นโ2) โค (((๐โ2) / 2) / 2)) |
74 | 15, 23, 7, 7, 72, 73 | le2addd 11781 |
. . . . . . . . . 10
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โค ((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2))) |
75 | 74, 27 | breqtrd 5136 |
. . . . . . . . 9
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โค ((๐โ2) / 2)) |
76 | 6, 41 | subge0d 11752 |
. . . . . . . . 9
โข (๐ โ (0 โค (((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) โ ((๐ธโ2) + (๐นโ2)) โค ((๐โ2) / 2))) |
77 | 75, 76 | mpbird 257 |
. . . . . . . 8
โข (๐ โ 0 โค (((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2)))) |
78 | 6, 56 | resubcld 11590 |
. . . . . . . 8
โข (๐ โ (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))) โ โ) |
79 | 42, 3, 43 | 4sqlem7 16823 |
. . . . . . . . . . 11
โข (๐ โ (๐บโ2) โค (((๐โ2) / 2) / 2)) |
80 | 49, 3, 50 | 4sqlem7 16823 |
. . . . . . . . . . 11
โข (๐ โ (๐ปโ2) โค (((๐โ2) / 2) / 2)) |
81 | 48, 55, 7, 7, 79, 80 | le2addd 11781 |
. . . . . . . . . 10
โข (๐ โ ((๐บโ2) + (๐ปโ2)) โค ((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2))) |
82 | 81, 27 | breqtrd 5136 |
. . . . . . . . 9
โข (๐ โ ((๐บโ2) + (๐ปโ2)) โค ((๐โ2) / 2)) |
83 | 6, 56 | subge0d 11752 |
. . . . . . . . 9
โข (๐ โ (0 โค (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))) โ ((๐บโ2) + (๐ปโ2)) โค ((๐โ2) / 2))) |
84 | 82, 83 | mpbird 257 |
. . . . . . . 8
โข (๐ โ 0 โค (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2)))) |
85 | | add20 11674 |
. . . . . . . 8
โข
((((((๐โ2) / 2)
โ ((๐ธโ2) +
(๐นโ2))) โ โ
โง 0 โค (((๐โ2) /
2) โ ((๐ธโ2) +
(๐นโ2)))) โง
((((๐โ2) / 2) โ
((๐บโ2) + (๐ปโ2))) โ โ โง
0 โค (((๐โ2) / 2)
โ ((๐บโ2) +
(๐ปโ2))))) โ
(((((๐โ2) / 2) โ
((๐ธโ2) + (๐นโ2))) + (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2)))) = 0 โ ((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) = 0 โง (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))) = 0))) |
86 | 71, 77, 78, 84, 85 | syl22anc 838 |
. . . . . . 7
โข (๐ โ (((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) + (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2)))) = 0 โ ((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) = 0 โง (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))) = 0))) |
87 | 86 | biimpa 478 |
. . . . . 6
โข ((๐ โง ((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) + (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2)))) = 0) โ ((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) = 0 โง (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))) = 0)) |
88 | 70, 87 | syldan 592 |
. . . . 5
โข ((๐ โง ๐
= ๐) โ ((((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) = 0 โง (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))) = 0)) |
89 | 88 | simpld 496 |
. . . 4
โข ((๐ โง ๐
= ๐) โ (((๐โ2) / 2) โ ((๐ธโ2) + (๐นโ2))) = 0) |
90 | 30, 89 | eqtrd 2777 |
. . 3
โข ((๐ โง ๐
= ๐) โ (((((๐โ2) / 2) / 2) โ (๐ธโ2)) + ((((๐โ2) / 2) / 2) โ
(๐นโ2))) =
0) |
91 | 7, 15 | resubcld 11590 |
. . . . 5
โข (๐ โ ((((๐โ2) / 2) / 2) โ (๐ธโ2)) โ
โ) |
92 | 7, 15 | subge0d 11752 |
. . . . . 6
โข (๐ โ (0 โค ((((๐โ2) / 2) / 2) โ
(๐ธโ2)) โ (๐ธโ2) โค (((๐โ2) / 2) /
2))) |
93 | 72, 92 | mpbird 257 |
. . . . 5
โข (๐ โ 0 โค ((((๐โ2) / 2) / 2) โ
(๐ธโ2))) |
94 | 7, 23 | resubcld 11590 |
. . . . 5
โข (๐ โ ((((๐โ2) / 2) / 2) โ (๐นโ2)) โ
โ) |
95 | 7, 23 | subge0d 11752 |
. . . . . 6
โข (๐ โ (0 โค ((((๐โ2) / 2) / 2) โ
(๐นโ2)) โ (๐นโ2) โค (((๐โ2) / 2) /
2))) |
96 | 73, 95 | mpbird 257 |
. . . . 5
โข (๐ โ 0 โค ((((๐โ2) / 2) / 2) โ
(๐นโ2))) |
97 | | add20 11674 |
. . . . 5
โข
(((((((๐โ2) /
2) / 2) โ (๐ธโ2))
โ โ โง 0 โค ((((๐โ2) / 2) / 2) โ (๐ธโ2))) โง (((((๐โ2) / 2) / 2) โ
(๐นโ2)) โ โ
โง 0 โค ((((๐โ2)
/ 2) / 2) โ (๐นโ2)))) โ ((((((๐โ2) / 2) / 2) โ (๐ธโ2)) + ((((๐โ2) / 2) / 2) โ
(๐นโ2))) = 0 โ
(((((๐โ2) / 2) / 2)
โ (๐ธโ2)) = 0
โง ((((๐โ2) / 2) /
2) โ (๐นโ2)) =
0))) |
98 | 91, 93, 94, 96, 97 | syl22anc 838 |
. . . 4
โข (๐ โ ((((((๐โ2) / 2) / 2) โ (๐ธโ2)) + ((((๐โ2) / 2) / 2) โ
(๐นโ2))) = 0 โ
(((((๐โ2) / 2) / 2)
โ (๐ธโ2)) = 0
โง ((((๐โ2) / 2) /
2) โ (๐นโ2)) =
0))) |
99 | 98 | biimpa 478 |
. . 3
โข ((๐ โง (((((๐โ2) / 2) / 2) โ (๐ธโ2)) + ((((๐โ2) / 2) / 2) โ
(๐นโ2))) = 0) โ
(((((๐โ2) / 2) / 2)
โ (๐ธโ2)) = 0
โง ((((๐โ2) / 2) /
2) โ (๐นโ2)) =
0)) |
100 | 90, 99 | syldan 592 |
. 2
โข ((๐ โง ๐
= ๐) โ (((((๐โ2) / 2) / 2) โ (๐ธโ2)) = 0 โง ((((๐โ2) / 2) / 2) โ
(๐นโ2)) =
0)) |
101 | 48 | recnd 11190 |
. . . . . . 7
โข (๐ โ (๐บโ2) โ โ) |
102 | 55 | recnd 11190 |
. . . . . . 7
โข (๐ โ (๐ปโ2) โ โ) |
103 | 8, 8, 101, 102 | addsub4d 11566 |
. . . . . 6
โข (๐ โ (((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2)) โ ((๐บโ2) + (๐ปโ2))) = (((((๐โ2) / 2) / 2) โ (๐บโ2)) + ((((๐โ2) / 2) / 2) โ
(๐ปโ2)))) |
104 | 27 | oveq1d 7377 |
. . . . . 6
โข (๐ โ (((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2)) โ ((๐บโ2) + (๐ปโ2))) = (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2)))) |
105 | 103, 104 | eqtr3d 2779 |
. . . . 5
โข (๐ โ (((((๐โ2) / 2) / 2) โ (๐บโ2)) + ((((๐โ2) / 2) / 2) โ
(๐ปโ2))) = (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2)))) |
106 | 105 | adantr 482 |
. . . 4
โข ((๐ โง ๐
= ๐) โ (((((๐โ2) / 2) / 2) โ (๐บโ2)) + ((((๐โ2) / 2) / 2) โ
(๐ปโ2))) = (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2)))) |
107 | 88 | simprd 497 |
. . . 4
โข ((๐ โง ๐
= ๐) โ (((๐โ2) / 2) โ ((๐บโ2) + (๐ปโ2))) = 0) |
108 | 106, 107 | eqtrd 2777 |
. . 3
โข ((๐ โง ๐
= ๐) โ (((((๐โ2) / 2) / 2) โ (๐บโ2)) + ((((๐โ2) / 2) / 2) โ
(๐ปโ2))) =
0) |
109 | 7, 48 | resubcld 11590 |
. . . . 5
โข (๐ โ ((((๐โ2) / 2) / 2) โ (๐บโ2)) โ
โ) |
110 | 7, 48 | subge0d 11752 |
. . . . . 6
โข (๐ โ (0 โค ((((๐โ2) / 2) / 2) โ
(๐บโ2)) โ (๐บโ2) โค (((๐โ2) / 2) /
2))) |
111 | 79, 110 | mpbird 257 |
. . . . 5
โข (๐ โ 0 โค ((((๐โ2) / 2) / 2) โ
(๐บโ2))) |
112 | 7, 55 | resubcld 11590 |
. . . . 5
โข (๐ โ ((((๐โ2) / 2) / 2) โ (๐ปโ2)) โ
โ) |
113 | 7, 55 | subge0d 11752 |
. . . . . 6
โข (๐ โ (0 โค ((((๐โ2) / 2) / 2) โ
(๐ปโ2)) โ (๐ปโ2) โค (((๐โ2) / 2) /
2))) |
114 | 80, 113 | mpbird 257 |
. . . . 5
โข (๐ โ 0 โค ((((๐โ2) / 2) / 2) โ
(๐ปโ2))) |
115 | | add20 11674 |
. . . . 5
โข
(((((((๐โ2) /
2) / 2) โ (๐บโ2))
โ โ โง 0 โค ((((๐โ2) / 2) / 2) โ (๐บโ2))) โง (((((๐โ2) / 2) / 2) โ
(๐ปโ2)) โ โ
โง 0 โค ((((๐โ2)
/ 2) / 2) โ (๐ปโ2)))) โ ((((((๐โ2) / 2) / 2) โ (๐บโ2)) + ((((๐โ2) / 2) / 2) โ
(๐ปโ2))) = 0 โ
(((((๐โ2) / 2) / 2)
โ (๐บโ2)) = 0
โง ((((๐โ2) / 2) /
2) โ (๐ปโ2)) =
0))) |
116 | 109, 111,
112, 114, 115 | syl22anc 838 |
. . . 4
โข (๐ โ ((((((๐โ2) / 2) / 2) โ (๐บโ2)) + ((((๐โ2) / 2) / 2) โ
(๐ปโ2))) = 0 โ
(((((๐โ2) / 2) / 2)
โ (๐บโ2)) = 0
โง ((((๐โ2) / 2) /
2) โ (๐ปโ2)) =
0))) |
117 | 116 | biimpa 478 |
. . 3
โข ((๐ โง (((((๐โ2) / 2) / 2) โ (๐บโ2)) + ((((๐โ2) / 2) / 2) โ
(๐ปโ2))) = 0) โ
(((((๐โ2) / 2) / 2)
โ (๐บโ2)) = 0
โง ((((๐โ2) / 2) /
2) โ (๐ปโ2)) =
0)) |
118 | 108, 117 | syldan 592 |
. 2
โข ((๐ โง ๐
= ๐) โ (((((๐โ2) / 2) / 2) โ (๐บโ2)) = 0 โง ((((๐โ2) / 2) / 2) โ
(๐ปโ2)) =
0)) |
119 | 100, 118 | jca 513 |
1
โข ((๐ โง ๐
= ๐) โ ((((((๐โ2) / 2) / 2) โ (๐ธโ2)) = 0 โง ((((๐โ2) / 2) / 2) โ
(๐นโ2)) = 0) โง
(((((๐โ2) / 2) / 2)
โ (๐บโ2)) = 0
โง ((((๐โ2) / 2) /
2) โ (๐ปโ2)) =
0))) |