Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ด /L ๐ฅ) = (๐ด /L ๐)) |
2 | 1 | oveq1d 7424 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐ด /L ๐ฅ) ยท (๐ด /L 0)) = ((๐ด /L ๐) ยท (๐ด /L 0))) |
3 | 2 | eqeq2d 2744 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ด /L 0) = ((๐ด /L ๐ฅ) ยท (๐ด /L 0)) โ (๐ด /L 0) =
((๐ด /L
๐) ยท (๐ด /L
0)))) |
4 | | sq1 14159 |
. . . . . . . . . . . . . . . 16
โข
(1โ2) = 1 |
5 | 4 | eqeq2i 2746 |
. . . . . . . . . . . . . . 15
โข ((๐ดโ2) = (1โ2) โ
(๐ดโ2) =
1) |
6 | | nn0re 12481 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โ0
โ ๐ด โ
โ) |
7 | | nn0ge0 12497 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โ0
โ 0 โค ๐ด) |
8 | | 1re 11214 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
โ |
9 | | 0le1 11737 |
. . . . . . . . . . . . . . . . . 18
โข 0 โค
1 |
10 | | sq11 14096 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง 0 โค
๐ด) โง (1 โ โ
โง 0 โค 1)) โ ((๐ดโ2) = (1โ2) โ ๐ด = 1)) |
11 | 8, 9, 10 | mpanr12 704 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ดโ2) = (1โ2) โ
๐ด = 1)) |
12 | 6, 7, 11 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ0
โ ((๐ดโ2) =
(1โ2) โ ๐ด =
1)) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ0
โง ๐ฅ โ โค)
โ ((๐ดโ2) =
(1โ2) โ ๐ด =
1)) |
14 | 5, 13 | bitr3id 285 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ0
โง ๐ฅ โ โค)
โ ((๐ดโ2) = 1
โ ๐ด =
1)) |
15 | 14 | biimpa 478 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ ๐ด =
1) |
16 | 15 | oveq1d 7424 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ (๐ด
/L ๐ฅ) =
(1 /L ๐ฅ)) |
17 | | 1lgs 26843 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โค โ (1
/L ๐ฅ) =
1) |
18 | 17 | ad2antlr 726 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ (1 /L ๐ฅ) = 1) |
19 | 16, 18 | eqtrd 2773 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ (๐ด
/L ๐ฅ) =
1) |
20 | 19 | oveq1d 7424 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ ((๐ด
/L ๐ฅ)
ยท (๐ด
/L 0)) = (1 ยท (๐ด /L 0))) |
21 | | nn0z 12583 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ0
โ ๐ด โ
โค) |
22 | 21 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ ๐ด โ
โค) |
23 | | 0z 12569 |
. . . . . . . . . . . . 13
โข 0 โ
โค |
24 | | lgscl 26814 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง 0 โ
โค) โ (๐ด
/L 0) โ โค) |
25 | 22, 23, 24 | sylancl 587 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ (๐ด
/L 0) โ โค) |
26 | 25 | zcnd 12667 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ (๐ด
/L 0) โ โ) |
27 | 26 | mullidd 11232 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ (1 ยท (๐ด
/L 0)) = (๐ด /L 0)) |
28 | 20, 27 | eqtr2d 2774 |
. . . . . . . . 9
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) = 1)
โ (๐ด
/L 0) = ((๐ด /L ๐ฅ) ยท (๐ด /L 0))) |
29 | | lgscl 26814 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง ๐ฅ โ โค) โ (๐ด /L ๐ฅ) โ
โค) |
30 | 21, 29 | sylan 581 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ0
โง ๐ฅ โ โค)
โ (๐ด
/L ๐ฅ)
โ โค) |
31 | 30 | zcnd 12667 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ฅ โ โค)
โ (๐ด
/L ๐ฅ)
โ โ) |
32 | 31 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) โ 1)
โ (๐ด
/L ๐ฅ)
โ โ) |
33 | 32 | mul01d 11413 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) โ 1)
โ ((๐ด
/L ๐ฅ)
ยท 0) = 0) |
34 | 21 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ0
โง ๐ฅ โ โค)
โ ๐ด โ
โค) |
35 | | lgs0 26813 |
. . . . . . . . . . . . 13
โข (๐ด โ โค โ (๐ด /L 0) =
if((๐ดโ2) = 1, 1,
0)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ฅ โ โค)
โ (๐ด
/L 0) = if((๐ดโ2) = 1, 1, 0)) |
37 | | ifnefalse 4541 |
. . . . . . . . . . . 12
โข ((๐ดโ2) โ 1 โ if((๐ดโ2) = 1, 1, 0) =
0) |
38 | 36, 37 | sylan9eq 2793 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) โ 1)
โ (๐ด
/L 0) = 0) |
39 | 38 | oveq2d 7425 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) โ 1)
โ ((๐ด
/L ๐ฅ)
ยท (๐ด
/L 0)) = ((๐ด /L ๐ฅ) ยท 0)) |
40 | 33, 39, 38 | 3eqtr4rd 2784 |
. . . . . . . . 9
โข (((๐ด โ โ0
โง ๐ฅ โ โค)
โง (๐ดโ2) โ 1)
โ (๐ด
/L 0) = ((๐ด /L ๐ฅ) ยท (๐ด /L 0))) |
41 | 28, 40 | pm2.61dane 3030 |
. . . . . . . 8
โข ((๐ด โ โ0
โง ๐ฅ โ โค)
โ (๐ด
/L 0) = ((๐ด /L ๐ฅ) ยท (๐ด /L 0))) |
42 | 41 | ralrimiva 3147 |
. . . . . . 7
โข (๐ด โ โ0
โ โ๐ฅ โ
โค (๐ด
/L 0) = ((๐ด /L ๐ฅ) ยท (๐ด /L 0))) |
43 | 42 | 3ad2ant1 1134 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ โ๐ฅ โ
โค (๐ด
/L 0) = ((๐ด /L ๐ฅ) ยท (๐ด /L 0))) |
44 | | simp3 1139 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ ๐ โ
โค) |
45 | 3, 43, 44 | rspcdva 3614 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (๐ด
/L 0) = ((๐ด /L ๐) ยท (๐ด /L 0))) |
46 | 45 | adantr 482 |
. . . 4
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L 0) =
((๐ด /L
๐) ยท (๐ด /L
0))) |
47 | 21 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ ๐ด โ
โค) |
48 | 47, 23, 24 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (๐ด
/L 0) โ โค) |
49 | 48 | zcnd 12667 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (๐ด
/L 0) โ โ) |
50 | 49 | adantr 482 |
. . . . 5
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L 0) โ
โ) |
51 | | lgscl 26814 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ โค) โ (๐ด /L ๐) โ
โค) |
52 | 47, 44, 51 | syl2anc 585 |
. . . . . . 7
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (๐ด
/L ๐)
โ โค) |
53 | 52 | zcnd 12667 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (๐ด
/L ๐)
โ โ) |
54 | 53 | adantr 482 |
. . . . 5
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L ๐) โ
โ) |
55 | 50, 54 | mulcomd 11235 |
. . . 4
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ ((๐ด /L 0)
ยท (๐ด
/L ๐)) =
((๐ด /L
๐) ยท (๐ด /L
0))) |
56 | 46, 55 | eqtr4d 2776 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L 0) =
((๐ด /L 0)
ยท (๐ด
/L ๐))) |
57 | | oveq1 7416 |
. . . . 5
โข (๐ = 0 โ (๐ ยท ๐) = (0 ยท ๐)) |
58 | 44 | zcnd 12667 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ ๐ โ
โ) |
59 | 58 | mul02d 11412 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (0 ยท ๐) =
0) |
60 | 57, 59 | sylan9eqr 2795 |
. . . 4
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ ยท ๐) = 0) |
61 | 60 | oveq2d 7425 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L (๐ ยท ๐)) = (๐ด /L 0)) |
62 | | simpr 486 |
. . . . 5
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ ๐ = 0) |
63 | 62 | oveq2d 7425 |
. . . 4
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L ๐) = (๐ด /L 0)) |
64 | 63 | oveq1d 7424 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ ((๐ด /L ๐) ยท (๐ด /L ๐)) = ((๐ด /L 0) ยท (๐ด /L ๐))) |
65 | 56, 61, 64 | 3eqtr4d 2783 |
. 2
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L (๐ ยท ๐)) = ((๐ด /L ๐) ยท (๐ด /L ๐))) |
66 | | oveq2 7417 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ด /L ๐ฅ) = (๐ด /L ๐)) |
67 | 66 | oveq1d 7424 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ด /L ๐ฅ) ยท (๐ด /L 0)) = ((๐ด /L ๐) ยท (๐ด /L 0))) |
68 | 67 | eqeq2d 2744 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐ด /L 0) = ((๐ด /L ๐ฅ) ยท (๐ด /L 0)) โ (๐ด /L 0) =
((๐ด /L
๐) ยท (๐ด /L
0)))) |
69 | | simp2 1138 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ ๐ โ
โค) |
70 | 68, 43, 69 | rspcdva 3614 |
. . . 4
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (๐ด
/L 0) = ((๐ด /L ๐) ยท (๐ด /L 0))) |
71 | 70 | adantr 482 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L 0) =
((๐ด /L
๐) ยท (๐ด /L
0))) |
72 | | oveq2 7417 |
. . . . 5
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0)) |
73 | 69 | zcnd 12667 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ ๐ โ
โ) |
74 | 73 | mul01d 11413 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (๐ ยท 0) =
0) |
75 | 72, 74 | sylan9eqr 2795 |
. . . 4
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ ยท ๐) = 0) |
76 | 75 | oveq2d 7425 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L (๐ ยท ๐)) = (๐ด /L 0)) |
77 | | simpr 486 |
. . . . 5
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ ๐ = 0) |
78 | 77 | oveq2d 7425 |
. . . 4
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L ๐) = (๐ด /L 0)) |
79 | 78 | oveq2d 7425 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ ((๐ด /L ๐) ยท (๐ด /L ๐)) = ((๐ด /L ๐) ยท (๐ด /L 0))) |
80 | 71, 76, 79 | 3eqtr4d 2783 |
. 2
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง ๐ = 0) โ (๐ด /L (๐ ยท ๐)) = ((๐ด /L ๐) ยท (๐ด /L ๐))) |
81 | | lgsdi 26837 |
. . 3
โข (((๐ด โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ โ 0 โง ๐ โ 0)) โ (๐ด /L (๐ ยท ๐)) = ((๐ด /L ๐) ยท (๐ด /L ๐))) |
82 | 21, 81 | syl3anl1 1413 |
. 2
โข (((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โง (๐ โ 0 โง ๐ โ 0)) โ (๐ด /L (๐ ยท ๐)) = ((๐ด /L ๐) ยท (๐ด /L ๐))) |
83 | 65, 80, 82 | pm2.61da2ne 3031 |
1
โข ((๐ด โ โ0
โง ๐ โ โค
โง ๐ โ โค)
โ (๐ด
/L (๐
ยท ๐)) = ((๐ด /L ๐) ยท (๐ด /L ๐))) |