Step | Hyp | Ref
| Expression |
1 | | nnuz 12807 |
. . 3
β’ β =
(β€β₯β1) |
2 | | 1zzd 12535 |
. . 3
β’ (π β 1 β
β€) |
3 | | nnex 12160 |
. . . . . 6
β’ β
β V |
4 | 3 | mptex 7174 |
. . . . 5
β’ (π β β β¦ 1)
β V |
5 | 4 | a1i 11 |
. . . 4
β’ (π β (π β β β¦ 1) β
V) |
6 | | 1cnd 11151 |
. . . 4
β’ (π β 1 β
β) |
7 | | eqidd 2738 |
. . . . . 6
β’ (π β β β (π β β β¦ 1) =
(π β β β¦
1)) |
8 | | eqidd 2738 |
. . . . . 6
β’ ((π β β β§ π = π) β 1 = 1) |
9 | | id 22 |
. . . . . 6
β’ (π β β β π β
β) |
10 | | 1cnd 11151 |
. . . . . 6
β’ (π β β β 1 β
β) |
11 | 7, 8, 9, 10 | fvmptd 6956 |
. . . . 5
β’ (π β β β ((π β β β¦
1)βπ) =
1) |
12 | 11 | adantl 483 |
. . . 4
β’ ((π β§ π β β) β ((π β β β¦ 1)βπ) = 1) |
13 | 1, 2, 5, 6, 12 | climconst 15426 |
. . 3
β’ (π β (π β β β¦ 1) β
1) |
14 | | clim1fr1.1 |
. . . . 5
β’ πΉ = (π β β β¦ (((π΄ Β· π) + π΅) / (π΄ Β· π))) |
15 | 3 | mptex 7174 |
. . . . 5
β’ (π β β β¦ (((π΄ Β· π) + π΅) / (π΄ Β· π))) β V |
16 | 14, 15 | eqeltri 2834 |
. . . 4
β’ πΉ β V |
17 | 16 | a1i 11 |
. . 3
β’ (π β πΉ β V) |
18 | | clim1fr1.4 |
. . . . . . 7
β’ (π β π΅ β β) |
19 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π΅ β β) |
20 | | clim1fr1.2 |
. . . . . . 7
β’ (π β π΄ β β) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π΄ β β) |
22 | | nncn 12162 |
. . . . . . 7
β’ (π β β β π β
β) |
23 | 22 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
24 | | clim1fr1.3 |
. . . . . . 7
β’ (π β π΄ β 0) |
25 | 24 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π΄ β 0) |
26 | | nnne0 12188 |
. . . . . . 7
β’ (π β β β π β 0) |
27 | 26 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β π β 0) |
28 | 19, 21, 23, 25, 27 | divdiv1d 11963 |
. . . . 5
β’ ((π β§ π β β) β ((π΅ / π΄) / π) = (π΅ / (π΄ Β· π))) |
29 | 28 | mpteq2dva 5206 |
. . . 4
β’ (π β (π β β β¦ ((π΅ / π΄) / π)) = (π β β β¦ (π΅ / (π΄ Β· π)))) |
30 | 18, 20, 24 | divcld 11932 |
. . . . 5
β’ (π β (π΅ / π΄) β β) |
31 | | divcnv 15739 |
. . . . 5
β’ ((π΅ / π΄) β β β (π β β β¦ ((π΅ / π΄) / π)) β 0) |
32 | 30, 31 | syl 17 |
. . . 4
β’ (π β (π β β β¦ ((π΅ / π΄) / π)) β 0) |
33 | 29, 32 | eqbrtrrd 5130 |
. . 3
β’ (π β (π β β β¦ (π΅ / (π΄ Β· π))) β 0) |
34 | | eqid 2737 |
. . . . . 6
β’ (π β β β¦ 1) =
(π β β β¦
1) |
35 | | 1cnd 11151 |
. . . . . 6
β’ (π β β β 1 β
β) |
36 | 34, 35 | fmpti 7061 |
. . . . 5
β’ (π β β β¦
1):ββΆβ |
37 | 36 | a1i 11 |
. . . 4
β’ (π β (π β β β¦
1):ββΆβ) |
38 | 37 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ 1)βπ) β
β) |
39 | 21, 23 | mulcld 11176 |
. . . . . 6
β’ ((π β§ π β β) β (π΄ Β· π) β β) |
40 | 21, 23, 25, 27 | mulne0d 11808 |
. . . . . 6
β’ ((π β§ π β β) β (π΄ Β· π) β 0) |
41 | 19, 39, 40 | divcld 11932 |
. . . . 5
β’ ((π β§ π β β) β (π΅ / (π΄ Β· π)) β β) |
42 | 41 | fmpttd 7064 |
. . . 4
β’ (π β (π β β β¦ (π΅ / (π΄ Β· π))):ββΆβ) |
43 | 42 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ (π΅ / (π΄ Β· π)))βπ) β β) |
44 | | oveq2 7366 |
. . . . . . 7
β’ (π = π β (π΄ Β· π) = (π΄ Β· π)) |
45 | 44 | oveq1d 7373 |
. . . . . 6
β’ (π = π β ((π΄ Β· π) + π΅) = ((π΄ Β· π) + π΅)) |
46 | 45, 44 | oveq12d 7376 |
. . . . 5
β’ (π = π β (((π΄ Β· π) + π΅) / (π΄ Β· π)) = (((π΄ Β· π) + π΅) / (π΄ Β· π))) |
47 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
48 | 20 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π΄ β β) |
49 | 47 | nncnd 12170 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
50 | 48, 49 | mulcld 11176 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄ Β· π) β β) |
51 | 18 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π΅ β β) |
52 | 50, 51 | addcld 11175 |
. . . . . 6
β’ ((π β§ π β β) β ((π΄ Β· π) + π΅) β β) |
53 | 24 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π΄ β 0) |
54 | 47 | nnne0d 12204 |
. . . . . . 7
β’ ((π β§ π β β) β π β 0) |
55 | 48, 49, 53, 54 | mulne0d 11808 |
. . . . . 6
β’ ((π β§ π β β) β (π΄ Β· π) β 0) |
56 | 52, 50, 55 | divcld 11932 |
. . . . 5
β’ ((π β§ π β β) β (((π΄ Β· π) + π΅) / (π΄ Β· π)) β β) |
57 | 14, 46, 47, 56 | fvmptd3 6972 |
. . . 4
β’ ((π β§ π β β) β (πΉβπ) = (((π΄ Β· π) + π΅) / (π΄ Β· π))) |
58 | 50, 51, 50, 55 | divdird 11970 |
. . . . 5
β’ ((π β§ π β β) β (((π΄ Β· π) + π΅) / (π΄ Β· π)) = (((π΄ Β· π) / (π΄ Β· π)) + (π΅ / (π΄ Β· π)))) |
59 | 50, 55 | dividd 11930 |
. . . . . 6
β’ ((π β§ π β β) β ((π΄ Β· π) / (π΄ Β· π)) = 1) |
60 | 59 | oveq1d 7373 |
. . . . 5
β’ ((π β§ π β β) β (((π΄ Β· π) / (π΄ Β· π)) + (π΅ / (π΄ Β· π))) = (1 + (π΅ / (π΄ Β· π)))) |
61 | 58, 60 | eqtrd 2777 |
. . . 4
β’ ((π β§ π β β) β (((π΄ Β· π) + π΅) / (π΄ Β· π)) = (1 + (π΅ / (π΄ Β· π)))) |
62 | 12 | eqcomd 2743 |
. . . . 5
β’ ((π β§ π β β) β 1 = ((π β β β¦
1)βπ)) |
63 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π β β) β (π β β β¦ (π΅ / (π΄ Β· π))) = (π β β β¦ (π΅ / (π΄ Β· π)))) |
64 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π = π) β π = π) |
65 | 64 | oveq2d 7374 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π = π) β (π΄ Β· π) = (π΄ Β· π)) |
66 | 65 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π β β) β§ π = π) β (π΅ / (π΄ Β· π)) = (π΅ / (π΄ Β· π))) |
67 | 51, 50, 55 | divcld 11932 |
. . . . . . 7
β’ ((π β§ π β β) β (π΅ / (π΄ Β· π)) β β) |
68 | 63, 66, 47, 67 | fvmptd 6956 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β β¦ (π΅ / (π΄ Β· π)))βπ) = (π΅ / (π΄ Β· π))) |
69 | 68 | eqcomd 2743 |
. . . . 5
β’ ((π β§ π β β) β (π΅ / (π΄ Β· π)) = ((π β β β¦ (π΅ / (π΄ Β· π)))βπ)) |
70 | 62, 69 | oveq12d 7376 |
. . . 4
β’ ((π β§ π β β) β (1 + (π΅ / (π΄ Β· π))) = (((π β β β¦ 1)βπ) + ((π β β β¦ (π΅ / (π΄ Β· π)))βπ))) |
71 | 57, 61, 70 | 3eqtrd 2781 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = (((π β β β¦ 1)βπ) + ((π β β β¦ (π΅ / (π΄ Β· π)))βπ))) |
72 | 1, 2, 13, 17, 33, 38, 43, 71 | climadd 15515 |
. 2
β’ (π β πΉ β (1 + 0)) |
73 | | 1p0e1 12278 |
. 2
β’ (1 + 0) =
1 |
74 | 72, 73 | breqtrdi 5147 |
1
β’ (π β πΉ β 1) |