Step | Hyp | Ref
| Expression |
1 | | ax-1cn 11110 |
. . . . . . 7
โข 1 โ
โ |
2 | | 0cn 11148 |
. . . . . . 7
โข 0 โ
โ |
3 | 1, 2 | ifcli 4534 |
. . . . . 6
โข if((๐ตโ2) = 1, 1, 0) โ
โ |
4 | 3 | mulid2i 11161 |
. . . . 5
โข (1
ยท if((๐ตโ2) = 1,
1, 0)) = if((๐ตโ2) = 1,
1, 0) |
5 | | iftrue 4493 |
. . . . . . 7
โข ((๐ดโ2) = 1 โ if((๐ดโ2) = 1, 1, 0) =
1) |
6 | 5 | adantl 483 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ if((๐ดโ2) = 1, 1, 0) =
1) |
7 | 6 | oveq1d 7373 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ (if((๐ดโ2) = 1, 1, 0) ยท
if((๐ตโ2) = 1, 1, 0)) =
(1 ยท if((๐ตโ2) =
1, 1, 0))) |
8 | | simpl1 1192 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ด โ โค) |
9 | 8 | zcnd 12609 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ด โ โ) |
10 | 9 | ad2antrr 725 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ ๐ด โ
โ) |
11 | | simpl2 1193 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ต โ โค) |
12 | 11 | zcnd 12609 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ต โ โ) |
13 | 12 | ad2antrr 725 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ ๐ต โ
โ) |
14 | 10, 13 | sqmuld 14064 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ ((๐ด ยท ๐ต)โ2) = ((๐ดโ2) ยท (๐ตโ2))) |
15 | | simpr 486 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ (๐ดโ2) = 1) |
16 | 15 | oveq1d 7373 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ ((๐ดโ2) ยท (๐ตโ2)) = (1 ยท (๐ตโ2))) |
17 | 12 | sqcld 14050 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ตโ2) โ โ) |
18 | 17 | ad2antrr 725 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ (๐ตโ2) โ
โ) |
19 | 18 | mulid2d 11174 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ (1 ยท
(๐ตโ2)) = (๐ตโ2)) |
20 | 14, 16, 19 | 3eqtrd 2781 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ ((๐ด ยท ๐ต)โ2) = (๐ตโ2)) |
21 | 20 | eqeq1d 2739 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ (((๐ด ยท ๐ต)โ2) = 1 โ (๐ตโ2) = 1)) |
22 | 21 | ifbid 4510 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ if(((๐ด ยท ๐ต)โ2) = 1, 1, 0) = if((๐ตโ2) = 1, 1, 0)) |
23 | 4, 7, 22 | 3eqtr4a 2803 |
. . . 4
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง (๐ดโ2) = 1) โ (if((๐ดโ2) = 1, 1, 0) ยท
if((๐ตโ2) = 1, 1, 0)) =
if(((๐ด ยท ๐ต)โ2) = 1, 1,
0)) |
24 | 3 | mul02i 11345 |
. . . . 5
โข (0
ยท if((๐ตโ2) = 1,
1, 0)) = 0 |
25 | | iffalse 4496 |
. . . . . . 7
โข (ยฌ
(๐ดโ2) = 1 โ
if((๐ดโ2) = 1, 1, 0) =
0) |
26 | 25 | adantl 483 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง ยฌ (๐ดโ2) = 1) โ if((๐ดโ2) = 1, 1, 0) =
0) |
27 | 26 | oveq1d 7373 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง ยฌ (๐ดโ2) = 1) โ (if((๐ดโ2) = 1, 1, 0) ยท
if((๐ตโ2) = 1, 1, 0)) =
(0 ยท if((๐ตโ2) =
1, 1, 0))) |
28 | | dvdsmul1 16161 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ด โฅ (๐ด ยท ๐ต)) |
29 | 8, 11, 28 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ด โฅ (๐ด ยท ๐ต)) |
30 | 8, 11 | zmulcld 12614 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ด ยท ๐ต) โ โค) |
31 | | dvdssq 16444 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง (๐ด ยท ๐ต) โ โค) โ (๐ด โฅ (๐ด ยท ๐ต) โ (๐ดโ2) โฅ ((๐ด ยท ๐ต)โ2))) |
32 | 8, 30, 31 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ด โฅ (๐ด ยท ๐ต) โ (๐ดโ2) โฅ ((๐ด ยท ๐ต)โ2))) |
33 | 29, 32 | mpbid 231 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ดโ2) โฅ ((๐ด ยท ๐ต)โ2)) |
34 | 33 | adantr 482 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (๐ดโ2) โฅ ((๐ด ยท ๐ต)โ2)) |
35 | | breq2 5110 |
. . . . . . . . 9
โข (((๐ด ยท ๐ต)โ2) = 1 โ ((๐ดโ2) โฅ ((๐ด ยท ๐ต)โ2) โ (๐ดโ2) โฅ 1)) |
36 | 34, 35 | syl5ibcom 244 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (((๐ด ยท ๐ต)โ2) = 1 โ (๐ดโ2) โฅ 1)) |
37 | | simprl 770 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ด โ 0) |
38 | 37 | neneqd 2949 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ยฌ ๐ด = 0) |
39 | | sqeq0 14026 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ โ ((๐ดโ2) = 0 โ ๐ด = 0)) |
40 | 9, 39 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ดโ2) = 0 โ ๐ด = 0)) |
41 | 38, 40 | mtbird 325 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ยฌ (๐ดโ2) = 0) |
42 | | zsqcl2 14044 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โค โ (๐ดโ2) โ
โ0) |
43 | 8, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ดโ2) โ
โ0) |
44 | | elnn0 12416 |
. . . . . . . . . . . . . . . 16
โข ((๐ดโ2) โ
โ0 โ ((๐ดโ2) โ โ โจ (๐ดโ2) = 0)) |
45 | 43, 44 | sylib 217 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ดโ2) โ โ โจ (๐ดโ2) = 0)) |
46 | 45 | ord 863 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (ยฌ (๐ดโ2) โ โ โ (๐ดโ2) = 0)) |
47 | 41, 46 | mt3d 148 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ดโ2) โ โ) |
48 | 47 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (๐ดโ2) โ โ) |
49 | 48 | nnzd 12527 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (๐ดโ2) โ โค) |
50 | | 1nn 12165 |
. . . . . . . . . . 11
โข 1 โ
โ |
51 | | dvdsle 16193 |
. . . . . . . . . . 11
โข (((๐ดโ2) โ โค โง 1
โ โ) โ ((๐ดโ2) โฅ 1 โ (๐ดโ2) โค 1)) |
52 | 49, 50, 51 | sylancl 587 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ ((๐ดโ2) โฅ 1 โ (๐ดโ2) โค 1)) |
53 | 48 | nnge1d 12202 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ 1 โค (๐ดโ2)) |
54 | 52, 53 | jctird 528 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ ((๐ดโ2) โฅ 1 โ ((๐ดโ2) โค 1 โง 1 โค
(๐ดโ2)))) |
55 | 48 | nnred 12169 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (๐ดโ2) โ โ) |
56 | | 1re 11156 |
. . . . . . . . . 10
โข 1 โ
โ |
57 | | letri3 11241 |
. . . . . . . . . 10
โข (((๐ดโ2) โ โ โง 1
โ โ) โ ((๐ดโ2) = 1 โ ((๐ดโ2) โค 1 โง 1 โค (๐ดโ2)))) |
58 | 55, 56, 57 | sylancl 587 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ ((๐ดโ2) = 1 โ ((๐ดโ2) โค 1 โง 1 โค (๐ดโ2)))) |
59 | 54, 58 | sylibrd 259 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ ((๐ดโ2) โฅ 1 โ (๐ดโ2) = 1)) |
60 | 36, 59 | syld 47 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (((๐ด ยท ๐ต)โ2) = 1 โ (๐ดโ2) = 1)) |
61 | 60 | con3dimp 410 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง ยฌ (๐ดโ2) = 1) โ ยฌ
((๐ด ยท ๐ต)โ2) = 1) |
62 | 61 | iffalsed 4498 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง ยฌ (๐ดโ2) = 1) โ if(((๐ด ยท ๐ต)โ2) = 1, 1, 0) = 0) |
63 | 24, 27, 62 | 3eqtr4a 2803 |
. . . 4
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ = 0) โง ยฌ (๐ดโ2) = 1) โ (if((๐ดโ2) = 1, 1, 0) ยท
if((๐ตโ2) = 1, 1, 0)) =
if(((๐ด ยท ๐ต)โ2) = 1, 1,
0)) |
64 | 23, 63 | pm2.61dan 812 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (if((๐ดโ2) = 1, 1, 0) ยท if((๐ตโ2) = 1, 1, 0)) =
if(((๐ด ยท ๐ต)โ2) = 1, 1,
0)) |
65 | | oveq2 7366 |
. . . . 5
โข (๐ = 0 โ (๐ด /L ๐) = (๐ด /L 0)) |
66 | | lgs0 26661 |
. . . . . 6
โข (๐ด โ โค โ (๐ด /L 0) =
if((๐ดโ2) = 1, 1,
0)) |
67 | 8, 66 | syl 17 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ด /L 0) = if((๐ดโ2) = 1, 1,
0)) |
68 | 65, 67 | sylan9eqr 2799 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (๐ด /L ๐) = if((๐ดโ2) = 1, 1, 0)) |
69 | | oveq2 7366 |
. . . . 5
โข (๐ = 0 โ (๐ต /L ๐) = (๐ต /L 0)) |
70 | | lgs0 26661 |
. . . . . 6
โข (๐ต โ โค โ (๐ต /L 0) =
if((๐ตโ2) = 1, 1,
0)) |
71 | 11, 70 | syl 17 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ต /L 0) = if((๐ตโ2) = 1, 1,
0)) |
72 | 69, 71 | sylan9eqr 2799 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ (๐ต /L ๐) = if((๐ตโ2) = 1, 1, 0)) |
73 | 68, 72 | oveq12d 7376 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ ((๐ด /L ๐) ยท (๐ต /L ๐)) = (if((๐ดโ2) = 1, 1, 0) ยท if((๐ตโ2) = 1, 1,
0))) |
74 | | oveq2 7366 |
. . . 4
โข (๐ = 0 โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด ยท ๐ต) /L 0)) |
75 | | lgs0 26661 |
. . . . 5
โข ((๐ด ยท ๐ต) โ โค โ ((๐ด ยท ๐ต) /L 0) = if(((๐ด ยท ๐ต)โ2) = 1, 1, 0)) |
76 | 30, 75 | syl 17 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) /L 0) = if(((๐ด ยท ๐ต)โ2) = 1, 1, 0)) |
77 | 74, 76 | sylan9eqr 2799 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ ((๐ด ยท ๐ต) /L ๐) = if(((๐ด ยท ๐ต)โ2) = 1, 1, 0)) |
78 | 64, 73, 77 | 3eqtr4rd 2788 |
. 2
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ = 0) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
79 | | lgsdilem 26675 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1))) |
80 | 79 | adantr 482 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1))) |
81 | | simpl3 1194 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ โ โค) |
82 | | nnabscl 15211 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
83 | 81, 82 | sylan 581 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (absโ๐) โ โ) |
84 | | nnuz 12807 |
. . . . . 6
โข โ =
(โคโฅโ1) |
85 | 83, 84 | eleqtrdi 2848 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (absโ๐) โ
(โคโฅโ1)) |
86 | | simpll1 1213 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ๐ด โ โค) |
87 | | simpll3 1215 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ๐ โ โค) |
88 | | simpr 486 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ๐ โ 0) |
89 | | eqid 2737 |
. . . . . . . . 9
โข (๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)) = (๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)) |
90 | 89 | lgsfcl3 26669 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)),
1)):โโถโค) |
91 | 86, 87, 88, 90 | syl3anc 1372 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)),
1)):โโถโค) |
92 | | elfznn 13471 |
. . . . . . 7
โข (๐ โ (1...(absโ๐)) โ ๐ โ โ) |
93 | | ffvelcdm 7033 |
. . . . . . 7
โข (((๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)):โโถโค โง ๐ โ โ) โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1))โ๐) โ โค) |
94 | 91, 92, 93 | syl2an 597 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1))โ๐) โ โค) |
95 | 94 | zcnd 12609 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1))โ๐) โ โ) |
96 | | simpll2 1214 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ๐ต โ โค) |
97 | | eqid 2737 |
. . . . . . . . 9
โข (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)) = (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)) |
98 | 97 | lgsfcl3 26669 |
. . . . . . . 8
โข ((๐ต โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)),
1)):โโถโค) |
99 | 96, 87, 88, 98 | syl3anc 1372 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)),
1)):โโถโค) |
100 | | ffvelcdm 7033 |
. . . . . . 7
โข (((๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)):โโถโค โง ๐ โ โ) โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))โ๐) โ โค) |
101 | 99, 92, 100 | syl2an 597 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))โ๐) โ โค) |
102 | 101 | zcnd 12609 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))โ๐) โ โ) |
103 | 86 | adantr 482 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ ๐ด โ
โค) |
104 | 96 | adantr 482 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ ๐ต โ
โค) |
105 | | simpr 486 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ ๐ โ
โ) |
106 | | lgsdirprm 26682 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
107 | 103, 104,
105, 106 | syl3anc 1372 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
108 | 107 | oveq1d 7373 |
. . . . . . . . . 10
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)) = (((๐ด /L ๐) ยท (๐ต /L ๐))โ(๐ pCnt ๐))) |
109 | | prmz 16552 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โค) |
110 | | lgscl 26662 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ โค) โ (๐ด /L ๐) โ
โค) |
111 | 86, 109, 110 | syl2an 597 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ (๐ด /L ๐) โ
โค) |
112 | 111 | zcnd 12609 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ (๐ด /L ๐) โ
โ) |
113 | | lgscl 26662 |
. . . . . . . . . . . . 13
โข ((๐ต โ โค โง ๐ โ โค) โ (๐ต /L ๐) โ
โค) |
114 | 96, 109, 113 | syl2an 597 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ (๐ต /L ๐) โ
โค) |
115 | 114 | zcnd 12609 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ (๐ต /L ๐) โ
โ) |
116 | 87 | adantr 482 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ ๐ โ
โค) |
117 | 88 | adantr 482 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ ๐ โ 0) |
118 | | pczcl 16721 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ โ โค โง ๐ โ 0)) โ (๐ pCnt ๐) โ
โ0) |
119 | 105, 116,
117, 118 | syl12anc 836 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ (๐ pCnt ๐) โ
โ0) |
120 | 112, 115,
119 | mulexpd 14067 |
. . . . . . . . . 10
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ (((๐ด /L ๐) ยท (๐ต /L ๐))โ(๐ pCnt ๐)) = (((๐ด /L ๐)โ(๐ pCnt ๐)) ยท ((๐ต /L ๐)โ(๐ pCnt ๐)))) |
121 | 108, 120 | eqtrd 2777 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)) = (((๐ด /L ๐)โ(๐ pCnt ๐)) ยท ((๐ต /L ๐)โ(๐ pCnt ๐)))) |
122 | | iftrue 4493 |
. . . . . . . . . 10
โข (๐ โ โ โ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐))) |
123 | 122 | adantl 483 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐))) |
124 | | iftrue 4493 |
. . . . . . . . . . 11
โข (๐ โ โ โ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) = ((๐ด /L ๐)โ(๐ pCnt ๐))) |
125 | | iftrue 4493 |
. . . . . . . . . . 11
โข (๐ โ โ โ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1) = ((๐ต /L ๐)โ(๐ pCnt ๐))) |
126 | 124, 125 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ โ โ (if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)) = (((๐ด /L ๐)โ(๐ pCnt ๐)) ยท ((๐ต /L ๐)โ(๐ pCnt ๐)))) |
127 | 126 | adantl 483 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ
(if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)) = (((๐ด /L ๐)โ(๐ pCnt ๐)) ยท ((๐ต /L ๐)โ(๐ pCnt ๐)))) |
128 | 121, 123,
127 | 3eqtr4d 2787 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ โ) โ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = (if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))) |
129 | | 1t1e1 12316 |
. . . . . . . . . . 11
โข (1
ยท 1) = 1 |
130 | 129 | eqcomi 2746 |
. . . . . . . . . 10
โข 1 = (1
ยท 1) |
131 | | iffalse 4496 |
. . . . . . . . . 10
โข (ยฌ
๐ โ โ โ
if(๐ โ โ,
(((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = 1) |
132 | | iffalse 4496 |
. . . . . . . . . . 11
โข (ยฌ
๐ โ โ โ
if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1) = 1) |
133 | | iffalse 4496 |
. . . . . . . . . . 11
โข (ยฌ
๐ โ โ โ
if(๐ โ โ,
((๐ต /L
๐)โ(๐ pCnt ๐)), 1) = 1) |
134 | 132, 133 | oveq12d 7376 |
. . . . . . . . . 10
โข (ยฌ
๐ โ โ โ
(if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)) = (1 ยท 1)) |
135 | 130, 131,
134 | 3eqtr4a 2803 |
. . . . . . . . 9
โข (ยฌ
๐ โ โ โ
if(๐ โ โ,
(((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = (if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))) |
136 | 135 | adantl 483 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ยฌ ๐ โ โ) โ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = (if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))) |
137 | 128, 136 | pm2.61dan 812 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = (if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))) |
138 | 137 | adantr 482 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = (if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))) |
139 | 92 | adantl 483 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ๐ โ โ) |
140 | | eleq1w 2821 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
141 | | oveq2 7366 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด ยท ๐ต) /L ๐)) |
142 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ pCnt ๐) = (๐ pCnt ๐)) |
143 | 141, 142 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = ๐ โ (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)) = (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐))) |
144 | 140, 143 | ifbieq1d 4511 |
. . . . . . . 8
โข (๐ = ๐ โ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) = if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)) |
145 | | eqid 2737 |
. . . . . . . 8
โข (๐ โ โ โฆ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)) = (๐ โ โ โฆ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)) |
146 | | ovex 7391 |
. . . . . . . . 9
โข (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)) โ V |
147 | | 1ex 11152 |
. . . . . . . . 9
โข 1 โ
V |
148 | 146, 147 | ifex 4537 |
. . . . . . . 8
โข if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1) โ V |
149 | 144, 145,
148 | fvmpt 6949 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ โ โฆ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1))โ๐) = if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)) |
150 | 139, 149 | syl 17 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ((๐ โ โ โฆ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1))โ๐) = if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)) |
151 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ด /L ๐) = (๐ด /L ๐)) |
152 | 151, 142 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ด /L ๐)โ(๐ pCnt ๐)) = ((๐ด /L ๐)โ(๐ pCnt ๐))) |
153 | 140, 152 | ifbieq1d 4511 |
. . . . . . . . 9
โข (๐ = ๐ โ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) = if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)) |
154 | | ovex 7391 |
. . . . . . . . . 10
โข ((๐ด /L ๐)โ(๐ pCnt ๐)) โ V |
155 | 154, 147 | ifex 4537 |
. . . . . . . . 9
โข if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) โ V |
156 | 153, 89, 155 | fvmpt 6949 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1))โ๐) = if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)) |
157 | 139, 156 | syl 17 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1))โ๐) = if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)) |
158 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ต /L ๐) = (๐ต /L ๐)) |
159 | 158, 142 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ต /L ๐)โ(๐ pCnt ๐)) = ((๐ต /L ๐)โ(๐ pCnt ๐))) |
160 | 140, 159 | ifbieq1d 4511 |
. . . . . . . . 9
โข (๐ = ๐ โ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1) = if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)) |
161 | | ovex 7391 |
. . . . . . . . . 10
โข ((๐ต /L ๐)โ(๐ pCnt ๐)) โ V |
162 | 161, 147 | ifex 4537 |
. . . . . . . . 9
โข if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1) โ V |
163 | 160, 97, 162 | fvmpt 6949 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))โ๐) = if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)) |
164 | 139, 163 | syl 17 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ((๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))โ๐) = if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)) |
165 | 157, 164 | oveq12d 7376 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ (((๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1))โ๐) ยท ((๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))โ๐)) = (if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1) ยท if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))) |
166 | 138, 150,
165 | 3eqtr4d 2787 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง ๐ โ (1...(absโ๐))) โ ((๐ โ โ โฆ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1))โ๐) = (((๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1))โ๐) ยท ((๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1))โ๐))) |
167 | 85, 95, 102, 166 | prodfmul 15776 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, (((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)) = ((seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)) ยท (seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) |
168 | 80, 167 | oveq12d 7376 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
(((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐))) = ((if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1)) ยท ((seq1( ยท
, (๐ โ โ โฆ
if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)) ยท (seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐))))) |
169 | 30 | adantr 482 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (๐ด ยท ๐ต) โ โค) |
170 | 145 | lgsval4 26668 |
. . . 4
โข (((๐ด ยท ๐ต) โ โค โง ๐ โ โค โง ๐ โ 0) โ ((๐ด ยท ๐ต) /L ๐) = (if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
(((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) |
171 | 169, 87, 88, 170 | syl3anc 1372 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ((๐ด ยท ๐ต) /L ๐) = (if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
(((๐ด ยท ๐ต) /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) |
172 | 89 | lgsval4 26668 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ด /L ๐) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) |
173 | 86, 87, 88, 172 | syl3anc 1372 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (๐ด /L ๐) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) |
174 | 97 | lgsval4 26668 |
. . . . . 6
โข ((๐ต โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ต /L ๐) = (if((๐ < 0 โง ๐ต < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
((๐ต /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) |
175 | 96, 87, 88, 174 | syl3anc 1372 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (๐ต /L ๐) = (if((๐ < 0 โง ๐ต < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
((๐ต /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) |
176 | 173, 175 | oveq12d 7376 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ((๐ด /L ๐) ยท (๐ต /L ๐)) = ((if((๐ < 0 โง ๐ด < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐))) ยท (if((๐ < 0 โง ๐ต < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
((๐ต /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐))))) |
177 | | neg1cn 12268 |
. . . . . . 7
โข -1 โ
โ |
178 | 177, 1 | ifcli 4534 |
. . . . . 6
โข if((๐ < 0 โง ๐ด < 0), -1, 1) โ
โ |
179 | 178 | a1i 11 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ if((๐ < 0 โง ๐ด < 0), -1, 1) โ
โ) |
180 | | mulcl 11136 |
. . . . . . 7
โข ((๐ โ โ โง ๐ฅ โ โ) โ (๐ ยท ๐ฅ) โ โ) |
181 | 180 | adantl 483 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค โง ๐ โ
โค) โง (๐ด โ 0
โง ๐ต โ 0)) โง
๐ โ 0) โง (๐ โ โ โง ๐ฅ โ โ)) โ (๐ ยท ๐ฅ) โ โ) |
182 | 85, 95, 181 | seqcl 13929 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)) โ โ) |
183 | 177, 1 | ifcli 4534 |
. . . . . 6
โข if((๐ < 0 โง ๐ต < 0), -1, 1) โ
โ |
184 | 183 | a1i 11 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ if((๐ < 0 โง ๐ต < 0), -1, 1) โ
โ) |
185 | 85, 102, 181 | seqcl 13929 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ (seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)) โ โ) |
186 | 179, 182,
184, 185 | mul4d 11368 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ((if((๐ < 0 โง ๐ด < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐))) ยท (if((๐ < 0 โง ๐ต < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
((๐ต /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) = ((if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1)) ยท ((seq1( ยท
, (๐ โ โ โฆ
if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)) ยท (seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐))))) |
187 | 176, 186 | eqtrd 2777 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ((๐ด /L ๐) ยท (๐ต /L ๐)) = ((if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1)) ยท ((seq1( ยท
, (๐ โ โ โฆ
if(๐ โ โ,
((๐ด /L
๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐)) ยท (seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, ((๐ต /L ๐)โ(๐ pCnt ๐)), 1)))โ(absโ๐))))) |
188 | 168, 171,
187 | 3eqtr4d 2787 |
. 2
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ โ 0) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
189 | 78, 188 | pm2.61dane 3033 |
1
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |