Step | Hyp | Ref
| Expression |
1 | | itcovalpc.f |
. . . . 5
β’ πΉ = (π β β0 β¦ (π + πΆ)) |
2 | | nn0ex 12478 |
. . . . . 6
β’
β0 β V |
3 | 2 | mptex 7225 |
. . . . 5
β’ (π β β0
β¦ (π + πΆ)) β V |
4 | 1, 3 | eqeltri 2830 |
. . . 4
β’ πΉ β V |
5 | | simpl 484 |
. . . 4
β’ ((π¦ β β0
β§ πΆ β
β0) β π¦ β β0) |
6 | | simpr 486 |
. . . 4
β’ (((π¦ β β0
β§ πΆ β
β0) β§ ((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦)))) β ((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦)))) |
7 | | itcovalsucov 47354 |
. . . 4
β’ ((πΉ β V β§ π¦ β β0
β§ ((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦)))) β ((IterCompβπΉ)β(π¦ + 1)) = (πΉ β (π β β0 β¦ (π + (πΆ Β· π¦))))) |
8 | 4, 5, 6, 7 | mp3an2ani 1469 |
. . 3
β’ (((π¦ β β0
β§ πΆ β
β0) β§ ((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦)))) β ((IterCompβπΉ)β(π¦ + 1)) = (πΉ β (π β β0 β¦ (π + (πΆ Β· π¦))))) |
9 | | simpr 486 |
. . . . . . 7
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β π β
β0) |
10 | | simplr 768 |
. . . . . . . 8
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β πΆ β
β0) |
11 | 5 | adantr 482 |
. . . . . . . 8
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β π¦ β
β0) |
12 | 10, 11 | nn0mulcld 12537 |
. . . . . . 7
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β (πΆ Β· π¦) β
β0) |
13 | 9, 12 | nn0addcld 12536 |
. . . . . 6
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β (π + (πΆ Β· π¦)) β
β0) |
14 | | eqidd 2734 |
. . . . . 6
β’ ((π¦ β β0
β§ πΆ β
β0) β (π β β0 β¦ (π + (πΆ Β· π¦))) = (π β β0 β¦ (π + (πΆ Β· π¦)))) |
15 | | oveq1 7416 |
. . . . . . . . 9
β’ (π = π β (π + πΆ) = (π + πΆ)) |
16 | 15 | cbvmptv 5262 |
. . . . . . . 8
β’ (π β β0
β¦ (π + πΆ)) = (π β β0 β¦ (π + πΆ)) |
17 | 1, 16 | eqtri 2761 |
. . . . . . 7
β’ πΉ = (π β β0 β¦ (π + πΆ)) |
18 | 17 | a1i 11 |
. . . . . 6
β’ ((π¦ β β0
β§ πΆ β
β0) β πΉ = (π β β0 β¦ (π + πΆ))) |
19 | | oveq1 7416 |
. . . . . 6
β’ (π = (π + (πΆ Β· π¦)) β (π + πΆ) = ((π + (πΆ Β· π¦)) + πΆ)) |
20 | 13, 14, 18, 19 | fmptco 7127 |
. . . . 5
β’ ((π¦ β β0
β§ πΆ β
β0) β (πΉ β (π β β0 β¦ (π + (πΆ Β· π¦)))) = (π β β0 β¦ ((π + (πΆ Β· π¦)) + πΆ))) |
21 | 9 | nn0cnd 12534 |
. . . . . . . 8
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β π β
β) |
22 | 12 | nn0cnd 12534 |
. . . . . . . 8
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β (πΆ Β· π¦) β β) |
23 | 10 | nn0cnd 12534 |
. . . . . . . 8
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β πΆ β
β) |
24 | 21, 22, 23 | addassd 11236 |
. . . . . . 7
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β ((π + (πΆ Β· π¦)) + πΆ) = (π + ((πΆ Β· π¦) + πΆ))) |
25 | | nn0cn 12482 |
. . . . . . . . . . . . . 14
β’ (πΆ β β0
β πΆ β
β) |
26 | 25 | mulridd 11231 |
. . . . . . . . . . . . 13
β’ (πΆ β β0
β (πΆ Β· 1) =
πΆ) |
27 | 26 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ πΆ β
β0) β (πΆ Β· 1) = πΆ) |
28 | 27 | eqcomd 2739 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ πΆ β
β0) β πΆ = (πΆ Β· 1)) |
29 | 28 | oveq2d 7425 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ πΆ β
β0) β ((πΆ Β· π¦) + πΆ) = ((πΆ Β· π¦) + (πΆ Β· 1))) |
30 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ πΆ β
β0) β πΆ β
β0) |
31 | 30 | nn0cnd 12534 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ πΆ β
β0) β πΆ β β) |
32 | 5 | nn0cnd 12534 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ πΆ β
β0) β π¦ β β) |
33 | | 1cnd 11209 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ πΆ β
β0) β 1 β β) |
34 | 31, 32, 33 | adddid 11238 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ πΆ β
β0) β (πΆ Β· (π¦ + 1)) = ((πΆ Β· π¦) + (πΆ Β· 1))) |
35 | 29, 34 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((π¦ β β0
β§ πΆ β
β0) β ((πΆ Β· π¦) + πΆ) = (πΆ Β· (π¦ + 1))) |
36 | 35 | oveq2d 7425 |
. . . . . . . 8
β’ ((π¦ β β0
β§ πΆ β
β0) β (π + ((πΆ Β· π¦) + πΆ)) = (π + (πΆ Β· (π¦ + 1)))) |
37 | 36 | adantr 482 |
. . . . . . 7
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β (π + ((πΆ Β· π¦) + πΆ)) = (π + (πΆ Β· (π¦ + 1)))) |
38 | 24, 37 | eqtrd 2773 |
. . . . . 6
β’ (((π¦ β β0
β§ πΆ β
β0) β§ π β β0) β ((π + (πΆ Β· π¦)) + πΆ) = (π + (πΆ Β· (π¦ + 1)))) |
39 | 38 | mpteq2dva 5249 |
. . . . 5
β’ ((π¦ β β0
β§ πΆ β
β0) β (π β β0 β¦ ((π + (πΆ Β· π¦)) + πΆ)) = (π β β0 β¦ (π + (πΆ Β· (π¦ + 1))))) |
40 | 20, 39 | eqtrd 2773 |
. . . 4
β’ ((π¦ β β0
β§ πΆ β
β0) β (πΉ β (π β β0 β¦ (π + (πΆ Β· π¦)))) = (π β β0 β¦ (π + (πΆ Β· (π¦ + 1))))) |
41 | 40 | adantr 482 |
. . 3
β’ (((π¦ β β0
β§ πΆ β
β0) β§ ((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦)))) β (πΉ β (π β β0 β¦ (π + (πΆ Β· π¦)))) = (π β β0 β¦ (π + (πΆ Β· (π¦ + 1))))) |
42 | 8, 41 | eqtrd 2773 |
. 2
β’ (((π¦ β β0
β§ πΆ β
β0) β§ ((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦)))) β ((IterCompβπΉ)β(π¦ + 1)) = (π β β0 β¦ (π + (πΆ Β· (π¦ + 1))))) |
43 | 42 | ex 414 |
1
β’ ((π¦ β β0
β§ πΆ β
β0) β (((IterCompβπΉ)βπ¦) = (π β β0 β¦ (π + (πΆ Β· π¦))) β ((IterCompβπΉ)β(π¦ + 1)) = (π β β0 β¦ (π + (πΆ Β· (π¦ + 1)))))) |