Step | Hyp | Ref
| Expression |
1 | | bfp.2 |
. . 3
β’ (π β π· β (CMetβπ)) |
2 | | cmetmet 24802 |
. . . . 5
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π· β (Metβπ)) |
4 | | nnuz 12864 |
. . . . 5
β’ β =
(β€β₯β1) |
5 | | bfp.10 |
. . . . 5
β’ πΊ = seq1((πΉ β 1st ), (β Γ
{π΄})) |
6 | | 1zzd 12592 |
. . . . 5
β’ (π β 1 β
β€) |
7 | | bfp.9 |
. . . . 5
β’ (π β π΄ β π) |
8 | | bfp.6 |
. . . . 5
β’ (π β πΉ:πβΆπ) |
9 | 4, 5, 6, 7, 8 | algrf 16509 |
. . . 4
β’ (π β πΊ:ββΆπ) |
10 | 8, 7 | ffvelcdmd 7087 |
. . . . . 6
β’ (π β (πΉβπ΄) β π) |
11 | | metcl 23837 |
. . . . . 6
β’ ((π· β (Metβπ) β§ π΄ β π β§ (πΉβπ΄) β π) β (π΄π·(πΉβπ΄)) β β) |
12 | 3, 7, 10, 11 | syl3anc 1371 |
. . . . 5
β’ (π β (π΄π·(πΉβπ΄)) β β) |
13 | | bfp.4 |
. . . . 5
β’ (π β πΎ β
β+) |
14 | 12, 13 | rerpdivcld 13046 |
. . . 4
β’ (π β ((π΄π·(πΉβπ΄)) / πΎ) β β) |
15 | | bfp.5 |
. . . 4
β’ (π β πΎ < 1) |
16 | | fveq2 6891 |
. . . . . . . . 9
β’ (π = 1 β (πΊβπ) = (πΊβ1)) |
17 | | fvoveq1 7431 |
. . . . . . . . 9
β’ (π = 1 β (πΊβ(π + 1)) = (πΊβ(1 + 1))) |
18 | 16, 17 | oveq12d 7426 |
. . . . . . . 8
β’ (π = 1 β ((πΊβπ)π·(πΊβ(π + 1))) = ((πΊβ1)π·(πΊβ(1 + 1)))) |
19 | | oveq2 7416 |
. . . . . . . . 9
β’ (π = 1 β (πΎβπ) = (πΎβ1)) |
20 | 19 | oveq2d 7424 |
. . . . . . . 8
β’ (π = 1 β (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) = (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ1))) |
21 | 18, 20 | breq12d 5161 |
. . . . . . 7
β’ (π = 1 β (((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β ((πΊβ1)π·(πΊβ(1 + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ1)))) |
22 | 21 | imbi2d 340 |
. . . . . 6
β’ (π = 1 β ((π β ((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ))) β (π β ((πΊβ1)π·(πΊβ(1 + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ1))))) |
23 | | fveq2 6891 |
. . . . . . . . 9
β’ (π = π β (πΊβπ) = (πΊβπ)) |
24 | | fvoveq1 7431 |
. . . . . . . . 9
β’ (π = π β (πΊβ(π + 1)) = (πΊβ(π + 1))) |
25 | 23, 24 | oveq12d 7426 |
. . . . . . . 8
β’ (π = π β ((πΊβπ)π·(πΊβ(π + 1))) = ((πΊβπ)π·(πΊβ(π + 1)))) |
26 | | oveq2 7416 |
. . . . . . . . 9
β’ (π = π β (πΎβπ) = (πΎβπ)) |
27 | 26 | oveq2d 7424 |
. . . . . . . 8
β’ (π = π β (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) = (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ))) |
28 | 25, 27 | breq12d 5161 |
. . . . . . 7
β’ (π = π β (((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β ((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)))) |
29 | 28 | imbi2d 340 |
. . . . . 6
β’ (π = π β ((π β ((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ))) β (π β ((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ))))) |
30 | | fveq2 6891 |
. . . . . . . . 9
β’ (π = (π + 1) β (πΊβπ) = (πΊβ(π + 1))) |
31 | | fvoveq1 7431 |
. . . . . . . . 9
β’ (π = (π + 1) β (πΊβ(π + 1)) = (πΊβ((π + 1) + 1))) |
32 | 30, 31 | oveq12d 7426 |
. . . . . . . 8
β’ (π = (π + 1) β ((πΊβπ)π·(πΊβ(π + 1))) = ((πΊβ(π + 1))π·(πΊβ((π + 1) + 1)))) |
33 | | oveq2 7416 |
. . . . . . . . 9
β’ (π = (π + 1) β (πΎβπ) = (πΎβ(π + 1))) |
34 | 33 | oveq2d 7424 |
. . . . . . . 8
β’ (π = (π + 1) β (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) = (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1)))) |
35 | 32, 34 | breq12d 5161 |
. . . . . . 7
β’ (π = (π + 1) β (((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β ((πΊβ(π + 1))π·(πΊβ((π + 1) + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))))) |
36 | 35 | imbi2d 340 |
. . . . . 6
β’ (π = (π + 1) β ((π β ((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ))) β (π β ((πΊβ(π + 1))π·(πΊβ((π + 1) + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1)))))) |
37 | 12 | leidd 11779 |
. . . . . . 7
β’ (π β (π΄π·(πΉβπ΄)) β€ (π΄π·(πΉβπ΄))) |
38 | 4, 5, 6, 7 | algr0 16508 |
. . . . . . . 8
β’ (π β (πΊβ1) = π΄) |
39 | | 1nn 12222 |
. . . . . . . . . 10
β’ 1 β
β |
40 | 4, 5, 6, 7, 8 | algrp1 16510 |
. . . . . . . . . 10
β’ ((π β§ 1 β β) β
(πΊβ(1 + 1)) = (πΉβ(πΊβ1))) |
41 | 39, 40 | mpan2 689 |
. . . . . . . . 9
β’ (π β (πΊβ(1 + 1)) = (πΉβ(πΊβ1))) |
42 | 38 | fveq2d 6895 |
. . . . . . . . 9
β’ (π β (πΉβ(πΊβ1)) = (πΉβπ΄)) |
43 | 41, 42 | eqtrd 2772 |
. . . . . . . 8
β’ (π β (πΊβ(1 + 1)) = (πΉβπ΄)) |
44 | 38, 43 | oveq12d 7426 |
. . . . . . 7
β’ (π β ((πΊβ1)π·(πΊβ(1 + 1))) = (π΄π·(πΉβπ΄))) |
45 | 13 | rpred 13015 |
. . . . . . . . . . 11
β’ (π β πΎ β β) |
46 | 45 | recnd 11241 |
. . . . . . . . . 10
β’ (π β πΎ β β) |
47 | 46 | exp1d 14105 |
. . . . . . . . 9
β’ (π β (πΎβ1) = πΎ) |
48 | 47 | oveq2d 7424 |
. . . . . . . 8
β’ (π β (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ1)) = (((π΄π·(πΉβπ΄)) / πΎ) Β· πΎ)) |
49 | 12 | recnd 11241 |
. . . . . . . . 9
β’ (π β (π΄π·(πΉβπ΄)) β β) |
50 | 13 | rpne0d 13020 |
. . . . . . . . 9
β’ (π β πΎ β 0) |
51 | 49, 46, 50 | divcan1d 11990 |
. . . . . . . 8
β’ (π β (((π΄π·(πΉβπ΄)) / πΎ) Β· πΎ) = (π΄π·(πΉβπ΄))) |
52 | 48, 51 | eqtrd 2772 |
. . . . . . 7
β’ (π β (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ1)) = (π΄π·(πΉβπ΄))) |
53 | 37, 44, 52 | 3brtr4d 5180 |
. . . . . 6
β’ (π β ((πΊβ1)π·(πΊβ(1 + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ1))) |
54 | 9 | ffvelcdmda 7086 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΊβπ) β π) |
55 | | peano2nn 12223 |
. . . . . . . . . . . . 13
β’ (π β β β (π + 1) β
β) |
56 | | ffvelcdm 7083 |
. . . . . . . . . . . . 13
β’ ((πΊ:ββΆπ β§ (π + 1) β β) β (πΊβ(π + 1)) β π) |
57 | 9, 55, 56 | syl2an 596 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΊβ(π + 1)) β π) |
58 | 54, 57 | jca 512 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πΊβπ) β π β§ (πΊβ(π + 1)) β π)) |
59 | | bfp.7 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((πΉβπ₯)π·(πΉβπ¦)) β€ (πΎ Β· (π₯π·π¦))) |
60 | 59 | ralrimivva 3200 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π βπ¦ β π ((πΉβπ₯)π·(πΉβπ¦)) β€ (πΎ Β· (π₯π·π¦))) |
61 | 60 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β βπ₯ β π βπ¦ β π ((πΉβπ₯)π·(πΉβπ¦)) β€ (πΎ Β· (π₯π·π¦))) |
62 | | fveq2 6891 |
. . . . . . . . . . . . . 14
β’ (π₯ = (πΊβπ) β (πΉβπ₯) = (πΉβ(πΊβπ))) |
63 | 62 | oveq1d 7423 |
. . . . . . . . . . . . 13
β’ (π₯ = (πΊβπ) β ((πΉβπ₯)π·(πΉβπ¦)) = ((πΉβ(πΊβπ))π·(πΉβπ¦))) |
64 | | oveq1 7415 |
. . . . . . . . . . . . . 14
β’ (π₯ = (πΊβπ) β (π₯π·π¦) = ((πΊβπ)π·π¦)) |
65 | 64 | oveq2d 7424 |
. . . . . . . . . . . . 13
β’ (π₯ = (πΊβπ) β (πΎ Β· (π₯π·π¦)) = (πΎ Β· ((πΊβπ)π·π¦))) |
66 | 63, 65 | breq12d 5161 |
. . . . . . . . . . . 12
β’ (π₯ = (πΊβπ) β (((πΉβπ₯)π·(πΉβπ¦)) β€ (πΎ Β· (π₯π·π¦)) β ((πΉβ(πΊβπ))π·(πΉβπ¦)) β€ (πΎ Β· ((πΊβπ)π·π¦)))) |
67 | | fveq2 6891 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πΊβ(π + 1)) β (πΉβπ¦) = (πΉβ(πΊβ(π + 1)))) |
68 | 67 | oveq2d 7424 |
. . . . . . . . . . . . 13
β’ (π¦ = (πΊβ(π + 1)) β ((πΉβ(πΊβπ))π·(πΉβπ¦)) = ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1))))) |
69 | | oveq2 7416 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πΊβ(π + 1)) β ((πΊβπ)π·π¦) = ((πΊβπ)π·(πΊβ(π + 1)))) |
70 | 69 | oveq2d 7424 |
. . . . . . . . . . . . 13
β’ (π¦ = (πΊβ(π + 1)) β (πΎ Β· ((πΊβπ)π·π¦)) = (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1))))) |
71 | 68, 70 | breq12d 5161 |
. . . . . . . . . . . 12
β’ (π¦ = (πΊβ(π + 1)) β (((πΉβ(πΊβπ))π·(πΉβπ¦)) β€ (πΎ Β· ((πΊβπ)π·π¦)) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))))) |
72 | 66, 71 | rspc2v 3622 |
. . . . . . . . . . 11
β’ (((πΊβπ) β π β§ (πΊβ(π + 1)) β π) β (βπ₯ β π βπ¦ β π ((πΉβπ₯)π·(πΉβπ¦)) β€ (πΎ Β· (π₯π·π¦)) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))))) |
73 | 58, 61, 72 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1))))) |
74 | 3 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π· β (Metβπ)) |
75 | 8 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β πΉ:πβΆπ) |
76 | 75, 54 | ffvelcdmd 7087 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΉβ(πΊβπ)) β π) |
77 | 75, 57 | ffvelcdmd 7087 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΉβ(πΊβ(π + 1))) β π) |
78 | | metcl 23837 |
. . . . . . . . . . . 12
β’ ((π· β (Metβπ) β§ (πΉβ(πΊβπ)) β π β§ (πΉβ(πΊβ(π + 1))) β π) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β β) |
79 | 74, 76, 77, 78 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β β) |
80 | 45 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β πΎ β β) |
81 | | metcl 23837 |
. . . . . . . . . . . . 13
β’ ((π· β (Metβπ) β§ (πΊβπ) β π β§ (πΊβ(π + 1)) β π) β ((πΊβπ)π·(πΊβ(π + 1))) β β) |
82 | 74, 54, 57, 81 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πΊβπ)π·(πΊβ(π + 1))) β β) |
83 | 80, 82 | remulcld 11243 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β β) |
84 | 14 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π΄π·(πΉβπ΄)) / πΎ) β β) |
85 | 55 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π + 1) β β) |
86 | 85 | nnnn0d 12531 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π + 1) β
β0) |
87 | 80, 86 | reexpcld 14127 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΎβ(π + 1)) β β) |
88 | 84, 87 | remulcld 11243 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))) β β) |
89 | | letr 11307 |
. . . . . . . . . . 11
β’ ((((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β β β§ (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β β β§ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))) β β) β ((((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β§ (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1)))) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))))) |
90 | 79, 83, 88, 89 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β§ (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1)))) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))))) |
91 | 73, 90 | mpand 693 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))))) |
92 | | nnnn0 12478 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β0) |
93 | | reexpcl 14043 |
. . . . . . . . . . . . 13
β’ ((πΎ β β β§ π β β0)
β (πΎβπ) β
β) |
94 | 45, 92, 93 | syl2an 596 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΎβπ) β β) |
95 | 84, 94 | remulcld 11243 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β β) |
96 | 13 | rpgt0d 13018 |
. . . . . . . . . . . 12
β’ (π β 0 < πΎ) |
97 | 96 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 0 < πΎ) |
98 | | lemul1 12065 |
. . . . . . . . . . 11
β’ ((((πΊβπ)π·(πΊβ(π + 1))) β β β§ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β β β§ (πΎ β β β§ 0 < πΎ)) β (((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β (((πΊβπ)π·(πΊβ(π + 1))) Β· πΎ) β€ ((((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) Β· πΎ))) |
99 | 82, 95, 80, 97, 98 | syl112anc 1374 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β (((πΊβπ)π·(πΊβ(π + 1))) Β· πΎ) β€ ((((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) Β· πΎ))) |
100 | 82 | recnd 11241 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πΊβπ)π·(πΊβ(π + 1))) β β) |
101 | 46 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β πΎ β β) |
102 | 100, 101 | mulcomd 11234 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((πΊβπ)π·(πΊβ(π + 1))) Β· πΎ) = (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1))))) |
103 | 84 | recnd 11241 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((π΄π·(πΉβπ΄)) / πΎ) β β) |
104 | 94 | recnd 11241 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΎβπ) β β) |
105 | 103, 104,
101 | mulassd 11236 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) Β· πΎ) = (((π΄π·(πΉβπ΄)) / πΎ) Β· ((πΎβπ) Β· πΎ))) |
106 | | expp1 14033 |
. . . . . . . . . . . . . 14
β’ ((πΎ β β β§ π β β0)
β (πΎβ(π + 1)) = ((πΎβπ) Β· πΎ)) |
107 | 46, 92, 106 | syl2an 596 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΎβ(π + 1)) = ((πΎβπ) Β· πΎ)) |
108 | 107 | oveq2d 7424 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))) = (((π΄π·(πΉβπ΄)) / πΎ) Β· ((πΎβπ) Β· πΎ))) |
109 | 105, 108 | eqtr4d 2775 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) Β· πΎ) = (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1)))) |
110 | 102, 109 | breq12d 5161 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((((πΊβπ)π·(πΊβ(π + 1))) Β· πΎ) β€ ((((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) Β· πΎ) β (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))))) |
111 | 99, 110 | bitrd 278 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β (πΎ Β· ((πΊβπ)π·(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))))) |
112 | 4, 5, 6, 7, 8 | algrp1 16510 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΊβ(π + 1)) = (πΉβ(πΊβπ))) |
113 | 4, 5, 6, 7, 8 | algrp1 16510 |
. . . . . . . . . . . 12
β’ ((π β§ (π + 1) β β) β (πΊβ((π + 1) + 1)) = (πΉβ(πΊβ(π + 1)))) |
114 | 55, 113 | sylan2 593 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΊβ((π + 1) + 1)) = (πΉβ(πΊβ(π + 1)))) |
115 | 112, 114 | oveq12d 7426 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πΊβ(π + 1))π·(πΊβ((π + 1) + 1))) = ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1))))) |
116 | 115 | breq1d 5158 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((πΊβ(π + 1))π·(πΊβ((π + 1) + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))) β ((πΉβ(πΊβπ))π·(πΉβ(πΊβ(π + 1)))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))))) |
117 | 91, 111, 116 | 3imtr4d 293 |
. . . . . . . 8
β’ ((π β§ π β β) β (((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β ((πΊβ(π + 1))π·(πΊβ((π + 1) + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1))))) |
118 | 117 | expcom 414 |
. . . . . . 7
β’ (π β β β (π β (((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)) β ((πΊβ(π + 1))π·(πΊβ((π + 1) + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1)))))) |
119 | 118 | a2d 29 |
. . . . . 6
β’ (π β β β ((π β ((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ))) β (π β ((πΊβ(π + 1))π·(πΊβ((π + 1) + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβ(π + 1)))))) |
120 | 22, 29, 36, 29, 53, 119 | nnind 12229 |
. . . . 5
β’ (π β β β (π β ((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ)))) |
121 | 120 | impcom 408 |
. . . 4
β’ ((π β§ π β β) β ((πΊβπ)π·(πΊβ(π + 1))) β€ (((π΄π·(πΉβπ΄)) / πΎ) Β· (πΎβπ))) |
122 | 3, 9, 14, 13, 15, 121 | geomcau 36622 |
. . 3
β’ (π β πΊ β (Cauβπ·)) |
123 | | bfp.8 |
. . . 4
β’ π½ = (MetOpenβπ·) |
124 | 123 | cmetcau 24805 |
. . 3
β’ ((π· β (CMetβπ) β§ πΊ β (Cauβπ·)) β πΊ β dom
(βπ‘βπ½)) |
125 | 1, 122, 124 | syl2anc 584 |
. 2
β’ (π β πΊ β dom
(βπ‘βπ½)) |
126 | | metxmet 23839 |
. . . 4
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
127 | 123 | methaus 24028 |
. . . 4
β’ (π· β (βMetβπ) β π½ β Haus) |
128 | 3, 126, 127 | 3syl 18 |
. . 3
β’ (π β π½ β Haus) |
129 | | lmfun 22884 |
. . 3
β’ (π½ β Haus β Fun
(βπ‘βπ½)) |
130 | | funfvbrb 7052 |
. . 3
β’ (Fun
(βπ‘βπ½) β (πΊ β dom
(βπ‘βπ½) β πΊ(βπ‘βπ½)((βπ‘βπ½)βπΊ))) |
131 | 128, 129,
130 | 3syl 18 |
. 2
β’ (π β (πΊ β dom
(βπ‘βπ½) β πΊ(βπ‘βπ½)((βπ‘βπ½)βπΊ))) |
132 | 125, 131 | mpbid 231 |
1
β’ (π β πΊ(βπ‘βπ½)((βπ‘βπ½)βπΊ)) |