MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  geomulcvg Structured version   Visualization version   GIF version

Theorem geomulcvg 15822
Description: The geometric series converges even if it is multiplied by ๐‘˜ to result in the larger series ๐‘˜ ยท ๐ดโ†‘๐‘˜. (Contributed by Mario Carneiro, 27-Mar-2015.)
Hypothesis
Ref Expression
geomulcvg.1 ๐น = (๐‘˜ โˆˆ โ„•0 โ†ฆ (๐‘˜ ยท (๐ดโ†‘๐‘˜)))
Assertion
Ref Expression
geomulcvg ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
Distinct variable group:   ๐ด,๐‘˜
Allowed substitution hint:   ๐น(๐‘˜)

Proof of Theorem geomulcvg
Dummy variables ๐‘š ๐‘› are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 geomulcvg.1 . . . . . . 7 ๐น = (๐‘˜ โˆˆ โ„•0 โ†ฆ (๐‘˜ ยท (๐ดโ†‘๐‘˜)))
2 elnn0 12474 . . . . . . . . 9 (๐‘˜ โˆˆ โ„•0 โ†” (๐‘˜ โˆˆ โ„• โˆจ ๐‘˜ = 0))
3 simpr 486 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ ๐ด = 0)
43oveq1d 7424 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ (๐ดโ†‘๐‘˜) = (0โ†‘๐‘˜))
5 0exp 14063 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ (0โ†‘๐‘˜) = 0)
64, 5sylan9eq 2793 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ดโ†‘๐‘˜) = 0)
76oveq2d 7425 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = (๐‘˜ ยท 0))
8 nncn 12220 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„‚)
98adantl 483 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„‚)
109mul01d 11413 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ ยท 0) = 0)
117, 10eqtrd 2773 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = 0)
12 simpr 486 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ ๐‘˜ = 0)
1312oveq1d 7424 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = (0 ยท (๐ดโ†‘๐‘˜)))
14 simplll 774 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ ๐ด โˆˆ โ„‚)
15 0nn0 12487 . . . . . . . . . . . . . 14 0 โˆˆ โ„•0
1612, 15eqeltrdi 2842 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ ๐‘˜ โˆˆ โ„•0)
1714, 16expcld 14111 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ (๐ดโ†‘๐‘˜) โˆˆ โ„‚)
1817mul02d 11412 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ (0 ยท (๐ดโ†‘๐‘˜)) = 0)
1913, 18eqtrd 2773 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = 0)
2011, 19jaodan 957 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง (๐‘˜ โˆˆ โ„• โˆจ ๐‘˜ = 0)) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = 0)
212, 20sylan2b 595 . . . . . . . 8 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = 0)
2221mpteq2dva 5249 . . . . . . 7 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ (๐‘˜ โˆˆ โ„•0 โ†ฆ (๐‘˜ ยท (๐ดโ†‘๐‘˜))) = (๐‘˜ โˆˆ โ„•0 โ†ฆ 0))
231, 22eqtrid 2785 . . . . . 6 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ ๐น = (๐‘˜ โˆˆ โ„•0 โ†ฆ 0))
24 fconstmpt 5739 . . . . . . 7 (โ„•0 ร— {0}) = (๐‘˜ โˆˆ โ„•0 โ†ฆ 0)
25 nn0uz 12864 . . . . . . . 8 โ„•0 = (โ„คโ‰ฅโ€˜0)
2625xpeq1i 5703 . . . . . . 7 (โ„•0 ร— {0}) = ((โ„คโ‰ฅโ€˜0) ร— {0})
2724, 26eqtr3i 2763 . . . . . 6 (๐‘˜ โˆˆ โ„•0 โ†ฆ 0) = ((โ„คโ‰ฅโ€˜0) ร— {0})
2823, 27eqtrdi 2789 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ ๐น = ((โ„คโ‰ฅโ€˜0) ร— {0}))
2928seqeq3d 13974 . . . 4 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ seq0( + , ๐น) = seq0( + , ((โ„คโ‰ฅโ€˜0) ร— {0})))
30 0z 12569 . . . . 5 0 โˆˆ โ„ค
31 serclim0 15521 . . . . 5 (0 โˆˆ โ„ค โ†’ seq0( + , ((โ„คโ‰ฅโ€˜0) ร— {0})) โ‡ 0)
3230, 31ax-mp 5 . . . 4 seq0( + , ((โ„คโ‰ฅโ€˜0) ร— {0})) โ‡ 0
3329, 32eqbrtrdi 5188 . . 3 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ seq0( + , ๐น) โ‡ 0)
34 seqex 13968 . . . 4 seq0( + , ๐น) โˆˆ V
35 c0ex 11208 . . . 4 0 โˆˆ V
3634, 35breldm 5909 . . 3 (seq0( + , ๐น) โ‡ 0 โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
3733, 36syl 17 . 2 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
38 1red 11215 . . . 4 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ 1 โˆˆ โ„)
39 abscl 15225 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜๐ด) โˆˆ โ„)
4039adantr 482 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜๐ด) โˆˆ โ„)
41 peano2re 11387 . . . . . . . 8 ((absโ€˜๐ด) โˆˆ โ„ โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„)
4240, 41syl 17 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„)
4342rehalfcld 12459 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (((absโ€˜๐ด) + 1) / 2) โˆˆ โ„)
4443adantr 482 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) + 1) / 2) โˆˆ โ„)
45 absrpcl 15235 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„+)
4645adantlr 714 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„+)
4744, 46rerpdivcld 13047 . . . 4 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ ((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด)) โˆˆ โ„)
4840recnd 11242 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
4948mullidd 11232 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (1 ยท (absโ€˜๐ด)) = (absโ€˜๐ด))
50 simpr 486 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜๐ด) < 1)
51 1re 11214 . . . . . . . . 9 1 โˆˆ โ„
52 avglt1 12450 . . . . . . . . 9 (((absโ€˜๐ด) โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ ((absโ€˜๐ด) < 1 โ†” (absโ€˜๐ด) < (((absโ€˜๐ด) + 1) / 2)))
5340, 51, 52sylancl 587 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ ((absโ€˜๐ด) < 1 โ†” (absโ€˜๐ด) < (((absโ€˜๐ด) + 1) / 2)))
5450, 53mpbid 231 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜๐ด) < (((absโ€˜๐ด) + 1) / 2))
5549, 54eqbrtrd 5171 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (1 ยท (absโ€˜๐ด)) < (((absโ€˜๐ด) + 1) / 2))
5655adantr 482 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (1 ยท (absโ€˜๐ด)) < (((absโ€˜๐ด) + 1) / 2))
5738, 44, 46ltmuldivd 13063 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ ((1 ยท (absโ€˜๐ด)) < (((absโ€˜๐ด) + 1) / 2) โ†” 1 < ((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))))
5856, 57mpbid 231 . . . 4 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ 1 < ((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด)))
59 expmulnbnd 14198 . . . 4 ((1 โˆˆ โ„ โˆง ((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด)) โˆˆ โ„ โˆง 1 < ((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))) โ†’ โˆƒ๐‘› โˆˆ โ„•0 โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜))
6038, 47, 58, 59syl3anc 1372 . . 3 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ โˆƒ๐‘› โˆˆ โ„•0 โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜))
61 eluznn0 12901 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘˜ โˆˆ โ„•0)
62 nn0cn 12482 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„‚)
6362adantl 483 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„‚)
6463mullidd 11232 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (1 ยท ๐‘˜) = ๐‘˜)
6543recnd 11242 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (((absโ€˜๐ด) + 1) / 2) โˆˆ โ„‚)
6665ad2antrr 725 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (((absโ€˜๐ด) + 1) / 2) โˆˆ โ„‚)
6748ad2antrr 725 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
6846adantr 482 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โˆˆ โ„+)
6968rpne0d 13021 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โ‰  0)
70 simpr 486 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„•0)
7166, 67, 69, 70expdivd 14125 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) = (((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) / ((absโ€˜๐ด)โ†‘๐‘˜)))
7264, 71breq12d 5162 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†” ๐‘˜ < (((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) / ((absโ€˜๐ด)โ†‘๐‘˜))))
73 nn0re 12481 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„)
7473adantl 483 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„)
75 reexpcl 14044 . . . . . . . . . . 11 (((((absโ€˜๐ด) + 1) / 2) โˆˆ โ„ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โˆˆ โ„)
7644, 75sylan 581 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โˆˆ โ„)
7740adantr 482 . . . . . . . . . . 11 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„)
78 reexpcl 14044 . . . . . . . . . . 11 (((absโ€˜๐ด) โˆˆ โ„ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘๐‘˜) โˆˆ โ„)
7977, 78sylan 581 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘๐‘˜) โˆˆ โ„)
8077adantr 482 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โˆˆ โ„)
81 nn0z 12583 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„ค)
8281adantl 483 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„ค)
8368rpgt0d 13019 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ 0 < (absโ€˜๐ด))
84 expgt0 14061 . . . . . . . . . . 11 (((absโ€˜๐ด) โˆˆ โ„ โˆง ๐‘˜ โˆˆ โ„ค โˆง 0 < (absโ€˜๐ด)) โ†’ 0 < ((absโ€˜๐ด)โ†‘๐‘˜))
8580, 82, 83, 84syl3anc 1372 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ 0 < ((absโ€˜๐ด)โ†‘๐‘˜))
86 ltmuldiv 12087 . . . . . . . . . 10 ((๐‘˜ โˆˆ โ„ โˆง ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โˆˆ โ„ โˆง (((absโ€˜๐ด)โ†‘๐‘˜) โˆˆ โ„ โˆง 0 < ((absโ€˜๐ด)โ†‘๐‘˜))) โ†’ ((๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โ†” ๐‘˜ < (((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) / ((absโ€˜๐ด)โ†‘๐‘˜))))
8774, 76, 79, 85, 86syl112anc 1375 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โ†” ๐‘˜ < (((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) / ((absโ€˜๐ด)โ†‘๐‘˜))))
8872, 87bitr4d 282 . . . . . . . 8 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†” (๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜)))
8961, 88sylan2 594 . . . . . . 7 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง (๐‘› โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›))) โ†’ ((1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†” (๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜)))
9089anassrs 469 . . . . . 6 (((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘› โˆˆ โ„•0) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†” (๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜)))
9190ralbidva 3176 . . . . 5 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘› โˆˆ โ„•0) โ†’ (โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†” โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜)))
92 simprl 770 . . . . . . . 8 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ†’ ๐‘› โˆˆ โ„•0)
93 oveq2 7417 . . . . . . . . . . 11 (๐‘˜ = ๐‘š โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
94 eqid 2733 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜)) = (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))
95 ovex 7442 . . . . . . . . . . 11 ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š) โˆˆ V
9693, 94, 95fvmpt 6999 . . . . . . . . . 10 (๐‘š โˆˆ โ„•0 โ†’ ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
9796adantl 483 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
9843ad2antrr 725 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (((absโ€˜๐ด) + 1) / 2) โˆˆ โ„)
99 simpr 486 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ ๐‘š โˆˆ โ„•0)
10098, 99reexpcld 14128 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š) โˆˆ โ„)
10197, 100eqeltrd 2834 . . . . . . . 8 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š) โˆˆ โ„)
102 id 22 . . . . . . . . . . . 12 (๐‘˜ = ๐‘š โ†’ ๐‘˜ = ๐‘š)
103 oveq2 7417 . . . . . . . . . . . 12 (๐‘˜ = ๐‘š โ†’ (๐ดโ†‘๐‘˜) = (๐ดโ†‘๐‘š))
104102, 103oveq12d 7427 . . . . . . . . . . 11 (๐‘˜ = ๐‘š โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = (๐‘š ยท (๐ดโ†‘๐‘š)))
105 ovex 7442 . . . . . . . . . . 11 (๐‘š ยท (๐ดโ†‘๐‘š)) โˆˆ V
106104, 1, 105fvmpt 6999 . . . . . . . . . 10 (๐‘š โˆˆ โ„•0 โ†’ (๐นโ€˜๐‘š) = (๐‘š ยท (๐ดโ†‘๐‘š)))
107106adantl 483 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘š) = (๐‘š ยท (๐ดโ†‘๐‘š)))
108 nn0cn 12482 . . . . . . . . . . 11 (๐‘š โˆˆ โ„•0 โ†’ ๐‘š โˆˆ โ„‚)
109108adantl 483 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ ๐‘š โˆˆ โ„‚)
110 expcl 14045 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐ดโ†‘๐‘š) โˆˆ โ„‚)
111110ad4ant14 751 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐ดโ†‘๐‘š) โˆˆ โ„‚)
112109, 111mulcld 11234 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐‘š ยท (๐ดโ†‘๐‘š)) โˆˆ โ„‚)
113107, 112eqeltrd 2834 . . . . . . . 8 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘š) โˆˆ โ„‚)
114 0red 11217 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ 0 โˆˆ โ„)
115 absge0 15234 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (absโ€˜๐ด))
116115adantr 482 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ 0 โ‰ค (absโ€˜๐ด))
117114, 40, 43, 116, 54lelttrd 11372 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ 0 < (((absโ€˜๐ด) + 1) / 2))
118114, 43, 117ltled 11362 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ 0 โ‰ค (((absโ€˜๐ด) + 1) / 2))
11943, 118absidd 15369 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜(((absโ€˜๐ด) + 1) / 2)) = (((absโ€˜๐ด) + 1) / 2))
120 avglt2 12451 . . . . . . . . . . . . . 14 (((absโ€˜๐ด) โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ ((absโ€˜๐ด) < 1 โ†” (((absโ€˜๐ด) + 1) / 2) < 1))
12140, 51, 120sylancl 587 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ ((absโ€˜๐ด) < 1 โ†” (((absโ€˜๐ด) + 1) / 2) < 1))
12250, 121mpbid 231 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (((absโ€˜๐ด) + 1) / 2) < 1)
123119, 122eqbrtrd 5171 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜(((absโ€˜๐ด) + 1) / 2)) < 1)
124 oveq2 7417 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘› โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘›))
125 ovex 7442 . . . . . . . . . . . . 13 ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘›) โˆˆ V
126124, 94, 125fvmpt 6999 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„•0 โ†’ ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘›) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘›))
127126adantl 483 . . . . . . . . . . 11 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐‘› โˆˆ โ„•0) โ†’ ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘›) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘›))
12865, 123, 127geolim 15816 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ seq0( + , (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ‡ (1 / (1 โˆ’ (((absโ€˜๐ด) + 1) / 2))))
129 seqex 13968 . . . . . . . . . . 11 seq0( + , (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆˆ V
130 ovex 7442 . . . . . . . . . . 11 (1 / (1 โˆ’ (((absโ€˜๐ด) + 1) / 2))) โˆˆ V
131129, 130breldm 5909 . . . . . . . . . 10 (seq0( + , (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ‡ (1 / (1 โˆ’ (((absโ€˜๐ด) + 1) / 2))) โ†’ seq0( + , (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆˆ dom โ‡ )
132128, 131syl 17 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ seq0( + , (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆˆ dom โ‡ )
133132adantr 482 . . . . . . . 8 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ†’ seq0( + , (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆˆ dom โ‡ )
134 1red 11215 . . . . . . . 8 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ†’ 1 โˆˆ โ„)
135 eluznn0 12901 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘š โˆˆ โ„•0)
13692, 135sylan 581 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘š โˆˆ โ„•0)
137136nn0red 12533 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘š โˆˆ โ„)
138 simplll 774 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐ด โˆˆ โ„‚)
139138abscld 15383 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜๐ด) โˆˆ โ„)
140139, 136reexpcld 14128 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((absโ€˜๐ด)โ†‘๐‘š) โˆˆ โ„)
141137, 140remulcld 11244 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)) โˆˆ โ„)
142136, 100syldan 592 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š) โˆˆ โ„)
143 simprr 772 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ†’ โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))
144 oveq2 7417 . . . . . . . . . . . . . . 15 (๐‘˜ = ๐‘š โ†’ ((absโ€˜๐ด)โ†‘๐‘˜) = ((absโ€˜๐ด)โ†‘๐‘š))
145102, 144oveq12d 7427 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘š โ†’ (๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) = (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)))
146145, 93breq12d 5162 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘š โ†’ ((๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โ†” (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š)))
147146rspccva 3612 . . . . . . . . . . . 12 ((โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
148143, 147sylan 581 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
149141, 142, 148ltled 11362 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)) โ‰ค ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
150136nn0cnd 12534 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘š โˆˆ โ„‚)
151138, 136expcld 14111 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐ดโ†‘๐‘š) โˆˆ โ„‚)
152150, 151absmuld 15401 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐‘š ยท (๐ดโ†‘๐‘š))) = ((absโ€˜๐‘š) ยท (absโ€˜(๐ดโ†‘๐‘š))))
153136nn0ge0d 12535 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ 0 โ‰ค ๐‘š)
154137, 153absidd 15369 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜๐‘š) = ๐‘š)
155138, 136absexpd 15399 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐ดโ†‘๐‘š)) = ((absโ€˜๐ด)โ†‘๐‘š))
156154, 155oveq12d 7427 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((absโ€˜๐‘š) ยท (absโ€˜(๐ดโ†‘๐‘š))) = (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)))
157152, 156eqtrd 2773 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐‘š ยท (๐ดโ†‘๐‘š))) = (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)))
158142recnd 11242 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š) โˆˆ โ„‚)
159158mullidd 11232 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (1 ยท ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š)) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
160149, 157, 1593brtr4d 5181 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐‘š ยท (๐ดโ†‘๐‘š))) โ‰ค (1 ยท ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š)))
161136, 106syl 17 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐นโ€˜๐‘š) = (๐‘š ยท (๐ดโ†‘๐‘š)))
162161fveq2d 6896 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐นโ€˜๐‘š)) = (absโ€˜(๐‘š ยท (๐ดโ†‘๐‘š))))
163136, 96syl 17 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
164163oveq2d 7425 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (1 ยท ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š)) = (1 ยท ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š)))
165160, 162, 1643brtr4d 5181 . . . . . . . 8 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐นโ€˜๐‘š)) โ‰ค (1 ยท ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š)))
16625, 92, 101, 113, 133, 134, 165cvgcmpce 15764 . . . . . . 7 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
167166expr 458 . . . . . 6 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐‘› โˆˆ โ„•0) โ†’ (โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ ))
168167adantlr 714 . . . . 5 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘› โˆˆ โ„•0) โ†’ (โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ ))
16991, 168sylbid 239 . . . 4 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘› โˆˆ โ„•0) โ†’ (โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ ))
170169rexlimdva 3156 . . 3 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (โˆƒ๐‘› โˆˆ โ„•0 โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ ))
17160, 170mpd 15 . 2 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
17237, 171pm2.61dane 3030 1 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941  โˆ€wral 3062  โˆƒwrex 3071  {csn 4629   class class class wbr 5149   โ†ฆ cmpt 5232   ร— cxp 5675  dom cdm 5677  โ€˜cfv 6544  (class class class)co 7409  โ„‚cc 11108  โ„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   ยท cmul 11115   < clt 11248   โ‰ค cle 11249   โˆ’ cmin 11444   / cdiv 11871  โ„•cn 12212  2c2 12267  โ„•0cn0 12472  โ„คcz 12558  โ„คโ‰ฅcuz 12822  โ„+crp 12974  seqcseq 13966  โ†‘cexp 14027  abscabs 15181   โ‡ cli 15428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-ico 13330  df-fz 13485  df-fzo 13628  df-fl 13757  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-limsup 15415  df-clim 15432  df-rlim 15433  df-sum 15633
This theorem is referenced by:  radcnvlem1  25925
  Copyright terms: Public domain W3C validator