ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cvgratz GIF version

Theorem cvgratz 11539
Description: Ratio test for convergence of a complex infinite series. If the ratio ๐ด of the absolute values of successive terms in an infinite sequence ๐น is less than 1 for all terms, then the infinite sum of the terms of ๐น converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
Hypotheses
Ref Expression
cvgratz.1 ๐‘ = (โ„คโ‰ฅโ€˜๐‘€)
cvgratz.m (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
cvgratz.3 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
cvgratz.4 (๐œ‘ โ†’ ๐ด < 1)
cvgratz.gt0 (๐œ‘ โ†’ 0 < ๐ด)
cvgratz.6 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
cvgratz.7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
Assertion
Ref Expression
cvgratz (๐œ‘ โ†’ seq๐‘€( + , ๐น) โˆˆ dom โ‡ )
Distinct variable groups:   ๐ด,๐‘˜   ๐‘˜,๐น   ๐‘˜,๐‘€   ๐‘˜,๐‘   ๐œ‘,๐‘˜

Proof of Theorem cvgratz
Dummy variables ๐‘– ๐‘ฅ ๐‘ฆ ๐‘Ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvgratz.m . . . . 5 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
21adantr 276 . . . 4 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ ๐‘€ โˆˆ โ„ค)
3 fveq2 5515 . . . . . 6 (๐‘˜ = ๐‘ฅ โ†’ (๐นโ€˜๐‘˜) = (๐นโ€˜๐‘ฅ))
43eleq1d 2246 . . . . 5 (๐‘˜ = ๐‘ฅ โ†’ ((๐นโ€˜๐‘˜) โˆˆ โ„‚ โ†” (๐นโ€˜๐‘ฅ) โˆˆ โ„‚))
5 cvgratz.6 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
65ralrimiva 2550 . . . . . 6 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ ๐‘ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
76ad2antrr 488 . . . . 5 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ โˆ€๐‘˜ โˆˆ ๐‘ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
8 cvgratz.1 . . . . . . . 8 ๐‘ = (โ„คโ‰ฅโ€˜๐‘€)
98eleq2i 2244 . . . . . . 7 (๐‘ฅ โˆˆ ๐‘ โ†” ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
109biimpri 133 . . . . . 6 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ ๐‘ฅ โˆˆ ๐‘)
1110adantl 277 . . . . 5 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘ฅ โˆˆ ๐‘)
124, 7, 11rspcdva 2846 . . . 4 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘ฅ) โˆˆ โ„‚)
13 eluzelz 9536 . . . . . . . 8 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ ๐‘˜ โˆˆ โ„ค)
1413adantl 277 . . . . . . 7 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘˜ โˆˆ โ„ค)
15 1red 7971 . . . . . . . 8 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ 1 โˆˆ โ„)
161zred 9374 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„)
1716ad2antrr 488 . . . . . . . 8 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘€ โˆˆ โ„)
1814zred 9374 . . . . . . . 8 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘˜ โˆˆ โ„)
19 simplr 528 . . . . . . . 8 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ 1 โ‰ค ๐‘€)
20 eluzle 9539 . . . . . . . . 9 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ ๐‘€ โ‰ค ๐‘˜)
2120adantl 277 . . . . . . . 8 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘€ โ‰ค ๐‘˜)
2215, 17, 18, 19, 21letrd 8080 . . . . . . 7 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ 1 โ‰ค ๐‘˜)
23 elnnz1 9275 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†” (๐‘˜ โˆˆ โ„ค โˆง 1 โ‰ค ๐‘˜))
2414, 22, 23sylanbrc 417 . . . . . 6 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘˜ โˆˆ โ„•)
25 elnnuz 9563 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†” ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1))
26 fveq2 5515 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘€ โ†’ (๐นโ€˜๐‘˜) = (๐นโ€˜๐‘€))
2726eleq1d 2246 . . . . . . . . . . . 12 (๐‘˜ = ๐‘€ โ†’ ((๐นโ€˜๐‘˜) โˆˆ โ„‚ โ†” (๐นโ€˜๐‘€) โˆˆ โ„‚))
28 uzid 9541 . . . . . . . . . . . . . 14 (๐‘€ โˆˆ โ„ค โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
291, 28syl 14 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
3029, 8eleqtrrdi 2271 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘)
3127, 6, 30rspcdva 2846 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐นโ€˜๐‘€) โˆˆ โ„‚)
3231ad3antrrr 492 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ (๐นโ€˜๐‘€) โˆˆ โ„‚)
33 cvgratz.3 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
34 cvgratz.gt0 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < ๐ด)
3533, 34elrpd 9692 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ด โˆˆ โ„+)
3635ad3antrrr 492 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ ๐ด โˆˆ โ„+)
372adantr 276 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ๐‘€ โˆˆ โ„ค)
3837adantr 276 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ ๐‘€ โˆˆ โ„ค)
3925biimpri 133 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ ๐‘˜ โˆˆ โ„•)
4039adantl 277 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ๐‘˜ โˆˆ โ„•)
4140nnzd 9373 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ๐‘˜ โˆˆ โ„ค)
4241adantr 276 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ ๐‘˜ โˆˆ โ„ค)
4338, 42zsubcld 9379 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ (๐‘€ โˆ’ ๐‘˜) โˆˆ โ„ค)
4436, 43rpexpcld 10677 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) โˆˆ โ„+)
4544rpcnd 9697 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) โˆˆ โ„‚)
4644rpap0d 9701 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) # 0)
4732, 45, 46divclapd 8746 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ < ๐‘€) โ†’ ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))) โˆˆ โ„‚)
48 simplll 533 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ๐œ‘)
4937adantr 276 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ๐‘€ โˆˆ โ„ค)
5041adantr 276 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ๐‘˜ โˆˆ โ„ค)
5116ad3antrrr 492 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ๐‘€ โˆˆ โ„)
5250zred 9374 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ๐‘˜ โˆˆ โ„)
53 simpr 110 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ยฌ ๐‘˜ < ๐‘€)
5451, 52, 53nltled 8077 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ๐‘€ โ‰ค ๐‘˜)
55 eluz2 9533 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†” (๐‘€ โˆˆ โ„ค โˆง ๐‘˜ โˆˆ โ„ค โˆง ๐‘€ โ‰ค ๐‘˜))
5649, 50, 54, 55syl3anbrc 1181 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
5756, 8eleqtrrdi 2271 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ ๐‘˜ โˆˆ ๐‘)
5848, 57, 5syl2anc 411 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘˜ < ๐‘€) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
59 zdclt 9329 . . . . . . . . . 10 ((๐‘˜ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ DECID ๐‘˜ < ๐‘€)
6041, 37, 59syl2anc 411 . . . . . . . . 9 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ DECID ๐‘˜ < ๐‘€)
6147, 58, 60ifcldadc 3563 . . . . . . . 8 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) โˆˆ โ„‚)
6225, 61sylan2b 287 . . . . . . 7 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) โˆˆ โ„‚)
6324, 62syldan 282 . . . . . 6 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) โˆˆ โ„‚)
64 breq1 4006 . . . . . . . 8 (๐‘– = ๐‘˜ โ†’ (๐‘– < ๐‘€ โ†” ๐‘˜ < ๐‘€))
65 oveq2 5882 . . . . . . . . . 10 (๐‘– = ๐‘˜ โ†’ (๐‘€ โˆ’ ๐‘–) = (๐‘€ โˆ’ ๐‘˜))
6665oveq2d 5890 . . . . . . . . 9 (๐‘– = ๐‘˜ โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘–)) = (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)))
6766oveq2d 5890 . . . . . . . 8 (๐‘– = ๐‘˜ โ†’ ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))) = ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))))
68 fveq2 5515 . . . . . . . 8 (๐‘– = ๐‘˜ โ†’ (๐นโ€˜๐‘–) = (๐นโ€˜๐‘˜))
6964, 67, 68ifbieq12d 3560 . . . . . . 7 (๐‘– = ๐‘˜ โ†’ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)) = if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))
70 eqid 2177 . . . . . . 7 (๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–))) = (๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))
7169, 70fvmptg 5592 . . . . . 6 ((๐‘˜ โˆˆ โ„• โˆง if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) โˆˆ โ„‚) โ†’ ((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜) = if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))
7224, 63, 71syl2anc 411 . . . . 5 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜) = if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))
7317, 18, 21lensymd 8078 . . . . . 6 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ยฌ ๐‘˜ < ๐‘€)
7473iffalsed 3544 . . . . 5 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) = (๐นโ€˜๐‘˜))
7572, 74eqtr2d 2211 . . . 4 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘˜) = ((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜))
76 addcl 7935 . . . . 5 ((๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ โ„‚)
7776adantl 277 . . . 4 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚)) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ โ„‚)
782, 12, 75, 77seq3feq 10471 . . 3 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ seq๐‘€( + , ๐น) = seq๐‘€( + , (๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))))
7933adantr 276 . . . . 5 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ ๐ด โˆˆ โ„)
80 cvgratz.4 . . . . . 6 (๐œ‘ โ†’ ๐ด < 1)
8180adantr 276 . . . . 5 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ ๐ด < 1)
8234adantr 276 . . . . 5 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ 0 < ๐ด)
8371eleq1d 2246 . . . . . . . 8 ((๐‘˜ โˆˆ โ„• โˆง if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) โˆˆ โ„‚) โ†’ (((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜) โˆˆ โ„‚ โ†” if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) โˆˆ โ„‚))
8440, 61, 83syl2anc 411 . . . . . . 7 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ (((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜) โˆˆ โ„‚ โ†” if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) โˆˆ โ„‚))
8561, 84mpbird 167 . . . . . 6 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜) โˆˆ โ„‚)
8625, 85sylan2b 287 . . . . 5 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜) โˆˆ โ„‚)
8731ad3antrrr 492 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐นโ€˜๐‘€) โˆˆ โ„‚)
8835ad3antrrr 492 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ๐ด โˆˆ โ„+)
892ad2antrr 488 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘€ โˆˆ โ„ค)
9025, 41sylan2b 287 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„ค)
9190adantr 276 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘˜ โˆˆ โ„ค)
9291peano2zd 9377 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐‘˜ + 1) โˆˆ โ„ค)
9389, 92zsubcld 9379 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐‘€ โˆ’ (๐‘˜ + 1)) โˆˆ โ„ค)
9488, 93rpexpcld 10677 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1))) โˆˆ โ„+)
9594rpcnd 9697 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1))) โˆˆ โ„‚)
9694rpap0d 9701 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1))) # 0)
9787, 95, 96divclapd 8746 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))) โˆˆ โ„‚)
98 fveq2 5515 . . . . . . . . . . . 12 (๐‘Ž = (๐‘˜ + 1) โ†’ (๐นโ€˜๐‘Ž) = (๐นโ€˜(๐‘˜ + 1)))
9998eleq1d 2246 . . . . . . . . . . 11 (๐‘Ž = (๐‘˜ + 1) โ†’ ((๐นโ€˜๐‘Ž) โˆˆ โ„‚ โ†” (๐นโ€˜(๐‘˜ + 1)) โˆˆ โ„‚))
100 fveq2 5515 . . . . . . . . . . . . . . 15 (๐‘˜ = ๐‘Ž โ†’ (๐นโ€˜๐‘˜) = (๐นโ€˜๐‘Ž))
101100eleq1d 2246 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘Ž โ†’ ((๐นโ€˜๐‘˜) โˆˆ โ„‚ โ†” (๐นโ€˜๐‘Ž) โˆˆ โ„‚))
102101cbvralv 2703 . . . . . . . . . . . . 13 (โˆ€๐‘˜ โˆˆ ๐‘ (๐นโ€˜๐‘˜) โˆˆ โ„‚ โ†” โˆ€๐‘Ž โˆˆ ๐‘ (๐นโ€˜๐‘Ž) โˆˆ โ„‚)
1036, 102sylib 122 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ ๐‘ (๐นโ€˜๐‘Ž) โˆˆ โ„‚)
104103ad3antrrr 492 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ โˆ€๐‘Ž โˆˆ ๐‘ (๐นโ€˜๐‘Ž) โˆˆ โ„‚)
1052ad2antrr 488 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘€ โˆˆ โ„ค)
106 peano2nn 8930 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„• โ†’ (๐‘˜ + 1) โˆˆ โ„•)
107106adantl 277 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + 1) โˆˆ โ„•)
108107nnzd 9373 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + 1) โˆˆ โ„ค)
109108adantr 276 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ (๐‘˜ + 1) โˆˆ โ„ค)
11016ad3antrrr 492 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘€ โˆˆ โ„)
111107nnred 8931 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + 1) โˆˆ โ„)
112111adantr 276 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ (๐‘˜ + 1) โˆˆ โ„)
113 simpr 110 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ ยฌ (๐‘˜ + 1) < ๐‘€)
114110, 112, 113nltled 8077 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘€ โ‰ค (๐‘˜ + 1))
115 eluz2 9533 . . . . . . . . . . . . 13 ((๐‘˜ + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†” (๐‘€ โˆˆ โ„ค โˆง (๐‘˜ + 1) โˆˆ โ„ค โˆง ๐‘€ โ‰ค (๐‘˜ + 1)))
116105, 109, 114, 115syl3anbrc 1181 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ (๐‘˜ + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
117116, 8eleqtrrdi 2271 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ (๐‘˜ + 1) โˆˆ ๐‘)
11899, 104, 117rspcdva 2846 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ยฌ (๐‘˜ + 1) < ๐‘€) โ†’ (๐นโ€˜(๐‘˜ + 1)) โˆˆ โ„‚)
1192adantr 276 . . . . . . . . . . 11 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„ค)
120 zdclt 9329 . . . . . . . . . . 11 (((๐‘˜ + 1) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ DECID (๐‘˜ + 1) < ๐‘€)
121108, 119, 120syl2anc 411 . . . . . . . . . 10 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ DECID (๐‘˜ + 1) < ๐‘€)
12297, 118, 121ifcldadc 3563 . . . . . . . . 9 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))) โˆˆ โ„‚)
123122abscld 11189 . . . . . . . 8 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) โˆˆ โ„)
12416recnd 7985 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
125124ad2antrr 488 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„‚)
126 simpr 110 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„•)
127126nncnd 8932 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„‚)
128 1cnd 7972 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ 1 โˆˆ โ„‚)
129125, 127, 128subsub4d 8298 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘€ โˆ’ ๐‘˜) โˆ’ 1) = (๐‘€ โˆ’ (๐‘˜ + 1)))
130129oveq2d 5890 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ดโ†‘((๐‘€ โˆ’ ๐‘˜) โˆ’ 1)) = (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1))))
13133recnd 7985 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
132131ad2antrr 488 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐ด โˆˆ โ„‚)
13333, 34gt0ap0d 8585 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ด # 0)
134133ad2antrr 488 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐ด # 0)
135119, 90zsubcld 9379 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘€ โˆ’ ๐‘˜) โˆˆ โ„ค)
136132, 134, 135expm1apd 10663 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ดโ†‘((๐‘€ โˆ’ ๐‘˜) โˆ’ 1)) = ((๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) / ๐ด))
137130, 136eqtr3d 2212 . . . . . . . . . . . . 13 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1))) = ((๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) / ๐ด))
138137oveq2d 5890 . . . . . . . . . . . 12 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))) = ((๐นโ€˜๐‘€) / ((๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) / ๐ด)))
139138adantr 276 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))) = ((๐นโ€˜๐‘€) / ((๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) / ๐ด)))
140 simpr 110 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐‘˜ + 1) < ๐‘€)
141140iftrued 3541 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))) = ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))))
142126nnred 8931 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„)
143142adantr 276 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘˜ โˆˆ โ„)
144 peano2re 8092 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ โ„ โ†’ (๐‘˜ + 1) โˆˆ โ„)
145143, 144syl 14 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐‘˜ + 1) โˆˆ โ„)
14616ad3antrrr 492 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘€ โˆˆ โ„)
147143ltp1d 8886 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘˜ < (๐‘˜ + 1))
148143, 145, 146, 147, 140lttrd 8082 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ๐‘˜ < ๐‘€)
149148iftrued 3541 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) = ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))))
150149oveq2d 5890 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜))) = (๐ด ยท ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)))))
15131ad2antrr 488 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐นโ€˜๐‘€) โˆˆ โ„‚)
152132, 134, 135expclzapd 10658 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) โˆˆ โ„‚)
153132, 134, 135expap0d 10659 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) # 0)
154151, 152, 132, 153, 134divdivap2d 8779 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐นโ€˜๐‘€) / ((๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) / ๐ด)) = (((๐นโ€˜๐‘€) ยท ๐ด) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))))
155151, 132mulcomd 7978 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐นโ€˜๐‘€) ยท ๐ด) = (๐ด ยท (๐นโ€˜๐‘€)))
156155oveq1d 5889 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (((๐นโ€˜๐‘€) ยท ๐ด) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))) = ((๐ด ยท (๐นโ€˜๐‘€)) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))))
157132, 151, 152, 153divassapd 8782 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐ด ยท (๐นโ€˜๐‘€)) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))) = (๐ด ยท ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)))))
158154, 156, 1573eqtrd 2214 . . . . . . . . . . . . 13 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐นโ€˜๐‘€) / ((๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) / ๐ด)) = (๐ด ยท ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)))))
159158adantr 276 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ((๐นโ€˜๐‘€) / ((๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) / ๐ด)) = (๐ด ยท ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)))))
160150, 159eqtr4d 2213 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜))) = ((๐นโ€˜๐‘€) / ((๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) / ๐ด)))
161139, 141, 1603eqtr4d 2220 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))) = (๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜))))
162161fveq2d 5519 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) = (absโ€˜(๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
163132, 62absmuld 11202 . . . . . . . . . 10 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜(๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = ((absโ€˜๐ด) ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
164163adantr 276 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (absโ€˜(๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = ((absโ€˜๐ด) ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
16535rpge0d 9699 . . . . . . . . . . . 12 (๐œ‘ โ†’ 0 โ‰ค ๐ด)
16633, 165absidd 11175 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜๐ด) = ๐ด)
167166oveq1d 5889 . . . . . . . . . 10 (๐œ‘ โ†’ ((absโ€˜๐ด) ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
168167ad3antrrr 492 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ ((absโ€˜๐ด) ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
169162, 164, 1683eqtrd 2214 . . . . . . . 8 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
170 eqle 8048 . . . . . . . 8 (((absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) โˆˆ โ„ โˆง (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜))))) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) โ‰ค (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
171123, 169, 170syl2an2r 595 . . . . . . 7 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) < ๐‘€) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) โ‰ค (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
17216ad2antrr 488 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„)
173111, 172lttri3d 8071 . . . . . . . . . . . . 13 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘˜ + 1) = ๐‘€ โ†” (ยฌ (๐‘˜ + 1) < ๐‘€ โˆง ยฌ ๐‘€ < (๐‘˜ + 1))))
174173simprbda 383 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ยฌ (๐‘˜ + 1) < ๐‘€)
175174iffalsed 3544 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))) = (๐นโ€˜(๐‘˜ + 1)))
176 simpr 110 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐‘˜ + 1) = ๐‘€)
177176fveq2d 5519 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐นโ€˜(๐‘˜ + 1)) = (๐นโ€˜๐‘€))
178175, 177eqtrd 2210 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))) = (๐นโ€˜๐‘€))
179178fveq2d 5519 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) = (absโ€˜(๐นโ€˜๐‘€)))
180142adantr 276 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ๐‘˜ โˆˆ โ„)
181180ltp1d 8886 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ๐‘˜ < (๐‘˜ + 1))
182 breq2 4007 . . . . . . . . . . . . . . . 16 ((๐‘˜ + 1) = ๐‘€ โ†’ (๐‘˜ < (๐‘˜ + 1) โ†” ๐‘˜ < ๐‘€))
183182adantl 277 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐‘˜ < (๐‘˜ + 1) โ†” ๐‘˜ < ๐‘€))
184181, 183mpbid 147 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ๐‘˜ < ๐‘€)
185184iftrued 3541 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) = ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))))
186176oveq1d 5889 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ((๐‘˜ + 1) โˆ’ ๐‘˜) = (๐‘€ โˆ’ ๐‘˜))
187127adantr 276 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ๐‘˜ โˆˆ โ„‚)
188 1cnd 7972 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ 1 โˆˆ โ„‚)
189187, 188pncan2d 8269 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ((๐‘˜ + 1) โˆ’ ๐‘˜) = 1)
190186, 189eqtr3d 2212 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐‘€ โˆ’ ๐‘˜) = 1)
191190oveq2d 5890 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) = (๐ดโ†‘1))
192132adantr 276 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ๐ด โˆˆ โ„‚)
193192exp1d 10648 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐ดโ†‘1) = ๐ด)
194191, 193eqtrd 2210 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜)) = ๐ด)
195194oveq2d 5890 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))) = ((๐นโ€˜๐‘€) / ๐ด))
196185, 195eqtrd 2210 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) = ((๐นโ€˜๐‘€) / ๐ด))
197196oveq2d 5890 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜))) = (๐ด ยท ((๐นโ€˜๐‘€) / ๐ด)))
19831, 131, 133divcanap2d 8748 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ด ยท ((๐นโ€˜๐‘€) / ๐ด)) = (๐นโ€˜๐‘€))
199198ad3antrrr 492 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐ด ยท ((๐นโ€˜๐‘€) / ๐ด)) = (๐นโ€˜๐‘€))
200197, 199eqtrd 2210 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜))) = (๐นโ€˜๐‘€))
201200fveq2d 5519 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (absโ€˜(๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = (absโ€˜(๐นโ€˜๐‘€)))
202167ad2antrr 488 . . . . . . . . . . 11 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((absโ€˜๐ด) ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
203163, 202eqtrd 2210 . . . . . . . . . 10 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜(๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
204203adantr 276 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (absโ€˜(๐ด ยท if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
205179, 201, 2043eqtr2d 2216 . . . . . . . 8 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
206123, 205, 170syl2an2r 595 . . . . . . 7 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง (๐‘˜ + 1) = ๐‘€) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) โ‰ค (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
207 simplll 533 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐œ‘)
208119adantr 276 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐‘€ โˆˆ โ„ค)
20990adantr 276 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
210 simpr 110 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐‘€ < (๐‘˜ + 1))
211 zleltp1 9307 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ โ„ค โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐‘€ โ‰ค ๐‘˜ โ†” ๐‘€ < (๐‘˜ + 1)))
212119, 209, 211syl2an2r 595 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ (๐‘€ โ‰ค ๐‘˜ โ†” ๐‘€ < (๐‘˜ + 1)))
213210, 212mpbird 167 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐‘€ โ‰ค ๐‘˜)
214208, 209, 213, 55syl3anbrc 1181 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
215214, 8eleqtrrdi 2271 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐‘˜ โˆˆ ๐‘)
216 cvgratz.7 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
217207, 215, 216syl2anc 411 . . . . . . . 8 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
218172adantr 276 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐‘€ โˆˆ โ„)
219111adantr 276 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ (๐‘˜ + 1) โˆˆ โ„)
220218, 219, 210ltnsymd 8076 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ยฌ (๐‘˜ + 1) < ๐‘€)
221220iffalsed 3544 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))) = (๐นโ€˜(๐‘˜ + 1)))
222221fveq2d 5519 . . . . . . . 8 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) = (absโ€˜(๐นโ€˜(๐‘˜ + 1))))
223142adantr 276 . . . . . . . . . . . 12 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ๐‘˜ โˆˆ โ„)
224218, 223, 213lensymd 8078 . . . . . . . . . . 11 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ ยฌ ๐‘˜ < ๐‘€)
225224iffalsed 3544 . . . . . . . . . 10 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)) = (๐นโ€˜๐‘˜))
226225fveq2d 5519 . . . . . . . . 9 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜))) = (absโ€˜(๐นโ€˜๐‘˜)))
227226oveq2d 5890 . . . . . . . 8 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))) = (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
228217, 222, 2273brtr4d 4035 . . . . . . 7 ((((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘€ < (๐‘˜ + 1)) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) โ‰ค (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
229 ztri3or 9295 . . . . . . . 8 (((๐‘˜ + 1) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((๐‘˜ + 1) < ๐‘€ โˆจ (๐‘˜ + 1) = ๐‘€ โˆจ ๐‘€ < (๐‘˜ + 1)))
230108, 119, 229syl2anc 411 . . . . . . 7 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘˜ + 1) < ๐‘€ โˆจ (๐‘˜ + 1) = ๐‘€ โˆจ ๐‘€ < (๐‘˜ + 1)))
231171, 206, 228, 230mpjao3dan 1307 . . . . . 6 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))) โ‰ค (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
232 breq1 4006 . . . . . . . . . 10 (๐‘– = (๐‘˜ + 1) โ†’ (๐‘– < ๐‘€ โ†” (๐‘˜ + 1) < ๐‘€))
233 oveq2 5882 . . . . . . . . . . . 12 (๐‘– = (๐‘˜ + 1) โ†’ (๐‘€ โˆ’ ๐‘–) = (๐‘€ โˆ’ (๐‘˜ + 1)))
234233oveq2d 5890 . . . . . . . . . . 11 (๐‘– = (๐‘˜ + 1) โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘–)) = (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1))))
235234oveq2d 5890 . . . . . . . . . 10 (๐‘– = (๐‘˜ + 1) โ†’ ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))) = ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))))
236 fveq2 5515 . . . . . . . . . 10 (๐‘– = (๐‘˜ + 1) โ†’ (๐นโ€˜๐‘–) = (๐นโ€˜(๐‘˜ + 1)))
237232, 235, 236ifbieq12d 3560 . . . . . . . . 9 (๐‘– = (๐‘˜ + 1) โ†’ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)) = if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))))
238237, 70fvmptg 5592 . . . . . . . 8 (((๐‘˜ + 1) โˆˆ โ„• โˆง if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))) โˆˆ โ„‚) โ†’ ((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜(๐‘˜ + 1)) = if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))))
239107, 122, 238syl2anc 411 . . . . . . 7 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜(๐‘˜ + 1)) = if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1))))
240239fveq2d 5519 . . . . . 6 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜(๐‘˜ + 1))) = (absโ€˜if((๐‘˜ + 1) < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ (๐‘˜ + 1)))), (๐นโ€˜(๐‘˜ + 1)))))
241126, 62, 71syl2anc 411 . . . . . . . 8 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜) = if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))
242241fveq2d 5519 . . . . . . 7 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜)) = (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜))))
243242oveq2d 5890 . . . . . 6 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ด ยท (absโ€˜((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜))) = (๐ด ยท (absโ€˜if(๐‘˜ < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘˜))), (๐นโ€˜๐‘˜)))))
244231, 240, 2433brtr4d 4035 . . . . 5 (((๐œ‘ โˆง 1 โ‰ค ๐‘€) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜((๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))โ€˜๐‘˜))))
24579, 81, 82, 86, 244cvgratnn 11538 . . . 4 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ seq1( + , (๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))) โˆˆ dom โ‡ )
246 eqid 2177 . . . . 5 (โ„คโ‰ฅโ€˜1) = (โ„คโ‰ฅโ€˜1)
247 1zzd 9279 . . . . . 6 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ 1 โˆˆ โ„ค)
248 simpr 110 . . . . . 6 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ 1 โ‰ค ๐‘€)
249 eluz2 9533 . . . . . 6 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜1) โ†” (1 โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง 1 โ‰ค ๐‘€))
250247, 2, 248, 249syl3anbrc 1181 . . . . 5 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜1))
251246, 250, 85iserex 11346 . . . 4 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ (seq1( + , (๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))) โˆˆ dom โ‡ โ†” seq๐‘€( + , (๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))) โˆˆ dom โ‡ ))
252245, 251mpbid 147 . . 3 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ seq๐‘€( + , (๐‘– โˆˆ โ„• โ†ฆ if(๐‘– < ๐‘€, ((๐นโ€˜๐‘€) / (๐ดโ†‘(๐‘€ โˆ’ ๐‘–))), (๐นโ€˜๐‘–)))) โˆˆ dom โ‡ )
25378, 252eqeltrd 2254 . 2 ((๐œ‘ โˆง 1 โ‰ค ๐‘€) โ†’ seq๐‘€( + , ๐น) โˆˆ dom โ‡ )
25433adantr 276 . . . 4 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ ๐ด โˆˆ โ„)
25580adantr 276 . . . 4 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ ๐ด < 1)
25634adantr 276 . . . 4 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ 0 < ๐ด)
2571adantr 276 . . . . . . 7 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ ๐‘€ โˆˆ โ„ค)
258257adantr 276 . . . . . 6 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„ค)
259 nnz 9271 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„ค)
260259adantl 277 . . . . . 6 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„ค)
261258zred 9374 . . . . . . 7 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„)
262 1red 7971 . . . . . . 7 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ 1 โˆˆ โ„)
263260zred 9374 . . . . . . 7 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„)
264 simplr 528 . . . . . . 7 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘€ โ‰ค 1)
265 nnge1 8941 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ 1 โ‰ค ๐‘˜)
266265adantl 277 . . . . . . 7 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ 1 โ‰ค ๐‘˜)
267261, 262, 263, 264, 266letrd 8080 . . . . . 6 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘€ โ‰ค ๐‘˜)
268258, 260, 267, 55syl3anbrc 1181 . . . . 5 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
2698eleq2i 2244 . . . . . . 7 (๐‘˜ โˆˆ ๐‘ โ†” ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
270269, 5sylan2br 288 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
271270adantlr 477 . . . . 5 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
272268, 271syldan 282 . . . 4 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
273269, 216sylan2br 288 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
274273adantlr 477 . . . . 5 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
275268, 274syldan 282 . . . 4 (((๐œ‘ โˆง ๐‘€ โ‰ค 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
276254, 255, 256, 272, 275cvgratnn 11538 . . 3 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
277 eqid 2177 . . . 4 (โ„คโ‰ฅโ€˜๐‘€) = (โ„คโ‰ฅโ€˜๐‘€)
278 1zzd 9279 . . . . 5 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ 1 โˆˆ โ„ค)
279 simpr 110 . . . . 5 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ ๐‘€ โ‰ค 1)
280 eluz2 9533 . . . . 5 (1 โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†” (๐‘€ โˆˆ โ„ค โˆง 1 โˆˆ โ„ค โˆง ๐‘€ โ‰ค 1))
281257, 278, 279, 280syl3anbrc 1181 . . . 4 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ 1 โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
282277, 281, 271iserex 11346 . . 3 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ (seq๐‘€( + , ๐น) โˆˆ dom โ‡ โ†” seq1( + , ๐น) โˆˆ dom โ‡ ))
283276, 282mpbird 167 . 2 ((๐œ‘ โˆง ๐‘€ โ‰ค 1) โ†’ seq๐‘€( + , ๐น) โˆˆ dom โ‡ )
284 1z 9278 . . 3 1 โˆˆ โ„ค
285 zletric 9296 . . 3 ((1 โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ (1 โ‰ค ๐‘€ โˆจ ๐‘€ โ‰ค 1))
286284, 1, 285sylancr 414 . 2 (๐œ‘ โ†’ (1 โ‰ค ๐‘€ โˆจ ๐‘€ โ‰ค 1))
287253, 283, 286mpjaodan 798 1 (๐œ‘ โ†’ seq๐‘€( + , ๐น) โˆˆ dom โ‡ )
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 708  DECID wdc 834   โˆจ w3o 977   = wceq 1353   โˆˆ wcel 2148  โˆ€wral 2455  ifcif 3534   class class class wbr 4003   โ†ฆ cmpt 4064  dom cdm 4626  โ€˜cfv 5216  (class class class)co 5874  โ„‚cc 7808  โ„cr 7809  0cc0 7810  1c1 7811   + caddc 7813   ยท cmul 7815   < clt 7991   โ‰ค cle 7992   โˆ’ cmin 8127   # cap 8537   / cdiv 8628  โ„•cn 8918  โ„คcz 9252  โ„คโ‰ฅcuz 9527  โ„+crp 9652  seqcseq 10444  โ†‘cexp 10518  abscabs 11005   โ‡ cli 11285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928  ax-arch 7929  ax-caucvg 7930
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-frec 6391  df-1o 6416  df-oadd 6420  df-er 6534  df-en 6740  df-dom 6741  df-fin 6742  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-3 8978  df-4 8979  df-n0 9176  df-z 9253  df-uz 9528  df-q 9619  df-rp 9653  df-ico 9893  df-fz 10008  df-fzo 10142  df-seqfrec 10445  df-exp 10519  df-ihash 10755  df-cj 10850  df-re 10851  df-im 10852  df-rsqrt 11006  df-abs 11007  df-clim 11286  df-sumdc 11361
This theorem is referenced by:  cvgratgt0  11540
  Copyright terms: Public domain W3C validator