Step | Hyp | Ref
| Expression |
1 | | bdayelon 27119 |
. . . . . . . . . 10
âĒ ( bday â(ðī |s ðĩ)) â On |
2 | 1 | onssneli 6434 |
. . . . . . . . 9
âĒ (( bday â(ðī |s ðĩ)) â ( bday
âðĨ) â
ÂŽ ( bday âðĨ) â ( bday
â(ðī |s ðĩ))) |
3 | | leftssold 27211 |
. . . . . . . . . . . . 13
âĒ ( L
âð) â ( O
â( bday âð)) |
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ( L âð) â ( O â(
bday âð))) |
5 | 4 | sselda 3945 |
. . . . . . . . . . 11
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ðĨ â ( O â(
bday âð))) |
6 | | bdayelon 27119 |
. . . . . . . . . . . 12
âĒ ( bday âð) â On |
7 | | leftssno 27213 |
. . . . . . . . . . . . . 14
âĒ ( L
âð) â No |
8 | 7 | a1i 11 |
. . . . . . . . . . . . 13
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ( L âð) â No
) |
9 | 8 | sselda 3945 |
. . . . . . . . . . . 12
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ðĨ â No
) |
10 | | oldbday 27233 |
. . . . . . . . . . . 12
âĒ ((( bday âð) â On ⧠ðĨ â No )
â (ðĨ â ( O
â( bday âð)) â ( bday
âðĨ) â
( bday âð))) |
11 | 6, 9, 10 | sylancr 588 |
. . . . . . . . . . 11
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â (ðĨ â ( O â(
bday âð))
â ( bday âðĨ) â ( bday
âð))) |
12 | 5, 11 | mpbid 231 |
. . . . . . . . . 10
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ( bday
âðĨ) â
( bday âð)) |
13 | | simplr 768 |
. . . . . . . . . . 11
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ð = (ðī |s ðĩ)) |
14 | 13 | fveq2d 6847 |
. . . . . . . . . 10
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ( bday
âð) = ( bday â(ðī |s ðĩ))) |
15 | 12, 14 | eleqtrd 2840 |
. . . . . . . . 9
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ( bday
âðĨ) â
( bday â(ðī |s ðĩ))) |
16 | 2, 15 | nsyl3 138 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ÂŽ ( bday
â(ðī |s ðĩ)) â ( bday âðĨ)) |
17 | | scutbday 27146 |
. . . . . . . . . 10
âĒ (ðī <<s ðĩ â ( bday
â(ðī |s ðĩ)) = âĐ ( bday â {ðĄ â
No âĢ (ðī
<<s {ðĄ} ⧠{ðĄ} <<s ðĩ)})) |
18 | 17 | ad3antrrr 729 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðī <<s {ðĨ}) â ( bday
â(ðī |s ðĩ)) = âĐ ( bday â {ðĄ â
No âĢ (ðī
<<s {ðĄ} ⧠{ðĄ} <<s ðĩ)})) |
19 | | bdayfn 27116 |
. . . . . . . . . . 11
âĒ bday Fn No
|
20 | | ssrab2 4038 |
. . . . . . . . . . 11
âĒ {ðĄ â
No âĢ (ðī
<<s {ðĄ} ⧠{ðĄ} <<s ðĩ)} â No
|
21 | | sneq 4597 |
. . . . . . . . . . . . . 14
âĒ (ðĄ = ðĨ â {ðĄ} = {ðĨ}) |
22 | 21 | breq2d 5118 |
. . . . . . . . . . . . 13
âĒ (ðĄ = ðĨ â (ðī <<s {ðĄ} â ðī <<s {ðĨ})) |
23 | 21 | breq1d 5116 |
. . . . . . . . . . . . 13
âĒ (ðĄ = ðĨ â ({ðĄ} <<s ðĩ â {ðĨ} <<s ðĩ)) |
24 | 22, 23 | anbi12d 632 |
. . . . . . . . . . . 12
âĒ (ðĄ = ðĨ â ((ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ) â (ðī <<s {ðĨ} ⧠{ðĨ} <<s ðĩ))) |
25 | 9 | adantr 482 |
. . . . . . . . . . . 12
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðī <<s {ðĨ}) â ðĨ â No
) |
26 | | vsnex 5387 |
. . . . . . . . . . . . . . 15
âĒ {ðĨ} â V |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â {ðĨ} â V) |
28 | | ssltex2 27130 |
. . . . . . . . . . . . . . 15
âĒ (ðī <<s ðĩ â ðĩ â V) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . . . . 14
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ðĩ â V) |
30 | 9 | snssd 4770 |
. . . . . . . . . . . . . 14
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â {ðĨ} â No
) |
31 | | ssltss2 27132 |
. . . . . . . . . . . . . . 15
âĒ (ðī <<s ðĩ â ðĩ â No
) |
32 | 31 | ad2antrr 725 |
. . . . . . . . . . . . . 14
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ðĩ â No
) |
33 | 9 | adantr 482 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â ðĩ) â ðĨ â No
) |
34 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ð = (ðī |s ðĩ)) |
35 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . 20
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ðī <<s ðĩ) |
36 | 35 | scutcld 27145 |
. . . . . . . . . . . . . . . . . . 19
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â (ðī |s ðĩ) â No
) |
37 | 34, 36 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ð â No
) |
38 | 37 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â ðĩ) â ð â No
) |
39 | 32 | sselda 3945 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â ðĩ) â ð â No
) |
40 | | leftval 27196 |
. . . . . . . . . . . . . . . . . . . . . 22
âĒ ( L
âð) = {ðĨ â ( O â( bday âð)) âĢ ðĨ <s ð} |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ( L âð) = {ðĨ â ( O â(
bday âð))
âĢ ðĨ <s ð}) |
42 | 41 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . 20
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â (ðĨ â ( L âð) â ðĨ â {ðĨ â ( O â(
bday âð))
âĢ ðĨ <s ð})) |
43 | | rabid 3428 |
. . . . . . . . . . . . . . . . . . . 20
âĒ (ðĨ â {ðĨ â ( O â(
bday âð))
âĢ ðĨ <s ð} â (ðĨ â ( O â(
bday âð))
⧠ðĨ <s ð)) |
44 | 42, 43 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . 19
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â (ðĨ â ( L âð) â (ðĨ â ( O â(
bday âð))
⧠ðĨ <s ð))) |
45 | 44 | simplbda 501 |
. . . . . . . . . . . . . . . . . 18
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ðĨ <s ð) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â ðĩ) â ðĨ <s ð) |
47 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â ðĩ) â ð = (ðī |s ðĩ)) |
48 | | scutcut 27143 |
. . . . . . . . . . . . . . . . . . . . 21
âĒ (ðī <<s ðĩ â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
49 | 48 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
50 | 49 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . 19
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â {(ðī |s ðĩ)} <<s ðĩ) |
51 | | ovex 7391 |
. . . . . . . . . . . . . . . . . . . . 21
âĒ (ðī |s ðĩ) â V |
52 | 51 | snid 4623 |
. . . . . . . . . . . . . . . . . . . 20
âĒ (ðī |s ðĩ) â {(ðī |s ðĩ)} |
53 | | ssltsepc 27135 |
. . . . . . . . . . . . . . . . . . . 20
âĒ (({(ðī |s ðĩ)} <<s ðĩ ⧠(ðī |s ðĩ) â {(ðī |s ðĩ)} ⧠ð â ðĩ) â (ðī |s ðĩ) <s ð) |
54 | 52, 53 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . 19
âĒ (({(ðī |s ðĩ)} <<s ðĩ ⧠ð â ðĩ) â (ðī |s ðĩ) <s ð) |
55 | 50, 54 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â ðĩ) â (ðī |s ðĩ) <s ð) |
56 | 47, 55 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â ðĩ) â ð <s ð) |
57 | 33, 38, 39, 46, 56 | slttrd 27110 |
. . . . . . . . . . . . . . . 16
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â ðĩ) â ðĨ <s ð) |
58 | 57 | 3adant2 1132 |
. . . . . . . . . . . . . . 15
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â {ðĨ} ⧠ð â ðĩ) â ðĨ <s ð) |
59 | | velsn 4603 |
. . . . . . . . . . . . . . . . 17
âĒ (ð â {ðĨ} â ð = ðĨ) |
60 | | breq1 5109 |
. . . . . . . . . . . . . . . . 17
âĒ (ð = ðĨ â (ð <s ð â ðĨ <s ð)) |
61 | 59, 60 | sylbi 216 |
. . . . . . . . . . . . . . . 16
âĒ (ð â {ðĨ} â (ð <s ð â ðĨ <s ð)) |
62 | 61 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â {ðĨ} ⧠ð â ðĩ) â (ð <s ð â ðĨ <s ð)) |
63 | 58, 62 | mpbird 257 |
. . . . . . . . . . . . . 14
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ð â {ðĨ} ⧠ð â ðĩ) â ð <s ð) |
64 | 27, 29, 30, 32, 63 | ssltd 27134 |
. . . . . . . . . . . . 13
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â {ðĨ} <<s ðĩ) |
65 | 64 | anim1ci 617 |
. . . . . . . . . . . 12
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðī <<s {ðĨ}) â (ðī <<s {ðĨ} ⧠{ðĨ} <<s ðĩ)) |
66 | 24, 25, 65 | elrabd 3648 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðī <<s {ðĨ}) â ðĨ â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) |
67 | | fnfvima 7184 |
. . . . . . . . . . 11
âĒ (( bday Fn No ⧠{ðĄ â
No âĢ (ðī
<<s {ðĄ} ⧠{ðĄ} <<s ðĩ)} â No
⧠ðĨ â {ðĄ â
No âĢ (ðī
<<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) â ( bday
âðĨ) â
( bday â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)})) |
68 | 19, 20, 66, 67 | mp3an12i 1466 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðī <<s {ðĨ}) â ( bday
âðĨ) â
( bday â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)})) |
69 | | intss1 4925 |
. . . . . . . . . 10
âĒ (( bday âðĨ) â ( bday
â {ðĄ â No âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) â âĐ
( bday â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) â ( bday
âðĨ)) |
70 | 68, 69 | syl 17 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðī <<s {ðĨ}) â âĐ ( bday â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) â ( bday
âðĨ)) |
71 | 18, 70 | eqsstrd 3983 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðī <<s {ðĨ}) â ( bday
â(ðī |s ðĩ)) â ( bday âðĨ)) |
72 | 16, 71 | mtand 815 |
. . . . . . 7
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ÂŽ ðī <<s {ðĨ}) |
73 | | ssltex1 27129 |
. . . . . . . . . 10
âĒ (ðī <<s ðĩ â ðī â V) |
74 | 73 | ad3antrrr 729 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) â ðī â V) |
75 | 74, 26 | jctir 522 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) â (ðī â V ⧠{ðĨ} â V)) |
76 | | ssltss1 27131 |
. . . . . . . . . 10
âĒ (ðī <<s ðĩ â ðī â No
) |
77 | 76 | ad3antrrr 729 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) â ðī â No
) |
78 | 9 | adantr 482 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) â ðĨ â No
) |
79 | 78 | snssd 4770 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) â {ðĨ} â No
) |
80 | | simpr 486 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) â âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) |
81 | 77, 79, 80 | 3jca 1129 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) â (ðī â No
⧠{ðĨ} â No ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ)) |
82 | | brsslt 27128 |
. . . . . . . 8
âĒ (ðī <<s {ðĨ} â ((ðī â V ⧠{ðĨ} â V) ⧠(ðī â No
⧠{ðĨ} â No ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ))) |
83 | 75, 81, 82 | sylanbrc 584 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) â ðī <<s {ðĨ}) |
84 | 72, 83 | mtand 815 |
. . . . . 6
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ÂŽ âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) |
85 | | rexnal 3104 |
. . . . . . 7
âĒ
(âðĄ â
{ðĨ} ÂŽ âðĶ â ðī ðĶ <s ðĄ â ÂŽ âðĄ â {ðĨ}âðĶ â ðī ðĶ <s ðĄ) |
86 | | ralcom 3273 |
. . . . . . 7
âĒ
(âðĄ â
{ðĨ}âðĶ â ðī ðĶ <s ðĄ â âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) |
87 | 85, 86 | xchbinx 334 |
. . . . . 6
âĒ
(âðĄ â
{ðĨ} ÂŽ âðĶ â ðī ðĶ <s ðĄ â ÂŽ âðĶ â ðī âðĄ â {ðĨ}ðĶ <s ðĄ) |
88 | 84, 87 | sylibr 233 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â âðĄ â {ðĨ} ÂŽ âðĶ â ðī ðĶ <s ðĄ) |
89 | | vex 3450 |
. . . . . 6
âĒ ðĨ â V |
90 | | breq2 5110 |
. . . . . . . 8
âĒ (ðĄ = ðĨ â (ðĶ <s ðĄ â ðĶ <s ðĨ)) |
91 | 90 | ralbidv 3175 |
. . . . . . 7
âĒ (ðĄ = ðĨ â (âðĶ â ðī ðĶ <s ðĄ â âðĶ â ðī ðĶ <s ðĨ)) |
92 | 91 | notbid 318 |
. . . . . 6
âĒ (ðĄ = ðĨ â (ÂŽ âðĶ â ðī ðĶ <s ðĄ â ÂŽ âðĶ â ðī ðĶ <s ðĨ)) |
93 | 89, 92 | rexsn 4644 |
. . . . 5
âĒ
(âðĄ â
{ðĨ} ÂŽ âðĶ â ðī ðĶ <s ðĄ â ÂŽ âðĶ â ðī ðĶ <s ðĨ) |
94 | 88, 93 | sylib 217 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ÂŽ âðĶ â ðī ðĶ <s ðĨ) |
95 | 76 | ad2antrr 725 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â ðī â No
) |
96 | 95 | sselda 3945 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðĶ â ðī) â ðĶ â No
) |
97 | | slenlt 27103 |
. . . . . . 7
âĒ ((ðĨ â
No ⧠ðĶ â
No ) â (ðĨ âĪs ðĶ â ÂŽ ðĶ <s ðĨ)) |
98 | 9, 96, 97 | syl2an2r 684 |
. . . . . 6
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) ⧠ðĶ â ðī) â (ðĨ âĪs ðĶ â ÂŽ ðĶ <s ðĨ)) |
99 | 98 | rexbidva 3174 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â (âðĶ â ðī ðĨ âĪs ðĶ â âðĶ â ðī ÂŽ ðĶ <s ðĨ)) |
100 | | rexnal 3104 |
. . . . 5
âĒ
(âðĶ â
ðī ÂŽ ðĶ <s ðĨ â ÂŽ âðĶ â ðī ðĶ <s ðĨ) |
101 | 99, 100 | bitrdi 287 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â (âðĶ â ðī ðĨ âĪs ðĶ â ÂŽ âðĶ â ðī ðĶ <s ðĨ)) |
102 | 94, 101 | mpbird 257 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ( L âð)) â âðĶ â ðī ðĨ âĪs ðĶ) |
103 | 102 | ralrimiva 3144 |
. 2
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â âðĨ â ( L âð)âðĶ â ðī ðĨ âĪs ðĶ) |
104 | 1 | onssneli 6434 |
. . . . . . . . 9
âĒ (( bday â(ðī |s ðĩ)) â ( bday
âð§) â
ÂŽ ( bday âð§) â ( bday
â(ðī |s ðĩ))) |
105 | | rightssold 27212 |
. . . . . . . . . . . . 13
âĒ ( R
âð) â ( O
â( bday âð)) |
106 | 105 | a1i 11 |
. . . . . . . . . . . 12
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ( R âð) â ( O â(
bday âð))) |
107 | 106 | sselda 3945 |
. . . . . . . . . . 11
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ð§ â ( O â(
bday âð))) |
108 | | rightssno 27214 |
. . . . . . . . . . . . . 14
âĒ ( R
âð) â No |
109 | 108 | a1i 11 |
. . . . . . . . . . . . 13
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ( R âð) â No
) |
110 | 109 | sselda 3945 |
. . . . . . . . . . . 12
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ð§ â No
) |
111 | | oldbday 27233 |
. . . . . . . . . . . 12
âĒ ((( bday âð) â On ⧠ð§ â No )
â (ð§ â ( O
â( bday âð)) â ( bday
âð§) â
( bday âð))) |
112 | 6, 110, 111 | sylancr 588 |
. . . . . . . . . . 11
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â (ð§ â ( O â(
bday âð))
â ( bday âð§) â ( bday
âð))) |
113 | 107, 112 | mpbid 231 |
. . . . . . . . . 10
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ( bday
âð§) â
( bday âð)) |
114 | | simplr 768 |
. . . . . . . . . . 11
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ð = (ðī |s ðĩ)) |
115 | 114 | fveq2d 6847 |
. . . . . . . . . 10
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ( bday
âð) = ( bday â(ðī |s ðĩ))) |
116 | 113, 115 | eleqtrd 2840 |
. . . . . . . . 9
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ( bday
âð§) â
( bday â(ðī |s ðĩ))) |
117 | 104, 116 | nsyl3 138 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ÂŽ ( bday
â(ðī |s ðĩ)) â ( bday âð§)) |
118 | 17 | ad3antrrr 729 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠{ð§} <<s ðĩ) â ( bday
â(ðī |s ðĩ)) = âĐ ( bday â {ðĄ â
No âĢ (ðī
<<s {ðĄ} ⧠{ðĄ} <<s ðĩ)})) |
119 | | sneq 4597 |
. . . . . . . . . . . . . 14
âĒ (ðĄ = ð§ â {ðĄ} = {ð§}) |
120 | 119 | breq2d 5118 |
. . . . . . . . . . . . 13
âĒ (ðĄ = ð§ â (ðī <<s {ðĄ} â ðī <<s {ð§})) |
121 | 119 | breq1d 5116 |
. . . . . . . . . . . . 13
âĒ (ðĄ = ð§ â ({ðĄ} <<s ðĩ â {ð§} <<s ðĩ)) |
122 | 120, 121 | anbi12d 632 |
. . . . . . . . . . . 12
âĒ (ðĄ = ð§ â ((ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ) â (ðī <<s {ð§} ⧠{ð§} <<s ðĩ))) |
123 | 110 | adantr 482 |
. . . . . . . . . . . 12
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠{ð§} <<s ðĩ) â ð§ â No
) |
124 | 73 | ad2antrr 725 |
. . . . . . . . . . . . . 14
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ðī â V) |
125 | | vsnex 5387 |
. . . . . . . . . . . . . . 15
âĒ {ð§} â V |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . 14
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â {ð§} â V) |
127 | 76 | ad2antrr 725 |
. . . . . . . . . . . . . 14
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ðī â No
) |
128 | 110 | snssd 4770 |
. . . . . . . . . . . . . 14
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â {ð§} â No
) |
129 | 127 | sselda 3945 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī) â ð â No
) |
130 | 37 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī) â ð â No
) |
131 | 110 | adantr 482 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī) â ð§ â No
) |
132 | 48 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
133 | 132 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . 19
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ðī <<s {(ðī |s ðĩ)}) |
134 | | ssltsepc 27135 |
. . . . . . . . . . . . . . . . . . . 20
âĒ ((ðī <<s {(ðī |s ðĩ)} ⧠ð â ðī ⧠(ðī |s ðĩ) â {(ðī |s ðĩ)}) â ð <s (ðī |s ðĩ)) |
135 | 52, 134 | mp3an3 1451 |
. . . . . . . . . . . . . . . . . . 19
âĒ ((ðī <<s {(ðī |s ðĩ)} ⧠ð â ðī) â ð <s (ðī |s ðĩ)) |
136 | 133, 135 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī) â ð <s (ðī |s ðĩ)) |
137 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī) â ð = (ðī |s ðĩ)) |
138 | 136, 137 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī) â ð <s ð) |
139 | | rightval 27197 |
. . . . . . . . . . . . . . . . . . . . . 22
âĒ ( R
âð) = {ð§ â ( O â( bday âð)) âĢ ð <s ð§} |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ( R âð) = {ð§ â ( O â(
bday âð))
âĢ ð <s ð§}) |
141 | 140 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . 20
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â (ð§ â ( R âð) â ð§ â {ð§ â ( O â(
bday âð))
âĢ ð <s ð§})) |
142 | | rabid 3428 |
. . . . . . . . . . . . . . . . . . . 20
âĒ (ð§ â {ð§ â ( O â(
bday âð))
âĢ ð <s ð§} â (ð§ â ( O â(
bday âð))
⧠ð <s ð§)) |
143 | 141, 142 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . 19
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â (ð§ â ( R âð) â (ð§ â ( O â(
bday âð))
⧠ð <s ð§))) |
144 | 143 | simplbda 501 |
. . . . . . . . . . . . . . . . . 18
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ð <s ð§) |
145 | 144 | adantr 482 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī) â ð <s ð§) |
146 | 129, 130,
131, 138, 145 | slttrd 27110 |
. . . . . . . . . . . . . . . 16
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī) â ð <s ð§) |
147 | 146 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī ⧠ð â {ð§}) â ð <s ð§) |
148 | | velsn 4603 |
. . . . . . . . . . . . . . . . 17
âĒ (ð â {ð§} â ð = ð§) |
149 | | breq2 5110 |
. . . . . . . . . . . . . . . . 17
âĒ (ð = ð§ â (ð <s ð â ð <s ð§)) |
150 | 148, 149 | sylbi 216 |
. . . . . . . . . . . . . . . 16
âĒ (ð â {ð§} â (ð <s ð â ð <s ð§)) |
151 | 150 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . 15
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī ⧠ð â {ð§}) â (ð <s ð â ð <s ð§)) |
152 | 147, 151 | mpbird 257 |
. . . . . . . . . . . . . 14
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ð â ðī ⧠ð â {ð§}) â ð <s ð) |
153 | 124, 126,
127, 128, 152 | ssltd 27134 |
. . . . . . . . . . . . 13
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ðī <<s {ð§}) |
154 | 153 | anim1i 616 |
. . . . . . . . . . . 12
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠{ð§} <<s ðĩ) â (ðī <<s {ð§} ⧠{ð§} <<s ðĩ)) |
155 | 122, 123,
154 | elrabd 3648 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠{ð§} <<s ðĩ) â ð§ â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) |
156 | | fnfvima 7184 |
. . . . . . . . . . 11
âĒ (( bday Fn No ⧠{ðĄ â
No âĢ (ðī
<<s {ðĄ} ⧠{ðĄ} <<s ðĩ)} â No
⧠ð§ â {ðĄ â
No âĢ (ðī
<<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) â ( bday
âð§) â
( bday â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)})) |
157 | 19, 20, 155, 156 | mp3an12i 1466 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠{ð§} <<s ðĩ) â ( bday
âð§) â
( bday â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)})) |
158 | | intss1 4925 |
. . . . . . . . . 10
âĒ (( bday âð§) â ( bday
â {ðĄ â No âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) â âĐ
( bday â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) â ( bday
âð§)) |
159 | 157, 158 | syl 17 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠{ð§} <<s ðĩ) â âĐ ( bday â {ðĄ â No
âĢ (ðī <<s {ðĄ} ⧠{ðĄ} <<s ðĩ)}) â ( bday
âð§)) |
160 | 118, 159 | eqsstrd 3983 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠{ð§} <<s ðĩ) â ( bday
â(ðī |s ðĩ)) â ( bday âð§)) |
161 | 117, 160 | mtand 815 |
. . . . . . 7
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ÂŽ {ð§} <<s ðĩ) |
162 | 28 | ad3antrrr 729 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) â ðĩ â V) |
163 | 162, 125 | jctil 521 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) â ({ð§} â V ⧠ðĩ â V)) |
164 | 128 | adantr 482 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) â {ð§} â No
) |
165 | 31 | ad3antrrr 729 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) â ðĩ â No
) |
166 | | simpr 486 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) â âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) |
167 | 164, 165,
166 | 3jca 1129 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) â ({ð§} â No
⧠ðĩ â No ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ)) |
168 | | brsslt 27128 |
. . . . . . . 8
âĒ ({ð§} <<s ðĩ â (({ð§} â V ⧠ðĩ â V) ⧠({ð§} â No
⧠ðĩ â No ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ))) |
169 | 163, 167,
168 | sylanbrc 584 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) â {ð§} <<s ðĩ) |
170 | 161, 169 | mtand 815 |
. . . . . 6
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ÂŽ âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) |
171 | | rexnal 3104 |
. . . . . 6
âĒ
(âðĄ â
{ð§} ÂŽ âðĪ â ðĩ ðĄ <s ðĪ â ÂŽ âðĄ â {ð§}âðĪ â ðĩ ðĄ <s ðĪ) |
172 | 170, 171 | sylibr 233 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â âðĄ â {ð§} ÂŽ âðĪ â ðĩ ðĄ <s ðĪ) |
173 | | vex 3450 |
. . . . . 6
âĒ ð§ â V |
174 | | breq1 5109 |
. . . . . . . 8
âĒ (ðĄ = ð§ â (ðĄ <s ðĪ â ð§ <s ðĪ)) |
175 | 174 | ralbidv 3175 |
. . . . . . 7
âĒ (ðĄ = ð§ â (âðĪ â ðĩ ðĄ <s ðĪ â âðĪ â ðĩ ð§ <s ðĪ)) |
176 | 175 | notbid 318 |
. . . . . 6
âĒ (ðĄ = ð§ â (ÂŽ âðĪ â ðĩ ðĄ <s ðĪ â ÂŽ âðĪ â ðĩ ð§ <s ðĪ)) |
177 | 173, 176 | rexsn 4644 |
. . . . 5
âĒ
(âðĄ â
{ð§} ÂŽ âðĪ â ðĩ ðĄ <s ðĪ â ÂŽ âðĪ â ðĩ ð§ <s ðĪ) |
178 | 172, 177 | sylib 217 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ÂŽ âðĪ â ðĩ ð§ <s ðĪ) |
179 | 31 | ad2antrr 725 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â ðĩ â No
) |
180 | 179 | sselda 3945 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ðĪ â ðĩ) â ðĪ â No
) |
181 | 110 | adantr 482 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ðĪ â ðĩ) â ð§ â No
) |
182 | | slenlt 27103 |
. . . . . . 7
âĒ ((ðĪ â
No ⧠ð§ â
No ) â (ðĪ âĪs ð§ â ÂŽ ð§ <s ðĪ)) |
183 | 180, 181,
182 | syl2anc 585 |
. . . . . 6
âĒ ((((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) ⧠ðĪ â ðĩ) â (ðĪ âĪs ð§ â ÂŽ ð§ <s ðĪ)) |
184 | 183 | rexbidva 3174 |
. . . . 5
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â (âðĪ â ðĩ ðĪ âĪs ð§ â âðĪ â ðĩ ÂŽ ð§ <s ðĪ)) |
185 | | rexnal 3104 |
. . . . 5
âĒ
(âðĪ â
ðĩ ÂŽ ð§ <s ðĪ â ÂŽ âðĪ â ðĩ ð§ <s ðĪ) |
186 | 184, 185 | bitrdi 287 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â (âðĪ â ðĩ ðĪ âĪs ð§ â ÂŽ âðĪ â ðĩ ð§ <s ðĪ)) |
187 | 178, 186 | mpbird 257 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ( R âð)) â âðĪ â ðĩ ðĪ âĪs ð§) |
188 | 187 | ralrimiva 3144 |
. 2
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â âð§ â ( R âð)âðĪ â ðĩ ðĪ âĪs ð§) |
189 | 103, 188 | jca 513 |
1
âĒ ((ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â (âðĨ â ( L âð)âðĶ â ðī ðĨ âĪs ðĶ ⧠âð§ â ( R âð)âðĪ â ðĩ ðĪ âĪs ð§)) |