Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stirlinglem3 Structured version   Visualization version   GIF version

Theorem stirlinglem3 45523
Description: Long but simple algebraic transformations are applied to show that ๐‘‰, the Wallis formula for ฯ€ , can be expressed in terms of ๐ด, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the ๐ด, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem3.1 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
stirlinglem3.2 ๐ท = (๐‘› โˆˆ โ„• โ†ฆ (๐ดโ€˜(2 ยท ๐‘›)))
stirlinglem3.3 ๐ธ = (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
stirlinglem3.4 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1)))
Assertion
Ref Expression
stirlinglem3 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))

Proof of Theorem stirlinglem3
Dummy variable ๐‘š is distinct from all other variables.
StepHypRef Expression
1 stirlinglem3.4 . 2 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1)))
2 nnnn0 12504 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•0)
3 faccl 14269 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„•0 โ†’ (!โ€˜๐‘›) โˆˆ โ„•)
4 nncn 12245 . . . . . . . . . . . . 13 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ (!โ€˜๐‘›) โˆˆ โ„‚)
52, 3, 43syl 18 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (!โ€˜๐‘›) โˆˆ โ„‚)
6 2cnd 12315 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„‚)
7 nncn 12245 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„‚)
86, 7mulcld 11259 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„‚)
98sqrtcld 15411 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
10 ere 16060 . . . . . . . . . . . . . . . . 17 e โˆˆ โ„
1110recni 11253 . . . . . . . . . . . . . . . 16 e โˆˆ โ„‚
1211a1i 11 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ e โˆˆ โ„‚)
13 epos 16178 . . . . . . . . . . . . . . . . 17 0 < e
1410, 13gt0ne0ii 11775 . . . . . . . . . . . . . . . 16 e โ‰  0
1514a1i 11 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ e โ‰  0)
167, 12, 15divcld 12015 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (๐‘› / e) โˆˆ โ„‚)
1716, 2expcld 14137 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘๐‘›) โˆˆ โ„‚)
189, 17mulcld 11259 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โˆˆ โ„‚)
19 2rp 13006 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„+
2019a1i 11 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„+)
21 nnrp 13012 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„+)
2220, 21rpmulcld 13059 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„+)
2322sqrtgt0d 15386 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ 0 < (โˆšโ€˜(2 ยท ๐‘›)))
2423gt0ne0d 11803 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท ๐‘›)) โ‰  0)
25 nnne0 12271 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ๐‘› โ‰  0)
267, 12, 25, 15divne0d 12031 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (๐‘› / e) โ‰  0)
27 nnz 12604 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„ค)
2816, 26, 27expne0d 14143 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘๐‘›) โ‰  0)
299, 17, 24, 28mulne0d 11891 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โ‰  0)
305, 18, 29divcld 12015 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) โˆˆ โ„‚)
31 stirlinglem3.1 . . . . . . . . . . . 12 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3231fvmpt2 7009 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘›) = ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3330, 32mpdan 685 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜๐‘›) = ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3433oveq1d 7428 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜๐‘›)โ†‘4) = (((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4))
35 stirlinglem3.3 . . . . . . . . . . . 12 ๐ธ = (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3635fvmpt2 7009 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โˆˆ โ„‚) โ†’ (๐ธโ€˜๐‘›) = ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3718, 36mpdan 685 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜๐‘›) = ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3837oveq1d 7428 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜๐‘›)โ†‘4) = (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4))
3934, 38oveq12d 7431 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) = ((((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
40 4nn0 12516 . . . . . . . . . . 11 4 โˆˆ โ„•0
4140a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„•0)
425, 18, 29, 41expdivd 14151 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) = (((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
4342oveq1d 7428 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) = ((((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
445, 41expcld 14137 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
4518, 41expcld 14137 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) โˆˆ โ„‚)
4641nn0zd 12609 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„ค)
4718, 29, 46expne0d 14143 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) โ‰  0)
4844, 45, 47divcan1d 12016 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) = ((!โ€˜๐‘›)โ†‘4))
4939, 43, 483eqtrd 2769 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) = ((!โ€˜๐‘›)โ†‘4))
5049eqcomd 2731 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›)โ†‘4) = (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)))
5150oveq2d 7429 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) = ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))))
52 2nn0 12514 . . . . . . . . . . . . 13 2 โˆˆ โ„•0
5352a1i 11 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„•0)
5453, 2nn0mulcld 12562 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•0)
55 faccl 14269 . . . . . . . . . . 11 ((2 ยท ๐‘›) โˆˆ โ„•0 โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„•)
56 nncn 12245 . . . . . . . . . . 11 ((!โ€˜(2 ยท ๐‘›)) โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
5754, 55, 563syl 18 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
5857sqcld 14135 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
596, 8mulcld 11259 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) โˆˆ โ„‚)
6059sqrtcld 15411 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท (2 ยท ๐‘›))) โˆˆ โ„‚)
618, 12, 15divcld 12015 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) / e) โˆˆ โ„‚)
6261, 54expcld 14137 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)) โˆˆ โ„‚)
6360, 62mulcld 11259 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))) โˆˆ โ„‚)
6463sqcld 14135 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) โˆˆ โ„‚)
6520, 22rpmulcld 13059 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) โˆˆ โ„+)
6665sqrtgt0d 15386 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 0 < (โˆšโ€˜(2 ยท (2 ยท ๐‘›))))
6766gt0ne0d 11803 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท (2 ยท ๐‘›))) โ‰  0)
6820rpne0d 13048 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ 2 โ‰  0)
696, 7, 68, 25mulne0d 11891 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โ‰  0)
708, 12, 69, 15divne0d 12031 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) / e) โ‰  0)
71 2z 12619 . . . . . . . . . . . . . 14 2 โˆˆ โ„ค
7271a1i 11 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„ค)
7372, 27zmulcld 12697 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„ค)
7461, 70, 73expne0d 14143 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)) โ‰  0)
7560, 62, 67, 74mulne0d 11891 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))) โ‰  0)
7663, 75, 72expne0d 14143 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) โ‰  0)
7758, 64, 76divcan1d 12016 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = ((!โ€˜(2 ยท ๐‘›))โ†‘2))
7857, 63, 75, 53expdivd 14151 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) = (((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
7978eqcomd 2731 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2))
8079oveq1d 7428 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = ((((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
8177, 80eqtr3d 2767 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = ((((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
82 fveq2 6890 . . . . . . . . . . . . . 14 (๐‘› = ๐‘š โ†’ (!โ€˜๐‘›) = (!โ€˜๐‘š))
83 oveq2 7421 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ (2 ยท ๐‘›) = (2 ยท ๐‘š))
8483fveq2d 6894 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘š โ†’ (โˆšโ€˜(2 ยท ๐‘›)) = (โˆšโ€˜(2 ยท ๐‘š)))
85 oveq1 7420 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ (๐‘› / e) = (๐‘š / e))
86 id 22 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ ๐‘› = ๐‘š)
8785, 86oveq12d 7431 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘š โ†’ ((๐‘› / e)โ†‘๐‘›) = ((๐‘š / e)โ†‘๐‘š))
8884, 87oveq12d 7431 . . . . . . . . . . . . . 14 (๐‘› = ๐‘š โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) = ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))
8982, 88oveq12d 7431 . . . . . . . . . . . . 13 (๐‘› = ๐‘š โ†’ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
9089cbvmptv 5257 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))) = (๐‘š โˆˆ โ„• โ†ฆ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
9131, 90eqtri 2753 . . . . . . . . . . 11 ๐ด = (๐‘š โˆˆ โ„• โ†ฆ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
92 fveq2 6890 . . . . . . . . . . . 12 (๐‘š = (2 ยท ๐‘›) โ†’ (!โ€˜๐‘š) = (!โ€˜(2 ยท ๐‘›)))
93 oveq2 7421 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ (2 ยท ๐‘š) = (2 ยท (2 ยท ๐‘›)))
9493fveq2d 6894 . . . . . . . . . . . . 13 (๐‘š = (2 ยท ๐‘›) โ†’ (โˆšโ€˜(2 ยท ๐‘š)) = (โˆšโ€˜(2 ยท (2 ยท ๐‘›))))
95 oveq1 7420 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ (๐‘š / e) = ((2 ยท ๐‘›) / e))
96 id 22 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ ๐‘š = (2 ยท ๐‘›))
9795, 96oveq12d 7431 . . . . . . . . . . . . 13 (๐‘š = (2 ยท ๐‘›) โ†’ ((๐‘š / e)โ†‘๐‘š) = (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))
9894, 97oveq12d 7431 . . . . . . . . . . . 12 (๐‘š = (2 ยท ๐‘›) โ†’ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
9992, 98oveq12d 7431 . . . . . . . . . . 11 (๐‘š = (2 ยท ๐‘›) โ†’ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))) = ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))))
100 2nn 12310 . . . . . . . . . . . . 13 2 โˆˆ โ„•
101100a1i 11 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
102 id 22 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•)
103101, 102nnmulcld 12290 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•)
10457, 63, 75divcld 12015 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))) โˆˆ โ„‚)
10591, 99, 103, 104fvmptd3 7021 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) = ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))))
106105oveq1d 7428 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) = (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2))
107106eqcomd 2731 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) = ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2))
108107oveq1d 7428 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
109 eqidd 2726 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
11098adantl 480 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘š = (2 ยท ๐‘›)) โ†’ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
111109, 110, 103, 63fvmptd 7005 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
112111oveq1d 7428 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2))
113112eqcomd 2731 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) = (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2))
114113oveq2d 7429 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)))
11581, 108, 1143eqtrd 2769 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)))
11688cbvmptv 5257 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))
117116a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
118117fveq1d 6892 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)) = ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)))
119118eqcomd 2731 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)) = ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)))
120119oveq1d 7428 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2))
121120oveq2d 7429 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2)))
122105, 104eqeltrd 2825 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
123 stirlinglem3.2 . . . . . . . . . . 11 ๐ท = (๐‘› โˆˆ โ„• โ†ฆ (๐ดโ€˜(2 ยท ๐‘›)))
124123fvmpt2 7009 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง (๐ดโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚) โ†’ (๐ทโ€˜๐‘›) = (๐ดโ€˜(2 ยท ๐‘›)))
125122, 124mpdan 685 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) = (๐ดโ€˜(2 ยท ๐‘›)))
126125eqcomd 2731 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) = (๐ทโ€˜๐‘›))
127126oveq1d 7428 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) = ((๐ทโ€˜๐‘›)โ†‘2))
12835a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐ธ = (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
129128fveq1d 6892 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) = ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)))
130129eqcomd 2731 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)) = (๐ธโ€˜(2 ยท ๐‘›)))
131130oveq1d 7428 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2) = ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))
132127, 131oveq12d 7431 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2)) = (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))
133115, 121, 1323eqtrd 2769 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))
13451, 133oveq12d 7431 . . . 4 (๐‘› โˆˆ โ„• โ†’ (((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) = (((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
135134oveq1d 7428 . . 3 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1)) = ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
136135mpteq2ia 5247 . 2 (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1))) = (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
13741, 2nn0mulcld 12562 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (4 ยท ๐‘›) โˆˆ โ„•0)
1386, 137expcld 14137 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (2โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
13949, 44eqeltrd 2825 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) โˆˆ โ„‚)
140138, 139mulcomd 11260 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) = ((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))))
141140oveq1d 7428 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
142141oveq1d 7428 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
143125, 122eqeltrd 2825 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) โˆˆ โ„‚)
144143sqcld 14135 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ทโ€˜๐‘›)โ†‘2) โˆˆ โ„‚)
145128, 117eqtrd 2765 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐ธ = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
146145, 110, 103, 63fvmptd 7005 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
147146, 63eqeltrd 2825 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
148147sqcld 14135 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
149 nnne0 12271 . . . . . . . . . . . 12 ((!โ€˜(2 ยท ๐‘›)) โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โ‰  0)
15054, 55, 1493syl 18 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โ‰  0)
15157, 63, 150, 75divne0d 12031 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))) โ‰  0)
152105, 151eqnetrd 2998 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) โ‰  0)
153125, 152eqnetrd 2998 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) โ‰  0)
154143, 153, 72expne0d 14143 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ทโ€˜๐‘›)โ†‘2) โ‰  0)
155146, 75eqnetrd 2998 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) โ‰  0)
156147, 155, 72expne0d 14143 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) โ‰  0)
157139, 144, 138, 148, 154, 156divmuldivd 12056 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
158157eqcomd 2731 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
159158oveq1d 7428 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
16033, 30eqeltrd 2825 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜๐‘›) โˆˆ โ„‚)
161160, 41expcld 14137 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
16238, 45eqeltrd 2825 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
163161, 162, 144, 154div23d 12052 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)))
164163oveq1d 7428 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
165164oveq1d 7428 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
166161, 144, 154divcld 12015 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) โˆˆ โ„‚)
167138, 148, 156divcld 12015 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) โˆˆ โ„‚)
168166, 162, 167mulassd 11262 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))))
169168oveq1d 7428 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)))
170162, 167mulcld 11259 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) โˆˆ โ„‚)
171 1cnd 11234 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
1728, 171addcld 11258 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„‚)
173 0red 11242 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ 0 โˆˆ โ„)
174103nnred 12252 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„)
175 2re 12311 . . . . . . . . . . . 12 2 โˆˆ โ„
176175a1i 11 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„)
177 nnre 12244 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„)
178176, 177remulcld 11269 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„)
179 1red 11240 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„)
180178, 179readdcld 11268 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„)
181103nngt0d 12286 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ 0 < (2 ยท ๐‘›))
182174ltp1d 12169 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) < ((2 ยท ๐‘›) + 1))
183173, 174, 180, 181, 182lttrd 11400 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ 0 < ((2 ยท ๐‘›) + 1))
184183gt0ne0d 11803 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โ‰  0)
185166, 170, 172, 184divassd 12050 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))))
186162, 138, 148, 156div12d 12051 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
1879, 17, 41mulexpd 14152 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) ยท (((๐‘› / e)โ†‘๐‘›)โ†‘4)))
18860, 62sqmuld 14149 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) ยท ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))
189187, 188oveq12d 7431 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) ยท (((๐‘› / e)โ†‘๐‘›)โ†‘4)) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) ยท ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))))
190146oveq1d 7428 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2))
19138, 190oveq12d 7431 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
1929, 41expcld 14137 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) โˆˆ โ„‚)
19360sqcld 14135 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) โˆˆ โ„‚)
19417, 41expcld 14137 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((๐‘› / e)โ†‘๐‘›)โ†‘4) โˆˆ โ„‚)
19562sqcld 14135 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
19660, 67, 72expne0d 14143 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) โ‰  0)
19762, 74, 72expne0d 14143 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) โ‰  0)
198192, 193, 194, 195, 196, 197divmuldivd 12056 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))) = ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) ยท (((๐‘› / e)โ†‘๐‘›)โ†‘4)) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) ยท ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))))
199189, 191, 1983eqtr4d 2775 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))))
200199oveq2d 7429 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))))
20165rprege0d 13050 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท (2 ยท ๐‘›)) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท (2 ยท ๐‘›))))
202 resqrtth 15229 . . . . . . . . . . . . . . . 16 (((2 ยท (2 ยท ๐‘›)) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท (2 ยท ๐‘›))) โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) = (2 ยท (2 ยท ๐‘›)))
203201, 202syl 17 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) = (2 ยท (2 ยท ๐‘›)))
204203oveq2d 7429 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / (2 ยท (2 ยท ๐‘›))))
205 2t2e4 12401 . . . . . . . . . . . . . . . . . . 19 (2 ยท 2) = 4
206205eqcomi 2734 . . . . . . . . . . . . . . . . . 18 4 = (2 ยท 2)
207206a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 = (2 ยท 2))
208207oveq2d 7429 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) = ((โˆšโ€˜(2 ยท ๐‘›))โ†‘(2 ยท 2)))
2099, 53, 53expmuld 14140 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘(2 ยท 2)) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘2)โ†‘2))
21022rprege0d 13050 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท ๐‘›)))
211 resqrtth 15229 . . . . . . . . . . . . . . . . . 18 (((2 ยท ๐‘›) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท ๐‘›)) โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘2) = (2 ยท ๐‘›))
212210, 211syl 17 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘2) = (2 ยท ๐‘›))
213212oveq1d 7428 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘2)โ†‘2) = ((2 ยท ๐‘›)โ†‘2))
214208, 209, 2133eqtrd 2769 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) = ((2 ยท ๐‘›)โ†‘2))
2156, 6, 7mulassd 11262 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท 2) ยท ๐‘›) = (2 ยท (2 ยท ๐‘›)))
216205a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (2 ยท 2) = 4)
217216oveq1d 7428 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท 2) ยท ๐‘›) = (4 ยท ๐‘›))
218215, 217eqtr3d 2767 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) = (4 ยท ๐‘›))
219214, 218oveq12d 7431 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / (2 ยท (2 ยท ๐‘›))) = (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)))
2206, 7sqmuld 14149 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘2) = ((2โ†‘2) ยท (๐‘›โ†‘2)))
221 sq2 14187 . . . . . . . . . . . . . . . . . . 19 (2โ†‘2) = 4
222221a1i 11 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ (2โ†‘2) = 4)
223222oveq1d 7428 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘2) ยท (๐‘›โ†‘2)) = (4 ยท (๐‘›โ†‘2)))
224220, 223eqtrd 2765 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘2) = (4 ยท (๐‘›โ†‘2)))
225224oveq1d 7428 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)) = ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)))
226 4cn 12322 . . . . . . . . . . . . . . . . . . 19 4 โˆˆ โ„‚
227 4ne0 12345 . . . . . . . . . . . . . . . . . . 19 4 โ‰  0
228226, 227dividi 11972 . . . . . . . . . . . . . . . . . 18 (4 / 4) = 1
229228a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (4 / 4) = 1)
2307sqvald 14134 . . . . . . . . . . . . . . . . . . 19 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘2) = (๐‘› ยท ๐‘›))
231230oveq1d 7428 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘2) / ๐‘›) = ((๐‘› ยท ๐‘›) / ๐‘›))
2327, 7, 25divcan4d 12021 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((๐‘› ยท ๐‘›) / ๐‘›) = ๐‘›)
233231, 232eqtrd 2765 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘2) / ๐‘›) = ๐‘›)
234229, 233oveq12d 7431 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((4 / 4) ยท ((๐‘›โ†‘2) / ๐‘›)) = (1 ยท ๐‘›))
23541nn0cnd 12559 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„‚)
2367sqcld 14135 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘2) โˆˆ โ„‚)
237227a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 โ‰  0)
238235, 235, 236, 7, 237, 25divmuldivd 12056 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((4 / 4) ยท ((๐‘›โ†‘2) / ๐‘›)) = ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)))
2397mullidd 11257 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (1 ยท ๐‘›) = ๐‘›)
240234, 238, 2393eqtr3d 2773 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)) = ๐‘›)
241225, 240eqtrd 2765 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)) = ๐‘›)
242204, 219, 2413eqtrd 2769 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) = ๐‘›)
2437, 235mulcomd 11260 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท 4) = (4 ยท ๐‘›))
244243oveq2d 7429 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(๐‘› ยท 4)) = ((๐‘› / e)โ†‘(4 ยท ๐‘›)))
24516, 41, 2expmuld 14140 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(๐‘› ยท 4)) = (((๐‘› / e)โ†‘๐‘›)โ†‘4))
2467, 12, 15, 137expdivd 14151 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(4 ยท ๐‘›)) = ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
247244, 245, 2463eqtr3d 2773 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (((๐‘› / e)โ†‘๐‘›)โ†‘4) = ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
2486, 7, 6mul32d 11449 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) ยท 2) = ((2 ยท 2) ยท ๐‘›))
249248, 217eqtrd 2765 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) ยท 2) = (4 ยท ๐‘›))
250249oveq2d 7429 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘((2 ยท ๐‘›) ยท 2)) = (((2 ยท ๐‘›) / e)โ†‘(4 ยท ๐‘›)))
25161, 53, 54expmuld 14140 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘((2 ยท ๐‘›) ยท 2)) = ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))
2528, 12, 15, 137expdivd 14151 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(4 ยท ๐‘›)) = (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
253250, 251, 2523eqtr3d 2773 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) = (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
254247, 253oveq12d 7431 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)) = (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) / (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›)))))
255247, 194eqeltrrd 2826 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) โˆˆ โ„‚)
2568, 137expcld 14137 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
25712, 137expcld 14137 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (eโ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
25846, 27zmulcld 12697 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (4 ยท ๐‘›) โˆˆ โ„ค)
2598, 69, 258expne0d 14143 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) โ‰  0)
26012, 15, 258expne0d 14143 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (eโ†‘(4 ยท ๐‘›)) โ‰  0)
261255, 256, 257, 259, 260divdiv2d 12047 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) / (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›)))) = ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))))
2627, 137expcld 14137 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
263262, 257, 260divcan1d 12016 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) = (๐‘›โ†‘(4 ยท ๐‘›)))
264263oveq1d 7428 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))))
2656, 7, 137mulexpd 14152 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) = ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›))))
266265oveq2d 7429 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))))
267138, 262mulcomd 11260 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›))))
268267oveq2d 7429 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›)))))
2697, 25, 258expne0d 14143 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(4 ยท ๐‘›)) โ‰  0)
2706, 68, 258expne0d 14143 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (2โ†‘(4 ยท ๐‘›)) โ‰  0)
271262, 262, 138, 269, 270divdiv1d 12046 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) / (2โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›)))))
272262, 269dividd 12013 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) = 1)
273272oveq1d 7428 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) / (2โ†‘(4 ยท ๐‘›))) = (1 / (2โ†‘(4 ยท ๐‘›))))
274268, 271, 2733eqtr2d 2771 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))) = (1 / (2โ†‘(4 ยท ๐‘›))))
275264, 266, 2743eqtrd 2769 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = (1 / (2โ†‘(4 ยท ๐‘›))))
276254, 261, 2753eqtrd 2769 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)) = (1 / (2โ†‘(4 ยท ๐‘›))))
277242, 276oveq12d 7431 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))) = (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›)))))
278277oveq2d 7429 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))) = ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›))))))
279138, 270reccld 12008 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (1 / (2โ†‘(4 ยท ๐‘›))) โˆˆ โ„‚)
280138, 7, 279mul12d 11448 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))))
2817mulridd 11256 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท 1) = ๐‘›)
282138, 270recidd 12010 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›)))) = 1)
283282oveq2d 7429 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = (๐‘› ยท 1))
284281, 283, 2333eqtr4d 2775 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = ((๐‘›โ†‘2) / ๐‘›))
285278, 280, 2843eqtrd 2769 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))) = ((๐‘›โ†‘2) / ๐‘›))
286186, 200, 2853eqtrd 2769 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((๐‘›โ†‘2) / ๐‘›))
287286oveq1d 7428 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = (((๐‘›โ†‘2) / ๐‘›) / ((2 ยท ๐‘›) + 1)))
288236, 7, 172, 25, 184divdiv1d 12046 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘2) / ๐‘›) / ((2 ยท ๐‘›) + 1)) = ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1))))
289287, 288eqtrd 2765 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1))))
290289oveq2d 7429 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
291185, 290eqtrd 2765 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
292165, 169, 2913eqtrd 2769 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
293142, 159, 2923eqtrd 2769 . . 3 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
294293mpteq2ia 5247 . 2 (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))) = (๐‘› โˆˆ โ„• โ†ฆ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
2951, 136, 2943eqtri 2757 1 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
Colors of variables: wff setvar class
Syntax hints:   โˆง wa 394   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2930   class class class wbr 5144   โ†ฆ cmpt 5227  โ€˜cfv 6543  (class class class)co 7413  โ„‚cc 11131  โ„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   ยท cmul 11138   โ‰ค cle 11274   / cdiv 11896  โ„•cn 12237  2c2 12292  4c4 12294  โ„•0cn0 12497  โ„คcz 12583  โ„+crp 13001  โ†‘cexp 14053  !cfa 14259  โˆšcsqrt 15207  eceu 16033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-pm 8841  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9460  df-inf 9461  df-oi 9528  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-4 12302  df-n0 12498  df-z 12584  df-uz 12848  df-q 12958  df-rp 13002  df-ico 13357  df-fz 13512  df-fzo 13655  df-fl 13784  df-seq 13994  df-exp 14054  df-fac 14260  df-bc 14289  df-hash 14317  df-shft 15041  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-limsup 15442  df-clim 15459  df-rlim 15460  df-sum 15660  df-ef 16038  df-e 16039
This theorem is referenced by:  stirlinglem15  45535
  Copyright terms: Public domain W3C validator