Step | Hyp | Ref
| Expression |
1 | | frmy 42236 |
. . . . . 6
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
2 | 1 | fovcl 7533 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
3 | 2 | 3adant3 1129 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β€) |
4 | 1 | fovcl 7533 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
5 | 4 | 3adant2 1128 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β€) |
6 | | frmx 42235 |
. . . . . . 7
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
7 | 6 | fovcl 7533 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
8 | 7 | 3adant3 1129 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β
β0) |
9 | 8 | nn0zd 12588 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β€) |
10 | 3, 9 | gcdcomd 16462 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) gcd (π΄ Xrm π)) = ((π΄ Xrm π) gcd (π΄ Yrm π))) |
11 | | jm2.19lem1 42311 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) gcd (π΄ Yrm π)) = 1) |
12 | 11 | 3adant3 1129 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) gcd (π΄ Yrm π)) = 1) |
13 | 10, 12 | eqtrd 2766 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) gcd (π΄ Xrm π)) = 1) |
14 | | coprmdvdsb 42307 |
. . . 4
β’ (((π΄ Yrm π) β β€ β§ (π΄ Yrm π) β β€ β§ ((π΄ Xrm π) β β€ β§ ((π΄ Yrm π) gcd (π΄ Xrm π)) = 1)) β ((π΄ Yrm π) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
15 | 3, 5, 9, 13, 14 | syl112anc 1371 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
16 | 8 | nn0cnd 12538 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β) |
17 | 5 | zcnd 12671 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β) |
18 | 16, 17 | mulcomd 11239 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) = ((π΄ Yrm π) Β· (π΄ Xrm π))) |
19 | 18 | breq2d 5153 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π)) β (π΄ Yrm π) β₯ ((π΄ Yrm π) Β· (π΄ Xrm π)))) |
20 | 15, 19 | bitrd 279 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ ((π΄ Yrm π) Β· (π΄ Xrm π)))) |
21 | 5, 9 | zmulcld 12676 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Xrm π)) β β€) |
22 | 6 | fovcl 7533 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
23 | 22 | 3adant2 1128 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β
β0) |
24 | 23 | nn0zd 12588 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β€) |
25 | 24, 3 | zmulcld 12676 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) β β€) |
26 | | dvdsmul2 16229 |
. . . 4
β’ (((π΄ Xrm π) β β€ β§ (π΄ Yrm π) β β€) β (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π))) |
27 | 24, 3, 26 | syl2anc 583 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π))) |
28 | | dvdsadd2b 16256 |
. . 3
β’ (((π΄ Yrm π) β β€ β§ ((π΄ Yrm π) Β· (π΄ Xrm π)) β β€ β§ (((π΄ Xrm π) Β· (π΄ Yrm π)) β β€ β§ (π΄ Yrm π) β₯ ((π΄ Xrm π) Β· (π΄ Yrm π)))) β ((π΄ Yrm π) β₯ ((π΄ Yrm π) Β· (π΄ Xrm π)) β (π΄ Yrm π) β₯ (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π))))) |
29 | 3, 21, 25, 27, 28 | syl112anc 1371 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ ((π΄ Yrm π) Β· (π΄ Xrm π)) β (π΄ Yrm π) β₯ (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π))))) |
30 | | rmyadd 42253 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm (π + π)) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
31 | 30 | 3com23 1123 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm (π + π)) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
32 | 17, 16 | mulcld 11238 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Xrm π)) β β) |
33 | 23 | nn0cnd 12538 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β) |
34 | 3 | zcnd 12671 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β) |
35 | 33, 34 | mulcld 11238 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) β β) |
36 | 32, 35 | addcomd 11420 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))) = (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π)))) |
37 | 31, 36 | eqtr2d 2767 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π))) = (π΄ Yrm (π + π))) |
38 | 37 | breq2d 5153 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Yrm π) Β· (π΄ Xrm π))) β (π΄ Yrm π) β₯ (π΄ Yrm (π + π)))) |
39 | 20, 29, 38 | 3bitrd 305 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ (π΄ Yrm (π + π)))) |