Step | Hyp | Ref
| Expression |
1 | | dchrisum.4 |
. . . 4
β’ ((π β§ π β β+) β π΄ β
β) |
2 | 1 | ralrimiva 3144 |
. . 3
β’ (π β βπ β β+ π΄ β β) |
3 | | nfcsb1v 3885 |
. . . . 5
β’
β²πβ¦πΌ / πβ¦π΄ |
4 | 3 | nfel1 2924 |
. . . 4
β’
β²πβ¦πΌ / πβ¦π΄ β β |
5 | | csbeq1a 3874 |
. . . . 5
β’ (π = πΌ β π΄ = β¦πΌ / πβ¦π΄) |
6 | 5 | eleq1d 2823 |
. . . 4
β’ (π = πΌ β (π΄ β β β β¦πΌ / πβ¦π΄ β β)) |
7 | 4, 6 | rspc 3572 |
. . 3
β’ (πΌ β β+
β (βπ β
β+ π΄
β β β β¦πΌ / πβ¦π΄ β β)) |
8 | 2, 7 | syl5com 31 |
. 2
β’ (π β (πΌ β β+ β
β¦πΌ / πβ¦π΄ β β)) |
9 | | eqid 2737 |
. . . 4
β’
(β€β₯β((ββπΌ) + 1)) =
(β€β₯β((ββπΌ) + 1)) |
10 | | dchrisum.3 |
. . . . . . . . 9
β’ (π β π β β) |
11 | 10 | nnred 12175 |
. . . . . . . 8
β’ (π β π β β) |
12 | | elicopnf 13369 |
. . . . . . . 8
β’ (π β β β (πΌ β (π[,)+β) β (πΌ β β β§ π β€ πΌ))) |
13 | 11, 12 | syl 17 |
. . . . . . 7
β’ (π β (πΌ β (π[,)+β) β (πΌ β β β§ π β€ πΌ))) |
14 | 13 | simprbda 500 |
. . . . . 6
β’ ((π β§ πΌ β (π[,)+β)) β πΌ β β) |
15 | 14 | flcld 13710 |
. . . . 5
β’ ((π β§ πΌ β (π[,)+β)) β (ββπΌ) β
β€) |
16 | 15 | peano2zd 12617 |
. . . 4
β’ ((π β§ πΌ β (π[,)+β)) β ((ββπΌ) + 1) β
β€) |
17 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
18 | | 1zzd 12541 |
. . . . . 6
β’ (π β 1 β
β€) |
19 | | dchrisum.6 |
. . . . . 6
β’ (π β (π β β+ β¦ π΄) βπ
0) |
20 | | nnrp 12933 |
. . . . . . . 8
β’ (π β β β π β
β+) |
21 | 20 | ssriv 3953 |
. . . . . . 7
β’ β
β β+ |
22 | | eqid 2737 |
. . . . . . . 8
β’ (π β β+
β¦ π΄) = (π β β+
β¦ π΄) |
23 | 22, 1 | dmmptd 6651 |
. . . . . . 7
β’ (π β dom (π β β+ β¦ π΄) =
β+) |
24 | 21, 23 | sseqtrrid 4002 |
. . . . . 6
β’ (π β β β dom (π β β+
β¦ π΄)) |
25 | 17, 18, 19, 24 | rlimclim1 15434 |
. . . . 5
β’ (π β (π β β+ β¦ π΄) β 0) |
26 | 25 | adantr 482 |
. . . 4
β’ ((π β§ πΌ β (π[,)+β)) β (π β β+ β¦ π΄) β 0) |
27 | | 0red 11165 |
. . . . . . . . 9
β’ ((π β§ πΌ β (π[,)+β)) β 0 β
β) |
28 | 11 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΌ β (π[,)+β)) β π β β) |
29 | 10 | nngt0d 12209 |
. . . . . . . . . 10
β’ (π β 0 < π) |
30 | 29 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΌ β (π[,)+β)) β 0 < π) |
31 | 13 | simplbda 501 |
. . . . . . . . 9
β’ ((π β§ πΌ β (π[,)+β)) β π β€ πΌ) |
32 | 27, 28, 14, 30, 31 | ltletrd 11322 |
. . . . . . . 8
β’ ((π β§ πΌ β (π[,)+β)) β 0 < πΌ) |
33 | 14, 32 | elrpd 12961 |
. . . . . . 7
β’ ((π β§ πΌ β (π[,)+β)) β πΌ β
β+) |
34 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΌ β (π[,)+β)) β βπ β β+
π΄ β
β) |
35 | 33, 34, 7 | sylc 65 |
. . . . . 6
β’ ((π β§ πΌ β (π[,)+β)) β β¦πΌ / πβ¦π΄ β β) |
36 | 35 | recnd 11190 |
. . . . 5
β’ ((π β§ πΌ β (π[,)+β)) β β¦πΌ / πβ¦π΄ β β) |
37 | | ssid 3971 |
. . . . . 6
β’
(β€β₯β((ββπΌ) + 1)) β
(β€β₯β((ββπΌ) + 1)) |
38 | | fvex 6860 |
. . . . . 6
β’
(β€β₯β((ββπΌ) + 1)) β V |
39 | 37, 38 | climconst2 15437 |
. . . . 5
β’
((β¦πΌ /
πβ¦π΄ β β β§
((ββπΌ) + 1)
β β€) β ((β€β₯β((ββπΌ) + 1)) Γ
{β¦πΌ / πβ¦π΄}) β β¦πΌ / πβ¦π΄) |
40 | 36, 16, 39 | syl2anc 585 |
. . . 4
β’ ((π β§ πΌ β (π[,)+β)) β
((β€β₯β((ββπΌ) + 1)) Γ {β¦πΌ / πβ¦π΄}) β β¦πΌ / πβ¦π΄) |
41 | 33 | rpge0d 12968 |
. . . . . . . . . 10
β’ ((π β§ πΌ β (π[,)+β)) β 0 β€ πΌ) |
42 | | flge0nn0 13732 |
. . . . . . . . . 10
β’ ((πΌ β β β§ 0 β€
πΌ) β
(ββπΌ) β
β0) |
43 | 14, 41, 42 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ πΌ β (π[,)+β)) β (ββπΌ) β
β0) |
44 | | nn0p1nn 12459 |
. . . . . . . . 9
β’
((ββπΌ)
β β0 β ((ββπΌ) + 1) β β) |
45 | 43, 44 | syl 17 |
. . . . . . . 8
β’ ((π β§ πΌ β (π[,)+β)) β ((ββπΌ) + 1) β
β) |
46 | | eluznn 12850 |
. . . . . . . 8
β’
((((ββπΌ)
+ 1) β β β§ π
β (β€β₯β((ββπΌ) + 1))) β π β β) |
47 | 45, 46 | sylan 581 |
. . . . . . 7
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β π β β) |
48 | 47 | nnrpd 12962 |
. . . . . 6
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β π β β+) |
49 | 2 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β βπ β β+ π΄ β β) |
50 | | nfcsb1v 3885 |
. . . . . . . . 9
β’
β²πβ¦π / πβ¦π΄ |
51 | 50 | nfel1 2924 |
. . . . . . . 8
β’
β²πβ¦π / πβ¦π΄ β β |
52 | | csbeq1a 3874 |
. . . . . . . . 9
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
53 | 52 | eleq1d 2823 |
. . . . . . . 8
β’ (π = π β (π΄ β β β β¦π / πβ¦π΄ β β)) |
54 | 51, 53 | rspc 3572 |
. . . . . . 7
β’ (π β β+
β (βπ β
β+ π΄
β β β β¦π / πβ¦π΄ β β)) |
55 | 48, 49, 54 | sylc 65 |
. . . . . 6
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β β¦π / πβ¦π΄ β β) |
56 | 22 | fvmpts 6956 |
. . . . . 6
β’ ((π β β+
β§ β¦π /
πβ¦π΄ β β) β ((π β β+
β¦ π΄)βπ) = β¦π / πβ¦π΄) |
57 | 48, 55, 56 | syl2anc 585 |
. . . . 5
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β ((π β β+ β¦ π΄)βπ) = β¦π / πβ¦π΄) |
58 | 57, 55 | eqeltrd 2838 |
. . . 4
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β ((π β β+ β¦ π΄)βπ) β β) |
59 | | fvconst2g 7156 |
. . . . . 6
β’
((β¦πΌ /
πβ¦π΄ β β β§ π β
(β€β₯β((ββπΌ) + 1))) β
(((β€β₯β((ββπΌ) + 1)) Γ {β¦πΌ / πβ¦π΄})βπ) = β¦πΌ / πβ¦π΄) |
60 | 35, 59 | sylan 581 |
. . . . 5
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β
(((β€β₯β((ββπΌ) + 1)) Γ {β¦πΌ / πβ¦π΄})βπ) = β¦πΌ / πβ¦π΄) |
61 | 35 | adantr 482 |
. . . . 5
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β β¦πΌ / πβ¦π΄ β β) |
62 | 60, 61 | eqeltrd 2838 |
. . . 4
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β
(((β€β₯β((ββπΌ) + 1)) Γ {β¦πΌ / πβ¦π΄})βπ) β β) |
63 | 33 | adantr 482 |
. . . . . . 7
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β πΌ β
β+) |
64 | | dchrisum.5 |
. . . . . . . . . 10
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
65 | 64 | 3expia 1122 |
. . . . . . . . 9
β’ ((π β§ (π β β+ β§ π₯ β β+))
β ((π β€ π β§ π β€ π₯) β π΅ β€ π΄)) |
66 | 65 | ralrimivva 3198 |
. . . . . . . 8
β’ (π β βπ β β+ βπ₯ β β+
((π β€ π β§ π β€ π₯) β π΅ β€ π΄)) |
67 | 66 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β βπ β β+ βπ₯ β β+
((π β€ π β§ π β€ π₯) β π΅ β€ π΄)) |
68 | | nfcv 2908 |
. . . . . . . . 9
β’
β²πβ+ |
69 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π β€ πΌ β§ πΌ β€ π₯) |
70 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²ππ΅ |
71 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π
β€ |
72 | 70, 71, 3 | nfbr 5157 |
. . . . . . . . . 10
β’
β²π π΅ β€ β¦πΌ / πβ¦π΄ |
73 | 69, 72 | nfim 1900 |
. . . . . . . . 9
β’
β²π((π β€ πΌ β§ πΌ β€ π₯) β π΅ β€ β¦πΌ / πβ¦π΄) |
74 | 68, 73 | nfralw 3297 |
. . . . . . . 8
β’
β²πβπ₯ β β+ ((π β€ πΌ β§ πΌ β€ π₯) β π΅ β€ β¦πΌ / πβ¦π΄) |
75 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π = πΌ β (π β€ π β π β€ πΌ)) |
76 | | breq1 5113 |
. . . . . . . . . . 11
β’ (π = πΌ β (π β€ π₯ β πΌ β€ π₯)) |
77 | 75, 76 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = πΌ β ((π β€ π β§ π β€ π₯) β (π β€ πΌ β§ πΌ β€ π₯))) |
78 | 5 | breq2d 5122 |
. . . . . . . . . 10
β’ (π = πΌ β (π΅ β€ π΄ β π΅ β€ β¦πΌ / πβ¦π΄)) |
79 | 77, 78 | imbi12d 345 |
. . . . . . . . 9
β’ (π = πΌ β (((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β ((π β€ πΌ β§ πΌ β€ π₯) β π΅ β€ β¦πΌ / πβ¦π΄))) |
80 | 79 | ralbidv 3175 |
. . . . . . . 8
β’ (π = πΌ β (βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β βπ₯ β β+ ((π β€ πΌ β§ πΌ β€ π₯) β π΅ β€ β¦πΌ / πβ¦π΄))) |
81 | 74, 80 | rspc 3572 |
. . . . . . 7
β’ (πΌ β β+
β (βπ β
β+ βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β βπ₯ β β+ ((π β€ πΌ β§ πΌ β€ π₯) β π΅ β€ β¦πΌ / πβ¦π΄))) |
82 | 63, 67, 81 | sylc 65 |
. . . . . 6
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β βπ₯ β β+ ((π β€ πΌ β§ πΌ β€ π₯) β π΅ β€ β¦πΌ / πβ¦π΄)) |
83 | 31 | adantr 482 |
. . . . . . 7
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β π β€ πΌ) |
84 | 14 | adantr 482 |
. . . . . . . 8
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β πΌ β β) |
85 | | reflcl 13708 |
. . . . . . . . 9
β’ (πΌ β β β
(ββπΌ) β
β) |
86 | | peano2re 11335 |
. . . . . . . . 9
β’
((ββπΌ)
β β β ((ββπΌ) + 1) β β) |
87 | 84, 85, 86 | 3syl 18 |
. . . . . . . 8
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β ((ββπΌ) + 1) β
β) |
88 | 47 | nnred 12175 |
. . . . . . . 8
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β π β β) |
89 | | fllep1 13713 |
. . . . . . . . . 10
β’ (πΌ β β β πΌ β€ ((ββπΌ) + 1)) |
90 | 14, 89 | syl 17 |
. . . . . . . . 9
β’ ((π β§ πΌ β (π[,)+β)) β πΌ β€ ((ββπΌ) + 1)) |
91 | 90 | adantr 482 |
. . . . . . . 8
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β πΌ β€ ((ββπΌ) + 1)) |
92 | | eluzle 12783 |
. . . . . . . . 9
β’ (π β
(β€β₯β((ββπΌ) + 1)) β ((ββπΌ) + 1) β€ π) |
93 | 92 | adantl 483 |
. . . . . . . 8
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β ((ββπΌ) + 1) β€ π) |
94 | 84, 87, 88, 91, 93 | letrd 11319 |
. . . . . . 7
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β πΌ β€ π) |
95 | 83, 94 | jca 513 |
. . . . . 6
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β (π β€ πΌ β§ πΌ β€ π)) |
96 | | breq2 5114 |
. . . . . . . . 9
β’ (π₯ = π β (πΌ β€ π₯ β πΌ β€ π)) |
97 | 96 | anbi2d 630 |
. . . . . . . 8
β’ (π₯ = π β ((π β€ πΌ β§ πΌ β€ π₯) β (π β€ πΌ β§ πΌ β€ π))) |
98 | | eqvisset 3465 |
. . . . . . . . . . 11
β’ (π₯ = π β π β V) |
99 | | equtr2 2031 |
. . . . . . . . . . . 12
β’ ((π₯ = π β§ π = π) β π₯ = π) |
100 | | dchrisum.2 |
. . . . . . . . . . . . 13
β’ (π = π₯ β π΄ = π΅) |
101 | 100 | equcoms 2024 |
. . . . . . . . . . . 12
β’ (π₯ = π β π΄ = π΅) |
102 | 99, 101 | syl 17 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ π = π) β π΄ = π΅) |
103 | 98, 102 | csbied 3898 |
. . . . . . . . . 10
β’ (π₯ = π β β¦π / πβ¦π΄ = π΅) |
104 | 103 | eqcomd 2743 |
. . . . . . . . 9
β’ (π₯ = π β π΅ = β¦π / πβ¦π΄) |
105 | 104 | breq1d 5120 |
. . . . . . . 8
β’ (π₯ = π β (π΅ β€ β¦πΌ / πβ¦π΄ β β¦π / πβ¦π΄ β€ β¦πΌ / πβ¦π΄)) |
106 | 97, 105 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π β (((π β€ πΌ β§ πΌ β€ π₯) β π΅ β€ β¦πΌ / πβ¦π΄) β ((π β€ πΌ β§ πΌ β€ π) β β¦π / πβ¦π΄ β€ β¦πΌ / πβ¦π΄))) |
107 | 106 | rspcv 3580 |
. . . . . 6
β’ (π β β+
β (βπ₯ β
β+ ((π
β€ πΌ β§ πΌ β€ π₯) β π΅ β€ β¦πΌ / πβ¦π΄) β ((π β€ πΌ β§ πΌ β€ π) β β¦π / πβ¦π΄ β€ β¦πΌ / πβ¦π΄))) |
108 | 48, 82, 95, 107 | syl3c 66 |
. . . . 5
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β β¦π / πβ¦π΄ β€ β¦πΌ / πβ¦π΄) |
109 | 108, 57, 60 | 3brtr4d 5142 |
. . . 4
β’ (((π β§ πΌ β (π[,)+β)) β§ π β
(β€β₯β((ββπΌ) + 1))) β ((π β β+ β¦ π΄)βπ) β€
(((β€β₯β((ββπΌ) + 1)) Γ {β¦πΌ / πβ¦π΄})βπ)) |
110 | 9, 16, 26, 40, 58, 62, 109 | climle 15529 |
. . 3
β’ ((π β§ πΌ β (π[,)+β)) β 0 β€
β¦πΌ / πβ¦π΄) |
111 | 110 | ex 414 |
. 2
β’ (π β (πΌ β (π[,)+β) β 0 β€
β¦πΌ / πβ¦π΄)) |
112 | 8, 111 | jca 513 |
1
β’ (π β ((πΌ β β+ β
β¦πΌ / πβ¦π΄ β β) β§ (πΌ β (π[,)+β) β 0 β€
β¦πΌ / πβ¦π΄))) |