Step | Hyp | Ref
| Expression |
1 | | oveq1 5882 |
. . . . . . . . 9
โข (๐ฅ = ๐ต โ (๐ฅ /L ๐) = (๐ต /L ๐)) |
2 | 1 | oveq1d 5890 |
. . . . . . . 8
โข (๐ฅ = ๐ต โ ((๐ฅ /L ๐) ยท (0 /L ๐)) = ((๐ต /L ๐) ยท (0 /L ๐))) |
3 | 2 | eqeq2d 2189 |
. . . . . . 7
โข (๐ฅ = ๐ต โ ((0 /L ๐) = ((๐ฅ /L ๐) ยท (0 /L ๐)) โ (0
/L ๐) =
((๐ต /L
๐) ยท (0
/L ๐)))) |
4 | | id 19 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ ๐ฅ โ
โค) |
5 | | nn0z 9273 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ๐ โ
โค) |
6 | | lgscl 14418 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ๐ โ โค) โ (๐ฅ /L ๐) โ
โค) |
7 | 4, 5, 6 | syl2anr 290 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (๐ฅ
/L ๐)
โ โค) |
8 | 7 | zcnd 9376 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (๐ฅ
/L ๐)
โ โ) |
9 | 8 | adantr 276 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) = 0) โ (๐ฅ /L ๐) โ โ) |
10 | 9 | mul01d 8350 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) = 0) โ ((๐ฅ /L ๐) ยท 0) = 0) |
11 | | simpr 110 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) = 0) โ (0 /L ๐) = 0) |
12 | 11 | oveq2d 5891 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) = 0) โ ((๐ฅ /L ๐) ยท (0 /L ๐)) = ((๐ฅ /L ๐) ยท 0)) |
13 | 10, 12, 11 | 3eqtr4rd 2221 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) = 0) โ (0 /L ๐) = ((๐ฅ /L ๐) ยท (0 /L ๐))) |
14 | | 0z 9264 |
. . . . . . . . . . . . . . 15
โข 0 โ
โค |
15 | 5 | adantr 276 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ ๐ โ
โค) |
16 | | lgsne0 14442 |
. . . . . . . . . . . . . . 15
โข ((0
โ โค โง ๐
โ โค) โ ((0 /L ๐) โ 0 โ (0 gcd ๐) = 1)) |
17 | 14, 15, 16 | sylancr 414 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ ((0 /L ๐) โ 0 โ (0 gcd ๐) = 1)) |
18 | | gcdcom 11974 |
. . . . . . . . . . . . . . . . . 18
โข ((0
โ โค โง ๐
โ โค) โ (0 gcd ๐) = (๐ gcd 0)) |
19 | 14, 15, 18 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (0 gcd ๐) = (๐ gcd 0)) |
20 | | nn0gcdid0 11982 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (๐ gcd 0) = ๐) |
21 | 20 | adantr 276 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (๐ gcd 0) = ๐) |
22 | 19, 21 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (0 gcd ๐) = ๐) |
23 | 22 | eqeq1d 2186 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ ((0 gcd ๐) = 1
โ ๐ =
1)) |
24 | | lgs1 14448 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ (๐ฅ /L 1) =
1) |
25 | 24 | adantl 277 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (๐ฅ
/L 1) = 1) |
26 | | oveq2 5883 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 1 โ (๐ฅ /L ๐) = (๐ฅ /L 1)) |
27 | 26 | eqeq1d 2186 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ ((๐ฅ /L ๐) = 1 โ (๐ฅ /L 1) =
1)) |
28 | 25, 27 | syl5ibrcom 157 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (๐ = 1 โ (๐ฅ /L ๐) = 1)) |
29 | 23, 28 | sylbid 150 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ ((0 gcd ๐) = 1
โ (๐ฅ
/L ๐) =
1)) |
30 | 17, 29 | sylbid 150 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ ((0 /L ๐) โ 0 โ (๐ฅ /L ๐) = 1)) |
31 | 30 | imp 124 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) โ 0) โ (๐ฅ /L ๐) = 1) |
32 | 31 | oveq1d 5890 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) โ 0) โ ((๐ฅ /L ๐) ยท (0 /L ๐)) = (1 ยท (0
/L ๐))) |
33 | 5 | ad2antrr 488 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) โ 0) โ ๐ โ โค) |
34 | | lgscl 14418 |
. . . . . . . . . . . . . 14
โข ((0
โ โค โง ๐
โ โค) โ (0 /L ๐) โ โค) |
35 | 14, 33, 34 | sylancr 414 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) โ 0) โ (0 /L
๐) โ
โค) |
36 | 35 | zcnd 9376 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) โ 0) โ (0 /L
๐) โ
โ) |
37 | 36 | mulid2d 7976 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) โ 0) โ (1 ยท (0
/L ๐)) =
(0 /L ๐)) |
38 | 32, 37 | eqtr2d 2211 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง ๐ฅ โ โค)
โง (0 /L ๐) โ 0) โ (0 /L
๐) = ((๐ฅ /L ๐) ยท (0 /L ๐))) |
39 | 14, 15, 34 | sylancr 414 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (0 /L ๐) โ โค) |
40 | | zdceq 9328 |
. . . . . . . . . . . 12
โข (((0
/L ๐)
โ โค โง 0 โ โค) โ DECID (0
/L ๐) =
0) |
41 | 39, 14, 40 | sylancl 413 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ DECID (0 /L ๐) = 0) |
42 | | dcne 2358 |
. . . . . . . . . . 11
โข
(DECID (0 /L ๐) = 0 โ ((0 /L ๐) = 0 โจ (0
/L ๐)
โ 0)) |
43 | 41, 42 | sylib 122 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ ((0 /L ๐) = 0 โจ (0 /L ๐) โ 0)) |
44 | 13, 38, 43 | mpjaodan 798 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (0 /L ๐) = ((๐ฅ /L ๐) ยท (0 /L ๐))) |
45 | 44 | ralrimiva 2550 |
. . . . . . . 8
โข (๐ โ โ0
โ โ๐ฅ โ
โค (0 /L ๐) = ((๐ฅ /L ๐) ยท (0 /L ๐))) |
46 | 45 | 3ad2ant3 1020 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ โ๐ฅ โ
โค (0 /L ๐) = ((๐ฅ /L ๐) ยท (0 /L ๐))) |
47 | | simp2 998 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ ๐ต โ
โค) |
48 | 3, 46, 47 | rspcdva 2847 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ (0 /L ๐) = ((๐ต /L ๐) ยท (0 /L ๐))) |
49 | 48 | adantr 276 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ (0
/L ๐) =
((๐ต /L
๐) ยท (0
/L ๐))) |
50 | 5 | 3ad2ant3 1020 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ ๐ โ
โค) |
51 | 14, 50, 34 | sylancr 414 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ (0 /L ๐) โ โค) |
52 | 51 | zcnd 9376 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ (0 /L ๐) โ โ) |
53 | 52 | adantr 276 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ (0
/L ๐)
โ โ) |
54 | | lgscl 14418 |
. . . . . . . . 9
โข ((๐ต โ โค โง ๐ โ โค) โ (๐ต /L ๐) โ
โค) |
55 | 47, 50, 54 | syl2anc 411 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ (๐ต
/L ๐)
โ โค) |
56 | 55 | zcnd 9376 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ (๐ต
/L ๐)
โ โ) |
57 | 56 | adantr 276 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ (๐ต /L ๐) โ
โ) |
58 | 53, 57 | mulcomd 7979 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ ((0
/L ๐)
ยท (๐ต
/L ๐)) =
((๐ต /L
๐) ยท (0
/L ๐))) |
59 | 49, 58 | eqtr4d 2213 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ (0
/L ๐) =
((0 /L ๐)
ยท (๐ต
/L ๐))) |
60 | | oveq1 5882 |
. . . . . 6
โข (๐ด = 0 โ (๐ด ยท ๐ต) = (0 ยท ๐ต)) |
61 | | zcn 9258 |
. . . . . . . 8
โข (๐ต โ โค โ ๐ต โ
โ) |
62 | 61 | 3ad2ant2 1019 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ ๐ต โ
โ) |
63 | 62 | mul02d 8349 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ (0 ยท ๐ต) =
0) |
64 | 60, 63 | sylan9eqr 2232 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ (๐ด ยท ๐ต) = 0) |
65 | 64 | oveq1d 5890 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ ((๐ด ยท ๐ต) /L ๐) = (0 /L ๐)) |
66 | | simpr 110 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ ๐ด = 0) |
67 | 66 | oveq1d 5890 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ (๐ด /L ๐) = (0 /L
๐)) |
68 | 67 | oveq1d 5890 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ ((๐ด /L ๐) ยท (๐ต /L ๐)) = ((0 /L ๐) ยท (๐ต /L ๐))) |
69 | 59, 65, 68 | 3eqtr4d 2220 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ด = 0) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
70 | | oveq1 5882 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ (๐ฅ /L ๐) = (๐ด /L ๐)) |
71 | 70 | oveq1d 5890 |
. . . . . . 7
โข (๐ฅ = ๐ด โ ((๐ฅ /L ๐) ยท (0 /L ๐)) = ((๐ด /L ๐) ยท (0 /L ๐))) |
72 | 71 | eqeq2d 2189 |
. . . . . 6
โข (๐ฅ = ๐ด โ ((0 /L ๐) = ((๐ฅ /L ๐) ยท (0 /L ๐)) โ (0
/L ๐) =
((๐ด /L
๐) ยท (0
/L ๐)))) |
73 | | simp1 997 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ ๐ด โ
โค) |
74 | 72, 46, 73 | rspcdva 2847 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ (0 /L ๐) = ((๐ด /L ๐) ยท (0 /L ๐))) |
75 | 74 | adantr 276 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ต = 0) โ (0
/L ๐) =
((๐ด /L
๐) ยท (0
/L ๐))) |
76 | | oveq2 5883 |
. . . . . 6
โข (๐ต = 0 โ (๐ด ยท ๐ต) = (๐ด ยท 0)) |
77 | 73 | zcnd 9376 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ ๐ด โ
โ) |
78 | 77 | mul01d 8350 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ (๐ด ยท 0) =
0) |
79 | 76, 78 | sylan9eqr 2232 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ต = 0) โ (๐ด ยท ๐ต) = 0) |
80 | 79 | oveq1d 5890 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ต = 0) โ ((๐ด ยท ๐ต) /L ๐) = (0 /L ๐)) |
81 | | simpr 110 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ต = 0) โ ๐ต = 0) |
82 | 81 | oveq1d 5890 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ต = 0) โ (๐ต /L ๐) = (0 /L
๐)) |
83 | 82 | oveq2d 5891 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ต = 0) โ ((๐ด /L ๐) ยท (๐ต /L ๐)) = ((๐ด /L ๐) ยท (0 /L ๐))) |
84 | 75, 80, 83 | 3eqtr4d 2220 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ๐ต = 0) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
85 | 69, 84 | jaodan 797 |
. 2
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง (๐ด = 0 โจ ๐ต = 0)) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
86 | | neanior 2434 |
. . 3
โข ((๐ด โ 0 โง ๐ต โ 0) โ ยฌ (๐ด = 0 โจ ๐ต = 0)) |
87 | | lgsdir 14439 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
88 | 5, 87 | syl3anl3 1288 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
89 | 86, 88 | sylan2br 288 |
. 2
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โง ยฌ (๐ด = 0 โจ
๐ต = 0)) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
90 | | zdceq 9328 |
. . . . 5
โข ((๐ด โ โค โง 0 โ
โค) โ DECID ๐ด = 0) |
91 | 73, 14, 90 | sylancl 413 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ DECID ๐ด = 0) |
92 | | zdceq 9328 |
. . . . 5
โข ((๐ต โ โค โง 0 โ
โค) โ DECID ๐ต = 0) |
93 | 47, 14, 92 | sylancl 413 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ DECID ๐ต = 0) |
94 | | dcor 935 |
. . . 4
โข
(DECID ๐ด = 0 โ (DECID ๐ต = 0 โ DECID
(๐ด = 0 โจ ๐ต = 0))) |
95 | 91, 93, 94 | sylc 62 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ DECID (๐ด = 0 โจ ๐ต = 0)) |
96 | | exmiddc 836 |
. . 3
โข
(DECID (๐ด = 0 โจ ๐ต = 0) โ ((๐ด = 0 โจ ๐ต = 0) โจ ยฌ (๐ด = 0 โจ ๐ต = 0))) |
97 | 95, 96 | syl 14 |
. 2
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ ((๐ด = 0 โจ ๐ต = 0) โจ ยฌ (๐ด = 0 โจ ๐ต = 0))) |
98 | 85, 89, 97 | mpjaodan 798 |
1
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0)
โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |