Step | Hyp | Ref
| Expression |
1 | | zssq 12886 |
. . . . . . . 8
β’ β€
β β |
2 | | simp1 1137 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β π΄ β
β€) |
3 | 1, 2 | sselid 3943 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β π΄ β
β) |
4 | | simp2 1138 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β π΅ β
β€) |
5 | 1, 4 | sselid 3943 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β π΅ β
β) |
6 | | nnne0 12192 |
. . . . . . . . . . . 12
β’ (-π΅ β β β -π΅ β 0) |
7 | 6 | 3ad2ant3 1136 |
. . . . . . . . . . 11
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -π΅ β 0) |
8 | | neg0 11452 |
. . . . . . . . . . . 12
β’ -0 =
0 |
9 | 8 | neeq2i 3006 |
. . . . . . . . . . 11
β’ (-π΅ β -0 β -π΅ β 0) |
10 | 7, 9 | sylibr 233 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -π΅ β -0) |
11 | 10 | neneqd 2945 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β Β¬
-π΅ = -0) |
12 | 4 | zcnd 12613 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β π΅ β
β) |
13 | | 0cnd 11153 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β 0 β
β) |
14 | 12, 13 | neg11ad 11513 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (-π΅ = -0 β π΅ = 0)) |
15 | 11, 14 | mtbid 324 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β Β¬
π΅ = 0) |
16 | 15 | neqned 2947 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β π΅ β 0) |
17 | | qdivcl 12900 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π΄ / π΅) β β) |
18 | 3, 5, 16, 17 | syl3anc 1372 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (π΄ / π΅) β β) |
19 | | qnumcl 16620 |
. . . . . 6
β’ ((π΄ / π΅) β β β (numerβ(π΄ / π΅)) β β€) |
20 | 18, 19 | syl 17 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(numerβ(π΄ / π΅)) β
β€) |
21 | 20 | zcnd 12613 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(numerβ(π΄ / π΅)) β
β) |
22 | | simpl 484 |
. . . . . . 7
β’ ((π΄ β β€ β§ -π΅ β β) β π΄ β
β€) |
23 | 22 | zcnd 12613 |
. . . . . 6
β’ ((π΄ β β€ β§ -π΅ β β) β π΄ β
β) |
24 | 23 | 3adant2 1132 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β π΄ β
β) |
25 | 2, 4 | gcdcld 16393 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (π΄ gcd π΅) β
β0) |
26 | 25 | nn0cnd 12480 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (π΄ gcd π΅) β β) |
27 | 26 | negcld 11504 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -(π΄ gcd π΅) β β) |
28 | 15 | intnand 490 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β Β¬
(π΄ = 0 β§ π΅ = 0)) |
29 | | gcdeq0 16402 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅) = 0 β (π΄ = 0 β§ π΅ = 0))) |
30 | 29 | necon3abid 2977 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅) β 0 β Β¬ (π΄ = 0 β§ π΅ = 0))) |
31 | 30 | 3adant3 1133 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β ((π΄ gcd π΅) β 0 β Β¬ (π΄ = 0 β§ π΅ = 0))) |
32 | 28, 31 | mpbird 257 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (π΄ gcd π΅) β 0) |
33 | 26, 32 | negne0d 11515 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -(π΄ gcd π΅) β 0) |
34 | 24, 27, 33 | divcld 11936 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (π΄ / -(π΄ gcd π΅)) β β) |
35 | 24, 12, 16 | divneg2d 11950 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -(π΄ / π΅) = (π΄ / -π΅)) |
36 | 35 | fveq2d 6847 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(numerβ-(π΄ / π΅)) = (numerβ(π΄ / -π΅))) |
37 | | numdenneg 31762 |
. . . . . . 7
β’ ((π΄ / π΅) β β β
((numerβ-(π΄ / π΅)) = -(numerβ(π΄ / π΅)) β§ (denomβ-(π΄ / π΅)) = (denomβ(π΄ / π΅)))) |
38 | 37 | simpld 496 |
. . . . . 6
β’ ((π΄ / π΅) β β β (numerβ-(π΄ / π΅)) = -(numerβ(π΄ / π΅))) |
39 | 18, 38 | syl 17 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(numerβ-(π΄ / π΅)) = -(numerβ(π΄ / π΅))) |
40 | | gcdneg 16407 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ gcd -π΅) = (π΄ gcd π΅)) |
41 | 40 | 3adant3 1133 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (π΄ gcd -π΅) = (π΄ gcd π΅)) |
42 | 41 | oveq2d 7374 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (π΄ / (π΄ gcd -π΅)) = (π΄ / (π΄ gcd π΅))) |
43 | | divnumden 16628 |
. . . . . . . 8
β’ ((π΄ β β€ β§ -π΅ β β) β
((numerβ(π΄ / -π΅)) = (π΄ / (π΄ gcd -π΅)) β§ (denomβ(π΄ / -π΅)) = (-π΅ / (π΄ gcd -π΅)))) |
44 | 43 | simpld 496 |
. . . . . . 7
β’ ((π΄ β β€ β§ -π΅ β β) β
(numerβ(π΄ / -π΅)) = (π΄ / (π΄ gcd -π΅))) |
45 | 44 | 3adant2 1132 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(numerβ(π΄ / -π΅)) = (π΄ / (π΄ gcd -π΅))) |
46 | 24, 27, 33 | divnegd 11949 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -(π΄ / -(π΄ gcd π΅)) = (-π΄ / -(π΄ gcd π΅))) |
47 | 24, 26, 32 | div2negd 11951 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (-π΄ / -(π΄ gcd π΅)) = (π΄ / (π΄ gcd π΅))) |
48 | 46, 47 | eqtrd 2773 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -(π΄ / -(π΄ gcd π΅)) = (π΄ / (π΄ gcd π΅))) |
49 | 42, 45, 48 | 3eqtr4d 2783 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(numerβ(π΄ / -π΅)) = -(π΄ / -(π΄ gcd π΅))) |
50 | 36, 39, 49 | 3eqtr3d 2781 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
-(numerβ(π΄ / π΅)) = -(π΄ / -(π΄ gcd π΅))) |
51 | 21, 34, 50 | neg11d 11529 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(numerβ(π΄ / π΅)) = (π΄ / -(π΄ gcd π΅))) |
52 | 24, 26, 32 | divneg2d 11950 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -(π΄ / (π΄ gcd π΅)) = (π΄ / -(π΄ gcd π΅))) |
53 | 51, 52 | eqtr4d 2776 |
. 2
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(numerβ(π΄ / π΅)) = -(π΄ / (π΄ gcd π΅))) |
54 | 35 | fveq2d 6847 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(denomβ-(π΄ / π΅)) = (denomβ(π΄ / -π΅))) |
55 | 37 | simprd 497 |
. . . . 5
β’ ((π΄ / π΅) β β β (denomβ-(π΄ / π΅)) = (denomβ(π΄ / π΅))) |
56 | 18, 55 | syl 17 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(denomβ-(π΄ / π΅)) = (denomβ(π΄ / π΅))) |
57 | 41 | oveq2d 7374 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (-π΅ / (π΄ gcd -π΅)) = (-π΅ / (π΄ gcd π΅))) |
58 | 43 | simprd 497 |
. . . . . 6
β’ ((π΄ β β€ β§ -π΅ β β) β
(denomβ(π΄ / -π΅)) = (-π΅ / (π΄ gcd -π΅))) |
59 | 58 | 3adant2 1132 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(denomβ(π΄ / -π΅)) = (-π΅ / (π΄ gcd -π΅))) |
60 | 12, 26, 32 | divneg2d 11950 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -(π΅ / (π΄ gcd π΅)) = (π΅ / -(π΄ gcd π΅))) |
61 | 12, 26, 32 | divnegd 11949 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β -(π΅ / (π΄ gcd π΅)) = (-π΅ / (π΄ gcd π΅))) |
62 | 60, 61 | eqtr3d 2775 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β (π΅ / -(π΄ gcd π΅)) = (-π΅ / (π΄ gcd π΅))) |
63 | 57, 59, 62 | 3eqtr4d 2783 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(denomβ(π΄ / -π΅)) = (π΅ / -(π΄ gcd π΅))) |
64 | 54, 56, 63 | 3eqtr3d 2781 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(denomβ(π΄ / π΅)) = (π΅ / -(π΄ gcd π΅))) |
65 | 64, 60 | eqtr4d 2776 |
. 2
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
(denomβ(π΄ / π΅)) = -(π΅ / (π΄ gcd π΅))) |
66 | 53, 65 | jca 513 |
1
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β
((numerβ(π΄ / π΅)) = -(π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = -(π΅ / (π΄ gcd π΅)))) |