Step | Hyp | Ref
| Expression |
1 | | nn0z 12529 |
. . . . . 6
β’ (π β β0
β π β
β€) |
2 | | frmx 41280 |
. . . . . . 7
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
3 | 2 | fovcl 7485 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
4 | 1, 3 | sylan2 594 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm π) β
β0) |
5 | 4 | nn0red 12479 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm π) β
β) |
6 | | eluzelre 12779 |
. . . . . 6
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
7 | 6 | adantr 482 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β π΄ β
β) |
8 | 5, 7 | remulcld 11190 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β ((π΄ Xrm π) Β· π΄) β β) |
9 | 1 | peano2zd 12615 |
. . . . . 6
β’ (π β β0
β (π + 1) β
β€) |
10 | 2 | fovcl 7485 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Xrm (π + 1)) β
β0) |
11 | 9, 10 | sylan2 594 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm (π + 1)) β
β0) |
12 | 11 | nn0red 12479 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm (π + 1)) β
β) |
13 | | eluz2b2 12851 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β (π΄ β β β§ 1 < π΄)) |
14 | 13 | simprbi 498 |
. . . . . 6
β’ (π΄ β
(β€β₯β2) β 1 < π΄) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β 1 <
π΄) |
16 | | rmxypos 41314 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (0 <
(π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) |
17 | 16 | simpld 496 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β 0 <
(π΄ Xrm π)) |
18 | | ltmulgt11 12020 |
. . . . . 6
β’ (((π΄ Xrm π) β β β§ π΄ β β β§ 0 <
(π΄ Xrm π)) β (1 < π΄ β (π΄ Xrm π) < ((π΄ Xrm π) Β· π΄))) |
19 | 5, 7, 17, 18 | syl3anc 1372 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (1 <
π΄ β (π΄ Xrm π) < ((π΄ Xrm π) Β· π΄))) |
20 | 15, 19 | mpbid 231 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm π) < ((π΄ Xrm π) Β· π΄)) |
21 | | rmspecnonsq 41273 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β (β β
β»NN)) |
22 | 21 | eldifad 3923 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β ((π΄β2) β 1) β
β) |
24 | 23 | nnred 12173 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β ((π΄β2) β 1) β
β) |
25 | | frmy 41281 |
. . . . . . . . . 10
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
26 | 25 | fovcl 7485 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
27 | 1, 26 | sylan2 594 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Yrm π) β
β€) |
28 | 27 | zred 12612 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Yrm π) β
β) |
29 | 23 | nnnn0d 12478 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β ((π΄β2) β 1) β
β0) |
30 | 29 | nn0ge0d 12481 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β 0 β€
((π΄β2) β
1)) |
31 | 16 | simprd 497 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β 0 β€
(π΄ Yrm π)) |
32 | 24, 28, 30, 31 | mulge0d 11737 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β 0 β€
(((π΄β2) β 1)
Β· (π΄ Yrm
π))) |
33 | 24, 28 | remulcld 11190 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (((π΄β2) β 1) Β·
(π΄ Yrm π)) β
β) |
34 | 8, 33 | addge01d 11748 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (0 β€
(((π΄β2) β 1)
Β· (π΄ Yrm
π)) β ((π΄ Xrm π) Β· π΄) β€ (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π))))) |
35 | 32, 34 | mpbid 231 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β ((π΄ Xrm π) Β· π΄) β€ (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
36 | | rmxp1 41299 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + 1)) = (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
37 | 1, 36 | sylan2 594 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm (π + 1)) = (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
38 | 35, 37 | breqtrrd 5134 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β ((π΄ Xrm π) Β· π΄) β€ (π΄ Xrm (π + 1))) |
39 | 5, 8, 12, 20, 38 | ltletrd 11320 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm π) < (π΄ Xrm (π + 1))) |
40 | | nn0z 12529 |
. . . . 5
β’ (π β β0
β π β
β€) |
41 | 2 | fovcl 7485 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
42 | 40, 41 | sylan2 594 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm π) β
β0) |
43 | 42 | nn0red 12479 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Xrm π) β
β) |
44 | | nn0uz 12810 |
. . 3
β’
β0 = (β€β₯β0) |
45 | | oveq2 7366 |
. . 3
β’ (π = (π + 1) β (π΄ Xrm π) = (π΄ Xrm (π + 1))) |
46 | | oveq2 7366 |
. . 3
β’ (π = π β (π΄ Xrm π) = (π΄ Xrm π)) |
47 | | oveq2 7366 |
. . 3
β’ (π = π β (π΄ Xrm π) = (π΄ Xrm π)) |
48 | | oveq2 7366 |
. . 3
β’ (π = π β (π΄ Xrm π) = (π΄ Xrm π)) |
49 | 39, 43, 44, 45, 46, 47, 48 | monotuz 41308 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ (π β β0 β§ π β β0))
β (π < π β (π΄ Xrm π) < (π΄ Xrm π))) |
50 | 49 | 3impb 1116 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (π < π β (π΄ Xrm π) < (π΄ Xrm π))) |