Step | Hyp | Ref
| Expression |
1 | | nnmordi 8627 |
. . . . 5
โข (((๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
2 | 1 | ex 414 |
. . . 4
โข ((๐ต โ ฯ โง ๐ถ โ ฯ) โ (โ
โ ๐ถ โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต)))) |
3 | 2 | impcomd 413 |
. . 3
โข ((๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ด โ ๐ต โง โ
โ ๐ถ) โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
4 | 3 | 3adant1 1131 |
. 2
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ด โ ๐ต โง โ
โ ๐ถ) โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
5 | | ne0i 4333 |
. . . . . . . 8
โข ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ต) โ โ
) |
6 | | nnm0r 8606 |
. . . . . . . . . 10
โข (๐ต โ ฯ โ (โ
ยทo ๐ต) =
โ
) |
7 | | oveq1 7411 |
. . . . . . . . . . 11
โข (๐ถ = โ
โ (๐ถ ยทo ๐ต) = (โ
ยทo ๐ต)) |
8 | 7 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ถ = โ
โ ((๐ถ ยทo ๐ต) = โ
โ (โ
ยทo ๐ต) =
โ
)) |
9 | 6, 8 | syl5ibrcom 246 |
. . . . . . . . 9
โข (๐ต โ ฯ โ (๐ถ = โ
โ (๐ถ ยทo ๐ต) = โ
)) |
10 | 9 | necon3d 2962 |
. . . . . . . 8
โข (๐ต โ ฯ โ ((๐ถ ยทo ๐ต) โ โ
โ ๐ถ โ โ
)) |
11 | 5, 10 | syl5 34 |
. . . . . . 7
โข (๐ต โ ฯ โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ๐ถ โ โ
)) |
12 | 11 | adantr 482 |
. . . . . 6
โข ((๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ๐ถ โ โ
)) |
13 | | nnord 7858 |
. . . . . . . 8
โข (๐ถ โ ฯ โ Ord ๐ถ) |
14 | | ord0eln0 6416 |
. . . . . . . 8
โข (Ord
๐ถ โ (โ
โ
๐ถ โ ๐ถ โ โ
)) |
15 | 13, 14 | syl 17 |
. . . . . . 7
โข (๐ถ โ ฯ โ (โ
โ ๐ถ โ ๐ถ โ โ
)) |
16 | 15 | adantl 483 |
. . . . . 6
โข ((๐ต โ ฯ โง ๐ถ โ ฯ) โ (โ
โ ๐ถ โ ๐ถ โ โ
)) |
17 | 12, 16 | sylibrd 259 |
. . . . 5
โข ((๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ โ
โ ๐ถ)) |
18 | 17 | 3adant1 1131 |
. . . 4
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ โ
โ ๐ถ)) |
19 | | oveq2 7412 |
. . . . . . . . . 10
โข (๐ด = ๐ต โ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต)) |
20 | 19 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ (๐ด = ๐ต โ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต))) |
21 | | nnmordi 8627 |
. . . . . . . . . 10
โข (((๐ด โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ (๐ต โ ๐ด โ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด))) |
22 | 21 | 3adantl2 1168 |
. . . . . . . . 9
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ (๐ต โ ๐ด โ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด))) |
23 | 20, 22 | orim12d 964 |
. . . . . . . 8
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ ((๐ด = ๐ต โจ ๐ต โ ๐ด) โ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
24 | 23 | con3d 152 |
. . . . . . 7
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ (ยฌ
((๐ถ ยทo
๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)) โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
25 | | simpl3 1194 |
. . . . . . . . 9
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ ๐ถ โ
ฯ) |
26 | | simpl1 1192 |
. . . . . . . . 9
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ ๐ด โ
ฯ) |
27 | | nnmcl 8608 |
. . . . . . . . 9
โข ((๐ถ โ ฯ โง ๐ด โ ฯ) โ (๐ถ ยทo ๐ด) โ
ฯ) |
28 | 25, 26, 27 | syl2anc 585 |
. . . . . . . 8
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ (๐ถ ยทo ๐ด) โ
ฯ) |
29 | | simpl2 1193 |
. . . . . . . . 9
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ ๐ต โ
ฯ) |
30 | | nnmcl 8608 |
. . . . . . . . 9
โข ((๐ถ โ ฯ โง ๐ต โ ฯ) โ (๐ถ ยทo ๐ต) โ
ฯ) |
31 | 25, 29, 30 | syl2anc 585 |
. . . . . . . 8
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ (๐ถ ยทo ๐ต) โ
ฯ) |
32 | | nnord 7858 |
. . . . . . . . 9
โข ((๐ถ ยทo ๐ด) โ ฯ โ Ord
(๐ถ ยทo
๐ด)) |
33 | | nnord 7858 |
. . . . . . . . 9
โข ((๐ถ ยทo ๐ต) โ ฯ โ Ord
(๐ถ ยทo
๐ต)) |
34 | | ordtri2 6396 |
. . . . . . . . 9
โข ((Ord
(๐ถ ยทo
๐ด) โง Ord (๐ถ ยทo ๐ต)) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
35 | 32, 33, 34 | syl2an 597 |
. . . . . . . 8
โข (((๐ถ ยทo ๐ด) โ ฯ โง (๐ถ ยทo ๐ต) โ ฯ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
36 | 28, 31, 35 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
37 | | nnord 7858 |
. . . . . . . . 9
โข (๐ด โ ฯ โ Ord ๐ด) |
38 | | nnord 7858 |
. . . . . . . . 9
โข (๐ต โ ฯ โ Ord ๐ต) |
39 | | ordtri2 6396 |
. . . . . . . . 9
โข ((Ord
๐ด โง Ord ๐ต) โ (๐ด โ ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
40 | 37, 38, 39 | syl2an 597 |
. . . . . . . 8
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (๐ด โ ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
41 | 26, 29, 40 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ (๐ด โ ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
42 | 24, 36, 41 | 3imtr4d 294 |
. . . . . 6
โข (((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โง โ
โ ๐ถ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ๐ด โ ๐ต)) |
43 | 42 | ex 414 |
. . . . 5
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ (โ
โ ๐ถ โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ๐ด โ ๐ต))) |
44 | 43 | com23 86 |
. . . 4
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ (โ
โ ๐ถ โ ๐ด โ ๐ต))) |
45 | 18, 44 | mpdd 43 |
. . 3
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ๐ด โ ๐ต)) |
46 | 45, 18 | jcad 514 |
. 2
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ (๐ด โ ๐ต โง โ
โ ๐ถ))) |
47 | 4, 46 | impbid 211 |
1
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ด โ ๐ต โง โ
โ ๐ถ) โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |