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

Theorem cvgratnnlemmn 11533
Description: Lemma for cvgratnn 11539. (Contributed by Jim Kingdon, 15-Nov-2022.)
Hypotheses
Ref Expression
cvgratnn.3 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
cvgratnn.4 (๐œ‘ โ†’ ๐ด < 1)
cvgratnn.gt0 (๐œ‘ โ†’ 0 < ๐ด)
cvgratnn.6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
cvgratnn.7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
cvgratnn.m (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
cvgratnn.n (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
Assertion
Ref Expression
cvgratnnlemmn (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ โˆ’ ๐‘€))))
Distinct variable groups:   ๐ด,๐‘˜   ๐‘˜,๐น   ๐‘˜,๐‘   ๐œ‘,๐‘˜   ๐‘˜,๐‘€

Proof of Theorem cvgratnnlemmn
Dummy variables ๐‘› ๐‘ค are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvgratnn.n . 2 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
2 2fveq3 5521 . . . . 5 (๐‘ค = ๐‘€ โ†’ (absโ€˜(๐นโ€˜๐‘ค)) = (absโ€˜(๐นโ€˜๐‘€)))
3 oveq1 5882 . . . . . . 7 (๐‘ค = ๐‘€ โ†’ (๐‘ค โˆ’ ๐‘€) = (๐‘€ โˆ’ ๐‘€))
43oveq2d 5891 . . . . . 6 (๐‘ค = ๐‘€ โ†’ (๐ดโ†‘(๐‘ค โˆ’ ๐‘€)) = (๐ดโ†‘(๐‘€ โˆ’ ๐‘€)))
54oveq2d 5891 . . . . 5 (๐‘ค = ๐‘€ โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€))) = ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘€ โˆ’ ๐‘€))))
62, 5breq12d 4017 . . . 4 (๐‘ค = ๐‘€ โ†’ ((absโ€˜(๐นโ€˜๐‘ค)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€))) โ†” (absโ€˜(๐นโ€˜๐‘€)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘€ โˆ’ ๐‘€)))))
76imbi2d 230 . . 3 (๐‘ค = ๐‘€ โ†’ ((๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘ค)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€)))) โ†” (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘€)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘€ โˆ’ ๐‘€))))))
8 2fveq3 5521 . . . . 5 (๐‘ค = ๐‘˜ โ†’ (absโ€˜(๐นโ€˜๐‘ค)) = (absโ€˜(๐นโ€˜๐‘˜)))
9 oveq1 5882 . . . . . . 7 (๐‘ค = ๐‘˜ โ†’ (๐‘ค โˆ’ ๐‘€) = (๐‘˜ โˆ’ ๐‘€))
109oveq2d 5891 . . . . . 6 (๐‘ค = ๐‘˜ โ†’ (๐ดโ†‘(๐‘ค โˆ’ ๐‘€)) = (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))
1110oveq2d 5891 . . . . 5 (๐‘ค = ๐‘˜ โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€))) = ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))))
128, 11breq12d 4017 . . . 4 (๐‘ค = ๐‘˜ โ†’ ((absโ€˜(๐นโ€˜๐‘ค)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€))) โ†” (absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))))
1312imbi2d 230 . . 3 (๐‘ค = ๐‘˜ โ†’ ((๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘ค)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€)))) โ†” (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))))))
14 2fveq3 5521 . . . . 5 (๐‘ค = (๐‘˜ + 1) โ†’ (absโ€˜(๐นโ€˜๐‘ค)) = (absโ€˜(๐นโ€˜(๐‘˜ + 1))))
15 oveq1 5882 . . . . . . 7 (๐‘ค = (๐‘˜ + 1) โ†’ (๐‘ค โˆ’ ๐‘€) = ((๐‘˜ + 1) โˆ’ ๐‘€))
1615oveq2d 5891 . . . . . 6 (๐‘ค = (๐‘˜ + 1) โ†’ (๐ดโ†‘(๐‘ค โˆ’ ๐‘€)) = (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))
1716oveq2d 5891 . . . . 5 (๐‘ค = (๐‘˜ + 1) โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€))) = ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))))
1814, 17breq12d 4017 . . . 4 (๐‘ค = (๐‘˜ + 1) โ†’ ((absโ€˜(๐นโ€˜๐‘ค)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€))) โ†” (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))))
1918imbi2d 230 . . 3 (๐‘ค = (๐‘˜ + 1) โ†’ ((๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘ค)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€)))) โ†” (๐œ‘ โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))))))
20 2fveq3 5521 . . . . 5 (๐‘ค = ๐‘ โ†’ (absโ€˜(๐นโ€˜๐‘ค)) = (absโ€˜(๐นโ€˜๐‘)))
21 oveq1 5882 . . . . . . 7 (๐‘ค = ๐‘ โ†’ (๐‘ค โˆ’ ๐‘€) = (๐‘ โˆ’ ๐‘€))
2221oveq2d 5891 . . . . . 6 (๐‘ค = ๐‘ โ†’ (๐ดโ†‘(๐‘ค โˆ’ ๐‘€)) = (๐ดโ†‘(๐‘ โˆ’ ๐‘€)))
2322oveq2d 5891 . . . . 5 (๐‘ค = ๐‘ โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€))) = ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ โˆ’ ๐‘€))))
2420, 23breq12d 4017 . . . 4 (๐‘ค = ๐‘ โ†’ ((absโ€˜(๐นโ€˜๐‘ค)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€))) โ†” (absโ€˜(๐นโ€˜๐‘)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ โˆ’ ๐‘€)))))
2524imbi2d 230 . . 3 (๐‘ค = ๐‘ โ†’ ((๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘ค)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ค โˆ’ ๐‘€)))) โ†” (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ โˆ’ ๐‘€))))))
26 fveq2 5516 . . . . . . . . 9 (๐‘˜ = ๐‘€ โ†’ (๐นโ€˜๐‘˜) = (๐นโ€˜๐‘€))
2726eleq1d 2246 . . . . . . . 8 (๐‘˜ = ๐‘€ โ†’ ((๐นโ€˜๐‘˜) โˆˆ โ„‚ โ†” (๐นโ€˜๐‘€) โˆˆ โ„‚))
28 cvgratnn.6 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
2928ralrimiva 2550 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐นโ€˜๐‘˜) โˆˆ โ„‚)
30 cvgratnn.m . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
3127, 29, 30rspcdva 2847 . . . . . . 7 (๐œ‘ โ†’ (๐นโ€˜๐‘€) โˆˆ โ„‚)
3231abscld 11190 . . . . . 6 (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘€)) โˆˆ โ„)
3332leidd 8471 . . . . 5 (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘€)) โ‰ค (absโ€˜(๐นโ€˜๐‘€)))
3430nncnd 8933 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
3534subidd 8256 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘€ โˆ’ ๐‘€) = 0)
3635oveq2d 5891 . . . . . . . 8 (๐œ‘ โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘€)) = (๐ดโ†‘0))
37 cvgratnn.3 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
3837recnd 7986 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
3938exp0d 10648 . . . . . . . 8 (๐œ‘ โ†’ (๐ดโ†‘0) = 1)
4036, 39eqtrd 2210 . . . . . . 7 (๐œ‘ โ†’ (๐ดโ†‘(๐‘€ โˆ’ ๐‘€)) = 1)
4140oveq2d 5891 . . . . . 6 (๐œ‘ โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘€ โˆ’ ๐‘€))) = ((absโ€˜(๐นโ€˜๐‘€)) ยท 1))
4232recnd 7986 . . . . . . 7 (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘€)) โˆˆ โ„‚)
4342mulridd 7974 . . . . . 6 (๐œ‘ โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท 1) = (absโ€˜(๐นโ€˜๐‘€)))
4441, 43eqtrd 2210 . . . . 5 (๐œ‘ โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘€ โˆ’ ๐‘€))) = (absโ€˜(๐นโ€˜๐‘€)))
4533, 44breqtrrd 4032 . . . 4 (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘€)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘€ โˆ’ ๐‘€))))
4645a1i 9 . . 3 (๐‘€ โˆˆ โ„ค โ†’ (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘€)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘€ โˆ’ ๐‘€)))))
47 eluznn 9600 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘˜ โˆˆ โ„•)
4830, 47sylan 283 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘˜ โˆˆ โ„•)
4948, 28syldan 282 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
5049abscld 11190 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (absโ€˜(๐นโ€˜๐‘˜)) โˆˆ โ„)
5132adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (absโ€˜(๐นโ€˜๐‘€)) โˆˆ โ„)
5237adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐ด โˆˆ โ„)
53 uznn0sub 9559 . . . . . . . . . . 11 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ (๐‘˜ โˆ’ ๐‘€) โˆˆ โ„•0)
5453adantl 277 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐‘˜ โˆ’ ๐‘€) โˆˆ โ„•0)
5552, 54reexpcld 10671 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)) โˆˆ โ„)
5651, 55remulcld 7988 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) โˆˆ โ„)
57 0red 7958 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ 0 โˆˆ โ„)
58 cvgratnn.gt0 . . . . . . . . . 10 (๐œ‘ โ†’ 0 < ๐ด)
5958adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ 0 < ๐ด)
6057, 52, 59ltled 8076 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ 0 โ‰ค ๐ด)
61 lemul2a 8816 . . . . . . . . 9 ((((absโ€˜(๐นโ€˜๐‘˜)) โˆˆ โ„ โˆง ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) โˆˆ โ„ โˆง (๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด)) โˆง (absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))) โ†’ (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค (๐ด ยท ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))))
6261ex 115 . . . . . . . 8 (((absโ€˜(๐นโ€˜๐‘˜)) โˆˆ โ„ โˆง ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) โˆˆ โ„ โˆง (๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด)) โ†’ ((absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) โ†’ (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค (๐ด ยท ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))))))
6350, 56, 52, 60, 62syl112anc 1242 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) โ†’ (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค (๐ด ยท ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))))))
6438adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐ด โˆˆ โ„‚)
6542adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (absโ€˜(๐นโ€˜๐‘€)) โˆˆ โ„‚)
6655recnd 7986 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)) โˆˆ โ„‚)
6764, 65, 66mul12d 8109 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ด ยท ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))) = ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ด ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))))
6864, 54expp1d 10655 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ดโ†‘((๐‘˜ โˆ’ ๐‘€) + 1)) = ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)) ยท ๐ด))
6948nncnd 8933 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘˜ โˆˆ โ„‚)
70 1cnd 7973 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ 1 โˆˆ โ„‚)
71 eluzel2 9533 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ ๐‘€ โˆˆ โ„ค)
7271adantl 277 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘€ โˆˆ โ„ค)
7372zcnd 9376 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘€ โˆˆ โ„‚)
7469, 70, 73addsubd 8289 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((๐‘˜ + 1) โˆ’ ๐‘€) = ((๐‘˜ โˆ’ ๐‘€) + 1))
7574oveq2d 5891 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)) = (๐ดโ†‘((๐‘˜ โˆ’ ๐‘€) + 1)))
7664, 66mulcomd 7979 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ด ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) = ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)) ยท ๐ด))
7768, 75, 763eqtr4rd 2221 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ด ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) = (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))
7877oveq2d 5891 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ด ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))) = ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))))
7967, 78eqtrd 2210 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ด ยท ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))) = ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))))
8079breq2d 4016 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค (๐ด ยท ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))) โ†” (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))))
8163, 80sylibd 149 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) โ†’ (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))))
82 cvgratnn.7 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
8348, 82syldan 282 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))))
84 fveq2 5516 . . . . . . . . . . 11 (๐‘› = (๐‘˜ + 1) โ†’ (๐นโ€˜๐‘›) = (๐นโ€˜(๐‘˜ + 1)))
8584eleq1d 2246 . . . . . . . . . 10 (๐‘› = (๐‘˜ + 1) โ†’ ((๐นโ€˜๐‘›) โˆˆ โ„‚ โ†” (๐นโ€˜(๐‘˜ + 1)) โˆˆ โ„‚))
86 fveq2 5516 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘› โ†’ (๐นโ€˜๐‘˜) = (๐นโ€˜๐‘›))
8786eleq1d 2246 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘› โ†’ ((๐นโ€˜๐‘˜) โˆˆ โ„‚ โ†” (๐นโ€˜๐‘›) โˆˆ โ„‚))
8887cbvralv 2704 . . . . . . . . . . . 12 (โˆ€๐‘˜ โˆˆ โ„• (๐นโ€˜๐‘˜) โˆˆ โ„‚ โ†” โˆ€๐‘› โˆˆ โ„• (๐นโ€˜๐‘›) โˆˆ โ„‚)
8929, 88sylib 122 . . . . . . . . . . 11 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ โ„• (๐นโ€˜๐‘›) โˆˆ โ„‚)
9089adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ โˆ€๐‘› โˆˆ โ„• (๐นโ€˜๐‘›) โˆˆ โ„‚)
9148peano2nnd 8934 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐‘˜ + 1) โˆˆ โ„•)
9285, 90, 91rspcdva 2847 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜(๐‘˜ + 1)) โˆˆ โ„‚)
9392abscld 11190 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โˆˆ โ„)
9452, 50remulcld 7988 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โˆˆ โ„)
95 peano2uz 9583 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ (๐‘˜ + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
9695adantl 277 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐‘˜ + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
97 uznn0sub 9559 . . . . . . . . . . 11 ((๐‘˜ + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ ((๐‘˜ + 1) โˆ’ ๐‘€) โˆˆ โ„•0)
9896, 97syl 14 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((๐‘˜ + 1) โˆ’ ๐‘€) โˆˆ โ„•0)
9952, 98reexpcld 10671 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)) โˆˆ โ„)
10051, 99remulcld 7988 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))) โˆˆ โ„)
101 letr 8040 . . . . . . . 8 (((absโ€˜(๐นโ€˜(๐‘˜ + 1))) โˆˆ โ„ โˆง (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โˆˆ โ„ โˆง ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))) โˆˆ โ„) โ†’ (((absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โˆง (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))))
10293, 94, 100, 101syl3anc 1238 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (((absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โˆง (๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))))
10383, 102mpand 429 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((๐ด ยท (absโ€˜(๐นโ€˜๐‘˜))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))))
10481, 103syld 45 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€)))))
105104expcom 116 . . . 4 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ (๐œ‘ โ†’ ((absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€))) โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))))))
106105a2d 26 . . 3 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ ((๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘˜)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘˜ โˆ’ ๐‘€)))) โ†’ (๐œ‘ โ†’ (absโ€˜(๐นโ€˜(๐‘˜ + 1))) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘((๐‘˜ + 1) โˆ’ ๐‘€))))))
1077, 13, 19, 25, 46, 106uzind4 9588 . 2 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ โˆ’ ๐‘€)))))
1081, 107mpcom 36 1 (๐œ‘ โ†’ (absโ€˜(๐นโ€˜๐‘)) โ‰ค ((absโ€˜(๐นโ€˜๐‘€)) ยท (๐ดโ†‘(๐‘ โˆ’ ๐‘€))))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148  โˆ€wral 2455   class class class wbr 4004  โ€˜cfv 5217  (class class class)co 5875  โ„‚cc 7809  โ„cr 7810  0cc0 7811  1c1 7812   + caddc 7814   ยท cmul 7816   < clt 7992   โ‰ค cle 7993   โˆ’ cmin 8128  โ„•cn 8919  โ„•0cn0 9176  โ„คcz 9253  โ„คโ‰ฅcuz 9528  โ†‘cexp 10519  abscabs 11006
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 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-mulrcl 7910  ax-addcom 7911  ax-mulcom 7912  ax-addass 7913  ax-mulass 7914  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-1rid 7918  ax-0id 7919  ax-rnegex 7920  ax-precex 7921  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-apti 7926  ax-pre-ltadd 7927  ax-pre-mulgt0 7928  ax-pre-mulext 7929  ax-arch 7930  ax-caucvg 7931
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 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-if 3536  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-po 4297  df-iso 4298  df-iord 4367  df-on 4369  df-ilim 4370  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-frec 6392  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-sub 8130  df-neg 8131  df-reap 8532  df-ap 8539  df-div 8630  df-inn 8920  df-2 8978  df-3 8979  df-4 8980  df-n0 9177  df-z 9254  df-uz 9529  df-rp 9654  df-seqfrec 10446  df-exp 10520  df-cj 10851  df-re 10852  df-im 10853  df-rsqrt 11007  df-abs 11008
This theorem is referenced by:  cvgratnnlemabsle  11535
  Copyright terms: Public domain W3C validator