Step | Hyp | Ref
| Expression |
1 | | addsunif.3 |
. . . 4
âĒ (ð â ðī = (ðŋ |s ð
)) |
2 | | addsunif.1 |
. . . . 5
âĒ (ð â ðŋ <<s ð
) |
3 | 2 | scutcld 27145 |
. . . 4
âĒ (ð â (ðŋ |s ð
) â No
) |
4 | 1, 3 | eqeltrd 2838 |
. . 3
âĒ (ð â ðī â No
) |
5 | | addsunif.4 |
. . . 4
âĒ (ð â ðĩ = (ð |s ð)) |
6 | | addsunif.2 |
. . . . 5
âĒ (ð â ð <<s ð) |
7 | 6 | scutcld 27145 |
. . . 4
âĒ (ð â (ð |s ð) â No
) |
8 | 5, 7 | eqeltrd 2838 |
. . 3
âĒ (ð â ðĩ â No
) |
9 | | addsval2 27278 |
. . 3
âĒ ((ðī â
No ⧠ðĩ â
No ) â (ðī +s ðĩ) = (({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) |s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}))) |
10 | 4, 8, 9 | syl2anc 585 |
. 2
âĒ (ð â (ðī +s ðĩ) = (({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) |s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}))) |
11 | 4, 8 | addscut 27292 |
. . . . 5
âĒ (ð â ((ðī +s ðĩ) â No
⧠({ð âĢ
âð â ( L
âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) <<s {(ðī +s ðĩ)} ⧠{(ðī +s ðĩ)} <<s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}))) |
12 | 11 | simp2d 1144 |
. . . 4
âĒ (ð â ({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) <<s {(ðī +s ðĩ)}) |
13 | 11 | simp3d 1145 |
. . . 4
âĒ (ð â {(ðī +s ðĩ)} <<s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})) |
14 | | ovex 7391 |
. . . . . 6
âĒ (ðī +s ðĩ) â V |
15 | 14 | snnz 4738 |
. . . . 5
âĒ {(ðī +s ðĩ)} â â
|
16 | | sslttr 27149 |
. . . . 5
âĒ ((({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) <<s {(ðī +s ðĩ)} ⧠{(ðī +s ðĩ)} <<s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}) ⧠{(ðī +s ðĩ)} â â
) â ({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) <<s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})) |
17 | 15, 16 | mp3an3 1451 |
. . . 4
âĒ ((({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) <<s {(ðī +s ðĩ)} ⧠{(ðī +s ðĩ)} <<s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})) â ({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) <<s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})) |
18 | 12, 13, 17 | syl2anc 585 |
. . 3
âĒ (ð â ({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) <<s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})) |
19 | 2, 1 | cofcutr1d 27247 |
. . . . . 6
âĒ (ð â âð â ( L âðī)âð â ðŋ ð âĪs ð) |
20 | | leftssno 27213 |
. . . . . . . . . . 11
âĒ ( L
âðī) â No |
21 | 20 | sseli 3941 |
. . . . . . . . . 10
âĒ (ð â ( L âðī) â ð â No
) |
22 | 21 | ad2antlr 726 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( L âðī)) ⧠ð â ðŋ) â ð â No
) |
23 | | ssltss1 27131 |
. . . . . . . . . . . 12
âĒ (ðŋ <<s ð
â ðŋ â No
) |
24 | 2, 23 | syl 17 |
. . . . . . . . . . 11
âĒ (ð â ðŋ â No
) |
25 | 24 | adantr 482 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ( L âðī)) â ðŋ â No
) |
26 | 25 | sselda 3945 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( L âðī)) ⧠ð â ðŋ) â ð â No
) |
27 | 8 | ad2antrr 725 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( L âðī)) ⧠ð â ðŋ) â ðĩ â No
) |
28 | 22, 26, 27 | sleadd1d 27307 |
. . . . . . . 8
âĒ (((ð ⧠ð â ( L âðī)) ⧠ð â ðŋ) â (ð âĪs ð â (ð +s ðĩ) âĪs (ð +s ðĩ))) |
29 | 28 | rexbidva 3174 |
. . . . . . 7
âĒ ((ð ⧠ð â ( L âðī)) â (âð â ðŋ ð âĪs ð â âð â ðŋ (ð +s ðĩ) âĪs (ð +s ðĩ))) |
30 | 29 | ralbidva 3173 |
. . . . . 6
âĒ (ð â (âð â ( L âðī)âð â ðŋ ð âĪs ð â âð â ( L âðī)âð â ðŋ (ð +s ðĩ) âĪs (ð +s ðĩ))) |
31 | 19, 30 | mpbid 231 |
. . . . 5
âĒ (ð â âð â ( L âðī)âð â ðŋ (ð +s ðĩ) âĪs (ð +s ðĩ)) |
32 | | eqeq1 2741 |
. . . . . . . . . 10
âĒ (ðĶ = ð â (ðĶ = (ð +s ðĩ) â ð = (ð +s ðĩ))) |
33 | 32 | rexbidv 3176 |
. . . . . . . . 9
âĒ (ðĶ = ð â (âð â ðŋ ðĶ = (ð +s ðĩ) â âð â ðŋ ð = (ð +s ðĩ))) |
34 | 33 | rexab 3653 |
. . . . . . . 8
âĒ
(âð â
{ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} (ð +s ðĩ) âĪs ð â âð (âð â ðŋ ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð )) |
35 | | rexcom4 3272 |
. . . . . . . . 9
âĒ
(âð â
ðŋ âð (ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð ) â âð âð â ðŋ (ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð )) |
36 | | ovex 7391 |
. . . . . . . . . . 11
âĒ (ð +s ðĩ) â V |
37 | | breq2 5110 |
. . . . . . . . . . 11
âĒ (ð = (ð +s ðĩ) â ((ð +s ðĩ) âĪs ð â (ð +s ðĩ) âĪs (ð +s ðĩ))) |
38 | 36, 37 | ceqsexv 3495 |
. . . . . . . . . 10
âĒ
(âð (ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð ) â (ð +s ðĩ) âĪs (ð +s ðĩ)) |
39 | 38 | rexbii 3098 |
. . . . . . . . 9
âĒ
(âð â
ðŋ âð (ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð ) â âð â ðŋ (ð +s ðĩ) âĪs (ð +s ðĩ)) |
40 | | r19.41v 3186 |
. . . . . . . . . 10
âĒ
(âð â
ðŋ (ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð ) â (âð â ðŋ ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð )) |
41 | 40 | exbii 1851 |
. . . . . . . . 9
âĒ
(âð âð â ðŋ (ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð ) â âð (âð â ðŋ ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð )) |
42 | 35, 39, 41 | 3bitr3ri 302 |
. . . . . . . 8
âĒ
(âð (âð â ðŋ ð = (ð +s ðĩ) ⧠(ð +s ðĩ) âĪs ð ) â âð â ðŋ (ð +s ðĩ) âĪs (ð +s ðĩ)) |
43 | 34, 42 | bitri 275 |
. . . . . . 7
âĒ
(âð â
{ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} (ð +s ðĩ) âĪs ð â âð â ðŋ (ð +s ðĩ) âĪs (ð +s ðĩ)) |
44 | | ssun1 4133 |
. . . . . . . 8
âĒ {ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) |
45 | | ssrexv 4012 |
. . . . . . . 8
âĒ ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) â (âð â {ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} (ð +s ðĩ) âĪs ð â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð )) |
46 | 44, 45 | ax-mp 5 |
. . . . . . 7
âĒ
(âð â
{ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} (ð +s ðĩ) âĪs ð â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ) |
47 | 43, 46 | sylbir 234 |
. . . . . 6
âĒ
(âð â
ðŋ (ð +s ðĩ) âĪs (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ) |
48 | 47 | ralimi 3087 |
. . . . 5
âĒ
(âð â (
L âðī)âð â ðŋ (ð +s ðĩ) âĪs (ð +s ðĩ) â âð â ( L âðī)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ) |
49 | 31, 48 | syl 17 |
. . . 4
âĒ (ð â âð â ( L âðī)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ) |
50 | 6, 5 | cofcutr1d 27247 |
. . . . . 6
âĒ (ð â âð â ( L âðĩ)âð â ð ð âĪs ð) |
51 | | leftssno 27213 |
. . . . . . . . . . 11
âĒ ( L
âðĩ) â No |
52 | 51 | sseli 3941 |
. . . . . . . . . 10
âĒ (ð â ( L âðĩ) â ð â No
) |
53 | 52 | ad2antlr 726 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( L âðĩ)) ⧠ð â ð) â ð â No
) |
54 | | ssltss1 27131 |
. . . . . . . . . . . 12
âĒ (ð <<s ð â ð â No
) |
55 | 6, 54 | syl 17 |
. . . . . . . . . . 11
âĒ (ð â ð â No
) |
56 | 55 | adantr 482 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ( L âðĩ)) â ð â No
) |
57 | 56 | sselda 3945 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( L âðĩ)) ⧠ð â ð) â ð â No
) |
58 | 4 | ad2antrr 725 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( L âðĩ)) ⧠ð â ð) â ðī â No
) |
59 | 53, 57, 58 | sleadd2d 27308 |
. . . . . . . 8
âĒ (((ð ⧠ð â ( L âðĩ)) ⧠ð â ð) â (ð âĪs ð â (ðī +s ð) âĪs (ðī +s ð))) |
60 | 59 | rexbidva 3174 |
. . . . . . 7
âĒ ((ð ⧠ð â ( L âðĩ)) â (âð â ð ð âĪs ð â âð â ð (ðī +s ð) âĪs (ðī +s ð))) |
61 | 60 | ralbidva 3173 |
. . . . . 6
âĒ (ð â (âð â ( L âðĩ)âð â ð ð âĪs ð â âð â ( L âðĩ)âð â ð (ðī +s ð) âĪs (ðī +s ð))) |
62 | 50, 61 | mpbid 231 |
. . . . 5
âĒ (ð â âð â ( L âðĩ)âð â ð (ðī +s ð) âĪs (ðī +s ð)) |
63 | | eqeq1 2741 |
. . . . . . . . . 10
âĒ (ð§ = ð â (ð§ = (ðī +s ð) â ð = (ðī +s ð))) |
64 | 63 | rexbidv 3176 |
. . . . . . . . 9
âĒ (ð§ = ð â (âð â ð ð§ = (ðī +s ð) â âð â ð ð = (ðī +s ð))) |
65 | 64 | rexab 3653 |
. . . . . . . 8
âĒ
(âð â
{ð§ âĢ âð â ð ð§ = (ðī +s ð)} (ðī +s ð) âĪs ð â âð (âð â ð ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð )) |
66 | | rexcom4 3272 |
. . . . . . . . 9
âĒ
(âð â
ð âð (ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð ) â âð âð â ð (ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð )) |
67 | | ovex 7391 |
. . . . . . . . . . 11
âĒ (ðī +s ð) â V |
68 | | breq2 5110 |
. . . . . . . . . . 11
âĒ (ð = (ðī +s ð) â ((ðī +s ð) âĪs ð â (ðī +s ð) âĪs (ðī +s ð))) |
69 | 67, 68 | ceqsexv 3495 |
. . . . . . . . . 10
âĒ
(âð (ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð ) â (ðī +s ð) âĪs (ðī +s ð)) |
70 | 69 | rexbii 3098 |
. . . . . . . . 9
âĒ
(âð â
ð âð (ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð ) â âð â ð (ðī +s ð) âĪs (ðī +s ð)) |
71 | | r19.41v 3186 |
. . . . . . . . . 10
âĒ
(âð â
ð (ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð ) â (âð â ð ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð )) |
72 | 71 | exbii 1851 |
. . . . . . . . 9
âĒ
(âð âð â ð (ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð ) â âð (âð â ð ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð )) |
73 | 66, 70, 72 | 3bitr3ri 302 |
. . . . . . . 8
âĒ
(âð (âð â ð ð = (ðī +s ð) ⧠(ðī +s ð) âĪs ð ) â âð â ð (ðī +s ð) âĪs (ðī +s ð)) |
74 | 65, 73 | bitri 275 |
. . . . . . 7
âĒ
(âð â
{ð§ âĢ âð â ð ð§ = (ðī +s ð)} (ðī +s ð) âĪs ð â âð â ð (ðī +s ð) âĪs (ðī +s ð)) |
75 | | ssun2 4134 |
. . . . . . . 8
âĒ {ð§ âĢ âð â ð ð§ = (ðī +s ð)} â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) |
76 | | ssrexv 4012 |
. . . . . . . 8
âĒ ({ð§ âĢ âð â ð ð§ = (ðī +s ð)} â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) â (âð â {ð§ âĢ âð â ð ð§ = (ðī +s ð)} (ðī +s ð) âĪs ð â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð )) |
77 | 75, 76 | ax-mp 5 |
. . . . . . 7
âĒ
(âð â
{ð§ âĢ âð â ð ð§ = (ðī +s ð)} (ðī +s ð) âĪs ð â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð ) |
78 | 74, 77 | sylbir 234 |
. . . . . 6
âĒ
(âð â
ð (ðī +s ð) âĪs (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð ) |
79 | 78 | ralimi 3087 |
. . . . 5
âĒ
(âð â (
L âðĩ)âð â ð (ðī +s ð) âĪs (ðī +s ð) â âð â ( L âðĩ)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð ) |
80 | 62, 79 | syl 17 |
. . . 4
âĒ (ð â âð â ( L âðĩ)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð ) |
81 | | ralunb 4152 |
. . . . 5
âĒ
(âð â
({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)})âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð â (âð â {ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)}âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ⧠âð â {ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
82 | | eqeq1 2741 |
. . . . . . . . 9
âĒ (ð = ð â (ð = (ð +s ðĩ) â ð = (ð +s ðĩ))) |
83 | 82 | rexbidv 3176 |
. . . . . . . 8
âĒ (ð = ð â (âð â ( L âðī)ð = (ð +s ðĩ) â âð â ( L âðī)ð = (ð +s ðĩ))) |
84 | 83 | ralab 3650 |
. . . . . . 7
âĒ
(âð â
{ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)}âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð â âð(âð â ( L âðī)ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
85 | | ralcom4 3270 |
. . . . . . . 8
âĒ
(âð â (
L âðī)âð(ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âðâð â ( L âðī)(ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
86 | | ovex 7391 |
. . . . . . . . . 10
âĒ (ð +s ðĩ) â V |
87 | | breq1 5109 |
. . . . . . . . . . 11
âĒ (ð = (ð +s ðĩ) â (ð âĪs ð â (ð +s ðĩ) âĪs ð )) |
88 | 87 | rexbidv 3176 |
. . . . . . . . . 10
âĒ (ð = (ð +s ðĩ) â (âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð )) |
89 | 86, 88 | ceqsalv 3482 |
. . . . . . . . 9
âĒ
(âð(ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ) |
90 | 89 | ralbii 3097 |
. . . . . . . 8
âĒ
(âð â (
L âðī)âð(ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âð â ( L âðī)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ) |
91 | | r19.23v 3180 |
. . . . . . . . 9
âĒ
(âð â (
L âðī)(ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â (âð â ( L âðī)ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
92 | 91 | albii 1822 |
. . . . . . . 8
âĒ
(âðâð â ( L âðī)(ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âð(âð â ( L âðī)ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
93 | 85, 90, 92 | 3bitr3ri 302 |
. . . . . . 7
âĒ
(âð(âð â ( L âðī)ð = (ð +s ðĩ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âð â ( L âðī)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ) |
94 | 84, 93 | bitri 275 |
. . . . . 6
âĒ
(âð â
{ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)}âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð â âð â ( L âðī)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ) |
95 | | eqeq1 2741 |
. . . . . . . . 9
âĒ (ð = ð â (ð = (ðī +s ð) â ð = (ðī +s ð))) |
96 | 95 | rexbidv 3176 |
. . . . . . . 8
âĒ (ð = ð â (âð â ( L âðĩ)ð = (ðī +s ð) â âð â ( L âðĩ)ð = (ðī +s ð))) |
97 | 96 | ralab 3650 |
. . . . . . 7
âĒ
(âð â
{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð â âð(âð â ( L âðĩ)ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
98 | | ralcom4 3270 |
. . . . . . . 8
âĒ
(âð â (
L âðĩ)âð(ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âðâð â ( L âðĩ)(ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
99 | | ovex 7391 |
. . . . . . . . . 10
âĒ (ðī +s ð) â V |
100 | | breq1 5109 |
. . . . . . . . . . 11
âĒ (ð = (ðī +s ð) â (ð âĪs ð â (ðī +s ð) âĪs ð )) |
101 | 100 | rexbidv 3176 |
. . . . . . . . . 10
âĒ (ð = (ðī +s ð) â (âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð )) |
102 | 99, 101 | ceqsalv 3482 |
. . . . . . . . 9
âĒ
(âð(ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð ) |
103 | 102 | ralbii 3097 |
. . . . . . . 8
âĒ
(âð â (
L âðĩ)âð(ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âð â ( L âðĩ)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð ) |
104 | | r19.23v 3180 |
. . . . . . . . 9
âĒ
(âð â (
L âðĩ)(ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â (âð â ( L âðĩ)ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
105 | 104 | albii 1822 |
. . . . . . . 8
âĒ
(âðâð â ( L âðĩ)(ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âð(âð â ( L âðĩ)ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð )) |
106 | 98, 103, 105 | 3bitr3ri 302 |
. . . . . . 7
âĒ
(âð(âð â ( L âðĩ)ð = (ðī +s ð) â âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â âð â ( L âðĩ)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð ) |
107 | 97, 106 | bitri 275 |
. . . . . 6
âĒ
(âð â
{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð â âð â ( L âðĩ)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð ) |
108 | 94, 107 | anbi12i 628 |
. . . . 5
âĒ
((âð â
{ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)}âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ⧠âð â {ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) â (âð â ( L âðī)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ⧠âð â ( L âðĩ)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð )) |
109 | 81, 108 | bitri 275 |
. . . 4
âĒ
(âð â
({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)})âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð â (âð â ( L âðī)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ð +s ðĩ) âĪs ð ⧠âð â ( L âðĩ)âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})(ðī +s ð) âĪs ð )) |
110 | 49, 80, 109 | sylanbrc 584 |
. . 3
âĒ (ð â âð â ({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)})âð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})ð âĪs ð ) |
111 | 2, 1 | cofcutr2d 27248 |
. . . . . 6
âĒ (ð â âð â ( R âðī)âð â ð
ð âĪs ð) |
112 | | ssltss2 27132 |
. . . . . . . . . . . 12
âĒ (ðŋ <<s ð
â ð
â No
) |
113 | 2, 112 | syl 17 |
. . . . . . . . . . 11
âĒ (ð â ð
â No
) |
114 | 113 | adantr 482 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ( R âðī)) â ð
â No
) |
115 | 114 | sselda 3945 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( R âðī)) ⧠ð â ð
) â ð â No
) |
116 | | rightssno 27214 |
. . . . . . . . . . 11
âĒ ( R
âðī) â No |
117 | 116 | sseli 3941 |
. . . . . . . . . 10
âĒ (ð â ( R âðī) â ð â No
) |
118 | 117 | ad2antlr 726 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( R âðī)) ⧠ð â ð
) â ð â No
) |
119 | 8 | ad2antrr 725 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( R âðī)) ⧠ð â ð
) â ðĩ â No
) |
120 | 115, 118,
119 | sleadd1d 27307 |
. . . . . . . 8
âĒ (((ð ⧠ð â ( R âðī)) ⧠ð â ð
) â (ð âĪs ð â (ð +s ðĩ) âĪs (ð +s ðĩ))) |
121 | 120 | rexbidva 3174 |
. . . . . . 7
âĒ ((ð ⧠ð â ( R âðī)) â (âð â ð
ð âĪs ð â âð â ð
(ð +s ðĩ) âĪs (ð +s ðĩ))) |
122 | 121 | ralbidva 3173 |
. . . . . 6
âĒ (ð â (âð â ( R âðī)âð â ð
ð âĪs ð â âð â ( R âðī)âð â ð
(ð +s ðĩ) âĪs (ð +s ðĩ))) |
123 | 111, 122 | mpbid 231 |
. . . . 5
âĒ (ð â âð â ( R âðī)âð â ð
(ð +s ðĩ) âĪs (ð +s ðĩ)) |
124 | | eqeq1 2741 |
. . . . . . . . . 10
âĒ (ðĪ = ð â (ðĪ = (ð +s ðĩ) â ð = (ð +s ðĩ))) |
125 | 124 | rexbidv 3176 |
. . . . . . . . 9
âĒ (ðĪ = ð â (âð â ð
ðĪ = (ð +s ðĩ) â âð â ð
ð = (ð +s ðĩ))) |
126 | 125 | rexab 3653 |
. . . . . . . 8
âĒ
(âð â
{ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)}ð âĪs (ð +s ðĩ) â âð(âð â ð
ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ))) |
127 | | rexcom4 3272 |
. . . . . . . . 9
âĒ
(âð â
ð
âð(ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ)) â âðâð â ð
(ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ))) |
128 | | ovex 7391 |
. . . . . . . . . . 11
âĒ (ð +s ðĩ) â V |
129 | | breq1 5109 |
. . . . . . . . . . 11
âĒ (ð = (ð +s ðĩ) â (ð âĪs (ð +s ðĩ) â (ð +s ðĩ) âĪs (ð +s ðĩ))) |
130 | 128, 129 | ceqsexv 3495 |
. . . . . . . . . 10
âĒ
(âð(ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ)) â (ð +s ðĩ) âĪs (ð +s ðĩ)) |
131 | 130 | rexbii 3098 |
. . . . . . . . 9
âĒ
(âð â
ð
âð(ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ)) â âð â ð
(ð +s ðĩ) âĪs (ð +s ðĩ)) |
132 | | r19.41v 3186 |
. . . . . . . . . 10
âĒ
(âð â
ð
(ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ)) â (âð â ð
ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ))) |
133 | 132 | exbii 1851 |
. . . . . . . . 9
âĒ
(âðâð â ð
(ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ)) â âð(âð â ð
ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ))) |
134 | 127, 131,
133 | 3bitr3ri 302 |
. . . . . . . 8
âĒ
(âð(âð â ð
ð = (ð +s ðĩ) ⧠ð âĪs (ð +s ðĩ)) â âð â ð
(ð +s ðĩ) âĪs (ð +s ðĩ)) |
135 | 126, 134 | bitri 275 |
. . . . . . 7
âĒ
(âð â
{ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)}ð âĪs (ð +s ðĩ) â âð â ð
(ð +s ðĩ) âĪs (ð +s ðĩ)) |
136 | | ssun1 4133 |
. . . . . . . 8
âĒ {ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) |
137 | | ssrexv 4012 |
. . . . . . . 8
âĒ ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â (âð â {ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)}ð âĪs (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ))) |
138 | 136, 137 | ax-mp 5 |
. . . . . . 7
âĒ
(âð â
{ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)}ð âĪs (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ)) |
139 | 135, 138 | sylbir 234 |
. . . . . 6
âĒ
(âð â
ð
(ð +s ðĩ) âĪs (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ)) |
140 | 139 | ralimi 3087 |
. . . . 5
âĒ
(âð â (
R âðī)âð â ð
(ð +s ðĩ) âĪs (ð +s ðĩ) â âð â ( R âðī)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ)) |
141 | 123, 140 | syl 17 |
. . . 4
âĒ (ð â âð â ( R âðī)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ)) |
142 | 6, 5 | cofcutr2d 27248 |
. . . . . 6
âĒ (ð â âð â ( R âðĩ)âð â ð ð âĪs ð) |
143 | | ssltss2 27132 |
. . . . . . . . . . . 12
âĒ (ð <<s ð â ð â No
) |
144 | 6, 143 | syl 17 |
. . . . . . . . . . 11
âĒ (ð â ð â No
) |
145 | 144 | adantr 482 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ( R âðĩ)) â ð â No
) |
146 | 145 | sselda 3945 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( R âðĩ)) ⧠ð â ð) â ð â No
) |
147 | | rightssno 27214 |
. . . . . . . . . . 11
âĒ ( R
âðĩ) â No |
148 | 147 | sseli 3941 |
. . . . . . . . . 10
âĒ (ð â ( R âðĩ) â ð â No
) |
149 | 148 | ad2antlr 726 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( R âðĩ)) ⧠ð â ð) â ð â No
) |
150 | 4 | ad2antrr 725 |
. . . . . . . . 9
âĒ (((ð ⧠ð â ( R âðĩ)) ⧠ð â ð) â ðī â No
) |
151 | 146, 149,
150 | sleadd2d 27308 |
. . . . . . . 8
âĒ (((ð ⧠ð â ( R âðĩ)) ⧠ð â ð) â (ð âĪs ð â (ðī +s ð ) âĪs (ðī +s ð))) |
152 | 151 | rexbidva 3174 |
. . . . . . 7
âĒ ((ð ⧠ð â ( R âðĩ)) â (âð â ð ð âĪs ð â âð â ð (ðī +s ð ) âĪs (ðī +s ð))) |
153 | 152 | ralbidva 3173 |
. . . . . 6
âĒ (ð â (âð â ( R âðĩ)âð â ð ð âĪs ð â âð â ( R âðĩ)âð â ð (ðī +s ð ) âĪs (ðī +s ð))) |
154 | 142, 153 | mpbid 231 |
. . . . 5
âĒ (ð â âð â ( R âðĩ)âð â ð (ðī +s ð ) âĪs (ðī +s ð)) |
155 | | eqeq1 2741 |
. . . . . . . . . 10
âĒ (ðĄ = ð â (ðĄ = (ðī +s ð ) â ð = (ðī +s ð ))) |
156 | 155 | rexbidv 3176 |
. . . . . . . . 9
âĒ (ðĄ = ð â (âð â ð ðĄ = (ðī +s ð ) â âð â ð ð = (ðī +s ð ))) |
157 | 156 | rexab 3653 |
. . . . . . . 8
âĒ
(âð â
{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}ð âĪs (ðī +s ð) â âð(âð â ð ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð))) |
158 | | rexcom4 3272 |
. . . . . . . . 9
âĒ
(âð â
ð âð(ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð)) â âðâð â ð (ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð))) |
159 | | ovex 7391 |
. . . . . . . . . . 11
âĒ (ðī +s ð ) â V |
160 | | breq1 5109 |
. . . . . . . . . . 11
âĒ (ð = (ðī +s ð ) â (ð âĪs (ðī +s ð) â (ðī +s ð ) âĪs (ðī +s ð))) |
161 | 159, 160 | ceqsexv 3495 |
. . . . . . . . . 10
âĒ
(âð(ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð)) â (ðī +s ð ) âĪs (ðī +s ð)) |
162 | 161 | rexbii 3098 |
. . . . . . . . 9
âĒ
(âð â
ð âð(ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð)) â âð â ð (ðī +s ð ) âĪs (ðī +s ð)) |
163 | | r19.41v 3186 |
. . . . . . . . . 10
âĒ
(âð â
ð (ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð)) â (âð â ð ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð))) |
164 | 163 | exbii 1851 |
. . . . . . . . 9
âĒ
(âðâð â ð (ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð)) â âð(âð â ð ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð))) |
165 | 158, 162,
164 | 3bitr3ri 302 |
. . . . . . . 8
âĒ
(âð(âð â ð ð = (ðī +s ð ) ⧠ð âĪs (ðī +s ð)) â âð â ð (ðī +s ð ) âĪs (ðī +s ð)) |
166 | 157, 165 | bitri 275 |
. . . . . . 7
âĒ
(âð â
{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}ð âĪs (ðī +s ð) â âð â ð (ðī +s ð ) âĪs (ðī +s ð)) |
167 | | ssun2 4134 |
. . . . . . . 8
âĒ {ðĄ âĢ âð â ð ðĄ = (ðī +s ð )} â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) |
168 | | ssrexv 4012 |
. . . . . . . 8
âĒ ({ðĄ âĢ âð â ð ðĄ = (ðī +s ð )} â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â (âð â {ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}ð âĪs (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð))) |
169 | 167, 168 | ax-mp 5 |
. . . . . . 7
âĒ
(âð â
{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}ð âĪs (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð)) |
170 | 166, 169 | sylbir 234 |
. . . . . 6
âĒ
(âð â
ð (ðī +s ð ) âĪs (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð)) |
171 | 170 | ralimi 3087 |
. . . . 5
âĒ
(âð â (
R âðĩ)âð â ð (ðī +s ð ) âĪs (ðī +s ð) â âð â ( R âðĩ)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð)) |
172 | 154, 171 | syl 17 |
. . . 4
âĒ (ð â âð â ( R âðĩ)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð)) |
173 | | ralunb 4152 |
. . . . 5
âĒ
(âð â
({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð â (âð â {ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)}âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð ⧠âð â {ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
174 | | eqeq1 2741 |
. . . . . . . . 9
âĒ (ð = ð â (ð = (ð +s ðĩ) â ð = (ð +s ðĩ))) |
175 | 174 | rexbidv 3176 |
. . . . . . . 8
âĒ (ð = ð â (âð â ( R âðī)ð = (ð +s ðĩ) â âð â ( R âðī)ð = (ð +s ðĩ))) |
176 | 175 | ralab 3650 |
. . . . . . 7
âĒ
(âð â
{ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)}âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð â âð(âð â ( R âðī)ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
177 | | ralcom4 3270 |
. . . . . . . 8
âĒ
(âð â (
R âðī)âð(ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âðâð â ( R âðī)(ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
178 | | ovex 7391 |
. . . . . . . . . 10
âĒ (ð +s ðĩ) â V |
179 | | breq2 5110 |
. . . . . . . . . . 11
âĒ (ð = (ð +s ðĩ) â (ð âĪs ð â ð âĪs (ð +s ðĩ))) |
180 | 179 | rexbidv 3176 |
. . . . . . . . . 10
âĒ (ð = (ð +s ðĩ) â (âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ))) |
181 | 178, 180 | ceqsalv 3482 |
. . . . . . . . 9
âĒ
(âð(ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ)) |
182 | 181 | ralbii 3097 |
. . . . . . . 8
âĒ
(âð â (
R âðī)âð(ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âð â ( R âðī)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ)) |
183 | | r19.23v 3180 |
. . . . . . . . 9
âĒ
(âð â (
R âðī)(ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â (âð â ( R âðī)ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
184 | 183 | albii 1822 |
. . . . . . . 8
âĒ
(âðâð â ( R âðī)(ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âð(âð â ( R âðī)ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
185 | 177, 182,
184 | 3bitr3ri 302 |
. . . . . . 7
âĒ
(âð(âð â ( R âðī)ð = (ð +s ðĩ) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âð â ( R âðī)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ)) |
186 | 176, 185 | bitri 275 |
. . . . . 6
âĒ
(âð â
{ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)}âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð â âð â ( R âðī)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ)) |
187 | | eqeq1 2741 |
. . . . . . . . 9
âĒ (ð = ð â (ð = (ðī +s ð) â ð = (ðī +s ð))) |
188 | 187 | rexbidv 3176 |
. . . . . . . 8
âĒ (ð = ð â (âð â ( R âðĩ)ð = (ðī +s ð) â âð â ( R âðĩ)ð = (ðī +s ð))) |
189 | 188 | ralab 3650 |
. . . . . . 7
âĒ
(âð â
{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð â âð(âð â ( R âðĩ)ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
190 | | ralcom4 3270 |
. . . . . . . 8
âĒ
(âð â (
R âðĩ)âð(ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âðâð â ( R âðĩ)(ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
191 | | ovex 7391 |
. . . . . . . . . 10
âĒ (ðī +s ð) â V |
192 | | breq2 5110 |
. . . . . . . . . . 11
âĒ (ð = (ðī +s ð) â (ð âĪs ð â ð âĪs (ðī +s ð))) |
193 | 192 | rexbidv 3176 |
. . . . . . . . . 10
âĒ (ð = (ðī +s ð) â (âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð))) |
194 | 191, 193 | ceqsalv 3482 |
. . . . . . . . 9
âĒ
(âð(ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð)) |
195 | 194 | ralbii 3097 |
. . . . . . . 8
âĒ
(âð â (
R âðĩ)âð(ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âð â ( R âðĩ)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð)) |
196 | | r19.23v 3180 |
. . . . . . . . 9
âĒ
(âð â (
R âðĩ)(ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â (âð â ( R âðĩ)ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
197 | 196 | albii 1822 |
. . . . . . . 8
âĒ
(âðâð â ( R âðĩ)(ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âð(âð â ( R âðĩ)ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð)) |
198 | 190, 195,
197 | 3bitr3ri 302 |
. . . . . . 7
âĒ
(âð(âð â ( R âðĩ)ð = (ðī +s ð) â âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â âð â ( R âðĩ)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð)) |
199 | 189, 198 | bitri 275 |
. . . . . 6
âĒ
(âð â
{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð â âð â ( R âðĩ)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð)) |
200 | 186, 199 | anbi12i 628 |
. . . . 5
âĒ
((âð â
{ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)}âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð ⧠âð â {ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) â (âð â ( R âðī)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ) ⧠âð â ( R âðĩ)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð))) |
201 | 173, 200 | bitri 275 |
. . . 4
âĒ
(âð â
({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð â (âð â ( R âðī)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ð +s ðĩ) ⧠âð â ( R âðĩ)âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs (ðī +s ð))) |
202 | 141, 172,
201 | sylanbrc 584 |
. . 3
âĒ (ð â âð â ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})âð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})ð âĪs ð) |
203 | | eqid 2737 |
. . . . . . . 8
âĒ (ð â ðŋ âĶ (ð +s ðĩ)) = (ð â ðŋ âĶ (ð +s ðĩ)) |
204 | 203 | rnmpt 5911 |
. . . . . . 7
âĒ ran
(ð â ðŋ âĶ (ð +s ðĩ)) = {ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} |
205 | | ssltex1 27129 |
. . . . . . . . . 10
âĒ (ðŋ <<s ð
â ðŋ â V) |
206 | 2, 205 | syl 17 |
. . . . . . . . 9
âĒ (ð â ðŋ â V) |
207 | 206 | mptexd 7175 |
. . . . . . . 8
âĒ (ð â (ð â ðŋ âĶ (ð +s ðĩ)) â V) |
208 | | rnexg 7842 |
. . . . . . . 8
âĒ ((ð â ðŋ âĶ (ð +s ðĩ)) â V â ran (ð â ðŋ âĶ (ð +s ðĩ)) â V) |
209 | 207, 208 | syl 17 |
. . . . . . 7
âĒ (ð â ran (ð â ðŋ âĶ (ð +s ðĩ)) â V) |
210 | 204, 209 | eqeltrrid 2843 |
. . . . . 6
âĒ (ð â {ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} â V) |
211 | | eqid 2737 |
. . . . . . . 8
âĒ (ð â ð âĶ (ðī +s ð)) = (ð â ð âĶ (ðī +s ð)) |
212 | 211 | rnmpt 5911 |
. . . . . . 7
âĒ ran
(ð â ð âĶ (ðī +s ð)) = {ð§ âĢ âð â ð ð§ = (ðī +s ð)} |
213 | | ssltex1 27129 |
. . . . . . . . . 10
âĒ (ð <<s ð â ð â V) |
214 | 6, 213 | syl 17 |
. . . . . . . . 9
âĒ (ð â ð â V) |
215 | 214 | mptexd 7175 |
. . . . . . . 8
âĒ (ð â (ð â ð âĶ (ðī +s ð)) â V) |
216 | | rnexg 7842 |
. . . . . . . 8
âĒ ((ð â ð âĶ (ðī +s ð)) â V â ran (ð â ð âĶ (ðī +s ð)) â V) |
217 | 215, 216 | syl 17 |
. . . . . . 7
âĒ (ð â ran (ð â ð âĶ (ðī +s ð)) â V) |
218 | 212, 217 | eqeltrrid 2843 |
. . . . . 6
âĒ (ð â {ð§ âĢ âð â ð ð§ = (ðī +s ð)} â V) |
219 | 210, 218 | unexd 7689 |
. . . . 5
âĒ (ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) â V) |
220 | | snex 5389 |
. . . . . 6
âĒ {(ðī +s ðĩ)} â V |
221 | 220 | a1i 11 |
. . . . 5
âĒ (ð â {(ðī +s ðĩ)} â V) |
222 | 24 | sselda 3945 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ðŋ) â ð â No
) |
223 | 8 | adantr 482 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ðŋ) â ðĩ â No
) |
224 | 222, 223 | addscld 27293 |
. . . . . . . . 9
âĒ ((ð ⧠ð â ðŋ) â (ð +s ðĩ) â No
) |
225 | | eleq1 2826 |
. . . . . . . . 9
âĒ (ðĶ = (ð +s ðĩ) â (ðĶ â No
â (ð +s
ðĩ) â No )) |
226 | 224, 225 | syl5ibrcom 247 |
. . . . . . . 8
âĒ ((ð ⧠ð â ðŋ) â (ðĶ = (ð +s ðĩ) â ðĶ â No
)) |
227 | 226 | rexlimdva 3153 |
. . . . . . 7
âĒ (ð â (âð â ðŋ ðĶ = (ð +s ðĩ) â ðĶ â No
)) |
228 | 227 | abssdv 4026 |
. . . . . 6
âĒ (ð â {ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} â No
) |
229 | 4 | adantr 482 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ð) â ðī â No
) |
230 | 55 | sselda 3945 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ð) â ð â No
) |
231 | 229, 230 | addscld 27293 |
. . . . . . . . 9
âĒ ((ð ⧠ð â ð) â (ðī +s ð) â No
) |
232 | | eleq1 2826 |
. . . . . . . . 9
âĒ (ð§ = (ðī +s ð) â (ð§ â No
â (ðī +s
ð) â No )) |
233 | 231, 232 | syl5ibrcom 247 |
. . . . . . . 8
âĒ ((ð ⧠ð â ð) â (ð§ = (ðī +s ð) â ð§ â No
)) |
234 | 233 | rexlimdva 3153 |
. . . . . . 7
âĒ (ð â (âð â ð ð§ = (ðī +s ð) â ð§ â No
)) |
235 | 234 | abssdv 4026 |
. . . . . 6
âĒ (ð â {ð§ âĢ âð â ð ð§ = (ðī +s ð)} â No
) |
236 | 228, 235 | unssd 4147 |
. . . . 5
âĒ (ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) â No
) |
237 | 4, 8 | addscld 27293 |
. . . . . 6
âĒ (ð â (ðī +s ðĩ) â No
) |
238 | 237 | snssd 4770 |
. . . . 5
âĒ (ð â {(ðī +s ðĩ)} â No
) |
239 | | velsn 4603 |
. . . . . . 7
âĒ (ð â {(ðī +s ðĩ)} â ð = (ðī +s ðĩ)) |
240 | | elun 4109 |
. . . . . . . . . . 11
âĒ (ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) â (ð â {ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} âĻ ð â {ð§ âĢ âð â ð ð§ = (ðī +s ð)})) |
241 | | vex 3450 |
. . . . . . . . . . . . 13
âĒ ð â V |
242 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
âĒ (ðĶ = ð â (ðĶ = (ð +s ðĩ) â ð = (ð +s ðĩ))) |
243 | 242 | rexbidv 3176 |
. . . . . . . . . . . . 13
âĒ (ðĶ = ð â (âð â ðŋ ðĶ = (ð +s ðĩ) â âð â ðŋ ð = (ð +s ðĩ))) |
244 | 241, 243 | elab 3631 |
. . . . . . . . . . . 12
âĒ (ð â {ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} â âð â ðŋ ð = (ð +s ðĩ)) |
245 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
âĒ (ð§ = ð â (ð§ = (ðī +s ð) â ð = (ðī +s ð))) |
246 | 245 | rexbidv 3176 |
. . . . . . . . . . . . 13
âĒ (ð§ = ð â (âð â ð ð§ = (ðī +s ð) â âð â ð ð = (ðī +s ð))) |
247 | 241, 246 | elab 3631 |
. . . . . . . . . . . 12
âĒ (ð â {ð§ âĢ âð â ð ð§ = (ðī +s ð)} â âð â ð ð = (ðī +s ð)) |
248 | 244, 247 | orbi12i 914 |
. . . . . . . . . . 11
âĒ ((ð â {ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} âĻ ð â {ð§ âĢ âð â ð ð§ = (ðī +s ð)}) â (âð â ðŋ ð = (ð +s ðĩ) âĻ âð â ð ð = (ðī +s ð))) |
249 | 240, 248 | bitri 275 |
. . . . . . . . . 10
âĒ (ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) â (âð â ðŋ ð = (ð +s ðĩ) âĻ âð â ð ð = (ðī +s ð))) |
250 | | scutcut 27143 |
. . . . . . . . . . . . . . . . . . 19
âĒ (ðŋ <<s ð
â ((ðŋ |s ð
) â No
⧠ðŋ <<s {(ðŋ |s ð
)} ⧠{(ðŋ |s ð
)} <<s ð
)) |
251 | 2, 250 | syl 17 |
. . . . . . . . . . . . . . . . . 18
âĒ (ð â ((ðŋ |s ð
) â No
⧠ðŋ <<s {(ðŋ |s ð
)} ⧠{(ðŋ |s ð
)} <<s ð
)) |
252 | 251 | simp2d 1144 |
. . . . . . . . . . . . . . . . 17
âĒ (ð â ðŋ <<s {(ðŋ |s ð
)}) |
253 | 252 | adantr 482 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ðŋ) â ðŋ <<s {(ðŋ |s ð
)}) |
254 | | simpr 486 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ðŋ) â ð â ðŋ) |
255 | | ovex 7391 |
. . . . . . . . . . . . . . . . . 18
âĒ (ðŋ |s ð
) â V |
256 | 255 | snid 4623 |
. . . . . . . . . . . . . . . . 17
âĒ (ðŋ |s ð
) â {(ðŋ |s ð
)} |
257 | 256 | a1i 11 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ðŋ) â (ðŋ |s ð
) â {(ðŋ |s ð
)}) |
258 | 253, 254,
257 | ssltsepcd 27136 |
. . . . . . . . . . . . . . 15
âĒ ((ð ⧠ð â ðŋ) â ð <s (ðŋ |s ð
)) |
259 | 1 | adantr 482 |
. . . . . . . . . . . . . . 15
âĒ ((ð ⧠ð â ðŋ) â ðī = (ðŋ |s ð
)) |
260 | 258, 259 | breqtrrd 5134 |
. . . . . . . . . . . . . 14
âĒ ((ð ⧠ð â ðŋ) â ð <s ðī) |
261 | 4 | adantr 482 |
. . . . . . . . . . . . . . 15
âĒ ((ð ⧠ð â ðŋ) â ðī â No
) |
262 | 222, 261,
223 | sltadd1d 27310 |
. . . . . . . . . . . . . 14
âĒ ((ð ⧠ð â ðŋ) â (ð <s ðī â (ð +s ðĩ) <s (ðī +s ðĩ))) |
263 | 260, 262 | mpbid 231 |
. . . . . . . . . . . . 13
âĒ ((ð ⧠ð â ðŋ) â (ð +s ðĩ) <s (ðī +s ðĩ)) |
264 | | breq1 5109 |
. . . . . . . . . . . . 13
âĒ (ð = (ð +s ðĩ) â (ð <s (ðī +s ðĩ) â (ð +s ðĩ) <s (ðī +s ðĩ))) |
265 | 263, 264 | syl5ibrcom 247 |
. . . . . . . . . . . 12
âĒ ((ð ⧠ð â ðŋ) â (ð = (ð +s ðĩ) â ð <s (ðī +s ðĩ))) |
266 | 265 | rexlimdva 3153 |
. . . . . . . . . . 11
âĒ (ð â (âð â ðŋ ð = (ð +s ðĩ) â ð <s (ðī +s ðĩ))) |
267 | | scutcut 27143 |
. . . . . . . . . . . . . . . . . . 19
âĒ (ð <<s ð â ((ð |s ð) â No
⧠ð <<s {(ð |s ð)} ⧠{(ð |s ð)} <<s ð)) |
268 | 6, 267 | syl 17 |
. . . . . . . . . . . . . . . . . 18
âĒ (ð â ((ð |s ð) â No
⧠ð <<s {(ð |s ð)} ⧠{(ð |s ð)} <<s ð)) |
269 | 268 | simp2d 1144 |
. . . . . . . . . . . . . . . . 17
âĒ (ð â ð <<s {(ð |s ð)}) |
270 | 269 | adantr 482 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ð) â ð <<s {(ð |s ð)}) |
271 | | simpr 486 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ð) â ð â ð) |
272 | | ovex 7391 |
. . . . . . . . . . . . . . . . . 18
âĒ (ð |s ð) â V |
273 | 272 | snid 4623 |
. . . . . . . . . . . . . . . . 17
âĒ (ð |s ð) â {(ð |s ð)} |
274 | 273 | a1i 11 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ð) â (ð |s ð) â {(ð |s ð)}) |
275 | 270, 271,
274 | ssltsepcd 27136 |
. . . . . . . . . . . . . . 15
âĒ ((ð ⧠ð â ð) â ð <s (ð |s ð)) |
276 | 5 | adantr 482 |
. . . . . . . . . . . . . . 15
âĒ ((ð ⧠ð â ð) â ðĩ = (ð |s ð)) |
277 | 275, 276 | breqtrrd 5134 |
. . . . . . . . . . . . . 14
âĒ ((ð ⧠ð â ð) â ð <s ðĩ) |
278 | 8 | adantr 482 |
. . . . . . . . . . . . . . 15
âĒ ((ð ⧠ð â ð) â ðĩ â No
) |
279 | 230, 278,
229 | sltadd2d 27309 |
. . . . . . . . . . . . . 14
âĒ ((ð ⧠ð â ð) â (ð <s ðĩ â (ðī +s ð) <s (ðī +s ðĩ))) |
280 | 277, 279 | mpbid 231 |
. . . . . . . . . . . . 13
âĒ ((ð ⧠ð â ð) â (ðī +s ð) <s (ðī +s ðĩ)) |
281 | | breq1 5109 |
. . . . . . . . . . . . 13
âĒ (ð = (ðī +s ð) â (ð <s (ðī +s ðĩ) â (ðī +s ð) <s (ðī +s ðĩ))) |
282 | 280, 281 | syl5ibrcom 247 |
. . . . . . . . . . . 12
âĒ ((ð ⧠ð â ð) â (ð = (ðī +s ð) â ð <s (ðī +s ðĩ))) |
283 | 282 | rexlimdva 3153 |
. . . . . . . . . . 11
âĒ (ð â (âð â ð ð = (ðī +s ð) â ð <s (ðī +s ðĩ))) |
284 | 266, 283 | jaod 858 |
. . . . . . . . . 10
âĒ (ð â ((âð â ðŋ ð = (ð +s ðĩ) âĻ âð â ð ð = (ðī +s ð)) â ð <s (ðī +s ðĩ))) |
285 | 249, 284 | biimtrid 241 |
. . . . . . . . 9
âĒ (ð â (ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) â ð <s (ðī +s ðĩ))) |
286 | 285 | imp 408 |
. . . . . . . 8
âĒ ((ð ⧠ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})) â ð <s (ðī +s ðĩ)) |
287 | | breq2 5110 |
. . . . . . . 8
âĒ (ð = (ðī +s ðĩ) â (ð <s ð â ð <s (ðī +s ðĩ))) |
288 | 286, 287 | syl5ibrcom 247 |
. . . . . . 7
âĒ ((ð ⧠ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})) â (ð = (ðī +s ðĩ) â ð <s ð)) |
289 | 239, 288 | biimtrid 241 |
. . . . . 6
âĒ ((ð ⧠ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)})) â (ð â {(ðī +s ðĩ)} â ð <s ð)) |
290 | 289 | 3impia 1118 |
. . . . 5
âĒ ((ð ⧠ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) ⧠ð â {(ðī +s ðĩ)}) â ð <s ð) |
291 | 219, 221,
236, 238, 290 | ssltd 27134 |
. . . 4
âĒ (ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) <<s {(ðī +s ðĩ)}) |
292 | 10 | sneqd 4599 |
. . . 4
âĒ (ð â {(ðī +s ðĩ)} = {(({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) |s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}))}) |
293 | 291, 292 | breqtrd 5132 |
. . 3
âĒ (ð â ({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) <<s {(({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) |s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}))}) |
294 | | eqid 2737 |
. . . . . . . 8
âĒ (ð â ð
âĶ (ð +s ðĩ)) = (ð â ð
âĶ (ð +s ðĩ)) |
295 | 294 | rnmpt 5911 |
. . . . . . 7
âĒ ran
(ð â ð
âĶ (ð +s ðĩ)) = {ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} |
296 | | ssltex2 27130 |
. . . . . . . . . 10
âĒ (ðŋ <<s ð
â ð
â V) |
297 | 2, 296 | syl 17 |
. . . . . . . . 9
âĒ (ð â ð
â V) |
298 | 297 | mptexd 7175 |
. . . . . . . 8
âĒ (ð â (ð â ð
âĶ (ð +s ðĩ)) â V) |
299 | | rnexg 7842 |
. . . . . . . 8
âĒ ((ð â ð
âĶ (ð +s ðĩ)) â V â ran (ð â ð
âĶ (ð +s ðĩ)) â V) |
300 | 298, 299 | syl 17 |
. . . . . . 7
âĒ (ð â ran (ð â ð
âĶ (ð +s ðĩ)) â V) |
301 | 295, 300 | eqeltrrid 2843 |
. . . . . 6
âĒ (ð â {ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} â V) |
302 | | eqid 2737 |
. . . . . . . 8
âĒ (ð â ð âĶ (ðī +s ð )) = (ð â ð âĶ (ðī +s ð )) |
303 | 302 | rnmpt 5911 |
. . . . . . 7
âĒ ran
(ð â ð âĶ (ðī +s ð )) = {ðĄ âĢ âð â ð ðĄ = (ðī +s ð )} |
304 | | ssltex2 27130 |
. . . . . . . . . 10
âĒ (ð <<s ð â ð â V) |
305 | 6, 304 | syl 17 |
. . . . . . . . 9
âĒ (ð â ð â V) |
306 | 305 | mptexd 7175 |
. . . . . . . 8
âĒ (ð â (ð â ð âĶ (ðī +s ð )) â V) |
307 | | rnexg 7842 |
. . . . . . . 8
âĒ ((ð â ð âĶ (ðī +s ð )) â V â ran (ð â ð âĶ (ðī +s ð )) â V) |
308 | 306, 307 | syl 17 |
. . . . . . 7
âĒ (ð â ran (ð â ð âĶ (ðī +s ð )) â V) |
309 | 303, 308 | eqeltrrid 2843 |
. . . . . 6
âĒ (ð â {ðĄ âĢ âð â ð ðĄ = (ðī +s ð )} â V) |
310 | 301, 309 | unexd 7689 |
. . . . 5
âĒ (ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â V) |
311 | 113 | sselda 3945 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ð
) â ð â No
) |
312 | 8 | adantr 482 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ð
) â ðĩ â No
) |
313 | 311, 312 | addscld 27293 |
. . . . . . . . 9
âĒ ((ð ⧠ð â ð
) â (ð +s ðĩ) â No
) |
314 | | eleq1 2826 |
. . . . . . . . 9
âĒ (ðĪ = (ð +s ðĩ) â (ðĪ â No
â (ð +s
ðĩ) â No )) |
315 | 313, 314 | syl5ibrcom 247 |
. . . . . . . 8
âĒ ((ð ⧠ð â ð
) â (ðĪ = (ð +s ðĩ) â ðĪ â No
)) |
316 | 315 | rexlimdva 3153 |
. . . . . . 7
âĒ (ð â (âð â ð
ðĪ = (ð +s ðĩ) â ðĪ â No
)) |
317 | 316 | abssdv 4026 |
. . . . . 6
âĒ (ð â {ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} â No
) |
318 | 4 | adantr 482 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ð) â ðī â No
) |
319 | 144 | sselda 3945 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ð) â ð â No
) |
320 | 318, 319 | addscld 27293 |
. . . . . . . . 9
âĒ ((ð ⧠ð â ð) â (ðī +s ð ) â No
) |
321 | | eleq1 2826 |
. . . . . . . . 9
âĒ (ðĄ = (ðī +s ð ) â (ðĄ â No
â (ðī +s
ð ) â No )) |
322 | 320, 321 | syl5ibrcom 247 |
. . . . . . . 8
âĒ ((ð ⧠ð â ð) â (ðĄ = (ðī +s ð ) â ðĄ â No
)) |
323 | 322 | rexlimdva 3153 |
. . . . . . 7
âĒ (ð â (âð â ð ðĄ = (ðī +s ð ) â ðĄ â No
)) |
324 | 323 | abssdv 4026 |
. . . . . 6
âĒ (ð â {ðĄ âĢ âð â ð ðĄ = (ðī +s ð )} â No
) |
325 | 317, 324 | unssd 4147 |
. . . . 5
âĒ (ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â No
) |
326 | | velsn 4603 |
. . . . . . 7
âĒ (ð â {(ðī +s ðĩ)} â ð = (ðī +s ðĩ)) |
327 | | elun 4109 |
. . . . . . . . . . . . 13
âĒ (ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â (ð â {ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} âĻ ð â {ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})) |
328 | | vex 3450 |
. . . . . . . . . . . . . . 15
âĒ ð â V |
329 | 328, 125 | elab 3631 |
. . . . . . . . . . . . . 14
âĒ (ð â {ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} â âð â ð
ð = (ð +s ðĩ)) |
330 | 328, 156 | elab 3631 |
. . . . . . . . . . . . . 14
âĒ (ð â {ðĄ âĢ âð â ð ðĄ = (ðī +s ð )} â âð â ð ð = (ðī +s ð )) |
331 | 329, 330 | orbi12i 914 |
. . . . . . . . . . . . 13
âĒ ((ð â {ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} âĻ ð â {ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â (âð â ð
ð = (ð +s ðĩ) âĻ âð â ð ð = (ðī +s ð ))) |
332 | 327, 331 | bitri 275 |
. . . . . . . . . . . 12
âĒ (ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â (âð â ð
ð = (ð +s ðĩ) âĻ âð â ð ð = (ðī +s ð ))) |
333 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . 17
âĒ ((ð ⧠ð â ð
) â ðī = (ðŋ |s ð
)) |
334 | 251 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . 19
âĒ (ð â {(ðŋ |s ð
)} <<s ð
) |
335 | 334 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
âĒ ((ð ⧠ð â ð
) â {(ðŋ |s ð
)} <<s ð
) |
336 | 256 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
âĒ ((ð ⧠ð â ð
) â (ðŋ |s ð
) â {(ðŋ |s ð
)}) |
337 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
âĒ ((ð ⧠ð â ð
) â ð â ð
) |
338 | 335, 336,
337 | ssltsepcd 27136 |
. . . . . . . . . . . . . . . . 17
âĒ ((ð ⧠ð â ð
) â (ðŋ |s ð
) <s ð) |
339 | 333, 338 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ð
) â ðī <s ð) |
340 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . 17
âĒ ((ð ⧠ð â ð
) â ðī â No
) |
341 | 340, 311,
312 | sltadd1d 27310 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ð
) â (ðī <s ð â (ðī +s ðĩ) <s (ð +s ðĩ))) |
342 | 339, 341 | mpbid 231 |
. . . . . . . . . . . . . . 15
âĒ ((ð ⧠ð â ð
) â (ðī +s ðĩ) <s (ð +s ðĩ)) |
343 | | breq2 5110 |
. . . . . . . . . . . . . . 15
âĒ (ð = (ð +s ðĩ) â ((ðī +s ðĩ) <s ð â (ðī +s ðĩ) <s (ð +s ðĩ))) |
344 | 342, 343 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
âĒ ((ð ⧠ð â ð
) â (ð = (ð +s ðĩ) â (ðī +s ðĩ) <s ð)) |
345 | 344 | rexlimdva 3153 |
. . . . . . . . . . . . 13
âĒ (ð â (âð â ð
ð = (ð +s ðĩ) â (ðī +s ðĩ) <s ð)) |
346 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . 17
âĒ ((ð ⧠ð â ð) â ðĩ = (ð |s ð)) |
347 | 268 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . 19
âĒ (ð â {(ð |s ð)} <<s ð) |
348 | 347 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
âĒ ((ð ⧠ð â ð) â {(ð |s ð)} <<s ð) |
349 | 273 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
âĒ ((ð ⧠ð â ð) â (ð |s ð) â {(ð |s ð)}) |
350 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
âĒ ((ð ⧠ð â ð) â ð â ð) |
351 | 348, 349,
350 | ssltsepcd 27136 |
. . . . . . . . . . . . . . . . 17
âĒ ((ð ⧠ð â ð) â (ð |s ð) <s ð ) |
352 | 346, 351 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ð) â ðĩ <s ð ) |
353 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . 17
âĒ ((ð ⧠ð â ð) â ðĩ â No
) |
354 | 353, 319,
318 | sltadd2d 27309 |
. . . . . . . . . . . . . . . 16
âĒ ((ð ⧠ð â ð) â (ðĩ <s ð â (ðī +s ðĩ) <s (ðī +s ð ))) |
355 | 352, 354 | mpbid 231 |
. . . . . . . . . . . . . . 15
âĒ ((ð ⧠ð â ð) â (ðī +s ðĩ) <s (ðī +s ð )) |
356 | | breq2 5110 |
. . . . . . . . . . . . . . 15
âĒ (ð = (ðī +s ð ) â ((ðī +s ðĩ) <s ð â (ðī +s ðĩ) <s (ðī +s ð ))) |
357 | 355, 356 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
âĒ ((ð ⧠ð â ð) â (ð = (ðī +s ð ) â (ðī +s ðĩ) <s ð)) |
358 | 357 | rexlimdva 3153 |
. . . . . . . . . . . . 13
âĒ (ð â (âð â ð ð = (ðī +s ð ) â (ðī +s ðĩ) <s ð)) |
359 | 345, 358 | jaod 858 |
. . . . . . . . . . . 12
âĒ (ð â ((âð â ð
ð = (ð +s ðĩ) âĻ âð â ð ð = (ðī +s ð )) â (ðī +s ðĩ) <s ð)) |
360 | 332, 359 | biimtrid 241 |
. . . . . . . . . . 11
âĒ (ð â (ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â (ðī +s ðĩ) <s ð)) |
361 | 360 | imp 408 |
. . . . . . . . . 10
âĒ ((ð ⧠ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})) â (ðī +s ðĩ) <s ð) |
362 | | breq1 5109 |
. . . . . . . . . 10
âĒ (ð = (ðī +s ðĩ) â (ð <s ð â (ðī +s ðĩ) <s ð)) |
363 | 361, 362 | syl5ibrcom 247 |
. . . . . . . . 9
âĒ ((ð ⧠ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})) â (ð = (ðī +s ðĩ) â ð <s ð)) |
364 | 363 | ex 414 |
. . . . . . . 8
âĒ (ð â (ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â (ð = (ðī +s ðĩ) â ð <s ð))) |
365 | 364 | com23 86 |
. . . . . . 7
âĒ (ð â (ð = (ðī +s ðĩ) â (ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â ð <s ð))) |
366 | 326, 365 | biimtrid 241 |
. . . . . 6
âĒ (ð â (ð â {(ðī +s ðĩ)} â (ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}) â ð <s ð))) |
367 | 366 | 3imp 1112 |
. . . . 5
âĒ ((ð ⧠ð â {(ðī +s ðĩ)} ⧠ð â ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})) â ð <s ð) |
368 | 221, 310,
238, 325, 367 | ssltd 27134 |
. . . 4
âĒ (ð â {(ðī +s ðĩ)} <<s ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})) |
369 | 292, 368 | eqbrtrrd 5130 |
. . 3
âĒ (ð â {(({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) |s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)}))} <<s ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )})) |
370 | 18, 110, 202, 293, 369 | cofcut1d 27243 |
. 2
âĒ (ð â (({ð âĢ âð â ( L âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( L âðĩ)ð = (ðī +s ð)}) |s ({ð âĢ âð â ( R âðī)ð = (ð +s ðĩ)} ⊠{ð âĢ âð â ( R âðĩ)ð = (ðī +s ð)})) = (({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) |s ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}))) |
371 | 10, 370 | eqtrd 2777 |
1
âĒ (ð â (ðī +s ðĩ) = (({ðĶ âĢ âð â ðŋ ðĶ = (ð +s ðĩ)} ⊠{ð§ âĢ âð â ð ð§ = (ðī +s ð)}) |s ({ðĪ âĢ âð â ð
ðĪ = (ð +s ðĩ)} ⊠{ðĄ âĢ âð â ð ðĄ = (ðī +s ð )}))) |