Step | Hyp | Ref
| Expression |
1 | | oveq1 7418 |
. . . . . . 7
âĒ (ðĨ = ðĨð â (ðĨ +s ð§) = (ðĨð +s ð§)) |
2 | 1 | breq2d 5160 |
. . . . . 6
âĒ (ðĨ = ðĨð â ((ðĶ +s ð§) <s (ðĨ +s ð§) â (ðĶ +s ð§) <s (ðĨð +s ð§))) |
3 | | breq2 5152 |
. . . . . 6
âĒ (ðĨ = ðĨð â (ðĶ <s ðĨ â ðĶ <s ðĨð)) |
4 | 2, 3 | imbi12d 344 |
. . . . 5
âĒ (ðĨ = ðĨð â (((ðĶ +s ð§) <s (ðĨ +s ð§) â ðĶ <s ðĨ) â ((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð))) |
5 | | oveq1 7418 |
. . . . . . 7
âĒ (ðĶ = ðĶð â (ðĶ +s ð§) = (ðĶð +s ð§)) |
6 | 5 | breq1d 5158 |
. . . . . 6
âĒ (ðĶ = ðĶð â ((ðĶ +s ð§) <s (ðĨð +s ð§) â (ðĶð +s ð§) <s (ðĨð +s ð§))) |
7 | | breq1 5151 |
. . . . . 6
âĒ (ðĶ = ðĶð â (ðĶ <s ðĨð â ðĶð <s ðĨð)) |
8 | 6, 7 | imbi12d 344 |
. . . . 5
âĒ (ðĶ = ðĶð â (((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) â ((ðĶð
+s ð§) <s
(ðĨð
+s ð§) â
ðĶð <s
ðĨð))) |
9 | | oveq2 7419 |
. . . . . . 7
âĒ (ð§ = ð§ð â (ðĶð
+s ð§) = (ðĶð
+s ð§ð)) |
10 | | oveq2 7419 |
. . . . . . 7
âĒ (ð§ = ð§ð â (ðĨð
+s ð§) = (ðĨð
+s ð§ð)) |
11 | 9, 10 | breq12d 5161 |
. . . . . 6
âĒ (ð§ = ð§ð â ((ðĶð
+s ð§) <s
(ðĨð
+s ð§) â
(ðĶð
+s ð§ð) <s (ðĨð
+s ð§ð))) |
12 | 11 | imbi1d 341 |
. . . . 5
âĒ (ð§ = ð§ð â (((ðĶð
+s ð§) <s
(ðĨð
+s ð§) â
ðĶð <s
ðĨð)
â ((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð))) |
13 | | oveq1 7418 |
. . . . . . 7
âĒ (ðĨ = ðĨð â (ðĨ +s ð§ð) = (ðĨð
+s ð§ð)) |
14 | 13 | breq2d 5160 |
. . . . . 6
âĒ (ðĨ = ðĨð â ((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
(ðĶð
+s ð§ð) <s (ðĨð
+s ð§ð))) |
15 | | breq2 5152 |
. . . . . 6
âĒ (ðĨ = ðĨð â (ðĶð <s ðĨ â ðĶð <s ðĨð)) |
16 | 14, 15 | imbi12d 344 |
. . . . 5
âĒ (ðĨ = ðĨð â (((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) â ((ðĶð
+s ð§ð) <s (ðĨð
+s ð§ð) â ðĶð <s ðĨð))) |
17 | | oveq1 7418 |
. . . . . . 7
âĒ (ðĶ = ðĶð â (ðĶ +s ð§ð) = (ðĶð
+s ð§ð)) |
18 | 17 | breq1d 5158 |
. . . . . 6
âĒ (ðĶ = ðĶð â ((ðĶ +s ð§ð) <s
(ðĨ +s ð§ð) â
(ðĶð
+s ð§ð) <s (ðĨ +s ð§ð))) |
19 | | breq1 5151 |
. . . . . 6
âĒ (ðĶ = ðĶð â (ðĶ <s ðĨ â ðĶð <s ðĨ)) |
20 | 18, 19 | imbi12d 344 |
. . . . 5
âĒ (ðĶ = ðĶð â (((ðĶ +s ð§ð) <s
(ðĨ +s ð§ð) â
ðĶ <s ðĨ) â ((ðĶð +s ð§ð) <s
(ðĨ +s ð§ð) â
ðĶð <s
ðĨ))) |
21 | 17 | breq1d 5158 |
. . . . . 6
âĒ (ðĶ = ðĶð â ((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â (ðĶð
+s ð§ð) <s (ðĨð
+s ð§ð))) |
22 | 21, 7 | imbi12d 344 |
. . . . 5
âĒ (ðĶ = ðĶð â (((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð) â ((ðĶð
+s ð§ð) <s (ðĨð
+s ð§ð) â ðĶð <s ðĨð))) |
23 | | oveq2 7419 |
. . . . . . 7
âĒ (ð§ = ð§ð â (ðĨ +s ð§) = (ðĨ +s ð§ð)) |
24 | 9, 23 | breq12d 5161 |
. . . . . 6
âĒ (ð§ = ð§ð â ((ðĶð
+s ð§) <s
(ðĨ +s ð§) â (ðĶð +s ð§ð) <s
(ðĨ +s ð§ð))) |
25 | 24 | imbi1d 341 |
. . . . 5
âĒ (ð§ = ð§ð â (((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ) â ((ðĶð +s ð§ð) <s
(ðĨ +s ð§ð) â
ðĶð <s
ðĨ))) |
26 | | oveq1 7418 |
. . . . . . 7
âĒ (ðĨ = ðī â (ðĨ +s ð§) = (ðī +s ð§)) |
27 | 26 | breq2d 5160 |
. . . . . 6
âĒ (ðĨ = ðī â ((ðĶ +s ð§) <s (ðĨ +s ð§) â (ðĶ +s ð§) <s (ðī +s ð§))) |
28 | | breq2 5152 |
. . . . . 6
âĒ (ðĨ = ðī â (ðĶ <s ðĨ â ðĶ <s ðī)) |
29 | 27, 28 | imbi12d 344 |
. . . . 5
âĒ (ðĨ = ðī â (((ðĶ +s ð§) <s (ðĨ +s ð§) â ðĶ <s ðĨ) â ((ðĶ +s ð§) <s (ðī +s ð§) â ðĶ <s ðī))) |
30 | | oveq1 7418 |
. . . . . . 7
âĒ (ðĶ = ðĩ â (ðĶ +s ð§) = (ðĩ +s ð§)) |
31 | 30 | breq1d 5158 |
. . . . . 6
âĒ (ðĶ = ðĩ â ((ðĶ +s ð§) <s (ðī +s ð§) â (ðĩ +s ð§) <s (ðī +s ð§))) |
32 | | breq1 5151 |
. . . . . 6
âĒ (ðĶ = ðĩ â (ðĶ <s ðī â ðĩ <s ðī)) |
33 | 31, 32 | imbi12d 344 |
. . . . 5
âĒ (ðĶ = ðĩ â (((ðĶ +s ð§) <s (ðī +s ð§) â ðĶ <s ðī) â ((ðĩ +s ð§) <s (ðī +s ð§) â ðĩ <s ðī))) |
34 | | oveq2 7419 |
. . . . . . 7
âĒ (ð§ = ðķ â (ðĩ +s ð§) = (ðĩ +s ðķ)) |
35 | | oveq2 7419 |
. . . . . . 7
âĒ (ð§ = ðķ â (ðī +s ð§) = (ðī +s ðķ)) |
36 | 34, 35 | breq12d 5161 |
. . . . . 6
âĒ (ð§ = ðķ â ((ðĩ +s ð§) <s (ðī +s ð§) â (ðĩ +s ðķ) <s (ðī +s ðķ))) |
37 | 36 | imbi1d 341 |
. . . . 5
âĒ (ð§ = ðķ â (((ðĩ +s ð§) <s (ðī +s ð§) â ðĩ <s ðī) â ((ðĩ +s ðķ) <s (ðī +s ðķ) â ðĩ <s ðī))) |
38 | | simp2 1137 |
. . . . . . . . . . . 12
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ðĶ â No ) |
39 | | simp3 1138 |
. . . . . . . . . . . 12
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ð§ â No ) |
40 | 38, 39 | addscut 27688 |
. . . . . . . . . . 11
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ((ðĶ +s
ð§) â No ⧠({ð âĢ âðĶðŋ â ( L âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s {(ðĶ +s ð§)} ⧠{(ðĶ +s ð§)} <<s ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)}))) |
41 | | simp2 1137 |
. . . . . . . . . . 11
âĒ (((ðĶ +s ð§) â
No ⧠({ð
âĢ âðĶðŋ â ( L âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s {(ðĶ +s ð§)} ⧠{(ðĶ +s ð§)} <<s ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})) â ({ð âĢ âðĶðŋ â ( L
âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s {(ðĶ +s ð§)}) |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ({ð âĢ
âðĶðŋ
â ( L âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s {(ðĶ +s ð§)}) |
43 | 40 | simp3d 1144 |
. . . . . . . . . 10
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â {(ðĶ +s
ð§)} <<s ({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})) |
44 | | ovex 7444 |
. . . . . . . . . . . 12
âĒ (ðĶ +s ð§) â V |
45 | 44 | snnz 4780 |
. . . . . . . . . . 11
âĒ {(ðĶ +s ð§)} â â
|
46 | | sslttr 27533 |
. . . . . . . . . . 11
âĒ ((({ð âĢ âðĶðŋ â ( L
âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s {(ðĶ +s ð§)} ⧠{(ðĶ +s ð§)} <<s ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)}) ⧠{(ðĶ +s ð§)} â â
) â ({ð âĢ âðĶðŋ â ( L
âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s ({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})) |
47 | 45, 46 | mp3an3 1450 |
. . . . . . . . . 10
âĒ ((({ð âĢ âðĶðŋ â ( L
âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s {(ðĶ +s ð§)} ⧠{(ðĶ +s ð§)} <<s ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})) â ({ð âĢ âðĶðŋ â ( L
âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s ({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})) |
48 | 42, 43, 47 | syl2anc 584 |
. . . . . . . . 9
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ({ð âĢ
âðĶðŋ
â ( L âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s ({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})) |
49 | | simp1 1136 |
. . . . . . . . . . . 12
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ðĨ â No ) |
50 | 49, 39 | addscut 27688 |
. . . . . . . . . . 11
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ((ðĨ +s
ð§) â No ⧠({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s {(ðĨ +s ð§)} ⧠{(ðĨ +s ð§)} <<s ({ð âĢ âðĨð
â ( R âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)}))) |
51 | | simp2 1137 |
. . . . . . . . . . 11
âĒ (((ðĨ +s ð§) â
No ⧠({ð
âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s {(ðĨ +s ð§)} ⧠{(ðĨ +s ð§)} <<s ({ð âĢ âðĨð
â ( R âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)})) â ({ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s {(ðĨ +s ð§)}) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ({ð âĢ
âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s {(ðĨ +s ð§)}) |
53 | 50 | simp3d 1144 |
. . . . . . . . . 10
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â {(ðĨ +s
ð§)} <<s ({ð âĢ âðĨð
â ( R
âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)})) |
54 | | ovex 7444 |
. . . . . . . . . . . 12
âĒ (ðĨ +s ð§) â V |
55 | 54 | snnz 4780 |
. . . . . . . . . . 11
âĒ {(ðĨ +s ð§)} â â
|
56 | | sslttr 27533 |
. . . . . . . . . . 11
âĒ ((({ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s {(ðĨ +s ð§)} ⧠{(ðĨ +s ð§)} <<s ({ð âĢ âðĨð
â ( R âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)}) ⧠{(ðĨ +s ð§)} â â
) â ({ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s ({ð âĢ âðĨð
â ( R
âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)})) |
57 | 55, 56 | mp3an3 1450 |
. . . . . . . . . 10
âĒ ((({ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s {(ðĨ +s ð§)} ⧠{(ðĨ +s ð§)} <<s ({ð âĢ âðĨð
â ( R âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)})) â ({ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s ({ð âĢ âðĨð
â ( R
âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)})) |
58 | 52, 53, 57 | syl2anc 584 |
. . . . . . . . 9
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ({ð âĢ
âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s ({ð âĢ âðĨð
â ( R
âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)})) |
59 | | addsval2 27673 |
. . . . . . . . . 10
âĒ ((ðĶ â
No ⧠ð§ â
No ) â (ðĶ +s ð§) = (({ð âĢ âðĶðŋ â ( L âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) |s ({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)}))) |
60 | 59 | 3adant1 1130 |
. . . . . . . . 9
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â (ðĶ +s
ð§) = (({ð âĢ âðĶðŋ â ( L âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) |s ({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)}))) |
61 | | addsval2 27673 |
. . . . . . . . . 10
âĒ ((ðĨ â
No ⧠ð§ â
No ) â (ðĨ +s ð§) = (({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) |s ({ð âĢ âðĨð
â ( R
âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)}))) |
62 | 61 | 3adant2 1131 |
. . . . . . . . 9
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â (ðĨ +s
ð§) = (({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) |s ({ð âĢ âðĨð
â ( R
âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)}))) |
63 | | sltrec 27546 |
. . . . . . . . 9
âĒ
(((({ð âĢ
âðĶðŋ
â ( L âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) <<s ({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)}) ⧠({ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) <<s ({ð âĢ âðĨð
â ( R
âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)})) ⧠((ðĶ +s ð§) = (({ð âĢ âðĶðŋ â ( L âðĶ)ð = (ðĶðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĶ +s ð§ðŋ)}) |s ({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})) ⧠(ðĨ +s ð§) = (({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)}) |s ({ð âĢ âðĨð
â ( R
âðĨ)ð = (ðĨð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĨ +s ð§ð
)})))) â ((ðĶ +s ð§) <s (ðĨ +s ð§) â (âð â ({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)})(ðĶ +s ð§) âĪs ð âĻ âð â ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})ð âĪs (ðĨ +s ð§)))) |
64 | 48, 58, 60, 62, 63 | syl22anc 837 |
. . . . . . . 8
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â ((ðĶ +s
ð§) <s (ðĨ +s ð§) â (âð â ({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)})(ðĶ +s ð§) âĪs ð âĻ âð â ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})ð âĪs (ðĨ +s ð§)))) |
65 | 64 | adantr 481 |
. . . . . . 7
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â ((ðĶ +s ð§) <s (ðĨ +s ð§) â (âð â ({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)})(ðĶ +s ð§) âĪs ð âĻ âð â ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})ð âĪs (ðĨ +s ð§)))) |
66 | | rexun 4190 |
. . . . . . . . . 10
âĒ
(âð â
({ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)})(ðĶ +s ð§) âĪs ð â (âð â {ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} (ðĶ +s ð§) âĪs ð âĻ âð â {ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)} (ðĶ +s ð§) âĪs ð)) |
67 | | eqeq1 2736 |
. . . . . . . . . . . . . 14
âĒ (ð = ð â (ð = (ðĨðŋ +s ð§) â ð = (ðĨðŋ +s ð§))) |
68 | 67 | rexbidv 3178 |
. . . . . . . . . . . . 13
âĒ (ð = ð â (âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§) â âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§))) |
69 | 68 | rexab 3690 |
. . . . . . . . . . . 12
âĒ
(âð â
{ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} (ðĶ +s ð§) âĪs ð â âð(âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð)) |
70 | | rexcom4 3285 |
. . . . . . . . . . . . . 14
âĒ
(âðĨðŋ â ( L âðĨ)âð(ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð) â âðâðĨðŋ â ( L âðĨ)(ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð)) |
71 | | r19.41v 3188 |
. . . . . . . . . . . . . . 15
âĒ
(âðĨðŋ â ( L âðĨ)(ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð) â (âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð)) |
72 | 71 | exbii 1850 |
. . . . . . . . . . . . . 14
âĒ
(âðâðĨðŋ â ( L âðĨ)(ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð) â âð(âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð)) |
73 | 70, 72 | bitri 274 |
. . . . . . . . . . . . 13
âĒ
(âðĨðŋ â ( L âðĨ)âð(ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð) â âð(âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð)) |
74 | | ovex 7444 |
. . . . . . . . . . . . . . 15
âĒ (ðĨðŋ
+s ð§) â
V |
75 | | breq2 5152 |
. . . . . . . . . . . . . . 15
âĒ (ð = (ðĨðŋ +s ð§) â ((ðĶ +s ð§) âĪs ð â (ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) |
76 | 74, 75 | ceqsexv 3525 |
. . . . . . . . . . . . . 14
âĒ
(âð(ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð) â (ðĶ +s ð§) âĪs (ðĨðŋ +s ð§)) |
77 | 76 | rexbii 3094 |
. . . . . . . . . . . . 13
âĒ
(âðĨðŋ â ( L âðĨ)âð(ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð) â âðĨðŋ â ( L âðĨ)(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§)) |
78 | 73, 77 | bitr3i 276 |
. . . . . . . . . . . 12
âĒ
(âð(âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§) ⧠(ðĶ +s ð§) âĪs ð) â âðĨðŋ â ( L âðĨ)(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§)) |
79 | 69, 78 | bitri 274 |
. . . . . . . . . . 11
âĒ
(âð â
{ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} (ðĶ +s ð§) âĪs ð â âðĨðŋ â ( L âðĨ)(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§)) |
80 | | eqeq1 2736 |
. . . . . . . . . . . . . 14
âĒ (ð = ð â (ð = (ðĨ +s ð§ðŋ) â ð = (ðĨ +s ð§ðŋ))) |
81 | 80 | rexbidv 3178 |
. . . . . . . . . . . . 13
âĒ (ð = ð â (âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ) â âð§ðŋ â ( L
âð§)ð = (ðĨ +s ð§ðŋ))) |
82 | 81 | rexab 3690 |
. . . . . . . . . . . 12
âĒ
(âð â
{ð âĢ âð§ðŋ â ( L
âð§)ð = (ðĨ +s ð§ðŋ)} (ðĶ +s ð§) âĪs ð â âð(âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð)) |
83 | | rexcom4 3285 |
. . . . . . . . . . . . . 14
âĒ
(âð§ðŋ â ( L âð§)âð(ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð) â âðâð§ðŋ â ( L âð§)(ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð)) |
84 | | r19.41v 3188 |
. . . . . . . . . . . . . . 15
âĒ
(âð§ðŋ â ( L âð§)(ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð) â (âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð)) |
85 | 84 | exbii 1850 |
. . . . . . . . . . . . . 14
âĒ
(âðâð§ðŋ â ( L âð§)(ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð) â âð(âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð)) |
86 | 83, 85 | bitri 274 |
. . . . . . . . . . . . 13
âĒ
(âð§ðŋ â ( L âð§)âð(ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð) â âð(âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð)) |
87 | | ovex 7444 |
. . . . . . . . . . . . . . 15
âĒ (ðĨ +s ð§ðŋ) â
V |
88 | | breq2 5152 |
. . . . . . . . . . . . . . 15
âĒ (ð = (ðĨ +s ð§ðŋ) â ((ðĶ +s ð§) âĪs ð â (ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) |
89 | 87, 88 | ceqsexv 3525 |
. . . . . . . . . . . . . 14
âĒ
(âð(ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð) â (ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ)) |
90 | 89 | rexbii 3094 |
. . . . . . . . . . . . 13
âĒ
(âð§ðŋ â ( L âð§)âð(ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð) â âð§ðŋ â ( L âð§)(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ)) |
91 | 86, 90 | bitr3i 276 |
. . . . . . . . . . . 12
âĒ
(âð(âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ) ⧠(ðĶ +s ð§) âĪs ð) â âð§ðŋ â ( L âð§)(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ)) |
92 | 82, 91 | bitri 274 |
. . . . . . . . . . 11
âĒ
(âð â
{ð âĢ âð§ðŋ â ( L
âð§)ð = (ðĨ +s ð§ðŋ)} (ðĶ +s ð§) âĪs ð â âð§ðŋ â ( L âð§)(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ)) |
93 | 79, 92 | orbi12i 913 |
. . . . . . . . . 10
âĒ
((âð â
{ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} (ðĶ +s ð§) âĪs ð âĻ âð â {ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)} (ðĶ +s ð§) âĪs ð) â (âðĨðŋ â ( L âðĨ)(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§) âĻ âð§ðŋ â ( L âð§)(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) |
94 | 66, 93 | bitri 274 |
. . . . . . . . 9
âĒ
(âð â
({ð âĢ âðĨðŋ â ( L
âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)})(ðĶ +s ð§) âĪs ð â (âðĨðŋ â ( L âðĨ)(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§) âĻ âð§ðŋ â ( L âð§)(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) |
95 | | simpll2 1213 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â ðĶ â No
) |
96 | | leftssno 27600 |
. . . . . . . . . . . . . . 15
âĒ ( L
âðĨ) â No |
97 | 96 | sseli 3978 |
. . . . . . . . . . . . . 14
âĒ (ðĨðŋ â ( L
âðĨ) â ðĨðŋ â
No ) |
98 | 97 | adantr 481 |
. . . . . . . . . . . . 13
âĒ ((ðĨðŋ â ( L
âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§)) â ðĨðŋ â No ) |
99 | 98 | adantl 482 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â ðĨðŋ â No ) |
100 | | simpll1 1212 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â ðĨ â No
) |
101 | | simprr 771 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â (ðĶ +s ð§) âĪs (ðĨðŋ +s ð§)) |
102 | | simpll3 1214 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â ð§ â No
) |
103 | | sleadd1im 27697 |
. . . . . . . . . . . . . 14
âĒ ((ðĶ â
No ⧠ðĨðŋ â No ⧠ð§ â No )
â ((ðĶ +s
ð§) âĪs (ðĨðŋ
+s ð§) â
ðĶ âĪs ðĨðŋ)) |
104 | 95, 99, 102, 103 | syl3anc 1371 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â ((ðĶ +s ð§) âĪs (ðĨðŋ +s ð§) â ðĶ âĪs ðĨðŋ)) |
105 | 101, 104 | mpd 15 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â ðĶ âĪs ðĨðŋ) |
106 | | leftval 27583 |
. . . . . . . . . . . . . . . 16
âĒ ( L
âðĨ) = {ðĨðŋ â ( O
â( bday âðĨ)) âĢ ðĨðŋ <s ðĨ} |
107 | 106 | reqabi 3454 |
. . . . . . . . . . . . . . 15
âĒ (ðĨðŋ â ( L
âðĨ) â (ðĨðŋ â ( O
â( bday âðĨ)) ⧠ðĨðŋ <s ðĨ)) |
108 | 107 | simprbi 497 |
. . . . . . . . . . . . . 14
âĒ (ðĨðŋ â ( L
âðĨ) â ðĨðŋ <s ðĨ) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . 13
âĒ ((ðĨðŋ â ( L
âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§)) â ðĨðŋ <s ðĨ) |
110 | 109 | adantl 482 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â ðĨðŋ <s ðĨ) |
111 | 95, 99, 100, 105, 110 | slelttrd 27488 |
. . . . . . . . . . 11
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĨðŋ â ( L âðĨ) ⧠(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§))) â ðĶ <s ðĨ) |
112 | 111 | rexlimdvaa 3156 |
. . . . . . . . . 10
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â (âðĨðŋ â ( L âðĨ)(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§) â ðĶ <s ðĨ)) |
113 | | simpll2 1213 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ðĶ â
No ) |
114 | | leftssno 27600 |
. . . . . . . . . . . . . . . . 17
âĒ ( L
âð§) â No |
115 | 114 | sseli 3978 |
. . . . . . . . . . . . . . . 16
âĒ (ð§ðŋ â ( L
âð§) â ð§ðŋ â
No ) |
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . 15
âĒ ((ð§ðŋ â ( L
âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ)) â ð§ðŋ â
No ) |
117 | 116 | adantl 482 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ð§ðŋ â
No ) |
118 | 113, 117 | addscld 27690 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â (ðĶ +s ð§ðŋ) â
No ) |
119 | | simpll3 1214 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ð§ â
No ) |
120 | 113, 119 | addscld 27690 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â (ðĶ +s ð§) â
No ) |
121 | | simpll1 1212 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ðĨ â
No ) |
122 | 121, 117 | addscld 27690 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â (ðĨ +s ð§ðŋ) â
No ) |
123 | | leftval 27583 |
. . . . . . . . . . . . . . . . . 18
âĒ ( L
âð§) = {ð§ðŋ â ( O
â( bday âð§)) âĢ ð§ðŋ <s ð§} |
124 | 123 | reqabi 3454 |
. . . . . . . . . . . . . . . . 17
âĒ (ð§ðŋ â ( L
âð§) â (ð§ðŋ â ( O
â( bday âð§)) ⧠ð§ðŋ <s ð§)) |
125 | 124 | simprbi 497 |
. . . . . . . . . . . . . . . 16
âĒ (ð§ðŋ â ( L
âð§) â ð§ðŋ <s ð§) |
126 | 125 | adantr 481 |
. . . . . . . . . . . . . . 15
âĒ ((ð§ðŋ â ( L
âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ)) â ð§ðŋ <s ð§) |
127 | 126 | adantl 482 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ð§ðŋ <s ð§) |
128 | | sltadd2im 27696 |
. . . . . . . . . . . . . . 15
âĒ ((ð§ðŋ â
No ⧠ð§ â No
⧠ðĶ â No ) â (ð§ðŋ <s ð§ â (ðĶ +s ð§ðŋ) <s (ðĶ +s ð§))) |
129 | 117, 119,
113, 128 | syl3anc 1371 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â (ð§ðŋ <s ð§ â (ðĶ +s ð§ðŋ) <s (ðĶ +s ð§))) |
130 | 127, 129 | mpd 15 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â (ðĶ +s ð§ðŋ) <s
(ðĶ +s ð§)) |
131 | | simprr 771 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â (ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ)) |
132 | 118, 120,
122, 130, 131 | sltletrd 27487 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â (ðĶ +s ð§ðŋ) <s
(ðĨ +s ð§ðŋ)) |
133 | | oveq2 7419 |
. . . . . . . . . . . . . . 15
âĒ (ð§ð = ð§ðŋ â
(ðĶ +s ð§ð) = (ðĶ +s ð§ðŋ)) |
134 | | oveq2 7419 |
. . . . . . . . . . . . . . 15
âĒ (ð§ð = ð§ðŋ â
(ðĨ +s ð§ð) = (ðĨ +s ð§ðŋ)) |
135 | 133, 134 | breq12d 5161 |
. . . . . . . . . . . . . 14
âĒ (ð§ð = ð§ðŋ â
((ðĶ +s ð§ð) <s
(ðĨ +s ð§ð) â
(ðĶ +s ð§ðŋ) <s
(ðĨ +s ð§ðŋ))) |
136 | 135 | imbi1d 341 |
. . . . . . . . . . . . 13
âĒ (ð§ð = ð§ðŋ â
(((ðĶ +s ð§ð) <s
(ðĨ +s ð§ð) â
ðĶ <s ðĨ) â ((ðĶ +s ð§ðŋ) <s (ðĨ +s ð§ðŋ) â
ðĶ <s ðĨ))) |
137 | | simplr3 1217 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨ +s ð§ð) â
ðĶ <s ðĨ)) |
138 | | simprl 769 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ð§ðŋ â ( L
âð§)) |
139 | | elun1 4176 |
. . . . . . . . . . . . . 14
âĒ (ð§ðŋ â ( L
âð§) â ð§ðŋ â (( L
âð§) ⊠( R
âð§))) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ð§ðŋ â (( L
âð§) ⊠( R
âð§))) |
141 | 136, 137,
140 | rspcdva 3613 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ((ðĶ +s ð§ðŋ) <s
(ðĨ +s ð§ðŋ) â
ðĶ <s ðĨ)) |
142 | 132, 141 | mpd 15 |
. . . . . . . . . . 11
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ðŋ â ( L âð§) ⧠(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ))) â ðĶ <s ðĨ) |
143 | 142 | rexlimdvaa 3156 |
. . . . . . . . . 10
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â (âð§ðŋ â ( L âð§)(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ) â ðĶ <s ðĨ)) |
144 | 112, 143 | jaod 857 |
. . . . . . . . 9
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â ((âðĨðŋ â ( L âðĨ)(ðĶ +s ð§) âĪs (ðĨðŋ +s ð§) âĻ âð§ðŋ â ( L âð§)(ðĶ +s ð§) âĪs (ðĨ +s ð§ðŋ)) â ðĶ <s ðĨ)) |
145 | 94, 144 | biimtrid 241 |
. . . . . . . 8
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â (âð â ({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)})(ðĶ +s ð§) âĪs ð â ðĶ <s ðĨ)) |
146 | | rexun 4190 |
. . . . . . . . . 10
âĒ
(âð â
({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})ð âĪs (ðĨ +s ð§) â (âð â {ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)}ð âĪs (ðĨ +s ð§) âĻ âð â {ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)}ð âĪs (ðĨ +s ð§))) |
147 | | eqeq1 2736 |
. . . . . . . . . . . . . 14
âĒ (ð = ð â (ð = (ðĶð
+s ð§) â ð = (ðĶð
+s ð§))) |
148 | 147 | rexbidv 3178 |
. . . . . . . . . . . . 13
âĒ (ð = ð â (âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§) â âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§))) |
149 | 148 | rexab 3690 |
. . . . . . . . . . . 12
âĒ
(âð â
{ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)}ð âĪs (ðĨ +s ð§) â âð(âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§))) |
150 | | rexcom4 3285 |
. . . . . . . . . . . . . 14
âĒ
(âðĶð
â ( R âðĶ)âð(ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§)) â âðâðĶð
â ( R âðĶ)(ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§))) |
151 | | r19.41v 3188 |
. . . . . . . . . . . . . . 15
âĒ
(âðĶð
â ( R âðĶ)(ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§)) â (âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§))) |
152 | 151 | exbii 1850 |
. . . . . . . . . . . . . 14
âĒ
(âðâðĶð
â ( R âðĶ)(ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§)) â âð(âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§))) |
153 | 150, 152 | bitri 274 |
. . . . . . . . . . . . 13
âĒ
(âðĶð
â ( R âðĶ)âð(ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§)) â âð(âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§))) |
154 | | ovex 7444 |
. . . . . . . . . . . . . . 15
âĒ (ðĶð
+s ð§) â
V |
155 | | breq1 5151 |
. . . . . . . . . . . . . . 15
âĒ (ð = (ðĶð
+s ð§) â (ð âĪs (ðĨ +s ð§) â (ðĶð
+s ð§) âĪs (ðĨ +s ð§))) |
156 | 154, 155 | ceqsexv 3525 |
. . . . . . . . . . . . . 14
âĒ
(âð(ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§)) â (ðĶð
+s ð§) âĪs (ðĨ +s ð§)) |
157 | 156 | rexbii 3094 |
. . . . . . . . . . . . 13
âĒ
(âðĶð
â ( R âðĶ)âð(ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§)) â âðĶð
â ( R âðĶ)(ðĶð
+s ð§) âĪs (ðĨ +s ð§)) |
158 | 153, 157 | bitr3i 276 |
. . . . . . . . . . . 12
âĒ
(âð(âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§) ⧠ð âĪs (ðĨ +s ð§)) â âðĶð
â ( R âðĶ)(ðĶð
+s ð§) âĪs (ðĨ +s ð§)) |
159 | 149, 158 | bitri 274 |
. . . . . . . . . . 11
âĒ
(âð â
{ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)}ð âĪs (ðĨ +s ð§) â âðĶð
â ( R âðĶ)(ðĶð
+s ð§) âĪs (ðĨ +s ð§)) |
160 | | eqeq1 2736 |
. . . . . . . . . . . . . 14
âĒ (ð = ð â (ð = (ðĶ +s ð§ð
) â ð = (ðĶ +s ð§ð
))) |
161 | 160 | rexbidv 3178 |
. . . . . . . . . . . . 13
âĒ (ð = ð â (âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
) â âð§ð
â ( R
âð§)ð = (ðĶ +s ð§ð
))) |
162 | 161 | rexab 3690 |
. . . . . . . . . . . 12
âĒ
(âð â
{ð âĢ âð§ð
â ( R
âð§)ð = (ðĶ +s ð§ð
)}ð âĪs (ðĨ +s ð§) â âð(âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§))) |
163 | | rexcom4 3285 |
. . . . . . . . . . . . . 14
âĒ
(âð§ð
â ( R âð§)âð(ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§)) â âðâð§ð
â ( R âð§)(ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§))) |
164 | | r19.41v 3188 |
. . . . . . . . . . . . . . 15
âĒ
(âð§ð
â ( R âð§)(ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§)) â (âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§))) |
165 | 164 | exbii 1850 |
. . . . . . . . . . . . . 14
âĒ
(âðâð§ð
â ( R âð§)(ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§)) â âð(âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§))) |
166 | 163, 165 | bitri 274 |
. . . . . . . . . . . . 13
âĒ
(âð§ð
â ( R âð§)âð(ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§)) â âð(âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§))) |
167 | | ovex 7444 |
. . . . . . . . . . . . . . 15
âĒ (ðĶ +s ð§ð
) â
V |
168 | | breq1 5151 |
. . . . . . . . . . . . . . 15
âĒ (ð = (ðĶ +s ð§ð
) â (ð âĪs (ðĨ +s ð§) â (ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) |
169 | 167, 168 | ceqsexv 3525 |
. . . . . . . . . . . . . 14
âĒ
(âð(ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§)) â (ðĶ +s ð§ð
) âĪs (ðĨ +s ð§)) |
170 | 169 | rexbii 3094 |
. . . . . . . . . . . . 13
âĒ
(âð§ð
â ( R âð§)âð(ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§)) â âð§ð
â ( R âð§)(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§)) |
171 | 166, 170 | bitr3i 276 |
. . . . . . . . . . . 12
âĒ
(âð(âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
) ⧠ð âĪs (ðĨ +s ð§)) â âð§ð
â ( R âð§)(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§)) |
172 | 162, 171 | bitri 274 |
. . . . . . . . . . 11
âĒ
(âð â
{ð âĢ âð§ð
â ( R
âð§)ð = (ðĶ +s ð§ð
)}ð âĪs (ðĨ +s ð§) â âð§ð
â ( R âð§)(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§)) |
173 | 159, 172 | orbi12i 913 |
. . . . . . . . . 10
âĒ
((âð â
{ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)}ð âĪs (ðĨ +s ð§) âĻ âð â {ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)}ð âĪs (ðĨ +s ð§)) â (âðĶð
â ( R âðĶ)(ðĶð
+s ð§) âĪs (ðĨ +s ð§) âĻ âð§ð
â ( R âð§)(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) |
174 | 146, 173 | bitri 274 |
. . . . . . . . 9
âĒ
(âð â
({ð âĢ âðĶð
â ( R
âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})ð âĪs (ðĨ +s ð§) â (âðĶð
â ( R âðĶ)(ðĶð
+s ð§) âĪs (ðĨ +s ð§) âĻ âð§ð
â ( R âð§)(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) |
175 | | simpll2 1213 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â ðĶ â No
) |
176 | | rightssno 27601 |
. . . . . . . . . . . . . . 15
âĒ ( R
âðĶ) â No |
177 | 176 | sseli 3978 |
. . . . . . . . . . . . . 14
âĒ (ðĶð
â ( R
âðĶ) â ðĶð
â
No ) |
178 | 177 | adantr 481 |
. . . . . . . . . . . . 13
âĒ ((ðĶð
â ( R
âðĶ) ⧠(ðĶð
+s ð§) âĪs
(ðĨ +s ð§)) â ðĶð
â No ) |
179 | 178 | adantl 482 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â ðĶð
â No ) |
180 | | simpll1 1212 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â ðĨ â No
) |
181 | | rightval 27584 |
. . . . . . . . . . . . . . . 16
âĒ ( R
âðĶ) = {ðĶð
â ( O
â( bday âðĶ)) âĢ ðĶ <s ðĶð
} |
182 | 181 | reqabi 3454 |
. . . . . . . . . . . . . . 15
âĒ (ðĶð
â ( R
âðĶ) â (ðĶð
â ( O
â( bday âðĶ)) ⧠ðĶ <s ðĶð
)) |
183 | 182 | simprbi 497 |
. . . . . . . . . . . . . 14
âĒ (ðĶð
â ( R
âðĶ) â ðĶ <s ðĶð
) |
184 | 183 | adantr 481 |
. . . . . . . . . . . . 13
âĒ ((ðĶð
â ( R
âðĶ) ⧠(ðĶð
+s ð§) âĪs
(ðĨ +s ð§)) â ðĶ <s ðĶð
) |
185 | 184 | adantl 482 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â ðĶ <s ðĶð
) |
186 | | simprr 771 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â (ðĶð
+s ð§) âĪs (ðĨ +s ð§)) |
187 | | simpll3 1214 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â ð§ â No
) |
188 | | sleadd1im 27697 |
. . . . . . . . . . . . . 14
âĒ ((ðĶð
â
No ⧠ðĨ â No
⧠ð§ â No ) â ((ðĶð
+s ð§) âĪs (ðĨ +s ð§) â ðĶð
âĪs ðĨ)) |
189 | 179, 180,
187, 188 | syl3anc 1371 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â ((ðĶð
+s ð§) âĪs (ðĨ +s ð§) â ðĶð
âĪs ðĨ)) |
190 | 186, 189 | mpd 15 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â ðĶð
âĪs ðĨ) |
191 | 175, 179,
180, 185, 190 | sltletrd 27487 |
. . . . . . . . . . 11
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ðĶð
â ( R âðĶ) ⧠(ðĶð
+s ð§) âĪs (ðĨ +s ð§))) â ðĶ <s ðĨ) |
192 | 191 | rexlimdvaa 3156 |
. . . . . . . . . 10
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â (âðĶð
â ( R âðĶ)(ðĶð
+s ð§) âĪs (ðĨ +s ð§) â ðĶ <s ðĨ)) |
193 | | simpll2 1213 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ðĶ â No
) |
194 | | rightssno 27601 |
. . . . . . . . . . . . . . . . 17
âĒ ( R
âð§) â No |
195 | 194 | sseli 3978 |
. . . . . . . . . . . . . . . 16
âĒ (ð§ð
â ( R
âð§) â ð§ð
â
No ) |
196 | 195 | adantr 481 |
. . . . . . . . . . . . . . 15
âĒ ((ð§ð
â ( R
âð§) ⧠(ðĶ +s ð§ð
) âĪs
(ðĨ +s ð§)) â ð§ð
â No ) |
197 | 196 | adantl 482 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ð§ð
â No ) |
198 | 193, 197 | addscld 27690 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â (ðĶ +s ð§ð
) â No ) |
199 | | simpll1 1212 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ðĨ â No
) |
200 | | simpll3 1214 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ð§ â No
) |
201 | 199, 200 | addscld 27690 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â (ðĨ +s ð§) â No
) |
202 | 199, 197 | addscld 27690 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â (ðĨ +s ð§ð
) â No ) |
203 | | simprr 771 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â (ðĶ +s ð§ð
) âĪs (ðĨ +s ð§)) |
204 | 200, 197,
199 | 3jca 1128 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â (ð§ â No
⧠ð§ð
â No ⧠ðĨ â No
)) |
205 | | rightval 27584 |
. . . . . . . . . . . . . . . . . 18
âĒ ( R
âð§) = {ð§ð
â ( O
â( bday âð§)) âĢ ð§ <s ð§ð
} |
206 | 205 | reqabi 3454 |
. . . . . . . . . . . . . . . . 17
âĒ (ð§ð
â ( R
âð§) â (ð§ð
â ( O
â( bday âð§)) ⧠ð§ <s ð§ð
)) |
207 | 206 | simprbi 497 |
. . . . . . . . . . . . . . . 16
âĒ (ð§ð
â ( R
âð§) â ð§ <s ð§ð
) |
208 | 207 | adantr 481 |
. . . . . . . . . . . . . . 15
âĒ ((ð§ð
â ( R
âð§) ⧠(ðĶ +s ð§ð
) âĪs
(ðĨ +s ð§)) â ð§ <s ð§ð
) |
209 | 208 | adantl 482 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ð§ <s ð§ð
) |
210 | | sltadd2im 27696 |
. . . . . . . . . . . . . 14
âĒ ((ð§ â
No ⧠ð§ð
â No ⧠ðĨ â No )
â (ð§ <s ð§ð
â
(ðĨ +s ð§) <s (ðĨ +s ð§ð
))) |
211 | 204, 209,
210 | sylc 65 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â (ðĨ +s ð§) <s (ðĨ +s ð§ð
)) |
212 | 198, 201,
202, 203, 211 | slelttrd 27488 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â (ðĶ +s ð§ð
) <s (ðĨ +s ð§ð
)) |
213 | | oveq2 7419 |
. . . . . . . . . . . . . . 15
âĒ (ð§ð = ð§ð
â
(ðĶ +s ð§ð) = (ðĶ +s ð§ð
)) |
214 | | oveq2 7419 |
. . . . . . . . . . . . . . 15
âĒ (ð§ð = ð§ð
â
(ðĨ +s ð§ð) = (ðĨ +s ð§ð
)) |
215 | 213, 214 | breq12d 5161 |
. . . . . . . . . . . . . 14
âĒ (ð§ð = ð§ð
â
((ðĶ +s ð§ð) <s
(ðĨ +s ð§ð) â
(ðĶ +s ð§ð
) <s
(ðĨ +s ð§ð
))) |
216 | 215 | imbi1d 341 |
. . . . . . . . . . . . 13
âĒ (ð§ð = ð§ð
â
(((ðĶ +s ð§ð) <s
(ðĨ +s ð§ð) â
ðĶ <s ðĨ) â ((ðĶ +s ð§ð
) <s (ðĨ +s ð§ð
) â
ðĶ <s ðĨ))) |
217 | | simplr3 1217 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨ +s ð§ð) â
ðĶ <s ðĨ)) |
218 | | simprl 769 |
. . . . . . . . . . . . . 14
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ð§ð
â ( R âð§)) |
219 | | elun2 4177 |
. . . . . . . . . . . . . 14
âĒ (ð§ð
â ( R
âð§) â ð§ð
â (( L
âð§) ⊠( R
âð§))) |
220 | 218, 219 | syl 17 |
. . . . . . . . . . . . 13
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ð§ð
â (( L âð§) ⊠( R âð§))) |
221 | 216, 217,
220 | rspcdva 3613 |
. . . . . . . . . . . 12
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ((ðĶ +s ð§ð
) <s (ðĨ +s ð§ð
) â
ðĶ <s ðĨ)) |
222 | 212, 221 | mpd 15 |
. . . . . . . . . . 11
âĒ ((((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) ⧠(ð§ð
â ( R âð§) ⧠(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§))) â ðĶ <s ðĨ) |
223 | 222 | rexlimdvaa 3156 |
. . . . . . . . . 10
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â (âð§ð
â ( R âð§)(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§) â ðĶ <s ðĨ)) |
224 | 192, 223 | jaod 857 |
. . . . . . . . 9
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â ((âðĶð
â ( R âðĶ)(ðĶð
+s ð§) âĪs (ðĨ +s ð§) âĻ âð§ð
â ( R âð§)(ðĶ +s ð§ð
) âĪs (ðĨ +s ð§)) â ðĶ <s ðĨ)) |
225 | 174, 224 | biimtrid 241 |
. . . . . . . 8
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â (âð â ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})ð âĪs (ðĨ +s ð§) â ðĶ <s ðĨ)) |
226 | 145, 225 | jaod 857 |
. . . . . . 7
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â ((âð â ({ð âĢ âðĨðŋ â ( L âðĨ)ð = (ðĨðŋ +s ð§)} ⊠{ð âĢ âð§ðŋ â ( L âð§)ð = (ðĨ +s ð§ðŋ)})(ðĶ +s ð§) âĪs ð âĻ âð â ({ð âĢ âðĶð
â ( R âðĶ)ð = (ðĶð
+s ð§)} ⊠{ð âĢ âð§ð
â ( R âð§)ð = (ðĶ +s ð§ð
)})ð âĪs (ðĨ +s ð§)) â ðĶ <s ðĨ)) |
227 | 65, 226 | sylbid 239 |
. . . . . 6
âĒ (((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
⧠((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ))) â ((ðĶ +s ð§) <s (ðĨ +s ð§) â ðĶ <s ðĨ)) |
228 | 227 | ex 413 |
. . . . 5
âĒ ((ðĨ â
No ⧠ðĶ â
No ⧠ð§ â No )
â (((âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))âð§ð â (( L âð§) ⊠( R âð§))((ðĶð +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶð <s ðĨð) â§
âðĨð â (( L âðĨ) ⊠( R âðĨ))âðĶð â (( L âðĶ) ⊠( R âðĶ))((ðĶð +s ð§) <s (ðĨð +s ð§) â ðĶð <s ðĨð) ⧠âðĨð â (( L
âðĨ) ⊠( R
âðĨ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶ +s ð§ð) <s
(ðĨð
+s ð§ð) â ðĶ <s ðĨð)) ⧠(âðĨð â (( L
âðĨ) ⊠( R
âðĨ))((ðĶ +s ð§) <s (ðĨð +s ð§) â ðĶ <s ðĨð) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))âð§ð â (( L
âð§) ⊠( R
âð§))((ðĶð
+s ð§ð) <s (ðĨ +s ð§ð) â
ðĶð <s
ðĨ) ⧠âðĶð â (( L
âðĶ) ⊠( R
âðĶ))((ðĶð
+s ð§) <s
(ðĨ +s ð§) â ðĶð <s ðĨ)) ⧠âð§ð â (( L âð§) ⊠( R âð§))((ðĶ +s ð§ð) <s (ðĨ +s ð§ð) â
ðĶ <s ðĨ)) â ((ðĶ +s ð§) <s (ðĨ +s ð§) â ðĶ <s ðĨ))) |
229 | 4, 8, 12, 16, 20, 22, 25, 29, 33, 37, 228 | no3inds 27668 |
. . . 4
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â ((ðĩ +s
ðķ) <s (ðī +s ðķ) â ðĩ <s ðī)) |
230 | | addscl 27691 |
. . . . . 6
âĒ ((ðĩ â
No ⧠ðķ â
No ) â (ðĩ +s ðķ) â No
) |
231 | 230 | 3adant1 1130 |
. . . . 5
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â (ðĩ +s
ðķ) â No ) |
232 | | addscl 27691 |
. . . . . 6
âĒ ((ðī â
No ⧠ðķ â
No ) â (ðī +s ðķ) â No
) |
233 | 232 | 3adant2 1131 |
. . . . 5
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â (ðī +s
ðķ) â No ) |
234 | | sltnle 27480 |
. . . . 5
âĒ (((ðĩ +s ðķ) â No
⧠(ðī +s
ðķ) â No ) â ((ðĩ +s ðķ) <s (ðī +s ðķ) â ÂŽ (ðī +s ðķ) âĪs (ðĩ +s ðķ))) |
235 | 231, 233,
234 | syl2anc 584 |
. . . 4
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â ((ðĩ +s
ðķ) <s (ðī +s ðķ) â ÂŽ (ðī +s ðķ) âĪs (ðĩ +s ðķ))) |
236 | | sltnle 27480 |
. . . . . 6
âĒ ((ðĩ â
No ⧠ðī â
No ) â (ðĩ <s ðī â ÂŽ ðī âĪs ðĩ)) |
237 | 236 | ancoms 459 |
. . . . 5
âĒ ((ðī â
No ⧠ðĩ â
No ) â (ðĩ <s ðī â ÂŽ ðī âĪs ðĩ)) |
238 | 237 | 3adant3 1132 |
. . . 4
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â (ðĩ <s ðī â ÂŽ ðī âĪs ðĩ)) |
239 | 229, 235,
238 | 3imtr3d 292 |
. . 3
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â (ÂŽ (ðī
+s ðķ) âĪs
(ðĩ +s ðķ) â ÂŽ ðī âĪs ðĩ)) |
240 | 239 | con4d 115 |
. 2
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â (ðī âĪs ðĩ â (ðī +s ðķ) âĪs (ðĩ +s ðķ))) |
241 | | sleadd1im 27697 |
. 2
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â ((ðī +s
ðķ) âĪs (ðĩ +s ðķ) â ðī âĪs ðĩ)) |
242 | 240, 241 | impbid 211 |
1
âĒ ((ðī â
No ⧠ðĩ â
No ⧠ðķ â No )
â (ðī âĪs ðĩ â (ðī +s ðķ) âĪs (ðĩ +s ðķ))) |