Step | Hyp | Ref
| Expression |
1 | | jm2.27a11 |
. . 3
โข (๐ โ ((๐ทโ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1) |
2 | | jm2.27a1 |
. . . 4
โข (๐ โ ๐ด โ
(โคโฅโ2)) |
3 | | jm2.27a4 |
. . . 4
โข (๐ โ ๐ท โ
โ0) |
4 | | jm2.27a3 |
. . . . 5
โข (๐ โ ๐ถ โ โ) |
5 | 4 | nnzd 12531 |
. . . 4
โข (๐ โ ๐ถ โ โค) |
6 | | rmxycomplete 41284 |
. . . 4
โข ((๐ด โ
(โคโฅโ2) โง ๐ท โ โ0 โง ๐ถ โ โค) โ (((๐ทโ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โ
โ๐ โ โค
(๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) |
7 | 2, 3, 5, 6 | syl3anc 1372 |
. . 3
โข (๐ โ (((๐ทโ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โ
โ๐ โ โค
(๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) |
8 | 1, 7 | mpbid 231 |
. 2
โข (๐ โ โ๐ โ โค (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐))) |
9 | | jm2.27a12 |
. . . . 5
โข (๐ โ ((๐นโ2) โ (((๐ดโ2) โ 1) ยท (๐ธโ2))) = 1) |
10 | 9 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ ((๐นโ2) โ (((๐ดโ2) โ 1) ยท (๐ธโ2))) = 1) |
11 | 2 | adantr 482 |
. . . . 5
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ ๐ด โ
(โคโฅโ2)) |
12 | | jm2.27a6 |
. . . . . 6
โข (๐ โ ๐น โ
โ0) |
13 | 12 | adantr 482 |
. . . . 5
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ ๐น โ
โ0) |
14 | | jm2.27a5 |
. . . . . . 7
โข (๐ โ ๐ธ โ
โ0) |
15 | 14 | nn0zd 12530 |
. . . . . 6
โข (๐ โ ๐ธ โ โค) |
16 | 15 | adantr 482 |
. . . . 5
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ ๐ธ โ โค) |
17 | | rmxycomplete 41284 |
. . . . 5
โข ((๐ด โ
(โคโฅโ2) โง ๐น โ โ0 โง ๐ธ โ โค) โ (((๐นโ2) โ (((๐ดโ2) โ 1) ยท
(๐ธโ2))) = 1 โ
โ๐ โ โค
(๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) |
18 | 11, 13, 16, 17 | syl3anc 1372 |
. . . 4
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ (((๐นโ2) โ (((๐ดโ2) โ 1) ยท (๐ธโ2))) = 1 โ
โ๐ โ โค
(๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) |
19 | 10, 18 | mpbid 231 |
. . 3
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ โ๐ โ โค (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐))) |
20 | | jm2.27a14 |
. . . . . 6
โข (๐ โ ((๐ผโ2) โ (((๐บโ2) โ 1) ยท (๐ปโ2))) = 1) |
21 | 20 | ad2antrr 725 |
. . . . 5
โข (((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โ ((๐ผโ2) โ (((๐บโ2) โ 1) ยท (๐ปโ2))) = 1) |
22 | | jm2.27a13 |
. . . . . . 7
โข (๐ โ ๐บ โ
(โคโฅโ2)) |
23 | 22 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โ ๐บ โ
(โคโฅโ2)) |
24 | | jm2.27a9 |
. . . . . . 7
โข (๐ โ ๐ผ โ
โ0) |
25 | 24 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โ ๐ผ โ
โ0) |
26 | | jm2.27a8 |
. . . . . . . 8
โข (๐ โ ๐ป โ
โ0) |
27 | 26 | nn0zd 12530 |
. . . . . . 7
โข (๐ โ ๐ป โ โค) |
28 | 27 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โ ๐ป โ โค) |
29 | | rmxycomplete 41284 |
. . . . . 6
โข ((๐บ โ
(โคโฅโ2) โง ๐ผ โ โ0 โง ๐ป โ โค) โ (((๐ผโ2) โ (((๐บโ2) โ 1) ยท
(๐ปโ2))) = 1 โ
โ๐ โ โค
(๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) |
30 | 23, 25, 28, 29 | syl3anc 1372 |
. . . . 5
โข (((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โ (((๐ผโ2) โ (((๐บโ2) โ 1) ยท (๐ปโ2))) = 1 โ
โ๐ โ โค
(๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) |
31 | 21, 30 | mpbid 231 |
. . . 4
โข (((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โ โ๐ โ โค (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐))) |
32 | 2 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ด โ
(โคโฅโ2)) |
33 | | jm2.27a2 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
34 | 33 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ต โ โ) |
35 | 4 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ถ โ โ) |
36 | 3 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ท โ
โ0) |
37 | 14 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ธ โ
โ0) |
38 | 12 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐น โ
โ0) |
39 | | jm2.27a7 |
. . . . . 6
โข (๐ โ ๐บ โ
โ0) |
40 | 39 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐บ โ
โ0) |
41 | 26 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ป โ
โ0) |
42 | 24 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ผ โ
โ0) |
43 | | jm2.27a10 |
. . . . . 6
โข (๐ โ ๐ฝ โ
โ0) |
44 | 43 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ฝ โ
โ0) |
45 | 1 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ((๐ทโ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1) |
46 | 9 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ((๐นโ2) โ (((๐ดโ2) โ 1) ยท (๐ธโ2))) = 1) |
47 | 22 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐บ โ
(โคโฅโ2)) |
48 | 20 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ((๐ผโ2) โ (((๐บโ2) โ 1) ยท (๐ปโ2))) = 1) |
49 | | jm2.27a15 |
. . . . . 6
โข (๐ โ ๐ธ = ((๐ฝ + 1) ยท (2 ยท (๐ถโ2)))) |
50 | 49 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ธ = ((๐ฝ + 1) ยท (2 ยท (๐ถโ2)))) |
51 | | jm2.27a16 |
. . . . . 6
โข (๐ โ ๐น โฅ (๐บ โ ๐ด)) |
52 | 51 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐น โฅ (๐บ โ ๐ด)) |
53 | | jm2.27a17 |
. . . . . 6
โข (๐ โ (2 ยท ๐ถ) โฅ (๐บ โ 1)) |
54 | 53 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ (2 ยท ๐ถ) โฅ (๐บ โ 1)) |
55 | | jm2.27a18 |
. . . . . 6
โข (๐ โ ๐น โฅ (๐ป โ ๐ถ)) |
56 | 55 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐น โฅ (๐ป โ ๐ถ)) |
57 | | jm2.27a19 |
. . . . . 6
โข (๐ โ (2 ยท ๐ถ) โฅ (๐ป โ ๐ต)) |
58 | 57 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ (2 ยท ๐ถ) โฅ (๐ป โ ๐ต)) |
59 | | jm2.27a20 |
. . . . . 6
โข (๐ โ ๐ต โค ๐ถ) |
60 | 59 | ad3antrrr 729 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ต โค ๐ถ) |
61 | | simprl 770 |
. . . . . 6
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ ๐ โ โค) |
62 | 61 | ad2antrr 725 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ โ โค) |
63 | | simprrl 780 |
. . . . . 6
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ ๐ท = (๐ด Xrm ๐)) |
64 | 63 | ad2antrr 725 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ท = (๐ด Xrm ๐)) |
65 | | simprrr 781 |
. . . . . 6
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ ๐ถ = (๐ด Yrm ๐)) |
66 | 65 | ad2antrr 725 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ถ = (๐ด Yrm ๐)) |
67 | | simplrl 776 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ โ โค) |
68 | | simprl 770 |
. . . . . 6
โข ((๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐))) โ ๐น = (๐ด Xrm ๐)) |
69 | 68 | ad2antlr 726 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐น = (๐ด Xrm ๐)) |
70 | | simprr 772 |
. . . . . 6
โข ((๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐))) โ ๐ธ = (๐ด Yrm ๐)) |
71 | 70 | ad2antlr 726 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ธ = (๐ด Yrm ๐)) |
72 | | simprl 770 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ โ โค) |
73 | | simprrl 780 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ผ = (๐บ Xrm ๐)) |
74 | | simprrr 781 |
. . . . 5
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ป = (๐บ Yrm ๐)) |
75 | 32, 34, 35, 36, 37, 38, 40, 41, 42, 44, 45, 46, 47, 48, 50, 52, 54, 56, 58, 60, 62, 64, 66, 67, 69, 71, 72, 73, 74 | jm2.27a 41372 |
. . . 4
โข ((((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐ผ = (๐บ Xrm ๐) โง ๐ป = (๐บ Yrm ๐)))) โ ๐ถ = (๐ด Yrm ๐ต)) |
76 | 31, 75 | rexlimddv 3155 |
. . 3
โข (((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โง (๐ โ โค โง (๐น = (๐ด Xrm ๐) โง ๐ธ = (๐ด Yrm ๐)))) โ ๐ถ = (๐ด Yrm ๐ต)) |
77 | 19, 76 | rexlimddv 3155 |
. 2
โข ((๐ โง (๐ โ โค โง (๐ท = (๐ด Xrm ๐) โง ๐ถ = (๐ด Yrm ๐)))) โ ๐ถ = (๐ด Yrm ๐ต)) |
78 | 8, 77 | rexlimddv 3155 |
1
โข (๐ โ ๐ถ = (๐ด Yrm ๐ต)) |