Step | Hyp | Ref
| Expression |
1 | | eluzelz 12778 |
. . . . . 6
β’ (π΄ β
(β€β₯β2) β π΄ β β€) |
2 | | peano2zm 12551 |
. . . . . 6
β’ (π΄ β β€ β (π΄ β 1) β
β€) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π΄ β
(β€β₯β2) β (π΄ β 1) β β€) |
4 | | 0z 12515 |
. . . . 5
β’ 0 β
β€ |
5 | | congid 41338 |
. . . . 5
β’ (((π΄ β 1) β β€ β§
0 β β€) β (π΄
β 1) β₯ (0 β 0)) |
6 | 3, 4, 5 | sylancl 587 |
. . . 4
β’ (π΄ β
(β€β₯β2) β (π΄ β 1) β₯ (0 β
0)) |
7 | | rmy0 41296 |
. . . . 5
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 0) = 0) |
8 | 7 | oveq1d 7373 |
. . . 4
β’ (π΄ β
(β€β₯β2) β ((π΄ Yrm 0) β 0) = (0 β
0)) |
9 | 6, 8 | breqtrrd 5134 |
. . 3
β’ (π΄ β
(β€β₯β2) β (π΄ β 1) β₯ ((π΄ Yrm 0) β
0)) |
10 | | 1z 12538 |
. . . . 5
β’ 1 β
β€ |
11 | | congid 41338 |
. . . . 5
β’ (((π΄ β 1) β β€ β§
1 β β€) β (π΄
β 1) β₯ (1 β 1)) |
12 | 3, 10, 11 | sylancl 587 |
. . . 4
β’ (π΄ β
(β€β₯β2) β (π΄ β 1) β₯ (1 β
1)) |
13 | | rmy1 41297 |
. . . . 5
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 1) = 1) |
14 | 13 | oveq1d 7373 |
. . . 4
β’ (π΄ β
(β€β₯β2) β ((π΄ Yrm 1) β 1) = (1 β
1)) |
15 | 12, 14 | breqtrrd 5134 |
. . 3
β’ (π΄ β
(β€β₯β2) β (π΄ β 1) β₯ ((π΄ Yrm 1) β
1)) |
16 | | pm3.43 475 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β (π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1))) β§ (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π))) β (π΄ β (β€β₯β2)
β ((π΄ β 1)
β₯ ((π΄ Yrm
(π β 1)) β
(π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π)))) |
17 | 1 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β
(β€β₯β2)) β π΄ β β€) |
18 | 17, 2 | syl 17 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π΄ β 1) β β€) |
19 | | eluzel2 12773 |
. . . . . . . . . . . 12
β’ (π΄ β
(β€β₯β2) β 2 β β€) |
20 | 19 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β
(β€β₯β2)) β 2 β β€) |
21 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π΄ β
(β€β₯β2)) β π΄ β
(β€β₯β2)) |
22 | | nnz 12525 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β€) |
23 | 22 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π΄ β
(β€β₯β2)) β π β β€) |
24 | | frmy 41281 |
. . . . . . . . . . . . . 14
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
25 | 24 | fovcl 7485 |
. . . . . . . . . . . . 13
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
26 | 21, 23, 25 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π΄ Yrm π) β β€) |
27 | 26, 17 | zmulcld 12618 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm π) Β· π΄) β β€) |
28 | 20, 27 | zmulcld 12618 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (2 Β· ((π΄ Yrm π) Β· π΄)) β β€) |
29 | | zmulcl 12557 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ 1 β
β€) β (π Β·
1) β β€) |
30 | 23, 10, 29 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π Β· 1) β β€) |
31 | 20, 30 | zmulcld 12618 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (2 Β· (π Β· 1)) β
β€) |
32 | 18, 28, 31 | 3jca 1129 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β
(β€β₯β2)) β ((π΄ β 1) β β€ β§ (2 Β·
((π΄ Yrm π) Β· π΄)) β β€ β§ (2 Β· (π Β· 1)) β
β€)) |
33 | 32 | 3adant3 1133 |
. . . . . . . 8
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β ((π΄ β 1) β β€ β§ (2 Β·
((π΄ Yrm π) Β· π΄)) β β€ β§ (2 Β· (π Β· 1)) β
β€)) |
34 | | peano2zm 12551 |
. . . . . . . . . . . 12
β’ (π β β€ β (π β 1) β
β€) |
35 | 23, 34 | syl 17 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π β 1) β β€) |
36 | 24 | fovcl 7485 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Yrm (π β 1)) β
β€) |
37 | 21, 35, 36 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π΄ Yrm (π β 1)) β β€) |
38 | 37, 35 | jca 513 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π β 1)) β β€ β§ (π β 1) β
β€)) |
39 | 38 | 3adant3 1133 |
. . . . . . . 8
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β ((π΄ Yrm (π β 1)) β β€ β§ (π β 1) β
β€)) |
40 | 18, 20, 20 | 3jca 1129 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2)) β ((π΄ β 1) β β€ β§ 2 β
β€ β§ 2 β β€)) |
41 | 40 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β ((π΄ β 1) β β€ β§ 2 β
β€ β§ 2 β β€)) |
42 | 27, 30 | jca 513 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (((π΄ Yrm π) Β· π΄) β β€ β§ (π Β· 1) β
β€)) |
43 | 42 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (((π΄ Yrm π) Β· π΄) β β€ β§ (π Β· 1) β
β€)) |
44 | | congid 41338 |
. . . . . . . . . . 11
β’ (((π΄ β 1) β β€ β§
2 β β€) β (π΄
β 1) β₯ (2 β 2)) |
45 | 18, 20, 44 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π΄ β 1) β₯ (2 β
2)) |
46 | 45 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β 1) β₯ (2 β
2)) |
47 | 18, 26, 23 | 3jca 1129 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β
(β€β₯β2)) β ((π΄ β 1) β β€ β§ (π΄ Yrm π) β β€ β§ π β
β€)) |
48 | 47 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β ((π΄ β 1) β β€ β§ (π΄ Yrm π) β β€ β§ π β
β€)) |
49 | 17, 10 | jctir 522 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π΄ β β€ β§ 1 β
β€)) |
50 | 49 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β β€ β§ 1 β
β€)) |
51 | | simp3r 1203 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β 1) β₯ ((π΄ Yrm π) β π)) |
52 | | iddvds 16157 |
. . . . . . . . . . . 12
β’ ((π΄ β 1) β β€
β (π΄ β 1)
β₯ (π΄ β
1)) |
53 | 18, 52 | syl 17 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π΄ β 1) β₯ (π΄ β 1)) |
54 | 53 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β 1) β₯ (π΄ β 1)) |
55 | | congmul 41334 |
. . . . . . . . . 10
β’ ((((π΄ β 1) β β€ β§
(π΄ Yrm π) β β€ β§ π β β€) β§ (π΄ β β€ β§ 1 β
β€) β§ ((π΄ β
1) β₯ ((π΄
Yrm π) β
π) β§ (π΄ β 1) β₯ (π΄ β 1))) β (π΄ β 1) β₯ (((π΄ Yrm π) Β· π΄) β (π Β· 1))) |
56 | 48, 50, 51, 54, 55 | syl112anc 1375 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β 1) β₯ (((π΄ Yrm π) Β· π΄) β (π Β· 1))) |
57 | | congmul 41334 |
. . . . . . . . 9
β’ ((((π΄ β 1) β β€ β§
2 β β€ β§ 2 β β€) β§ (((π΄ Yrm π) Β· π΄) β β€ β§ (π Β· 1) β β€) β§ ((π΄ β 1) β₯ (2 β
2) β§ (π΄ β 1)
β₯ (((π΄ Yrm
π) Β· π΄) β (π Β· 1)))) β (π΄ β 1) β₯ ((2 Β· ((π΄ Yrm π) Β· π΄)) β (2 Β· (π Β· 1)))) |
58 | 41, 43, 46, 56, 57 | syl112anc 1375 |
. . . . . . . 8
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β 1) β₯ ((2 Β· ((π΄ Yrm π) Β· π΄)) β (2 Β· (π Β· 1)))) |
59 | | simp3l 1202 |
. . . . . . . 8
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1))) |
60 | | congsub 41337 |
. . . . . . . 8
β’ ((((π΄ β 1) β β€ β§
(2 Β· ((π΄
Yrm π) Β·
π΄)) β β€ β§ (2
Β· (π Β· 1))
β β€) β§ ((π΄
Yrm (π β
1)) β β€ β§ (π
β 1) β β€) β§ ((π΄ β 1) β₯ ((2 Β· ((π΄ Yrm π) Β· π΄)) β (2 Β· (π Β· 1))) β§ (π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)))) β (π΄ β 1) β₯ (((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1))) β ((2 Β· (π Β· 1)) β (π β 1)))) |
61 | 33, 39, 58, 59, 60 | syl112anc 1375 |
. . . . . . 7
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β 1) β₯ (((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1))) β ((2 Β· (π Β· 1)) β (π β 1)))) |
62 | | rmyluc 41304 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm (π + 1)) = ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1)))) |
63 | 21, 23, 62 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π΄ Yrm (π + 1)) = ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1)))) |
64 | | nncn 12166 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
65 | 64 | mulid1d 11177 |
. . . . . . . . . . . . . 14
β’ (π β β β (π Β· 1) = π) |
66 | 65 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π β β β (2
Β· (π Β· 1)) =
(2 Β· π)) |
67 | 64 | 2timesd 12401 |
. . . . . . . . . . . . 13
β’ (π β β β (2
Β· π) = (π + π)) |
68 | 66, 67 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β β β (2
Β· (π Β· 1)) =
(π + π)) |
69 | 68 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π β β β ((2
Β· (π Β· 1))
β (π β 1)) =
((π + π) β (π β 1))) |
70 | | 1cnd 11155 |
. . . . . . . . . . . 12
β’ (π β β β 1 β
β) |
71 | 64, 64, 70 | pnncand 11556 |
. . . . . . . . . . 11
β’ (π β β β ((π + π) β (π β 1)) = (π + 1)) |
72 | 69, 71 | eqtr2d 2774 |
. . . . . . . . . 10
β’ (π β β β (π + 1) = ((2 Β· (π Β· 1)) β (π β 1))) |
73 | 72 | adantr 482 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β
(β€β₯β2)) β (π + 1) = ((2 Β· (π Β· 1)) β (π β 1))) |
74 | 63, 73 | oveq12d 7376 |
. . . . . . . 8
β’ ((π β β β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π + 1)) β (π + 1)) = (((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1))) β ((2 Β· (π Β· 1)) β (π β 1)))) |
75 | 74 | 3adant3 1133 |
. . . . . . 7
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β ((π΄ Yrm (π + 1)) β (π + 1)) = (((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1))) β ((2 Β· (π Β· 1)) β (π β 1)))) |
76 | 61, 75 | breqtrrd 5134 |
. . . . . 6
β’ ((π β β β§ π΄ β
(β€β₯β2) β§ ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β 1) β₯ ((π΄ Yrm (π + 1)) β (π + 1))) |
77 | 76 | 3exp 1120 |
. . . . 5
β’ (π β β β (π΄ β
(β€β₯β2) β (((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π)) β (π΄ β 1) β₯ ((π΄ Yrm (π + 1)) β (π + 1))))) |
78 | 77 | a2d 29 |
. . . 4
β’ (π β β β ((π΄ β
(β€β₯β2) β ((π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)) β§ (π΄ β 1) β₯ ((π΄ Yrm π) β π))) β (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
(π + 1)) β (π + 1))))) |
79 | 16, 78 | syl5 34 |
. . 3
β’ (π β β β (((π΄ β
(β€β₯β2) β (π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1))) β§ (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π))) β (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
(π + 1)) β (π + 1))))) |
80 | | oveq2 7366 |
. . . . . 6
β’ (π = 0 β (π΄ Yrm π) = (π΄ Yrm 0)) |
81 | | id 22 |
. . . . . 6
β’ (π = 0 β π = 0) |
82 | 80, 81 | oveq12d 7376 |
. . . . 5
β’ (π = 0 β ((π΄ Yrm π) β π) = ((π΄ Yrm 0) β
0)) |
83 | 82 | breq2d 5118 |
. . . 4
β’ (π = 0 β ((π΄ β 1) β₯ ((π΄ Yrm π) β π) β (π΄ β 1) β₯ ((π΄ Yrm 0) β
0))) |
84 | 83 | imbi2d 341 |
. . 3
β’ (π = 0 β ((π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π)) β (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
0) β 0)))) |
85 | | oveq2 7366 |
. . . . . 6
β’ (π = 1 β (π΄ Yrm π) = (π΄ Yrm 1)) |
86 | | id 22 |
. . . . . 6
β’ (π = 1 β π = 1) |
87 | 85, 86 | oveq12d 7376 |
. . . . 5
β’ (π = 1 β ((π΄ Yrm π) β π) = ((π΄ Yrm 1) β
1)) |
88 | 87 | breq2d 5118 |
. . . 4
β’ (π = 1 β ((π΄ β 1) β₯ ((π΄ Yrm π) β π) β (π΄ β 1) β₯ ((π΄ Yrm 1) β
1))) |
89 | 88 | imbi2d 341 |
. . 3
β’ (π = 1 β ((π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π)) β (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
1) β 1)))) |
90 | | oveq2 7366 |
. . . . . 6
β’ (π = (π β 1) β (π΄ Yrm π) = (π΄ Yrm (π β 1))) |
91 | | id 22 |
. . . . . 6
β’ (π = (π β 1) β π = (π β 1)) |
92 | 90, 91 | oveq12d 7376 |
. . . . 5
β’ (π = (π β 1) β ((π΄ Yrm π) β π) = ((π΄ Yrm (π β 1)) β (π β 1))) |
93 | 92 | breq2d 5118 |
. . . 4
β’ (π = (π β 1) β ((π΄ β 1) β₯ ((π΄ Yrm π) β π) β (π΄ β 1) β₯ ((π΄ Yrm (π β 1)) β (π β 1)))) |
94 | 93 | imbi2d 341 |
. . 3
β’ (π = (π β 1) β ((π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π)) β (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
(π β 1)) β
(π β
1))))) |
95 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (π΄ Yrm π) = (π΄ Yrm π)) |
96 | | id 22 |
. . . . . 6
β’ (π = π β π = π) |
97 | 95, 96 | oveq12d 7376 |
. . . . 5
β’ (π = π β ((π΄ Yrm π) β π) = ((π΄ Yrm π) β π)) |
98 | 97 | breq2d 5118 |
. . . 4
β’ (π = π β ((π΄ β 1) β₯ ((π΄ Yrm π) β π) β (π΄ β 1) β₯ ((π΄ Yrm π) β π))) |
99 | 98 | imbi2d 341 |
. . 3
β’ (π = π β ((π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π)) β (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π)))) |
100 | | oveq2 7366 |
. . . . . 6
β’ (π = (π + 1) β (π΄ Yrm π) = (π΄ Yrm (π + 1))) |
101 | | id 22 |
. . . . . 6
β’ (π = (π + 1) β π = (π + 1)) |
102 | 100, 101 | oveq12d 7376 |
. . . . 5
β’ (π = (π + 1) β ((π΄ Yrm π) β π) = ((π΄ Yrm (π + 1)) β (π + 1))) |
103 | 102 | breq2d 5118 |
. . . 4
β’ (π = (π + 1) β ((π΄ β 1) β₯ ((π΄ Yrm π) β π) β (π΄ β 1) β₯ ((π΄ Yrm (π + 1)) β (π + 1)))) |
104 | 103 | imbi2d 341 |
. . 3
β’ (π = (π + 1) β ((π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π)) β (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
(π + 1)) β (π + 1))))) |
105 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (π΄ Yrm π) = (π΄ Yrm π)) |
106 | | id 22 |
. . . . . 6
β’ (π = π β π = π) |
107 | 105, 106 | oveq12d 7376 |
. . . . 5
β’ (π = π β ((π΄ Yrm π) β π) = ((π΄ Yrm π) β π)) |
108 | 107 | breq2d 5118 |
. . . 4
β’ (π = π β ((π΄ β 1) β₯ ((π΄ Yrm π) β π) β (π΄ β 1) β₯ ((π΄ Yrm π) β π))) |
109 | 108 | imbi2d 341 |
. . 3
β’ (π = π β ((π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π)) β (π΄ β (β€β₯β2)
β (π΄ β 1)
β₯ ((π΄ Yrm
π) β π)))) |
110 | 9, 15, 79, 84, 89, 94, 99, 104, 109 | 2nn0ind 41312 |
. 2
β’ (π β β0
β (π΄ β
(β€β₯β2) β (π΄ β 1) β₯ ((π΄ Yrm π) β π))) |
111 | 110 | impcom 409 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ β 1) β₯ ((π΄ Yrm π) β π)) |