Step | Hyp | Ref
| Expression |
1 | | rpvmasum.z |
. . 3
β’ π =
(β€/nβ€βπ) |
2 | | rpvmasum.l |
. . 3
β’ πΏ = (β€RHomβπ) |
3 | | rpvmasum.a |
. . 3
β’ (π β π β β) |
4 | | rpvmasum2.g |
. . 3
β’ πΊ = (DChrβπ) |
5 | | rpvmasum2.d |
. . 3
β’ π· = (BaseβπΊ) |
6 | | rpvmasum2.1 |
. . 3
β’ 1 =
(0gβπΊ) |
7 | | rpvmasum2.w |
. . . . . 6
β’ π = {π¦ β (π· β { 1 }) β£ Ξ£π β β ((π¦β(πΏβπ)) / π) = 0} |
8 | 7 | ssrab3 4045 |
. . . . 5
β’ π β (π· β { 1 }) |
9 | | dchrisum0.b |
. . . . 5
β’ (π β π β π) |
10 | 8, 9 | sselid 3947 |
. . . 4
β’ (π β π β (π· β { 1 })) |
11 | 10 | eldifad 3927 |
. . 3
β’ (π β π β π·) |
12 | | eldifsni 4755 |
. . . 4
β’ (π β (π· β { 1 }) β π β 1 ) |
13 | 10, 12 | syl 17 |
. . 3
β’ (π β π β 1 ) |
14 | | fveq2 6847 |
. . . 4
β’ (π = π₯ β (ββπ) = (ββπ₯)) |
15 | 14 | oveq2d 7378 |
. . 3
β’ (π = π₯ β (1 / (ββπ)) = (1 / (ββπ₯))) |
16 | | 1nn 12171 |
. . . 4
β’ 1 β
β |
17 | 16 | a1i 11 |
. . 3
β’ (π β 1 β
β) |
18 | | rpsqrtcl 15156 |
. . . . 5
β’ (π β β+
β (ββπ)
β β+) |
19 | 18 | adantl 483 |
. . . 4
β’ ((π β§ π β β+) β
(ββπ) β
β+) |
20 | 19 | rprecred 12975 |
. . 3
β’ ((π β§ π β β+) β (1 /
(ββπ)) β
β) |
21 | | simp3r 1203 |
. . . . 5
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β π β€ π₯) |
22 | | simp2l 1200 |
. . . . . . 7
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β π β β+) |
23 | 22 | rprege0d 12971 |
. . . . . 6
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (π β β β§ 0 β€ π)) |
24 | | simp2r 1201 |
. . . . . . 7
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β π₯ β β+) |
25 | 24 | rprege0d 12971 |
. . . . . 6
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (π₯ β β β§ 0 β€ π₯)) |
26 | | sqrtle 15152 |
. . . . . 6
β’ (((π β β β§ 0 β€
π) β§ (π₯ β β β§ 0 β€
π₯)) β (π β€ π₯ β (ββπ) β€ (ββπ₯))) |
27 | 23, 25, 26 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (π β€ π₯ β (ββπ) β€ (ββπ₯))) |
28 | 21, 27 | mpbid 231 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (ββπ) β€ (ββπ₯)) |
29 | 22 | rpsqrtcld 15303 |
. . . . 5
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (ββπ) β
β+) |
30 | 24 | rpsqrtcld 15303 |
. . . . 5
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (ββπ₯) β
β+) |
31 | 29, 30 | lerecd 12983 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β ((ββπ) β€ (ββπ₯) β (1 / (ββπ₯)) β€ (1 /
(ββπ)))) |
32 | 28, 31 | mpbid 231 |
. . 3
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (1 / (ββπ₯)) β€ (1 /
(ββπ))) |
33 | | sqrtlim 26338 |
. . . 4
β’ (π β β+
β¦ (1 / (ββπ))) βπ
0 |
34 | 33 | a1i 11 |
. . 3
β’ (π β (π β β+ β¦ (1 /
(ββπ)))
βπ 0) |
35 | | 2fveq3 6852 |
. . . . 5
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
36 | | fveq2 6847 |
. . . . . 6
β’ (π = π β (ββπ) = (ββπ)) |
37 | 36 | oveq2d 7378 |
. . . . 5
β’ (π = π β (1 / (ββπ)) = (1 / (ββπ))) |
38 | 35, 37 | oveq12d 7380 |
. . . 4
β’ (π = π β ((πβ(πΏβπ)) Β· (1 / (ββπ))) = ((πβ(πΏβπ)) Β· (1 / (ββπ)))) |
39 | 38 | cbvmptv 5223 |
. . 3
β’ (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ)))) = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ)))) |
40 | 1, 2, 3, 4, 5, 6, 11, 13, 15, 17, 20, 32, 34, 39 | dchrisum 26856 |
. 2
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / (ββπ₯))))) |
41 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β π·) |
42 | | nnz 12527 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
43 | 42 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β€) |
44 | 4, 1, 5, 2, 41, 43 | dchrzrhcl 26609 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
45 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
46 | 45 | nnrpd 12962 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β+) |
47 | 46 | rpsqrtcld 15303 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (ββπ) β
β+) |
48 | 47 | rpcnd 12966 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (ββπ) β
β) |
49 | 47 | rpne0d 12969 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (ββπ) β 0) |
50 | 44, 48, 49 | divrecd 11941 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πβ(πΏβπ)) / (ββπ)) = ((πβ(πΏβπ)) Β· (1 / (ββπ)))) |
51 | 50 | mpteq2dva 5210 |
. . . . . . . . 9
β’ (π β (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) |
52 | | dchrisum0lem1.f |
. . . . . . . . . 10
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
53 | 35, 36 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((πβ(πΏβπ)) / (ββπ)) = ((πβ(πΏβπ)) / (ββπ))) |
54 | 53 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
55 | 52, 54 | eqtri 2765 |
. . . . . . . . 9
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
56 | 51, 55, 39 | 3eqtr4g 2802 |
. . . . . . . 8
β’ (π β πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) |
57 | 56 | seqeq3d 13921 |
. . . . . . 7
β’ (π β seq1( + , πΉ) = seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ)))))) |
58 | 57 | breq1d 5120 |
. . . . . 6
β’ (π β (seq1( + , πΉ) β π‘ β seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) β π‘)) |
59 | 58 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0[,)+β)) β (seq1( + ,
πΉ) β π‘ β seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) β π‘)) |
60 | | 2fveq3 6852 |
. . . . . . . . 9
β’ (π¦ = π₯ β (seq1( + , πΉ)β(ββπ¦)) = (seq1( + , πΉ)β(ββπ₯))) |
61 | 60 | fvoveq1d 7384 |
. . . . . . . 8
β’ (π¦ = π₯ β (absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) = (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘))) |
62 | | fveq2 6847 |
. . . . . . . . 9
β’ (π¦ = π₯ β (ββπ¦) = (ββπ₯)) |
63 | 62 | oveq2d 7378 |
. . . . . . . 8
β’ (π¦ = π₯ β (π / (ββπ¦)) = (π / (ββπ₯))) |
64 | 61, 63 | breq12d 5123 |
. . . . . . 7
β’ (π¦ = π₯ β ((absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / (ββπ¦)) β (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π / (ββπ₯)))) |
65 | 64 | cbvralvw 3228 |
. . . . . 6
β’
(βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / (ββπ¦)) β βπ₯ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ₯)) β π‘)) β€ (π / (ββπ₯))) |
66 | 56 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) |
67 | 66 | seqeq3d 13921 |
. . . . . . . . . 10
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
seq1( + , πΉ) = seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / (ββπ)))))) |
68 | 67 | fveq1d 6849 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(seq1( + , πΉ)β(ββπ₯)) = (seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯))) |
69 | 68 | fvoveq1d 7384 |
. . . . . . . 8
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) = (absβ((seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯)) β π‘))) |
70 | | elrege0 13378 |
. . . . . . . . . . . 12
β’ (π β (0[,)+β) β
(π β β β§ 0
β€ π)) |
71 | 70 | simplbi 499 |
. . . . . . . . . . 11
β’ (π β (0[,)+β) β
π β
β) |
72 | 71 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π β
β) |
73 | 72 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π β
β) |
74 | | 1re 11162 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
75 | | elicopnf 13369 |
. . . . . . . . . . . . . . 15
β’ (1 β
β β (π₯ β
(1[,)+β) β (π₯
β β β§ 1 β€ π₯))) |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (π₯ β (1[,)+β) β
(π₯ β β β§ 1
β€ π₯)) |
77 | 76 | simplbi 499 |
. . . . . . . . . . . . 13
β’ (π₯ β (1[,)+β) β
π₯ β
β) |
78 | 77 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π₯ β
β) |
79 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
β β) |
80 | | 1red 11163 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 1
β β) |
81 | | 0lt1 11684 |
. . . . . . . . . . . . . 14
β’ 0 <
1 |
82 | 81 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
< 1) |
83 | 76 | simprbi 498 |
. . . . . . . . . . . . . 14
β’ (π₯ β (1[,)+β) β 1
β€ π₯) |
84 | 83 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 1
β€ π₯) |
85 | 79, 80, 78, 82, 84 | ltletrd 11322 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
< π₯) |
86 | 78, 85 | elrpd 12961 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π₯ β
β+) |
87 | 86 | rpsqrtcld 15303 |
. . . . . . . . . 10
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(ββπ₯) β
β+) |
88 | 87 | rpcnd 12966 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(ββπ₯) β
β) |
89 | 87 | rpne0d 12969 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(ββπ₯) β
0) |
90 | 73, 88, 89 | divrecd 11941 |
. . . . . . . 8
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(π / (ββπ₯)) = (π Β· (1 / (ββπ₯)))) |
91 | 69, 90 | breq12d 5123 |
. . . . . . 7
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
((absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π / (ββπ₯)) β (absβ((seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / (ββπ₯))))) |
92 | 91 | ralbidva 3173 |
. . . . . 6
β’ ((π β§ π β (0[,)+β)) β (βπ₯ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π / (ββπ₯)) β βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / (ββπ₯))))) |
93 | 65, 92 | bitrid 283 |
. . . . 5
β’ ((π β§ π β (0[,)+β)) β (βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / (ββπ¦)) β βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / (ββπ₯))))) |
94 | 59, 93 | anbi12d 632 |
. . . 4
β’ ((π β§ π β (0[,)+β)) β ((seq1( + ,
πΉ) β π‘ β§ βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / (ββπ¦))) β (seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / (ββπ₯)))))) |
95 | 94 | rexbidva 3174 |
. . 3
β’ (π β (βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π / (ββπ¦))) β βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / (ββπ₯)))))) |
96 | 95 | exbidv 1925 |
. 2
β’ (π β (βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π / (ββπ¦))) β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / (ββπ))))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / (ββπ)))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / (ββπ₯)))))) |
97 | 40, 96 | mpbird 257 |
1
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π / (ββπ¦)))) |