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

Theorem geomulcvg 15768
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 12422 . . . . . . . . 9 (๐‘˜ โˆˆ โ„•0 โ†” (๐‘˜ โˆˆ โ„• โˆจ ๐‘˜ = 0))
3 simpr 486 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ ๐ด = 0)
43oveq1d 7377 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ (๐ดโ†‘๐‘˜) = (0โ†‘๐‘˜))
5 0exp 14010 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ (0โ†‘๐‘˜) = 0)
64, 5sylan9eq 2797 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ดโ†‘๐‘˜) = 0)
76oveq2d 7378 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = (๐‘˜ ยท 0))
8 nncn 12168 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„‚)
98adantl 483 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„‚)
109mul01d 11361 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ ยท 0) = 0)
117, 10eqtrd 2777 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = 0)
12 simpr 486 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ ๐‘˜ = 0)
1312oveq1d 7377 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = (0 ยท (๐ดโ†‘๐‘˜)))
14 simplll 774 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ ๐ด โˆˆ โ„‚)
15 0nn0 12435 . . . . . . . . . . . . . 14 0 โˆˆ โ„•0
1612, 15eqeltrdi 2846 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ ๐‘˜ โˆˆ โ„•0)
1714, 16expcld 14058 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ (๐ดโ†‘๐‘˜) โˆˆ โ„‚)
1817mul02d 11360 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โˆง ๐‘˜ = 0) โ†’ (0 ยท (๐ดโ†‘๐‘˜)) = 0)
1913, 18eqtrd 2777 . . . . . . . . . 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 5210 . . . . . . 7 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ (๐‘˜ โˆˆ โ„•0 โ†ฆ (๐‘˜ ยท (๐ดโ†‘๐‘˜))) = (๐‘˜ โˆˆ โ„•0 โ†ฆ 0))
231, 22eqtrid 2789 . . . . . 6 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ ๐น = (๐‘˜ โˆˆ โ„•0 โ†ฆ 0))
24 fconstmpt 5699 . . . . . . 7 (โ„•0 ร— {0}) = (๐‘˜ โˆˆ โ„•0 โ†ฆ 0)
25 nn0uz 12812 . . . . . . . 8 โ„•0 = (โ„คโ‰ฅโ€˜0)
2625xpeq1i 5664 . . . . . . 7 (โ„•0 ร— {0}) = ((โ„คโ‰ฅโ€˜0) ร— {0})
2724, 26eqtr3i 2767 . . . . . 6 (๐‘˜ โˆˆ โ„•0 โ†ฆ 0) = ((โ„คโ‰ฅโ€˜0) ร— {0})
2823, 27eqtrdi 2793 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ ๐น = ((โ„คโ‰ฅโ€˜0) ร— {0}))
2928seqeq3d 13921 . . . 4 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ seq0( + , ๐น) = seq0( + , ((โ„คโ‰ฅโ€˜0) ร— {0})))
30 0z 12517 . . . . 5 0 โˆˆ โ„ค
31 serclim0 15466 . . . . 5 (0 โˆˆ โ„ค โ†’ seq0( + , ((โ„คโ‰ฅโ€˜0) ร— {0})) โ‡ 0)
3230, 31ax-mp 5 . . . 4 seq0( + , ((โ„คโ‰ฅโ€˜0) ร— {0})) โ‡ 0
3329, 32eqbrtrdi 5149 . . 3 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ seq0( + , ๐น) โ‡ 0)
34 seqex 13915 . . . 4 seq0( + , ๐น) โˆˆ V
35 c0ex 11156 . . . 4 0 โˆˆ V
3634, 35breldm 5869 . . 3 (seq0( + , ๐น) โ‡ 0 โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
3733, 36syl 17 . 2 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด = 0) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
38 1red 11163 . . . 4 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ 1 โˆˆ โ„)
39 abscl 15170 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜๐ด) โˆˆ โ„)
4039adantr 482 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜๐ด) โˆˆ โ„)
41 peano2re 11335 . . . . . . . 8 ((absโ€˜๐ด) โˆˆ โ„ โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„)
4240, 41syl 17 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„)
4342rehalfcld 12407 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (((absโ€˜๐ด) + 1) / 2) โˆˆ โ„)
4443adantr 482 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) + 1) / 2) โˆˆ โ„)
45 absrpcl 15180 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„+)
4645adantlr 714 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„+)
4744, 46rerpdivcld 12995 . . . 4 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ ((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด)) โˆˆ โ„)
4840recnd 11190 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
4948mulid2d 11180 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (1 ยท (absโ€˜๐ด)) = (absโ€˜๐ด))
50 simpr 486 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜๐ด) < 1)
51 1re 11162 . . . . . . . . 9 1 โˆˆ โ„
52 avglt1 12398 . . . . . . . . 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 5132 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (1 ยท (absโ€˜๐ด)) < (((absโ€˜๐ด) + 1) / 2))
5655adantr 482 . . . . 5 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (1 ยท (absโ€˜๐ด)) < (((absโ€˜๐ด) + 1) / 2))
5738, 44, 46ltmuldivd 13011 . . . . 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 14145 . . . 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 12849 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘˜ โˆˆ โ„•0)
62 nn0cn 12430 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„‚)
6362adantl 483 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„‚)
6463mulid2d 11180 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (1 ยท ๐‘˜) = ๐‘˜)
6543recnd 11190 . . . . . . . . . . . 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 12969 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โ‰  0)
70 simpr 486 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„•0)
7166, 67, 69, 70expdivd 14072 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) = (((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) / ((absโ€˜๐ด)โ†‘๐‘˜)))
7264, 71breq12d 5123 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†” ๐‘˜ < (((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) / ((absโ€˜๐ด)โ†‘๐‘˜))))
73 nn0re 12429 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„)
7473adantl 483 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„)
75 reexpcl 13991 . . . . . . . . . . 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 13991 . . . . . . . . . . 11 (((absโ€˜๐ด) โˆˆ โ„ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘๐‘˜) โˆˆ โ„)
7977, 78sylan 581 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘๐‘˜) โˆˆ โ„)
8077adantr 482 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โˆˆ โ„)
81 nn0z 12531 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„ค)
8281adantl 483 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„ค)
8368rpgt0d 12967 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ 0 < (absโ€˜๐ด))
84 expgt0 14008 . . . . . . . . . . 11 (((absโ€˜๐ด) โˆˆ โ„ โˆง ๐‘˜ โˆˆ โ„ค โˆง 0 < (absโ€˜๐ด)) โ†’ 0 < ((absโ€˜๐ด)โ†‘๐‘˜))
8580, 82, 83, 84syl3anc 1372 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ 0 < ((absโ€˜๐ด)โ†‘๐‘˜))
86 ltmuldiv 12035 . . . . . . . . . 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 3173 . . . . 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 7370 . . . . . . . . . . 11 (๐‘˜ = ๐‘š โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
94 eqid 2737 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜)) = (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))
95 ovex 7395 . . . . . . . . . . 11 ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š) โˆˆ V
9693, 94, 95fvmpt 6953 . . . . . . . . . 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 14075 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š) โˆˆ โ„)
10197, 100eqeltrd 2838 . . . . . . . 8 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š) โˆˆ โ„)
102 id 22 . . . . . . . . . . . 12 (๐‘˜ = ๐‘š โ†’ ๐‘˜ = ๐‘š)
103 oveq2 7370 . . . . . . . . . . . 12 (๐‘˜ = ๐‘š โ†’ (๐ดโ†‘๐‘˜) = (๐ดโ†‘๐‘š))
104102, 103oveq12d 7380 . . . . . . . . . . 11 (๐‘˜ = ๐‘š โ†’ (๐‘˜ ยท (๐ดโ†‘๐‘˜)) = (๐‘š ยท (๐ดโ†‘๐‘š)))
105 ovex 7395 . . . . . . . . . . 11 (๐‘š ยท (๐ดโ†‘๐‘š)) โˆˆ V
106104, 1, 105fvmpt 6953 . . . . . . . . . 10 (๐‘š โˆˆ โ„•0 โ†’ (๐นโ€˜๐‘š) = (๐‘š ยท (๐ดโ†‘๐‘š)))
107106adantl 483 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘š) = (๐‘š ยท (๐ดโ†‘๐‘š)))
108 nn0cn 12430 . . . . . . . . . . 11 (๐‘š โˆˆ โ„•0 โ†’ ๐‘š โˆˆ โ„‚)
109108adantl 483 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ ๐‘š โˆˆ โ„‚)
110 expcl 13992 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐ดโ†‘๐‘š) โˆˆ โ„‚)
111110ad4ant14 751 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐ดโ†‘๐‘š) โˆˆ โ„‚)
112109, 111mulcld 11182 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐‘š ยท (๐ดโ†‘๐‘š)) โˆˆ โ„‚)
113107, 112eqeltrd 2838 . . . . . . . 8 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘š) โˆˆ โ„‚)
114 0red 11165 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ 0 โˆˆ โ„)
115 absge0 15179 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (absโ€˜๐ด))
116115adantr 482 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ 0 โ‰ค (absโ€˜๐ด))
117114, 40, 43, 116, 54lelttrd 11320 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ 0 < (((absโ€˜๐ด) + 1) / 2))
118114, 43, 117ltled 11310 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ 0 โ‰ค (((absโ€˜๐ด) + 1) / 2))
11943, 118absidd 15314 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜(((absโ€˜๐ด) + 1) / 2)) = (((absโ€˜๐ด) + 1) / 2))
120 avglt2 12399 . . . . . . . . . . . . . 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 5132 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ (absโ€˜(((absโ€˜๐ด) + 1) / 2)) < 1)
124 oveq2 7370 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘› โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘›))
125 ovex 7395 . . . . . . . . . . . . 13 ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘›) โˆˆ V
126124, 94, 125fvmpt 6953 . . . . . . . . . . . 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 15762 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โ†’ seq0( + , (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ‡ (1 / (1 โˆ’ (((absโ€˜๐ด) + 1) / 2))))
129 seqex 13915 . . . . . . . . . . 11 seq0( + , (๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆˆ V
130 ovex 7395 . . . . . . . . . . 11 (1 / (1 โˆ’ (((absโ€˜๐ด) + 1) / 2))) โˆˆ V
131129, 130breldm 5869 . . . . . . . . . 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 11163 . . . . . . . 8 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โ†’ 1 โˆˆ โ„)
135 eluznn0 12849 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘š โˆˆ โ„•0)
13692, 135sylan 581 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘š โˆˆ โ„•0)
137136nn0red 12481 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘š โˆˆ โ„)
138 simplll 774 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐ด โˆˆ โ„‚)
139138abscld 15328 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜๐ด) โˆˆ โ„)
140139, 136reexpcld 14075 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((absโ€˜๐ด)โ†‘๐‘š) โˆˆ โ„)
141137, 140remulcld 11192 . . . . . . . . . . 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 7370 . . . . . . . . . . . . . . 15 (๐‘˜ = ๐‘š โ†’ ((absโ€˜๐ด)โ†‘๐‘˜) = ((absโ€˜๐ด)โ†‘๐‘š))
145102, 144oveq12d 7380 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘š โ†’ (๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) = (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)))
146145, 93breq12d 5123 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘š โ†’ ((๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜) โ†” (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š)))
147146rspccva 3583 . . . . . . . . . . . 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 11310 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)) โ‰ค ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
150136nn0cnd 12482 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘š โˆˆ โ„‚)
151138, 136expcld 14058 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐ดโ†‘๐‘š) โˆˆ โ„‚)
152150, 151absmuld 15346 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐‘š ยท (๐ดโ†‘๐‘š))) = ((absโ€˜๐‘š) ยท (absโ€˜(๐ดโ†‘๐‘š))))
153136nn0ge0d 12483 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ 0 โ‰ค ๐‘š)
154137, 153absidd 15314 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜๐‘š) = ๐‘š)
155138, 136absexpd 15344 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐ดโ†‘๐‘š)) = ((absโ€˜๐ด)โ†‘๐‘š))
156154, 155oveq12d 7380 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((absโ€˜๐‘š) ยท (absโ€˜(๐ดโ†‘๐‘š))) = (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)))
157152, 156eqtrd 2777 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐‘š ยท (๐ดโ†‘๐‘š))) = (๐‘š ยท ((absโ€˜๐ด)โ†‘๐‘š)))
158142recnd 11190 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š) โˆˆ โ„‚)
159158mulid2d 11180 . . . . . . . . . 10 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (1 ยท ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š)) = ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š))
160149, 157, 1593brtr4d 5142 . . . . . . . . 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 6851 . . . . . . . . 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 7378 . . . . . . . . 9 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (1 ยท ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š)) = (1 ยท ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘š)))
165160, 162, 1643brtr4d 5142 . . . . . . . 8 ((((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง (๐‘› โˆˆ โ„•0 โˆง โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘˜ ยท ((absโ€˜๐ด)โ†‘๐‘˜)) < ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (absโ€˜(๐นโ€˜๐‘š)) โ‰ค (1 ยท ((๐‘˜ โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด) + 1) / 2)โ†‘๐‘˜))โ€˜๐‘š)))
16625, 92, 101, 113, 133, 134, 165cvgcmpce 15710 . . . . . . 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 3153 . . 3 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ (โˆƒ๐‘› โˆˆ โ„•0 โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(1 ยท ๐‘˜) < (((((absโ€˜๐ด) + 1) / 2) / (absโ€˜๐ด))โ†‘๐‘˜) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ ))
17160, 170mpd 15 . 2 (((๐ด โˆˆ โ„‚ โˆง (absโ€˜๐ด) < 1) โˆง ๐ด โ‰  0) โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
17237, 171pm2.61dane 3033 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 2944  โˆ€wral 3065  โˆƒwrex 3074  {csn 4591   class class class wbr 5110   โ†ฆ cmpt 5193   ร— cxp 5636  dom cdm 5638  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392   / cdiv 11819  โ„•cn 12160  2c2 12215  โ„•0cn0 12420  โ„คcz 12506  โ„คโ‰ฅcuz 12770  โ„+crp 12922  seqcseq 13913  โ†‘cexp 13974  abscabs 15126   โ‡ cli 15373
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-ico 13277  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578
This theorem is referenced by:  radcnvlem1  25788
  Copyright terms: Public domain W3C validator