Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β π΄ β
β€) |
2 | | nnz 12527 |
. . . . 5
β’ (π΅ β β β π΅ β
β€) |
3 | 2 | adantl 483 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β π΅ β
β€) |
4 | | nnne0 12194 |
. . . . . . . 8
β’ (π΅ β β β π΅ β 0) |
5 | 4 | neneqd 2949 |
. . . . . . 7
β’ (π΅ β β β Β¬
π΅ = 0) |
6 | 5 | adantl 483 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β) β Β¬
π΅ = 0) |
7 | 6 | intnand 490 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β) β Β¬
(π΄ = 0 β§ π΅ = 0)) |
8 | | gcdn0cl 16389 |
. . . . 5
β’ (((π΄ β β€ β§ π΅ β β€) β§ Β¬
(π΄ = 0 β§ π΅ = 0)) β (π΄ gcd π΅) β β) |
9 | 1, 3, 7, 8 | syl21anc 837 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ gcd π΅) β β) |
10 | | gcddvds 16390 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅) β₯ π΄ β§ (π΄ gcd π΅) β₯ π΅)) |
11 | 2, 10 | sylan2 594 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β ((π΄ gcd π΅) β₯ π΄ β§ (π΄ gcd π΅) β₯ π΅)) |
12 | | gcddiv 16439 |
. . . 4
β’ (((π΄ β β€ β§ π΅ β β€ β§ (π΄ gcd π΅) β β) β§ ((π΄ gcd π΅) β₯ π΄ β§ (π΄ gcd π΅) β₯ π΅)) β ((π΄ gcd π΅) / (π΄ gcd π΅)) = ((π΄ / (π΄ gcd π΅)) gcd (π΅ / (π΄ gcd π΅)))) |
13 | 1, 3, 9, 11, 12 | syl31anc 1374 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β) β ((π΄ gcd π΅) / (π΄ gcd π΅)) = ((π΄ / (π΄ gcd π΅)) gcd (π΅ / (π΄ gcd π΅)))) |
14 | 9 | nncnd 12176 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ gcd π΅) β β) |
15 | 9 | nnne0d 12210 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ gcd π΅) β 0) |
16 | 14, 15 | dividd 11936 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β) β ((π΄ gcd π΅) / (π΄ gcd π΅)) = 1) |
17 | 13, 16 | eqtr3d 2779 |
. 2
β’ ((π΄ β β€ β§ π΅ β β) β ((π΄ / (π΄ gcd π΅)) gcd (π΅ / (π΄ gcd π΅))) = 1) |
18 | | zcn 12511 |
. . . 4
β’ (π΄ β β€ β π΄ β
β) |
19 | 18 | adantr 482 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β) β π΄ β
β) |
20 | | nncn 12168 |
. . . 4
β’ (π΅ β β β π΅ β
β) |
21 | 20 | adantl 483 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β) β π΅ β
β) |
22 | 4 | adantl 483 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β) β π΅ β 0) |
23 | | divcan7 11871 |
. . . 4
β’ ((π΄ β β β§ (π΅ β β β§ π΅ β 0) β§ ((π΄ gcd π΅) β β β§ (π΄ gcd π΅) β 0)) β ((π΄ / (π΄ gcd π΅)) / (π΅ / (π΄ gcd π΅))) = (π΄ / π΅)) |
24 | 23 | eqcomd 2743 |
. . 3
β’ ((π΄ β β β§ (π΅ β β β§ π΅ β 0) β§ ((π΄ gcd π΅) β β β§ (π΄ gcd π΅) β 0)) β (π΄ / π΅) = ((π΄ / (π΄ gcd π΅)) / (π΅ / (π΄ gcd π΅)))) |
25 | 19, 21, 22, 14, 15, 24 | syl122anc 1380 |
. 2
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ / π΅) = ((π΄ / (π΄ gcd π΅)) / (π΅ / (π΄ gcd π΅)))) |
26 | | znq 12884 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ / π΅) β β) |
27 | 11 | simpld 496 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ gcd π΅) β₯ π΄) |
28 | | gcdcl 16393 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ gcd π΅) β
β0) |
29 | 28 | nn0zd 12532 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ gcd π΅) β β€) |
30 | 2, 29 | sylan2 594 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ gcd π΅) β β€) |
31 | | dvdsval2 16146 |
. . . . 5
β’ (((π΄ gcd π΅) β β€ β§ (π΄ gcd π΅) β 0 β§ π΄ β β€) β ((π΄ gcd π΅) β₯ π΄ β (π΄ / (π΄ gcd π΅)) β β€)) |
32 | 30, 15, 1, 31 | syl3anc 1372 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β ((π΄ gcd π΅) β₯ π΄ β (π΄ / (π΄ gcd π΅)) β β€)) |
33 | 27, 32 | mpbid 231 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ / (π΄ gcd π΅)) β β€) |
34 | 11 | simprd 497 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β (π΄ gcd π΅) β₯ π΅) |
35 | | simpr 486 |
. . . . 5
β’ ((π΄ β β€ β§ π΅ β β) β π΅ β
β) |
36 | | nndivdvds 16152 |
. . . . 5
β’ ((π΅ β β β§ (π΄ gcd π΅) β β) β ((π΄ gcd π΅) β₯ π΅ β (π΅ / (π΄ gcd π΅)) β β)) |
37 | 35, 9, 36 | syl2anc 585 |
. . . 4
β’ ((π΄ β β€ β§ π΅ β β) β ((π΄ gcd π΅) β₯ π΅ β (π΅ / (π΄ gcd π΅)) β β)) |
38 | 34, 37 | mpbid 231 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β) β (π΅ / (π΄ gcd π΅)) β β) |
39 | | qnumdenbi 16626 |
. . 3
β’ (((π΄ / π΅) β β β§ (π΄ / (π΄ gcd π΅)) β β€ β§ (π΅ / (π΄ gcd π΅)) β β) β ((((π΄ / (π΄ gcd π΅)) gcd (π΅ / (π΄ gcd π΅))) = 1 β§ (π΄ / π΅) = ((π΄ / (π΄ gcd π΅)) / (π΅ / (π΄ gcd π΅)))) β ((numerβ(π΄ / π΅)) = (π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = (π΅ / (π΄ gcd π΅))))) |
40 | 26, 33, 38, 39 | syl3anc 1372 |
. 2
β’ ((π΄ β β€ β§ π΅ β β) β
((((π΄ / (π΄ gcd π΅)) gcd (π΅ / (π΄ gcd π΅))) = 1 β§ (π΄ / π΅) = ((π΄ / (π΄ gcd π΅)) / (π΅ / (π΄ gcd π΅)))) β ((numerβ(π΄ / π΅)) = (π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = (π΅ / (π΄ gcd π΅))))) |
41 | 17, 25, 40 | mpbi2and 711 |
1
β’ ((π΄ β β€ β§ π΅ β β) β
((numerβ(π΄ / π΅)) = (π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = (π΅ / (π΄ gcd π΅)))) |