Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ðķ <<s ð·) |
2 | | simpll 766 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ðī <<s ðĩ) |
3 | | simprr 772 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ð = (ðķ |s ð·)) |
4 | | simprl 770 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ð = (ðī |s ðĩ)) |
5 | | slerec 27180 |
. . . . 5
âĒ (((ðķ <<s ð· ⧠ðī <<s ðĩ) ⧠(ð = (ðķ |s ð·) ⧠ð = (ðī |s ðĩ))) â (ð âĪs ð â (âð â ðĩ ð <s ð ⧠âð â ðķ ð <s ð))) |
6 | 1, 2, 3, 4, 5 | syl22anc 838 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (ð âĪs ð â (âð â ðĩ ð <s ð ⧠âð â ðķ ð <s ð))) |
7 | | ancom 462 |
. . . 4
âĒ
((âð â
ðĩ ð <s ð ⧠âð â ðķ ð <s ð) â (âð â ðķ ð <s ð ⧠âð â ðĩ ð <s ð)) |
8 | 6, 7 | bitrdi 287 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (ð âĪs ð â (âð â ðķ ð <s ð ⧠âð â ðĩ ð <s ð))) |
9 | | scutcut 27162 |
. . . . . . 7
âĒ (ðķ <<s ð· â ((ðķ |s ð·) â No
⧠ðķ <<s {(ðķ |s ð·)} ⧠{(ðķ |s ð·)} <<s ð·)) |
10 | 9 | simp1d 1143 |
. . . . . 6
âĒ (ðķ <<s ð· â (ðķ |s ð·) â No
) |
11 | 10 | ad2antlr 726 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (ðķ |s ð·) â No
) |
12 | 3, 11 | eqeltrd 2834 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ð â No
) |
13 | | scutcut 27162 |
. . . . . . 7
âĒ (ðī <<s ðĩ â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
14 | 13 | simp1d 1143 |
. . . . . 6
âĒ (ðī <<s ðĩ â (ðī |s ðĩ) â No
) |
15 | 14 | ad2antrr 725 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (ðī |s ðĩ) â No
) |
16 | 4, 15 | eqeltrd 2834 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ð â No
) |
17 | | slenlt 27116 |
. . . 4
âĒ ((ð â
No ⧠ð â
No ) â (ð âĪs ð â ÂŽ ð <s ð)) |
18 | 12, 16, 17 | syl2anc 585 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (ð âĪs ð â ÂŽ ð <s ð)) |
19 | | ssltss1 27150 |
. . . . . . . . 9
âĒ (ðķ <<s ð· â ðķ â No
) |
20 | 19 | ad2antlr 726 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ðķ â No
) |
21 | 20 | sselda 3945 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) ⧠ð â ðķ) â ð â No
) |
22 | 16 | adantr 482 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) ⧠ð â ðķ) â ð â No
) |
23 | | sltnle 27117 |
. . . . . . 7
âĒ ((ð â
No ⧠ð â
No ) â (ð <s ð â ÂŽ ð âĪs ð)) |
24 | 21, 22, 23 | syl2anc 585 |
. . . . . 6
âĒ ((((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) ⧠ð â ðķ) â (ð <s ð â ÂŽ ð âĪs ð)) |
25 | 24 | ralbidva 3169 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (âð â ðķ ð <s ð â âð â ðķ ÂŽ ð âĪs ð)) |
26 | 12 | adantr 482 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) ⧠ð â ðĩ) â ð â No
) |
27 | | ssltss2 27151 |
. . . . . . . . 9
âĒ (ðī <<s ðĩ â ðĩ â No
) |
28 | 27 | ad2antrr 725 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ðĩ â No
) |
29 | 28 | sselda 3945 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) ⧠ð â ðĩ) â ð â No
) |
30 | | sltnle 27117 |
. . . . . . 7
âĒ ((ð â
No ⧠ð â
No ) â (ð <s ð â ÂŽ ð âĪs ð)) |
31 | 26, 29, 30 | syl2anc 585 |
. . . . . 6
âĒ ((((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) ⧠ð â ðĩ) â (ð <s ð â ÂŽ ð âĪs ð)) |
32 | 31 | ralbidva 3169 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (âð â ðĩ ð <s ð â âð â ðĩ ÂŽ ð âĪs ð)) |
33 | 25, 32 | anbi12d 632 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ((âð â ðķ ð <s ð ⧠âð â ðĩ ð <s ð) â (âð â ðķ ÂŽ ð âĪs ð ⧠âð â ðĩ ÂŽ ð âĪs ð))) |
34 | | ralnex 3072 |
. . . . . 6
âĒ
(âð â
ðķ ÂŽ ð âĪs ð â ÂŽ âð â ðķ ð âĪs ð) |
35 | | ralnex 3072 |
. . . . . 6
âĒ
(âð â
ðĩ ÂŽ ð âĪs ð â ÂŽ âð â ðĩ ð âĪs ð) |
36 | 34, 35 | anbi12i 628 |
. . . . 5
âĒ
((âð â
ðķ ÂŽ ð âĪs ð ⧠âð â ðĩ ÂŽ ð âĪs ð) â (ÂŽ âð â ðķ ð âĪs ð ⧠Ž âð â ðĩ ð âĪs ð)) |
37 | | ioran 983 |
. . . . 5
âĒ (ÂŽ
(âð â ðķ ð âĪs ð âĻ âð â ðĩ ð âĪs ð) â (ÂŽ âð â ðķ ð âĪs ð ⧠Ž âð â ðĩ ð âĪs ð)) |
38 | 36, 37 | bitr4i 278 |
. . . 4
âĒ
((âð â
ðķ ÂŽ ð âĪs ð ⧠âð â ðĩ ÂŽ ð âĪs ð) â ÂŽ (âð â ðķ ð âĪs ð âĻ âð â ðĩ ð âĪs ð)) |
39 | 33, 38 | bitrdi 287 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â ((âð â ðķ ð <s ð ⧠âð â ðĩ ð <s ð) â ÂŽ (âð â ðķ ð âĪs ð âĻ âð â ðĩ ð âĪs ð))) |
40 | 8, 18, 39 | 3bitr3d 309 |
. 2
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (ÂŽ ð <s ð â ÂŽ (âð â ðķ ð âĪs ð âĻ âð â ðĩ ð âĪs ð))) |
41 | 40 | con4bid 317 |
1
âĒ (((ðī <<s ðĩ ⧠ðķ <<s ð·) ⧠(ð = (ðī |s ðĩ) ⧠ð = (ðķ |s ð·))) â (ð <s ð â (âð â ðķ ð âĪs ð âĻ âð â ðĩ ð âĪs ð))) |