Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . . 6
β’ (π = 0 β (π΄ Xrm π) = (π΄ Xrm 0)) |
2 | 1 | breq2d 5118 |
. . . . 5
β’ (π = 0 β (0 < (π΄ Xrm π) β 0 < (π΄ Xrm
0))) |
3 | | oveq2 7366 |
. . . . . 6
β’ (π = 0 β (π΄ Yrm π) = (π΄ Yrm 0)) |
4 | 3 | breq2d 5118 |
. . . . 5
β’ (π = 0 β (0 β€ (π΄ Yrm π) β 0 β€ (π΄ Yrm
0))) |
5 | 2, 4 | anbi12d 632 |
. . . 4
β’ (π = 0 β ((0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π)) β (0 < (π΄ Xrm 0) β§ 0 β€
(π΄ Yrm
0)))) |
6 | 5 | imbi2d 341 |
. . 3
β’ (π = 0 β ((π΄ β (β€β₯β2)
β (0 < (π΄
Xrm π) β§ 0
β€ (π΄ Yrm
π))) β (π΄ β
(β€β₯β2) β (0 < (π΄ Xrm 0) β§ 0 β€ (π΄ Yrm
0))))) |
7 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (π΄ Xrm π) = (π΄ Xrm π)) |
8 | 7 | breq2d 5118 |
. . . . 5
β’ (π = π β (0 < (π΄ Xrm π) β 0 < (π΄ Xrm π))) |
9 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (π΄ Yrm π) = (π΄ Yrm π)) |
10 | 9 | breq2d 5118 |
. . . . 5
β’ (π = π β (0 β€ (π΄ Yrm π) β 0 β€ (π΄ Yrm π))) |
11 | 8, 10 | anbi12d 632 |
. . . 4
β’ (π = π β ((0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π)) β (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π)))) |
12 | 11 | imbi2d 341 |
. . 3
β’ (π = π β ((π΄ β (β€β₯β2)
β (0 < (π΄
Xrm π) β§ 0
β€ (π΄ Yrm
π))) β (π΄ β
(β€β₯β2) β (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))))) |
13 | | oveq2 7366 |
. . . . . 6
β’ (π = (π + 1) β (π΄ Xrm π) = (π΄ Xrm (π + 1))) |
14 | 13 | breq2d 5118 |
. . . . 5
β’ (π = (π + 1) β (0 < (π΄ Xrm π) β 0 < (π΄ Xrm (π + 1)))) |
15 | | oveq2 7366 |
. . . . . 6
β’ (π = (π + 1) β (π΄ Yrm π) = (π΄ Yrm (π + 1))) |
16 | 15 | breq2d 5118 |
. . . . 5
β’ (π = (π + 1) β (0 β€ (π΄ Yrm π) β 0 β€ (π΄ Yrm (π + 1)))) |
17 | 14, 16 | anbi12d 632 |
. . . 4
β’ (π = (π + 1) β ((0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π)) β (0 < (π΄ Xrm (π + 1)) β§ 0 β€ (π΄ Yrm (π + 1))))) |
18 | 17 | imbi2d 341 |
. . 3
β’ (π = (π + 1) β ((π΄ β (β€β₯β2)
β (0 < (π΄
Xrm π) β§ 0
β€ (π΄ Yrm
π))) β (π΄ β
(β€β₯β2) β (0 < (π΄ Xrm (π + 1)) β§ 0 β€ (π΄ Yrm (π + 1)))))) |
19 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (π΄ Xrm π) = (π΄ Xrm π)) |
20 | 19 | breq2d 5118 |
. . . . 5
β’ (π = π β (0 < (π΄ Xrm π) β 0 < (π΄ Xrm π))) |
21 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (π΄ Yrm π) = (π΄ Yrm π)) |
22 | 21 | breq2d 5118 |
. . . . 5
β’ (π = π β (0 β€ (π΄ Yrm π) β 0 β€ (π΄ Yrm π))) |
23 | 20, 22 | anbi12d 632 |
. . . 4
β’ (π = π β ((0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π)) β (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π)))) |
24 | 23 | imbi2d 341 |
. . 3
β’ (π = π β ((π΄ β (β€β₯β2)
β (0 < (π΄
Xrm π) β§ 0
β€ (π΄ Yrm
π))) β (π΄ β
(β€β₯β2) β (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))))) |
25 | | 0lt1 11682 |
. . . . 5
β’ 0 <
1 |
26 | | rmx0 41292 |
. . . . 5
β’ (π΄ β
(β€β₯β2) β (π΄ Xrm 0) = 1) |
27 | 25, 26 | breqtrrid 5144 |
. . . 4
β’ (π΄ β
(β€β₯β2) β 0 < (π΄ Xrm 0)) |
28 | | 0le0 12259 |
. . . . 5
β’ 0 β€
0 |
29 | | rmy0 41296 |
. . . . 5
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 0) = 0) |
30 | 28, 29 | breqtrrid 5144 |
. . . 4
β’ (π΄ β
(β€β₯β2) β 0 β€ (π΄ Yrm 0)) |
31 | 27, 30 | jca 513 |
. . 3
β’ (π΄ β
(β€β₯β2) β (0 < (π΄ Xrm 0) β§ 0 β€ (π΄ Yrm
0))) |
32 | | simp2 1138 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β π΄ β
(β€β₯β2)) |
33 | | nn0z 12529 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β€) |
34 | 33 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β π β β€) |
35 | | frmx 41280 |
. . . . . . . . . . . 12
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
36 | 35 | fovcl 7485 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
37 | 32, 34, 36 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (π΄ Xrm π) β
β0) |
38 | 37 | nn0red 12479 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (π΄ Xrm π) β β) |
39 | | eluzelre 12779 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
40 | 39 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β π΄ β β) |
41 | 38, 40 | remulcld 11190 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β ((π΄ Xrm π) Β· π΄) β β) |
42 | | rmspecpos 41283 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β+) |
43 | 42 | rpred 12962 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
44 | 43 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β ((π΄β2) β 1) β
β) |
45 | | frmy 41281 |
. . . . . . . . . . . 12
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
46 | 45 | fovcl 7485 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
47 | 32, 34, 46 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (π΄ Yrm π) β β€) |
48 | 47 | zred 12612 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (π΄ Yrm π) β β) |
49 | 44, 48 | remulcld 11190 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (((π΄β2) β 1) Β· (π΄ Yrm π)) β
β) |
50 | | simp3l 1202 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 < (π΄ Xrm π)) |
51 | | eluz2nn 12814 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
52 | 51 | nngt0d 12207 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β 0 < π΄) |
53 | 52 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 < π΄) |
54 | 38, 40, 50, 53 | mulgt0d 11315 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 < ((π΄ Xrm π) Β· π΄)) |
55 | 42 | rpge0d 12966 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β 0 β€ ((π΄β2) β 1)) |
56 | 55 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 β€ ((π΄β2) β 1)) |
57 | | simp3r 1203 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 β€ (π΄ Yrm π)) |
58 | 44, 48, 56, 57 | mulge0d 11737 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 β€ (((π΄β2) β 1) Β· (π΄ Yrm π))) |
59 | 41, 49, 54, 58 | addgtge0d 11734 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 < (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
60 | | rmxp1 41299 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + 1)) = (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
61 | 32, 34, 60 | syl2anc 585 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (π΄ Xrm (π + 1)) = (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
62 | 59, 61 | breqtrrd 5134 |
. . . . . 6
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 < (π΄ Xrm (π + 1))) |
63 | 48, 40 | remulcld 11190 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β ((π΄ Yrm π) Β· π΄) β β) |
64 | | eluzge2nn0 12817 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β π΄ β
β0) |
65 | 64 | nn0ge0d 12481 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β 0 β€ π΄) |
66 | 65 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 β€ π΄) |
67 | 48, 40, 57, 66 | mulge0d 11737 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 β€ ((π΄ Yrm π) Β· π΄)) |
68 | 37 | nn0ge0d 12481 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 β€ (π΄ Xrm π)) |
69 | 63, 38, 67, 68 | addge0d 11736 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 β€ (((π΄ Yrm π) Β· π΄) + (π΄ Xrm π))) |
70 | | rmyp1 41300 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm (π + 1)) = (((π΄ Yrm π) Β· π΄) + (π΄ Xrm π))) |
71 | 32, 34, 70 | syl2anc 585 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (π΄ Yrm (π + 1)) = (((π΄ Yrm π) Β· π΄) + (π΄ Xrm π))) |
72 | 69, 71 | breqtrrd 5134 |
. . . . . 6
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β 0 β€ (π΄ Yrm (π + 1))) |
73 | 62, 72 | jca 513 |
. . . . 5
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (0 < (π΄ Xrm (π + 1)) β§ 0 β€ (π΄ Yrm (π + 1)))) |
74 | 73 | 3exp 1120 |
. . . 4
β’ (π β β0
β (π΄ β
(β€β₯β2) β ((0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π)) β (0 < (π΄ Xrm (π + 1)) β§ 0 β€ (π΄ Yrm (π + 1)))))) |
75 | 74 | a2d 29 |
. . 3
β’ (π β β0
β ((π΄ β
(β€β₯β2) β (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) β (π΄ β (β€β₯β2)
β (0 < (π΄
Xrm (π + 1))
β§ 0 β€ (π΄
Yrm (π +
1)))))) |
76 | 6, 12, 18, 24, 31, 75 | nn0ind 12603 |
. 2
β’ (π β β0
β (π΄ β
(β€β₯β2) β (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π)))) |
77 | 76 | impcom 409 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (0 <
(π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) |