Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β π΄ β
(β€β₯β2)) |
2 | | nnz 12521 |
. . . . . . . . . . 11
β’ (π β β β π β
β€) |
3 | 2 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β π β β€) |
4 | | frmy 41241 |
. . . . . . . . . . 11
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
5 | 4 | fovcl 7485 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
6 | 1, 3, 5 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm π) β β€) |
7 | 6 | zcnd 12609 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm π) β β) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm π) β β) |
9 | 8 | sqvald 14049 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) = ((π΄ Yrm π) Β· (π΄ Yrm π))) |
10 | | zsqcl 14035 |
. . . . . . . . 9
β’ ((π΄ Yrm π) β β€ β ((π΄ Yrm π)β2) β
β€) |
11 | 6, 10 | syl 17 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β2) β β€) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) β β€) |
13 | | frmx 41240 |
. . . . . . . . . . . 12
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
14 | 13 | fovcl 7485 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
15 | 1, 3, 14 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Xrm π) β
β0) |
16 | 15 | nn0zd 12526 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Xrm π) β β€) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Xrm π) β β€) |
18 | 7 | sqvald 14049 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β2) = ((π΄ Yrm π) Β· (π΄ Yrm π))) |
19 | 18 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) = ((π΄ Yrm π) Β· (π΄ Yrm π))) |
20 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) |
21 | 19, 20 | eqbrtrrd 5130 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π) Β· (π΄ Yrm π)) β₯ (π΄ Yrm π)) |
22 | | nnz 12521 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β€) |
23 | 22 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β π β β€) |
24 | 4 | fovcl 7485 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
25 | 1, 23, 24 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm π) β β€) |
26 | | muldvds1 16164 |
. . . . . . . . . . . . . 14
β’ (((π΄ Yrm π) β β€ β§ (π΄ Yrm π) β β€ β§ (π΄ Yrm π) β β€) β
(((π΄ Yrm π) Β· (π΄ Yrm π)) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ (π΄ Yrm π))) |
27 | 6, 6, 25, 26 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (((π΄ Yrm π) Β· (π΄ Yrm π)) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ (π΄ Yrm π))) |
28 | 27 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (((π΄ Yrm π) Β· (π΄ Yrm π)) β₯ (π΄ Yrm π) β (π΄ Yrm π) β₯ (π΄ Yrm π))) |
29 | 21, 28 | mpd 15 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm π) β₯ (π΄ Yrm π)) |
30 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β π΄ β
(β€β₯β2)) |
31 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β π β β€) |
32 | 23 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β π β β€) |
33 | | jm2.19 41320 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π β₯ π β (π΄ Yrm π) β₯ (π΄ Yrm π))) |
34 | 30, 31, 32, 33 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π β₯ π β (π΄ Yrm π) β₯ (π΄ Yrm π))) |
35 | 29, 34 | mpbird 257 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β π β₯ π) |
36 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β π β β) |
37 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β π β β) |
38 | | nndivdvds 16146 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β (π β₯ π β (π / π) β β)) |
39 | 36, 37, 38 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π β₯ π β (π / π) β β)) |
40 | 35, 39 | mpbid 231 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π / π) β β) |
41 | | nnm1nn0 12455 |
. . . . . . . . 9
β’ ((π / π) β β β ((π / π) β 1) β
β0) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π / π) β 1) β
β0) |
43 | | zexpcl 13983 |
. . . . . . . 8
β’ (((π΄ Xrm π) β β€ β§ ((π / π) β 1) β β0)
β ((π΄ Xrm
π)β((π / π) β 1)) β
β€) |
44 | 17, 42, 43 | syl2anc 585 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Xrm π)β((π / π) β 1)) β
β€) |
45 | 40 | nnzd 12527 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π / π) β β€) |
46 | 6 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm π) β β€) |
47 | 45, 46 | zmulcld 12614 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π / π) Β· (π΄ Yrm π)) β β€) |
48 | 25 | adantr 482 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm π) β β€) |
49 | | nncn 12162 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
50 | 49 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β π β β) |
51 | | nncn 12162 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
52 | 51 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β π β β) |
53 | | nnne0 12188 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β 0) |
54 | 53 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β π β 0) |
55 | 50, 52, 54 | divcan2d 11934 |
. . . . . . . . . . . . 13
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π Β· (π / π)) = π) |
56 | 55 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm (π Β· (π / π))) = (π΄ Yrm π)) |
57 | 56, 25 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm (π Β· (π / π))) β β€) |
58 | 57 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm (π Β· (π / π))) β β€) |
59 | 44, 46 | zmulcld 12614 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)) β β€) |
60 | 45, 59 | zmulcld 12614 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))) β β€) |
61 | 58, 60 | zsubcld 12613 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))) β β€) |
62 | | 3nn0 12432 |
. . . . . . . . . . . . 13
β’ 3 β
β0 |
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β 3 β
β0) |
64 | | zexpcl 13983 |
. . . . . . . . . . . 12
β’ (((π΄ Yrm π) β β€ β§ 3 β
β0) β ((π΄ Yrm π)β3) β β€) |
65 | 6, 63, 64 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β3) β β€) |
66 | 65 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β3) β β€) |
67 | | 2nn0 12431 |
. . . . . . . . . . . . 13
β’ 2 β
β0 |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β 2 β
β0) |
69 | | 3z 12537 |
. . . . . . . . . . . . . 14
β’ 3 β
β€ |
70 | | 2re 12228 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
71 | | 3re 12234 |
. . . . . . . . . . . . . . 15
β’ 3 β
β |
72 | | 2lt3 12326 |
. . . . . . . . . . . . . . 15
β’ 2 <
3 |
73 | 70, 71, 72 | ltleii 11279 |
. . . . . . . . . . . . . 14
β’ 2 β€
3 |
74 | | 2z 12536 |
. . . . . . . . . . . . . . 15
β’ 2 β
β€ |
75 | 74 | eluz1i 12772 |
. . . . . . . . . . . . . 14
β’ (3 β
(β€β₯β2) β (3 β β€ β§ 2 β€
3)) |
76 | 69, 73, 75 | mpbir2an 710 |
. . . . . . . . . . . . 13
β’ 3 β
(β€β₯β2) |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β 3 β
(β€β₯β2)) |
78 | | dvdsexp 16211 |
. . . . . . . . . . . 12
β’ (((π΄ Yrm π) β β€ β§ 2 β
β0 β§ 3 β (β€β₯β2)) β
((π΄ Yrm π)β2) β₯ ((π΄ Yrm π)β3)) |
79 | 6, 68, 77, 78 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm π)β3)) |
80 | 79 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm π)β3)) |
81 | | jm2.23 41323 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ (π / π) β β) β ((π΄ Yrm π)β3) β₯ ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) |
82 | 30, 31, 40, 81 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β3) β₯ ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) |
83 | 12, 66, 61, 80, 82 | dvdstrd 16178 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) |
84 | | dvds2sub 16174 |
. . . . . . . . . 10
β’ ((((π΄ Yrm π)β2) β β€ β§
(π΄ Yrm π) β β€ β§ ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))) β β€) β ((((π΄ Yrm π)β2) β₯ (π΄ Yrm π) β§ ((π΄ Yrm π)β2) β₯ ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm π) β ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))))) |
85 | 84 | imp 408 |
. . . . . . . . 9
β’
(((((π΄
Yrm π)β2)
β β€ β§ (π΄
Yrm π) β
β€ β§ ((π΄
Yrm (π Β·
(π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))) β β€) β§ (((π΄ Yrm π)β2) β₯ (π΄ Yrm π) β§ ((π΄ Yrm π)β2) β₯ ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))))) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm π) β ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))))) |
86 | 12, 48, 61, 20, 83, 85 | syl32anc 1379 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm π) β ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))))) |
87 | 55 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π Β· (π / π)) = π) |
88 | 87 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm (π Β· (π / π))) = (π΄ Yrm π)) |
89 | 88 | oveq1d 7373 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))) = ((π΄ Yrm π) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) |
90 | 89 | oveq2d 7374 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π) β ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) = ((π΄ Yrm π) β ((π΄ Yrm π) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))))) |
91 | 25 | zcnd 12609 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm π) β β) |
92 | 91 | adantr 482 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm π) β β) |
93 | 60 | zcnd 12609 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))) β β) |
94 | 92, 93 | nncand 11518 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π) β ((π΄ Yrm π) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) = ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π)))) |
95 | 45 | zcnd 12609 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π / π) β β) |
96 | 44 | zcnd 12609 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Xrm π)β((π / π) β 1)) β
β) |
97 | 95, 96, 8 | mul12d 11365 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))) = (((π΄ Xrm π)β((π / π) β 1)) Β· ((π / π) Β· (π΄ Yrm π)))) |
98 | 94, 97 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π) β ((π΄ Yrm π) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) = (((π΄ Xrm π)β((π / π) β 1)) Β· ((π / π) Β· (π΄ Yrm π)))) |
99 | 90, 98 | eqtrd 2777 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π) β ((π΄ Yrm (π Β· (π / π))) β ((π / π) Β· (((π΄ Xrm π)β((π / π) β 1)) Β· (π΄ Yrm π))))) = (((π΄ Xrm π)β((π / π) β 1)) Β· ((π / π) Β· (π΄ Yrm π)))) |
100 | 86, 99 | breqtrd 5132 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) β₯ (((π΄ Xrm π)β((π / π) β 1)) Β· ((π / π) Β· (π΄ Yrm π)))) |
101 | 6, 16 | gcdcomd 16395 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π) gcd (π΄ Xrm π)) = ((π΄ Xrm π) gcd (π΄ Yrm π))) |
102 | | jm2.19lem1 41316 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) gcd (π΄ Yrm π)) = 1) |
103 | 1, 3, 102 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Xrm π) gcd (π΄ Yrm π)) = 1) |
104 | 101, 103 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π) gcd (π΄ Xrm π)) = 1) |
105 | 104 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π) gcd (π΄ Xrm π)) = 1) |
106 | 67 | a1i 11 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β 2 β
β0) |
107 | | rpexp12i 16601 |
. . . . . . . . 9
β’ (((π΄ Yrm π) β β€ β§ (π΄ Xrm π) β β€ β§ (2 β
β0 β§ ((π / π) β 1) β β0))
β (((π΄ Yrm
π) gcd (π΄ Xrm π)) = 1 β (((π΄ Yrm π)β2) gcd ((π΄ Xrm π)β((π / π) β 1))) = 1)) |
108 | 46, 17, 106, 42, 107 | syl112anc 1375 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (((π΄ Yrm π) gcd (π΄ Xrm π)) = 1 β (((π΄ Yrm π)β2) gcd ((π΄ Xrm π)β((π / π) β 1))) = 1)) |
109 | 105, 108 | mpd 15 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (((π΄ Yrm π)β2) gcd ((π΄ Xrm π)β((π / π) β 1))) = 1) |
110 | | coprmdvds 16530 |
. . . . . . . 8
β’ ((((π΄ Yrm π)β2) β β€ β§
((π΄ Xrm π)β((π / π) β 1)) β β€ β§ ((π / π) Β· (π΄ Yrm π)) β β€) β ((((π΄ Yrm π)β2) β₯ (((π΄ Xrm π)β((π / π) β 1)) Β· ((π / π) Β· (π΄ Yrm π))) β§ (((π΄ Yrm π)β2) gcd ((π΄ Xrm π)β((π / π) β 1))) = 1) β ((π΄ Yrm π)β2) β₯ ((π / π) Β· (π΄ Yrm π)))) |
111 | 110 | imp 408 |
. . . . . . 7
β’
(((((π΄
Yrm π)β2)
β β€ β§ ((π΄
Xrm π)β((π / π) β 1)) β β€ β§ ((π / π) Β· (π΄ Yrm π)) β β€) β§ (((π΄ Yrm π)β2) β₯ (((π΄ Xrm π)β((π / π) β 1)) Β· ((π / π) Β· (π΄ Yrm π))) β§ (((π΄ Yrm π)β2) gcd ((π΄ Xrm π)β((π / π) β 1))) = 1)) β ((π΄ Yrm π)β2) β₯ ((π / π) Β· (π΄ Yrm π))) |
112 | 12, 44, 47, 100, 109, 111 | syl32anc 1379 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π)β2) β₯ ((π / π) Β· (π΄ Yrm π))) |
113 | 9, 112 | eqbrtrrd 5130 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π΄ Yrm π) Β· (π΄ Yrm π)) β₯ ((π / π) Β· (π΄ Yrm π))) |
114 | | rmy0 41256 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 0) = 0) |
115 | 114 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm 0) = 0) |
116 | | nngt0 12185 |
. . . . . . . . . . . 12
β’ (π β β β 0 <
π) |
117 | 116 | 3ad2ant3 1136 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β 0 < π) |
118 | | 0zd 12512 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β 0 β
β€) |
119 | | ltrmy 41279 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ 0 β β€ β§ π β β€) β (0 < π β (π΄ Yrm 0) < (π΄ Yrm π))) |
120 | 1, 118, 3, 119 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (0 < π β (π΄ Yrm 0) < (π΄ Yrm π))) |
121 | 117, 120 | mpbid 231 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm 0) < (π΄ Yrm π)) |
122 | 115, 121 | eqbrtrrd 5130 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β 0 < (π΄ Yrm π)) |
123 | | elnnz 12510 |
. . . . . . . . 9
β’ ((π΄ Yrm π) β β β ((π΄ Yrm π) β β€ β§ 0 <
(π΄ Yrm π))) |
124 | 6, 122, 123 | sylanbrc 584 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm π) β β) |
125 | | nnne0 12188 |
. . . . . . . 8
β’ ((π΄ Yrm π) β β β (π΄ Yrm π) β 0) |
126 | 124, 125 | syl 17 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm π) β 0) |
127 | 126 | adantr 482 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm π) β 0) |
128 | | dvdsmulcr 16169 |
. . . . . 6
β’ (((π΄ Yrm π) β β€ β§ (π / π) β β€ β§ ((π΄ Yrm π) β β€ β§ (π΄ Yrm π) β 0)) β (((π΄ Yrm π) Β· (π΄ Yrm π)) β₯ ((π / π) Β· (π΄ Yrm π)) β (π΄ Yrm π) β₯ (π / π))) |
129 | 46, 45, 46, 127, 128 | syl112anc 1375 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (((π΄ Yrm π) Β· (π΄ Yrm π)) β₯ ((π / π) Β· (π΄ Yrm π)) β (π΄ Yrm π) β₯ (π / π))) |
130 | 113, 129 | mpbid 231 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π΄ Yrm π) β₯ (π / π)) |
131 | 54 | adantr 482 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β π β 0) |
132 | | dvdscmulr 16168 |
. . . . 5
β’ (((π΄ Yrm π) β β€ β§ (π / π) β β€ β§ (π β β€ β§ π β 0)) β ((π Β· (π΄ Yrm π)) β₯ (π Β· (π / π)) β (π΄ Yrm π) β₯ (π / π))) |
133 | 46, 45, 31, 131, 132 | syl112anc 1375 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β ((π Β· (π΄ Yrm π)) β₯ (π Β· (π / π)) β (π΄ Yrm π) β₯ (π / π))) |
134 | 130, 133 | mpbird 257 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π Β· (π΄ Yrm π)) β₯ (π Β· (π / π))) |
135 | 134, 87 | breqtrd 5132 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) β (π Β· (π΄ Yrm π)) β₯ π) |
136 | 11 | adantr 482 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β ((π΄ Yrm π)β2) β β€) |
137 | 3, 6 | zmulcld 12614 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π Β· (π΄ Yrm π)) β β€) |
138 | 4 | fovcl 7485 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ (π Β· (π΄ Yrm π)) β β€) β (π΄ Yrm (π Β· (π΄ Yrm π))) β β€) |
139 | 1, 137, 138 | syl2anc 585 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (π΄ Yrm (π Β· (π΄ Yrm π))) β β€) |
140 | 139 | adantr 482 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β (π΄ Yrm (π Β· (π΄ Yrm π))) β β€) |
141 | 25 | adantr 482 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β (π΄ Yrm π) β β€) |
142 | | nnm1nn0 12455 |
. . . . . . . . 9
β’ ((π΄ Yrm π) β β β ((π΄ Yrm π) β 1) β
β0) |
143 | 124, 142 | syl 17 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π) β 1) β
β0) |
144 | | zexpcl 13983 |
. . . . . . . 8
β’ (((π΄ Xrm π) β β€ β§ ((π΄ Yrm π) β 1) β
β0) β ((π΄ Xrm π)β((π΄ Yrm π) β 1)) β
β€) |
145 | 16, 143, 144 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Xrm π)β((π΄ Yrm π) β 1)) β
β€) |
146 | | dvdsmul2 16162 |
. . . . . . 7
β’ ((((π΄ Xrm π)β((π΄ Yrm π) β 1)) β β€ β§ ((π΄ Yrm π)β2) β β€) β
((π΄ Yrm π)β2) β₯ (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· ((π΄ Yrm π)β2))) |
147 | 145, 11, 146 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β2) β₯ (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· ((π΄ Yrm π)β2))) |
148 | 18 | oveq2d 7374 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· ((π΄ Yrm π)β2)) = (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) |
149 | 145 | zcnd 12609 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Xrm π)β((π΄ Yrm π) β 1)) β
β) |
150 | 149, 7, 7 | mul12d 11365 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· ((π΄ Yrm π) Β· (π΄ Yrm π))) = ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π)))) |
151 | 148, 150 | eqtrd 2777 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· ((π΄ Yrm π)β2)) = ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π)))) |
152 | 147, 151 | breqtrd 5132 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π)))) |
153 | 145, 6 | zmulcld 12614 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π)) β β€) |
154 | 6, 153 | zmulcld 12614 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π))) β β€) |
155 | 139, 154 | zsubcld 12613 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm (π Β· (π΄ Yrm π))) β ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π)))) β β€) |
156 | | jm2.23 41323 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ (π΄ Yrm π) β β) β ((π΄ Yrm π)β3) β₯ ((π΄ Yrm (π Β· (π΄ Yrm π))) β ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π))))) |
157 | 1, 3, 124, 156 | syl3anc 1372 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β3) β₯ ((π΄ Yrm (π Β· (π΄ Yrm π))) β ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π))))) |
158 | 11, 65, 155, 79, 157 | dvdstrd 16178 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm (π Β· (π΄ Yrm π))) β ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π))))) |
159 | | dvdssub2 16184 |
. . . . . 6
β’
(((((π΄
Yrm π)β2)
β β€ β§ (π΄
Yrm (π Β·
(π΄ Yrm π))) β β€ β§ ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π))) β β€) β§ ((π΄ Yrm π)β2) β₯ ((π΄ Yrm (π Β· (π΄ Yrm π))) β ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π))))) β (((π΄ Yrm π)β2) β₯ (π΄ Yrm (π Β· (π΄ Yrm π))) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π))))) |
160 | 11, 139, 154, 158, 159 | syl31anc 1374 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (((π΄ Yrm π)β2) β₯ (π΄ Yrm (π Β· (π΄ Yrm π))) β ((π΄ Yrm π)β2) β₯ ((π΄ Yrm π) Β· (((π΄ Xrm π)β((π΄ Yrm π) β 1)) Β· (π΄ Yrm π))))) |
161 | 152, 160 | mpbird 257 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β ((π΄ Yrm π)β2) β₯ (π΄ Yrm (π Β· (π΄ Yrm π)))) |
162 | 161 | adantr 482 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β ((π΄ Yrm π)β2) β₯ (π΄ Yrm (π Β· (π΄ Yrm π)))) |
163 | | simpr 486 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β (π Β· (π΄ Yrm π)) β₯ π) |
164 | | simpl1 1192 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β π΄ β
(β€β₯β2)) |
165 | 137 | adantr 482 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β (π Β· (π΄ Yrm π)) β β€) |
166 | 23 | adantr 482 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β π β β€) |
167 | | jm2.19 41320 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ (π Β· (π΄ Yrm π)) β β€ β§ π β β€) β ((π Β· (π΄ Yrm π)) β₯ π β (π΄ Yrm (π Β· (π΄ Yrm π))) β₯ (π΄ Yrm π))) |
168 | 164, 165,
166, 167 | syl3anc 1372 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β ((π Β· (π΄ Yrm π)) β₯ π β (π΄ Yrm (π Β· (π΄ Yrm π))) β₯ (π΄ Yrm π))) |
169 | 163, 168 | mpbid 231 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β (π΄ Yrm (π Β· (π΄ Yrm π))) β₯ (π΄ Yrm π)) |
170 | 136, 140,
141, 162, 169 | dvdstrd 16178 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β§ (π Β· (π΄ Yrm π)) β₯ π) β ((π΄ Yrm π)β2) β₯ (π΄ Yrm π)) |
171 | 135, 170 | impbida 800 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β β§ π β β) β (((π΄ Yrm π)β2) β₯ (π΄ Yrm π) β (π Β· (π΄ Yrm π)) β₯ π)) |