Step | Hyp | Ref
| Expression |
1 | | eluzelz 12778 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β π΄ β β€) |
2 | | eluzelz 12778 |
. . . . . . 7
β’ (π΅ β
(β€β₯β2) β π΅ β β€) |
3 | | zsubcl 12550 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ β π΅) β β€) |
4 | 1, 2, 3 | syl2an 597 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (π΄ β π΅) β
β€) |
5 | | 0z 12515 |
. . . . . 6
β’ 0 β
β€ |
6 | | congid 41338 |
. . . . . 6
β’ (((π΄ β π΅) β β€ β§ 0 β β€)
β (π΄ β π΅) β₯ (0 β
0)) |
7 | 4, 5, 6 | sylancl 587 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (π΄ β π΅) β₯ (0 β
0)) |
8 | | rmy0 41296 |
. . . . . 6
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 0) = 0) |
9 | | rmy0 41296 |
. . . . . 6
β’ (π΅ β
(β€β₯β2) β (π΅ Yrm 0) = 0) |
10 | 8, 9 | oveqan12d 7377 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β ((π΄ Yrm
0) β (π΅
Yrm 0)) = (0 β 0)) |
11 | 7, 10 | breqtrrd 5134 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (π΄ β π΅) β₯ ((π΄ Yrm 0) β (π΅ Yrm
0))) |
12 | | 1z 12538 |
. . . . . 6
β’ 1 β
β€ |
13 | | congid 41338 |
. . . . . 6
β’ (((π΄ β π΅) β β€ β§ 1 β β€)
β (π΄ β π΅) β₯ (1 β
1)) |
14 | 4, 12, 13 | sylancl 587 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (π΄ β π΅) β₯ (1 β
1)) |
15 | | rmy1 41297 |
. . . . . 6
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 1) = 1) |
16 | | rmy1 41297 |
. . . . . 6
β’ (π΅ β
(β€β₯β2) β (π΅ Yrm 1) = 1) |
17 | 15, 16 | oveqan12d 7377 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β ((π΄ Yrm
1) β (π΅
Yrm 1)) = (1 β 1)) |
18 | 14, 17 | breqtrrd 5134 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (π΄ β π΅) β₯ ((π΄ Yrm 1) β (π΅ Yrm
1))) |
19 | | pm3.43 475 |
. . . . 5
β’ ((((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1)))) β§ ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))))) |
20 | 4 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β β€) |
21 | | 2z 12540 |
. . . . . . . . . . 11
β’ 2 β
β€ |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β 2 β
β€) |
23 | | simp2l 1200 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β π΄ β
(β€β₯β2)) |
24 | | nnz 12525 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
25 | 24 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β π β β€) |
26 | | frmy 41281 |
. . . . . . . . . . . . 13
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
27 | 26 | fovcl 7485 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
28 | 23, 25, 27 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ Yrm π) β β€) |
29 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β π΄ β
β€) |
30 | 29 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β π΄ β β€) |
31 | 28, 30 | zmulcld 12618 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β ((π΄ Yrm π) Β· π΄) β β€) |
32 | 22, 31 | zmulcld 12618 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (2 Β· ((π΄ Yrm π) Β· π΄)) β β€) |
33 | | simp2r 1201 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β π΅ β
(β€β₯β2)) |
34 | 26 | fovcl 7485 |
. . . . . . . . . . . 12
β’ ((π΅ β
(β€β₯β2) β§ π β β€) β (π΅ Yrm π) β β€) |
35 | 33, 25, 34 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΅ Yrm π) β β€) |
36 | 2 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β π΅ β
β€) |
37 | 36 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β π΅ β β€) |
38 | 35, 37 | zmulcld 12618 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β ((π΅ Yrm π) Β· π΅) β β€) |
39 | 22, 38 | zmulcld 12618 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (2 Β· ((π΅ Yrm π) Β· π΅)) β β€) |
40 | | peano2zm 12551 |
. . . . . . . . . . . 12
β’ (π β β€ β (π β 1) β
β€) |
41 | 24, 40 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
β€) |
42 | 41 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π β 1) β β€) |
43 | 26 | fovcl 7485 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Yrm (π β 1)) β
β€) |
44 | 23, 42, 43 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ Yrm (π β 1)) β β€) |
45 | 26 | fovcl 7485 |
. . . . . . . . . 10
β’ ((π΅ β
(β€β₯β2) β§ (π β 1) β β€) β (π΅ Yrm (π β 1)) β
β€) |
46 | 33, 42, 45 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΅ Yrm (π β 1)) β β€) |
47 | | congid 41338 |
. . . . . . . . . . 11
β’ (((π΄ β π΅) β β€ β§ 2 β β€)
β (π΄ β π΅) β₯ (2 β
2)) |
48 | 20, 21, 47 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β₯ (2 β 2)) |
49 | | simp3r 1203 |
. . . . . . . . . . 11
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) |
50 | | iddvds 16157 |
. . . . . . . . . . . 12
β’ ((π΄ β π΅) β β€ β (π΄ β π΅) β₯ (π΄ β π΅)) |
51 | 20, 50 | syl 17 |
. . . . . . . . . . 11
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β₯ (π΄ β π΅)) |
52 | | congmul 41334 |
. . . . . . . . . . 11
β’ ((((π΄ β π΅) β β€ β§ (π΄ Yrm π) β β€ β§ (π΅ Yrm π) β β€) β§ (π΄ β β€ β§ π΅ β β€) β§ ((π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)) β§ (π΄ β π΅) β₯ (π΄ β π΅))) β (π΄ β π΅) β₯ (((π΄ Yrm π) Β· π΄) β ((π΅ Yrm π) Β· π΅))) |
53 | 20, 28, 35, 30, 37, 49, 51, 52 | syl322anc 1399 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β₯ (((π΄ Yrm π) Β· π΄) β ((π΅ Yrm π) Β· π΅))) |
54 | | congmul 41334 |
. . . . . . . . . 10
β’ ((((π΄ β π΅) β β€ β§ 2 β β€
β§ 2 β β€) β§ (((π΄ Yrm π) Β· π΄) β β€ β§ ((π΅ Yrm π) Β· π΅) β β€) β§ ((π΄ β π΅) β₯ (2 β 2) β§ (π΄ β π΅) β₯ (((π΄ Yrm π) Β· π΄) β ((π΅ Yrm π) Β· π΅)))) β (π΄ β π΅) β₯ ((2 Β· ((π΄ Yrm π) Β· π΄)) β (2 Β· ((π΅ Yrm π) Β· π΅)))) |
55 | 20, 22, 22, 31, 38, 48, 53, 54 | syl322anc 1399 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β₯ ((2 Β· ((π΄ Yrm π) Β· π΄)) β (2 Β· ((π΅ Yrm π) Β· π΅)))) |
56 | | simp3l 1202 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1)))) |
57 | | congsub 41337 |
. . . . . . . . 9
β’ ((((π΄ β π΅) β β€ β§ (2 Β· ((π΄ Yrm π) Β· π΄)) β β€ β§ (2 Β· ((π΅ Yrm π) Β· π΅)) β β€) β§ ((π΄ Yrm (π β 1)) β β€ β§ (π΅ Yrm (π β 1)) β β€)
β§ ((π΄ β π΅) β₯ ((2 Β· ((π΄ Yrm π) Β· π΄)) β (2 Β· ((π΅ Yrm π) Β· π΅))) β§ (π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))))) β (π΄ β π΅) β₯ (((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1))) β ((2 Β· ((π΅ Yrm π) Β· π΅)) β (π΅ Yrm (π β 1))))) |
58 | 20, 32, 39, 44, 46, 55, 56, 57 | syl322anc 1399 |
. . . . . . . 8
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β₯ (((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1))) β ((2 Β· ((π΅ Yrm π) Β· π΅)) β (π΅ Yrm (π β 1))))) |
59 | | rmyluc 41304 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm (π + 1)) = ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1)))) |
60 | 23, 25, 59 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ Yrm (π + 1)) = ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1)))) |
61 | | rmyluc 41304 |
. . . . . . . . . 10
β’ ((π΅ β
(β€β₯β2) β§ π β β€) β (π΅ Yrm (π + 1)) = ((2 Β· ((π΅ Yrm π) Β· π΅)) β (π΅ Yrm (π β 1)))) |
62 | 33, 25, 61 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΅ Yrm (π + 1)) = ((2 Β· ((π΅ Yrm π) Β· π΅)) β (π΅ Yrm (π β 1)))) |
63 | 60, 62 | oveq12d 7376 |
. . . . . . . 8
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β ((π΄ Yrm (π + 1)) β (π΅ Yrm (π + 1))) = (((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1))) β ((2 Β· ((π΅ Yrm π) Β· π΅)) β (π΅ Yrm (π β 1))))) |
64 | 58, 63 | breqtrrd 5134 |
. . . . . . 7
β’ ((π β β β§ (π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β (π΄ β π΅) β₯ ((π΄ Yrm (π + 1)) β (π΅ Yrm (π + 1)))) |
65 | 64 | 3exp 1120 |
. . . . . 6
β’ (π β β β ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) β (π΄ β π΅) β₯ ((π΄ Yrm (π + 1)) β (π΅ Yrm (π + 1)))))) |
66 | 65 | a2d 29 |
. . . . 5
β’ (π β β β (((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β ((π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))) β§ (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm (π + 1)) β (π΅ Yrm (π + 1)))))) |
67 | 19, 66 | syl5 34 |
. . . 4
β’ (π β β β ((((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1)))) β§ ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm (π + 1)) β (π΅ Yrm (π + 1)))))) |
68 | | oveq2 7366 |
. . . . . . 7
β’ (π = 0 β (π΄ Yrm π) = (π΄ Yrm 0)) |
69 | | oveq2 7366 |
. . . . . . 7
β’ (π = 0 β (π΅ Yrm π) = (π΅ Yrm 0)) |
70 | 68, 69 | oveq12d 7376 |
. . . . . 6
β’ (π = 0 β ((π΄ Yrm π) β (π΅ Yrm π)) = ((π΄ Yrm 0) β (π΅ Yrm
0))) |
71 | 70 | breq2d 5118 |
. . . . 5
β’ (π = 0 β ((π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)) β (π΄ β π΅) β₯ ((π΄ Yrm 0) β (π΅ Yrm
0)))) |
72 | 71 | imbi2d 341 |
. . . 4
β’ (π = 0 β (((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm 0) β (π΅ Yrm
0))))) |
73 | | oveq2 7366 |
. . . . . . 7
β’ (π = 1 β (π΄ Yrm π) = (π΄ Yrm 1)) |
74 | | oveq2 7366 |
. . . . . . 7
β’ (π = 1 β (π΅ Yrm π) = (π΅ Yrm 1)) |
75 | 73, 74 | oveq12d 7376 |
. . . . . 6
β’ (π = 1 β ((π΄ Yrm π) β (π΅ Yrm π)) = ((π΄ Yrm 1) β (π΅ Yrm
1))) |
76 | 75 | breq2d 5118 |
. . . . 5
β’ (π = 1 β ((π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)) β (π΄ β π΅) β₯ ((π΄ Yrm 1) β (π΅ Yrm
1)))) |
77 | 76 | imbi2d 341 |
. . . 4
β’ (π = 1 β (((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm 1) β (π΅ Yrm
1))))) |
78 | | oveq2 7366 |
. . . . . . 7
β’ (π = (π β 1) β (π΄ Yrm π) = (π΄ Yrm (π β 1))) |
79 | | oveq2 7366 |
. . . . . . 7
β’ (π = (π β 1) β (π΅ Yrm π) = (π΅ Yrm (π β 1))) |
80 | 78, 79 | oveq12d 7376 |
. . . . . 6
β’ (π = (π β 1) β ((π΄ Yrm π) β (π΅ Yrm π)) = ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1)))) |
81 | 80 | breq2d 5118 |
. . . . 5
β’ (π = (π β 1) β ((π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)) β (π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1))))) |
82 | 81 | imbi2d 341 |
. . . 4
β’ (π = (π β 1) β (((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm (π β 1)) β (π΅ Yrm (π β 1)))))) |
83 | | oveq2 7366 |
. . . . . . 7
β’ (π = π β (π΄ Yrm π) = (π΄ Yrm π)) |
84 | | oveq2 7366 |
. . . . . . 7
β’ (π = π β (π΅ Yrm π) = (π΅ Yrm π)) |
85 | 83, 84 | oveq12d 7376 |
. . . . . 6
β’ (π = π β ((π΄ Yrm π) β (π΅ Yrm π)) = ((π΄ Yrm π) β (π΅ Yrm π))) |
86 | 85 | breq2d 5118 |
. . . . 5
β’ (π = π β ((π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) |
87 | 86 | imbi2d 341 |
. . . 4
β’ (π = π β (((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))))) |
88 | | oveq2 7366 |
. . . . . . 7
β’ (π = (π + 1) β (π΄ Yrm π) = (π΄ Yrm (π + 1))) |
89 | | oveq2 7366 |
. . . . . . 7
β’ (π = (π + 1) β (π΅ Yrm π) = (π΅ Yrm (π + 1))) |
90 | 88, 89 | oveq12d 7376 |
. . . . . 6
β’ (π = (π + 1) β ((π΄ Yrm π) β (π΅ Yrm π)) = ((π΄ Yrm (π + 1)) β (π΅ Yrm (π + 1)))) |
91 | 90 | breq2d 5118 |
. . . . 5
β’ (π = (π + 1) β ((π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)) β (π΄ β π΅) β₯ ((π΄ Yrm (π + 1)) β (π΅ Yrm (π + 1))))) |
92 | 91 | imbi2d 341 |
. . . 4
β’ (π = (π + 1) β (((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm (π + 1)) β (π΅ Yrm (π + 1)))))) |
93 | | oveq2 7366 |
. . . . . . 7
β’ (π = π β (π΄ Yrm π) = (π΄ Yrm π)) |
94 | | oveq2 7366 |
. . . . . . 7
β’ (π = π β (π΅ Yrm π) = (π΅ Yrm π)) |
95 | 93, 94 | oveq12d 7376 |
. . . . . 6
β’ (π = π β ((π΄ Yrm π) β (π΅ Yrm π)) = ((π΄ Yrm π) β (π΅ Yrm π))) |
96 | 95 | breq2d 5118 |
. . . . 5
β’ (π = π β ((π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) |
97 | 96 | imbi2d 341 |
. . . 4
β’ (π = π β (((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) β ((π΄ β (β€β₯β2)
β§ π΅ β
(β€β₯β2)) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))))) |
98 | 11, 18, 67, 72, 77, 82, 87, 92, 97 | 2nn0ind 41312 |
. . 3
β’ (π β β0
β ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π)))) |
99 | 98 | impcom 409 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2))
β§ π β
β0) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) |
100 | 99 | 3impa 1111 |
1
β’ ((π΄ β
(β€β₯β2) β§ π΅ β (β€β₯β2)
β§ π β
β0) β (π΄ β π΅) β₯ ((π΄ Yrm π) β (π΅ Yrm π))) |