Step | Hyp | Ref
| Expression |
1 | | frmy 41281 |
. . . . . 6
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
2 | 1 | fovcl 7485 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
3 | 2 | 3adant3 1133 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β€) |
4 | 1 | fovcl 7485 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
5 | 4 | 3adant2 1132 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β€) |
6 | | frmx 41280 |
. . . . . . 7
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
7 | 6 | fovcl 7485 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
8 | 7 | 3adant3 1133 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β
β0) |
9 | 8 | nn0zd 12530 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β€) |
10 | 3, 9 | gcdcomd 16399 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) gcd (π΄ Xrm π)) = ((π΄ Xrm π) gcd (π΄ Yrm π))) |
11 | | jm2.19lem1 41356 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) gcd (π΄ Yrm π)) = 1) |
12 | 11 | 3adant3 1133 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) gcd (π΄ Yrm π)) = 1) |
13 | 10, 12 | eqtrd 2773 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) gcd (π΄ Xrm π)) = 1) |
14 | | coprmdvdsb 41352 |
. . . 4
β’ (((π΄ Yrm π) β β€ β§ (π΄ Yrm π) β β€ β§ ((π΄ Xrm π) β β€ β§ ((π΄ Yrm π) gcd (π΄ Xrm π)) = 1)) β ((π΄ Yrm π) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
15 | 3, 5, 9, 13, 14 | syl112anc 1375 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
16 | 8 | nn0cnd 12480 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β) |
17 | 5 | zcnd 12613 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β) |
18 | 16, 17 | mulcomd 11181 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) = ((π΄ Yrm π) Β· (π΄ Xrm π))) |
19 | 18 | breq2d 5118 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π)) β (π΄ Yrm π) β₯ ((π΄ Yrm π) Β· (π΄ Xrm π)))) |
20 | 15, 19 | bitrd 279 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ ((π΄ Yrm π) Β· (π΄ Xrm π)))) |
21 | 5, 9 | zmulcld 12618 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Xrm π)) β β€) |
22 | 6 | fovcl 7485 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
23 | 22 | 3adant2 1132 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β
β0) |
24 | 23 | nn0zd 12530 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β€) |
25 | 24, 3 | zmulcld 12618 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) β β€) |
26 | | dvdsmul2 16166 |
. . . 4
β’ (((π΄ Xrm π) β β€ β§ (π΄ Yrm π) β β€) β (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π))) |
27 | 24, 3, 26 | syl2anc 585 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π))) |
28 | | dvdsadd2b 16193 |
. . 3
β’ (((π΄ Yrm π) β β€ β§ ((π΄ Yrm π) Β· (π΄ Xrm π)) β β€ β§ (((π΄ Xrm π) Β· (π΄ Yrm π)) β β€ β§ (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π)))) β ((π΄ Yrm π) β₯ ((π΄ Yrm π) Β· (π΄ Xrm π)) β (π΄ Yrm π) β₯ (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π))))) |
29 | 3, 21, 25, 27, 28 | syl112anc 1375 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ ((π΄ Yrm π) Β· (π΄ Xrm π)) β (π΄ Yrm π) β₯ (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π))))) |
30 | | rmyadd 41298 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm (π + π)) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
31 | 30 | 3com23 1127 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm (π + π)) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
32 | 17, 16 | mulcld 11180 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Xrm π)) β β) |
33 | 23 | nn0cnd 12480 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β) |
34 | 3 | zcnd 12613 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β) |
35 | 33, 34 | mulcld 11180 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) β β) |
36 | 32, 35 | addcomd 11362 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))) = (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π)))) |
37 | 31, 36 | eqtr2d 2774 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π))) = (π΄ Yrm (π + π))) |
38 | 37 | breq2d 5118 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π))) β (π΄ Yrm π) β₯ (π΄ Yrm (π + π)))) |
39 | 20, 29, 38 | 3bitrd 305 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ (π΄ Yrm (π + π)))) |