Step | Hyp | Ref
| Expression |
1 | | zsqcl 10558 |
. . . . 5
โข (๐ด โ โค โ (๐ดโ2) โ
โค) |
2 | 1 | adantr 276 |
. . . 4
โข ((๐ด โ โค โง ๐ด โ 0) โ (๐ดโ2) โ
โค) |
3 | | simpl 109 |
. . . 4
โข ((๐ต โ โค โง ๐ต โ 0) โ ๐ต โ
โค) |
4 | | simpl 109 |
. . . 4
โข ((๐ โ โค โง (๐ด gcd ๐) = 1) โ ๐ โ โค) |
5 | 2, 3, 4 | 3anim123i 1184 |
. . 3
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ ((๐ดโ2) โ โค โง ๐ต โ โค โง ๐ โ
โค)) |
6 | | zcn 9229 |
. . . . . . 7
โข (๐ด โ โค โ ๐ด โ
โ) |
7 | | sqne0 10553 |
. . . . . . 7
โข (๐ด โ โ โ ((๐ดโ2) โ 0 โ ๐ด โ 0)) |
8 | 6, 7 | syl 14 |
. . . . . 6
โข (๐ด โ โค โ ((๐ดโ2) โ 0 โ ๐ด โ 0)) |
9 | 8 | biimpar 297 |
. . . . 5
โข ((๐ด โ โค โง ๐ด โ 0) โ (๐ดโ2) โ
0) |
10 | | simpr 110 |
. . . . 5
โข ((๐ต โ โค โง ๐ต โ 0) โ ๐ต โ 0) |
11 | 9, 10 | anim12i 338 |
. . . 4
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ((๐ดโ2) โ 0 โง ๐ต โ 0)) |
12 | 11 | 3adant3 1017 |
. . 3
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ ((๐ดโ2) โ 0 โง ๐ต โ 0)) |
13 | | lgsdir 13929 |
. . 3
โข ((((๐ดโ2) โ โค โง
๐ต โ โค โง
๐ โ โค) โง
((๐ดโ2) โ 0 โง
๐ต โ 0)) โ (((๐ดโ2) ยท ๐ต) /L ๐) = (((๐ดโ2) /L ๐) ยท (๐ต /L ๐))) |
14 | 5, 12, 13 | syl2anc 411 |
. 2
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (((๐ดโ2) ยท ๐ต) /L ๐) = (((๐ดโ2) /L ๐) ยท (๐ต /L ๐))) |
15 | | 3anass 982 |
. . . . . 6
โข (((๐ด โ โค โง ๐ด โ 0) โง ๐ โ โค โง (๐ด gcd ๐) = 1) โ ((๐ด โ โค โง ๐ด โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1))) |
16 | 15 | biimpri 133 |
. . . . 5
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ ((๐ด โ โค โง ๐ด โ 0) โง ๐ โ โค โง (๐ด gcd ๐) = 1)) |
17 | 16 | 3adant2 1016 |
. . . 4
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ ((๐ด โ โค โง ๐ด โ 0) โง ๐ โ โค โง (๐ด gcd ๐) = 1)) |
18 | | lgssq 13934 |
. . . 4
โข (((๐ด โ โค โง ๐ด โ 0) โง ๐ โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ2) /L ๐) = 1) |
19 | 17, 18 | syl 14 |
. . 3
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ ((๐ดโ2) /L ๐) = 1) |
20 | 19 | oveq1d 5880 |
. 2
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (((๐ดโ2) /L ๐) ยท (๐ต /L ๐)) = (1 ยท (๐ต /L ๐))) |
21 | 3, 4 | anim12i 338 |
. . . . . 6
โข (((๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (๐ต โ โค โง ๐ โ โค)) |
22 | 21 | 3adant1 1015 |
. . . . 5
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (๐ต โ โค โง ๐ โ โค)) |
23 | | lgscl 13908 |
. . . . 5
โข ((๐ต โ โค โง ๐ โ โค) โ (๐ต /L ๐) โ
โค) |
24 | 22, 23 | syl 14 |
. . . 4
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (๐ต /L ๐) โ โค) |
25 | 24 | zcnd 9347 |
. . 3
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (๐ต /L ๐) โ โ) |
26 | 25 | mulid2d 7950 |
. 2
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (1 ยท (๐ต /L ๐)) = (๐ต /L ๐)) |
27 | 14, 20, 26 | 3eqtrd 2212 |
1
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (((๐ดโ2) ยท ๐ต) /L ๐) = (๐ต /L ๐)) |