Step | Hyp | Ref
| Expression |
1 | | nnz 12525 |
. . . . . 6
β’ (π β β β π β
β€) |
2 | | 1z 12538 |
. . . . . 6
β’ 1 β
β€ |
3 | | zsubcl 12550 |
. . . . . 6
β’ ((π β β€ β§ 1 β
β€) β (π β
1) β β€) |
4 | 1, 2, 3 | sylancl 587 |
. . . . 5
β’ (π β β β (π β 1) β
β€) |
5 | | frmy 41281 |
. . . . . 6
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
6 | 5 | fovcl 7485 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Yrm (π β 1)) β
β€) |
7 | 4, 6 | sylan2 594 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm (π β 1)) β
β€) |
8 | 7 | zred 12612 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm (π β 1)) β
β) |
9 | 5 | fovcl 7485 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
10 | 1, 9 | sylan2 594 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm π) β β€) |
11 | 10 | zred 12612 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm π) β β) |
12 | 8, 11 | readdcld 11189 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) β β) |
13 | | 2re 12232 |
. . . 4
β’ 2 β
β |
14 | | remulcl 11141 |
. . . 4
β’ ((2
β β β§ (π΄
Yrm π) β
β) β (2 Β· (π΄ Yrm π)) β β) |
15 | 13, 11, 14 | sylancr 588 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· (π΄ Yrm π)) β
β) |
16 | 15, 8 | resubcld 11588 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1))) β
β) |
17 | | frmx 41280 |
. . . . 5
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
18 | 17 | fovcl 7485 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
19 | 1, 18 | sylan2 594 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Xrm π) β
β0) |
20 | 19 | nn0red 12479 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Xrm π) β β) |
21 | 11, 8 | resubcld 11588 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm π) β (π΄ Yrm (π β 1))) β
β) |
22 | | remulcl 11141 |
. . . . . . . 8
β’ ((2
β β β§ (π΄
Yrm (π β
1)) β β) β (2 Β· (π΄ Yrm (π β 1))) β
β) |
23 | 13, 8, 22 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· (π΄ Yrm (π β 1))) β
β) |
24 | | eluzelre 12779 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
25 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π΄ β β) |
26 | 25, 8 | remulcld 11190 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Β· (π΄ Yrm (π β 1))) β
β) |
27 | 8, 25 | remulcld 11190 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm (π β 1)) Β· π΄) β β) |
28 | 17 | fovcl 7485 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Xrm (π β 1)) β
β0) |
29 | 4, 28 | sylan2 594 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Xrm (π β 1)) β
β0) |
30 | 29 | nn0red 12479 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Xrm (π β 1)) β
β) |
31 | 27, 30 | readdcld 11189 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((π΄ Yrm (π β 1)) Β· π΄) + (π΄ Xrm (π β 1))) β
β) |
32 | 13 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 2 β
β) |
33 | | nnm1nn0 12459 |
. . . . . . . . 9
β’ (π β β β (π β 1) β
β0) |
34 | | rmxypos 41314 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β0)
β (0 < (π΄
Xrm (π β
1)) β§ 0 β€ (π΄
Yrm (π β
1)))) |
35 | 34 | simprd 497 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β0)
β 0 β€ (π΄
Yrm (π β
1))) |
36 | 33, 35 | sylan2 594 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 β€ (π΄ Yrm (π β 1))) |
37 | | eluzle 12781 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β 2 β€ π΄) |
38 | 37 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 2 β€ π΄) |
39 | 32, 25, 8, 36, 38 | lemul1ad 12099 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· (π΄ Yrm (π β 1))) β€ (π΄ Β· (π΄ Yrm (π β 1)))) |
40 | 25 | recnd 11188 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π΄ β β) |
41 | 8 | recnd 11188 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm (π β 1)) β
β) |
42 | 40, 41 | mulcomd 11181 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Β· (π΄ Yrm (π β 1))) = ((π΄ Yrm (π β 1)) Β· π΄)) |
43 | 34 | simpld 496 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β0)
β 0 < (π΄
Xrm (π β
1))) |
44 | 33, 43 | sylan2 594 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 < (π΄ Xrm (π β 1))) |
45 | 30, 27 | ltaddposd 11744 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (0 < (π΄ Xrm (π β 1)) β ((π΄ Yrm (π β 1)) Β· π΄) < (((π΄ Yrm (π β 1)) Β· π΄) + (π΄ Xrm (π β 1))))) |
46 | 44, 45 | mpbid 231 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm (π β 1)) Β· π΄) < (((π΄ Yrm (π β 1)) Β· π΄) + (π΄ Xrm (π β 1)))) |
47 | 42, 46 | eqbrtrd 5128 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Β· (π΄ Yrm (π β 1))) < (((π΄ Yrm (π β 1)) Β· π΄) + (π΄ Xrm (π β 1)))) |
48 | 23, 26, 31, 39, 47 | lelttrd 11318 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· (π΄ Yrm (π β 1))) < (((π΄ Yrm (π β 1)) Β· π΄) + (π΄ Xrm (π β 1)))) |
49 | 41 | 2timesd 12401 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· (π΄ Yrm (π β 1))) = ((π΄ Yrm (π β 1)) + (π΄ Yrm (π β 1)))) |
50 | | rmyp1 41300 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Yrm ((π β 1) + 1)) = (((π΄ Yrm (π β 1)) Β· π΄) + (π΄ Xrm (π β 1)))) |
51 | 4, 50 | sylan2 594 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm ((π β 1) + 1)) = (((π΄ Yrm (π β 1)) Β· π΄) + (π΄ Xrm (π β 1)))) |
52 | | nnre 12165 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
53 | 52 | adantl 483 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π β β) |
54 | 53 | recnd 11188 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π β β) |
55 | | ax-1cn 11114 |
. . . . . . . . 9
β’ 1 β
β |
56 | | npcan 11415 |
. . . . . . . . 9
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
57 | 54, 55, 56 | sylancl 587 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π β 1) + 1) = π) |
58 | 57 | oveq2d 7374 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm ((π β 1) + 1)) = (π΄ Yrm π)) |
59 | 51, 58 | eqtr3d 2775 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((π΄ Yrm (π β 1)) Β· π΄) + (π΄ Xrm (π β 1))) = (π΄ Yrm π)) |
60 | 48, 49, 59 | 3brtr3d 5137 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm (π β 1)) + (π΄ Yrm (π β 1))) < (π΄ Yrm π)) |
61 | 8, 8, 11 | ltaddsubd 11760 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((π΄ Yrm (π β 1)) + (π΄ Yrm (π β 1))) < (π΄ Yrm π) β (π΄ Yrm (π β 1)) < ((π΄ Yrm π) β (π΄ Yrm (π β 1))))) |
62 | 60, 61 | mpbid 231 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm (π β 1)) < ((π΄ Yrm π) β (π΄ Yrm (π β 1)))) |
63 | 8, 21, 11, 62 | ltadd1dd 11771 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) < (((π΄ Yrm π) β (π΄ Yrm (π β 1))) + (π΄ Yrm π))) |
64 | 11 | recnd 11188 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm π) β β) |
65 | 64 | 2timesd 12401 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· (π΄ Yrm π)) = ((π΄ Yrm π) + (π΄ Yrm π))) |
66 | 65 | oveq1d 7373 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1))) = (((π΄ Yrm π) + (π΄ Yrm π)) β (π΄ Yrm (π β 1)))) |
67 | 64, 64, 41 | addsubd 11538 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((π΄ Yrm π) + (π΄ Yrm π)) β (π΄ Yrm (π β 1))) = (((π΄ Yrm π) β (π΄ Yrm (π β 1))) + (π΄ Yrm π))) |
68 | 66, 67 | eqtrd 2773 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1))) = (((π΄ Yrm π) β (π΄ Yrm (π β 1))) + (π΄ Yrm π))) |
69 | 63, 68 | breqtrrd 5134 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) < ((2 Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1)))) |
70 | 25, 11 | remulcld 11190 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Β· (π΄ Yrm π)) β β) |
71 | | rmy0 41296 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 0) = 0) |
72 | 71 | adantr 482 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm 0) = 0) |
73 | | nngt0 12189 |
. . . . . . . . 9
β’ (π β β β 0 <
π) |
74 | 73 | adantl 483 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 < π) |
75 | | simpl 484 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π΄ β
(β€β₯β2)) |
76 | | 0zd 12516 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 β
β€) |
77 | 1 | adantl 483 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π β β€) |
78 | | ltrmy 41319 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ 0 β β€ β§ π β β€) β (0 < π β (π΄ Yrm 0) < (π΄ Yrm π))) |
79 | 75, 76, 77, 78 | syl3anc 1372 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (0 < π β (π΄ Yrm 0) < (π΄ Yrm π))) |
80 | 74, 79 | mpbid 231 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm 0) < (π΄ Yrm π)) |
81 | 72, 80 | eqbrtrrd 5130 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 < (π΄ Yrm π)) |
82 | | lemul1 12012 |
. . . . . 6
β’ ((2
β β β§ π΄
β β β§ ((π΄
Yrm π) β
β β§ 0 < (π΄
Yrm π))) β
(2 β€ π΄ β (2
Β· (π΄ Yrm
π)) β€ (π΄ Β· (π΄ Yrm π)))) |
83 | 32, 25, 11, 81, 82 | syl112anc 1375 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 β€ π΄ β (2 Β· (π΄ Yrm π)) β€ (π΄ Β· (π΄ Yrm π)))) |
84 | 38, 83 | mpbid 231 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· (π΄ Yrm π)) β€ (π΄ Β· (π΄ Yrm π))) |
85 | 15, 70, 8, 84 | lesub1dd 11776 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1))) β€ ((π΄ Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1)))) |
86 | | rmym1 41302 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm (π β 1)) = (((π΄ Yrm π) Β· π΄) β (π΄ Xrm π))) |
87 | 1, 86 | sylan2 594 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm (π β 1)) = (((π΄ Yrm π) Β· π΄) β (π΄ Xrm π))) |
88 | 64, 40 | mulcomd 11181 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm π) Β· π΄) = (π΄ Β· (π΄ Yrm π))) |
89 | 88 | oveq1d 7373 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((π΄ Yrm π) Β· π΄) β (π΄ Xrm π)) = ((π΄ Β· (π΄ Yrm π)) β (π΄ Xrm π))) |
90 | 87, 89 | eqtr2d 2774 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Β· (π΄ Yrm π)) β (π΄ Xrm π)) = (π΄ Yrm (π β 1))) |
91 | 70 | recnd 11188 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Β· (π΄ Yrm π)) β β) |
92 | 20 | recnd 11188 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Xrm π) β β) |
93 | | subsub23 11411 |
. . . . 5
β’ (((π΄ Β· (π΄ Yrm π)) β β β§ (π΄ Xrm π) β β β§ (π΄ Yrm (π β 1)) β β) β (((π΄ Β· (π΄ Yrm π)) β (π΄ Xrm π)) = (π΄ Yrm (π β 1)) β ((π΄ Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1))) = (π΄ Xrm π))) |
94 | 91, 92, 41, 93 | syl3anc 1372 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((π΄ Β· (π΄ Yrm π)) β (π΄ Xrm π)) = (π΄ Yrm (π β 1)) β ((π΄ Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1))) = (π΄ Xrm π))) |
95 | 90, 94 | mpbid 231 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1))) = (π΄ Xrm π)) |
96 | 85, 95 | breqtrd 5132 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1))) β€ (π΄ Xrm π)) |
97 | 12, 16, 20, 69, 96 | ltletrd 11320 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) < (π΄ Xrm π)) |