Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  faclim2 Structured version   Visualization version   GIF version

Theorem faclim2 34441
Description: Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.)
Hypothesis
Ref Expression
faclim2.1 ๐น = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘€)) / (!โ€˜(๐‘› + ๐‘€))))
Assertion
Ref Expression
faclim2 (๐‘€ โˆˆ โ„•0 โ†’ ๐น โ‡ 1)
Distinct variable group:   ๐‘›,๐‘€
Allowed substitution hint:   ๐น(๐‘›)

Proof of Theorem faclim2
Dummy variables ๐‘š ๐‘Ž ๐‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 faclim2.1 . 2 ๐น = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘€)) / (!โ€˜(๐‘› + ๐‘€))))
2 oveq2 7385 . . . . . . 7 (๐‘Ž = 0 โ†’ ((๐‘› + 1)โ†‘๐‘Ž) = ((๐‘› + 1)โ†‘0))
32oveq2d 7393 . . . . . 6 (๐‘Ž = 0 โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) = ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)))
4 oveq2 7385 . . . . . . 7 (๐‘Ž = 0 โ†’ (๐‘› + ๐‘Ž) = (๐‘› + 0))
54fveq2d 6866 . . . . . 6 (๐‘Ž = 0 โ†’ (!โ€˜(๐‘› + ๐‘Ž)) = (!โ€˜(๐‘› + 0)))
63, 5oveq12d 7395 . . . . 5 (๐‘Ž = 0 โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž))) = (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0))))
76mpteq2dv 5227 . . . 4 (๐‘Ž = 0 โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž)))) = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0)))))
87breq1d 5135 . . 3 (๐‘Ž = 0 โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž)))) โ‡ 1 โ†” (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0)))) โ‡ 1))
9 oveq2 7385 . . . . . . 7 (๐‘Ž = ๐‘š โ†’ ((๐‘› + 1)โ†‘๐‘Ž) = ((๐‘› + 1)โ†‘๐‘š))
109oveq2d 7393 . . . . . 6 (๐‘Ž = ๐‘š โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) = ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)))
11 oveq2 7385 . . . . . . 7 (๐‘Ž = ๐‘š โ†’ (๐‘› + ๐‘Ž) = (๐‘› + ๐‘š))
1211fveq2d 6866 . . . . . 6 (๐‘Ž = ๐‘š โ†’ (!โ€˜(๐‘› + ๐‘Ž)) = (!โ€˜(๐‘› + ๐‘š)))
1310, 12oveq12d 7395 . . . . 5 (๐‘Ž = ๐‘š โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž))) = (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))
1413mpteq2dv 5227 . . . 4 (๐‘Ž = ๐‘š โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž)))) = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))))
1514breq1d 5135 . . 3 (๐‘Ž = ๐‘š โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž)))) โ‡ 1 โ†” (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1))
16 oveq2 7385 . . . . . . 7 (๐‘Ž = (๐‘š + 1) โ†’ ((๐‘› + 1)โ†‘๐‘Ž) = ((๐‘› + 1)โ†‘(๐‘š + 1)))
1716oveq2d 7393 . . . . . 6 (๐‘Ž = (๐‘š + 1) โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) = ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))))
18 oveq2 7385 . . . . . . 7 (๐‘Ž = (๐‘š + 1) โ†’ (๐‘› + ๐‘Ž) = (๐‘› + (๐‘š + 1)))
1918fveq2d 6866 . . . . . 6 (๐‘Ž = (๐‘š + 1) โ†’ (!โ€˜(๐‘› + ๐‘Ž)) = (!โ€˜(๐‘› + (๐‘š + 1))))
2017, 19oveq12d 7395 . . . . 5 (๐‘Ž = (๐‘š + 1) โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž))) = (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1)))))
2120mpteq2dv 5227 . . . 4 (๐‘Ž = (๐‘š + 1) โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž)))) = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1))))))
2221breq1d 5135 . . 3 (๐‘Ž = (๐‘š + 1) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž)))) โ‡ 1 โ†” (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1))))) โ‡ 1))
23 oveq2 7385 . . . . . . 7 (๐‘Ž = ๐‘€ โ†’ ((๐‘› + 1)โ†‘๐‘Ž) = ((๐‘› + 1)โ†‘๐‘€))
2423oveq2d 7393 . . . . . 6 (๐‘Ž = ๐‘€ โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) = ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘€)))
25 oveq2 7385 . . . . . . 7 (๐‘Ž = ๐‘€ โ†’ (๐‘› + ๐‘Ž) = (๐‘› + ๐‘€))
2625fveq2d 6866 . . . . . 6 (๐‘Ž = ๐‘€ โ†’ (!โ€˜(๐‘› + ๐‘Ž)) = (!โ€˜(๐‘› + ๐‘€)))
2724, 26oveq12d 7395 . . . . 5 (๐‘Ž = ๐‘€ โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž))) = (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘€)) / (!โ€˜(๐‘› + ๐‘€))))
2827mpteq2dv 5227 . . . 4 (๐‘Ž = ๐‘€ โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž)))) = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘€)) / (!โ€˜(๐‘› + ๐‘€)))))
2928breq1d 5135 . . 3 (๐‘Ž = ๐‘€ โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘Ž)) / (!โ€˜(๐‘› + ๐‘Ž)))) โ‡ 1 โ†” (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘€)) / (!โ€˜(๐‘› + ๐‘€)))) โ‡ 1))
30 nnuz 12830 . . . . 5 โ„• = (โ„คโ‰ฅโ€˜1)
31 1zzd 12558 . . . . 5 (โŠค โ†’ 1 โˆˆ โ„ค)
32 nnex 12183 . . . . . . 7 โ„• โˆˆ V
3332mptex 7193 . . . . . 6 (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0)))) โˆˆ V
3433a1i 11 . . . . 5 (โŠค โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0)))) โˆˆ V)
35 1cnd 11174 . . . . 5 (โŠค โ†’ 1 โˆˆ โ„‚)
36 fveq2 6862 . . . . . . . . . 10 (๐‘› = ๐‘š โ†’ (!โ€˜๐‘›) = (!โ€˜๐‘š))
37 oveq1 7384 . . . . . . . . . . 11 (๐‘› = ๐‘š โ†’ (๐‘› + 1) = (๐‘š + 1))
3837oveq1d 7392 . . . . . . . . . 10 (๐‘› = ๐‘š โ†’ ((๐‘› + 1)โ†‘0) = ((๐‘š + 1)โ†‘0))
3936, 38oveq12d 7395 . . . . . . . . 9 (๐‘› = ๐‘š โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) = ((!โ€˜๐‘š) ยท ((๐‘š + 1)โ†‘0)))
40 fvoveq1 7400 . . . . . . . . 9 (๐‘› = ๐‘š โ†’ (!โ€˜(๐‘› + 0)) = (!โ€˜(๐‘š + 0)))
4139, 40oveq12d 7395 . . . . . . . 8 (๐‘› = ๐‘š โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0))) = (((!โ€˜๐‘š) ยท ((๐‘š + 1)โ†‘0)) / (!โ€˜(๐‘š + 0))))
42 eqid 2731 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0)))) = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0))))
43 ovex 7410 . . . . . . . 8 (((!โ€˜๐‘š) ยท ((๐‘š + 1)โ†‘0)) / (!โ€˜(๐‘š + 0))) โˆˆ V
4441, 42, 43fvmpt 6968 . . . . . . 7 (๐‘š โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0))))โ€˜๐‘š) = (((!โ€˜๐‘š) ยท ((๐‘š + 1)โ†‘0)) / (!โ€˜(๐‘š + 0))))
45 peano2nn 12189 . . . . . . . . . . . 12 (๐‘š โˆˆ โ„• โ†’ (๐‘š + 1) โˆˆ โ„•)
4645nncnd 12193 . . . . . . . . . . 11 (๐‘š โˆˆ โ„• โ†’ (๐‘š + 1) โˆˆ โ„‚)
4746exp0d 14070 . . . . . . . . . 10 (๐‘š โˆˆ โ„• โ†’ ((๐‘š + 1)โ†‘0) = 1)
4847oveq2d 7393 . . . . . . . . 9 (๐‘š โˆˆ โ„• โ†’ ((!โ€˜๐‘š) ยท ((๐‘š + 1)โ†‘0)) = ((!โ€˜๐‘š) ยท 1))
49 nnnn0 12444 . . . . . . . . . . . 12 (๐‘š โˆˆ โ„• โ†’ ๐‘š โˆˆ โ„•0)
50 faccl 14208 . . . . . . . . . . . 12 (๐‘š โˆˆ โ„•0 โ†’ (!โ€˜๐‘š) โˆˆ โ„•)
5149, 50syl 17 . . . . . . . . . . 11 (๐‘š โˆˆ โ„• โ†’ (!โ€˜๐‘š) โˆˆ โ„•)
5251nncnd 12193 . . . . . . . . . 10 (๐‘š โˆˆ โ„• โ†’ (!โ€˜๐‘š) โˆˆ โ„‚)
5352mulridd 11196 . . . . . . . . 9 (๐‘š โˆˆ โ„• โ†’ ((!โ€˜๐‘š) ยท 1) = (!โ€˜๐‘š))
5448, 53eqtrd 2771 . . . . . . . 8 (๐‘š โˆˆ โ„• โ†’ ((!โ€˜๐‘š) ยท ((๐‘š + 1)โ†‘0)) = (!โ€˜๐‘š))
55 nncn 12185 . . . . . . . . . 10 (๐‘š โˆˆ โ„• โ†’ ๐‘š โˆˆ โ„‚)
5655addridd 11379 . . . . . . . . 9 (๐‘š โˆˆ โ„• โ†’ (๐‘š + 0) = ๐‘š)
5756fveq2d 6866 . . . . . . . 8 (๐‘š โˆˆ โ„• โ†’ (!โ€˜(๐‘š + 0)) = (!โ€˜๐‘š))
5854, 57oveq12d 7395 . . . . . . 7 (๐‘š โˆˆ โ„• โ†’ (((!โ€˜๐‘š) ยท ((๐‘š + 1)โ†‘0)) / (!โ€˜(๐‘š + 0))) = ((!โ€˜๐‘š) / (!โ€˜๐‘š)))
5951nnne0d 12227 . . . . . . . 8 (๐‘š โˆˆ โ„• โ†’ (!โ€˜๐‘š) โ‰  0)
6052, 59dividd 11953 . . . . . . 7 (๐‘š โˆˆ โ„• โ†’ ((!โ€˜๐‘š) / (!โ€˜๐‘š)) = 1)
6144, 58, 603eqtrd 2775 . . . . . 6 (๐‘š โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0))))โ€˜๐‘š) = 1)
6261adantl 482 . . . . 5 ((โŠค โˆง ๐‘š โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0))))โ€˜๐‘š) = 1)
6330, 31, 34, 35, 62climconst 15452 . . . 4 (โŠค โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0)))) โ‡ 1)
6463mptru 1548 . . 3 (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘0)) / (!โ€˜(๐‘› + 0)))) โ‡ 1
65 1zzd 12558 . . . . . 6 ((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โ†’ 1 โˆˆ โ„ค)
66 simpr 485 . . . . . 6 ((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1)
6732mptex 7193 . . . . . . 7 (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1))))) โˆˆ V
6867a1i 11 . . . . . 6 ((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1))))) โˆˆ V)
69 1zzd 12558 . . . . . . . 8 (๐‘š โˆˆ โ„•0 โ†’ 1 โˆˆ โ„ค)
70 1cnd 11174 . . . . . . . 8 (๐‘š โˆˆ โ„•0 โ†’ 1 โˆˆ โ„‚)
71 nn0p1nn 12476 . . . . . . . . 9 (๐‘š โˆˆ โ„•0 โ†’ (๐‘š + 1) โˆˆ โ„•)
7271nnzd 12550 . . . . . . . 8 (๐‘š โˆˆ โ„•0 โ†’ (๐‘š + 1) โˆˆ โ„ค)
7332mptex 7193 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1)))) โˆˆ V
7473a1i 11 . . . . . . . 8 (๐‘š โˆˆ โ„•0 โ†’ (๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1)))) โˆˆ V)
75 oveq1 7384 . . . . . . . . . . 11 (๐‘› = ๐‘˜ โ†’ (๐‘› + 1) = (๐‘˜ + 1))
76 oveq1 7384 . . . . . . . . . . 11 (๐‘› = ๐‘˜ โ†’ (๐‘› + (๐‘š + 1)) = (๐‘˜ + (๐‘š + 1)))
7775, 76oveq12d 7395 . . . . . . . . . 10 (๐‘› = ๐‘˜ โ†’ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))) = ((๐‘˜ + 1) / (๐‘˜ + (๐‘š + 1))))
78 eqid 2731 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1)))) = (๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))
79 ovex 7410 . . . . . . . . . 10 ((๐‘˜ + 1) / (๐‘˜ + (๐‘š + 1))) โˆˆ V
8077, 78, 79fvmpt 6968 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))โ€˜๐‘˜) = ((๐‘˜ + 1) / (๐‘˜ + (๐‘š + 1))))
8180adantl 482 . . . . . . . 8 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))โ€˜๐‘˜) = ((๐‘˜ + 1) / (๐‘˜ + (๐‘š + 1))))
8230, 69, 70, 72, 74, 81divcnvlin 34425 . . . . . . 7 (๐‘š โˆˆ โ„•0 โ†’ (๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1)))) โ‡ 1)
8382adantr 481 . . . . . 6 ((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โ†’ (๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1)))) โ‡ 1)
84 simpr 485 . . . . . . . . . . . . . . 15 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘› โˆˆ โ„•)
8584nnnn0d 12497 . . . . . . . . . . . . . 14 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘› โˆˆ โ„•0)
86 faccl 14208 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„•0 โ†’ (!โ€˜๐‘›) โˆˆ โ„•)
8785, 86syl 17 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (!โ€˜๐‘›) โˆˆ โ„•)
88 peano2nn 12189 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„•)
89 nnexpcl 14005 . . . . . . . . . . . . . . 15 (((๐‘› + 1) โˆˆ โ„• โˆง ๐‘š โˆˆ โ„•0) โ†’ ((๐‘› + 1)โ†‘๐‘š) โˆˆ โ„•)
9088, 89sylan 580 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘š โˆˆ โ„•0) โ†’ ((๐‘› + 1)โ†‘๐‘š) โˆˆ โ„•)
9190ancoms 459 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ ((๐‘› + 1)โ†‘๐‘š) โˆˆ โ„•)
9287, 91nnmulcld 12230 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) โˆˆ โ„•)
9392nnred 12192 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) โˆˆ โ„)
94 nnnn0addcl 12467 . . . . . . . . . . . . . 14 ((๐‘› โˆˆ โ„• โˆง ๐‘š โˆˆ โ„•0) โ†’ (๐‘› + ๐‘š) โˆˆ โ„•)
9594ancoms 459 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘› + ๐‘š) โˆˆ โ„•)
9695nnnn0d 12497 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘› + ๐‘š) โˆˆ โ„•0)
97 faccl 14208 . . . . . . . . . . . 12 ((๐‘› + ๐‘š) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› + ๐‘š)) โˆˆ โ„•)
9896, 97syl 17 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (!โ€˜(๐‘› + ๐‘š)) โˆˆ โ„•)
9993, 98nndivred 12231 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))) โˆˆ โ„)
10099recnd 11207 . . . . . . . . 9 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))) โˆˆ โ„‚)
101100fmpttd 7083 . . . . . . . 8 (๐‘š โˆˆ โ„•0 โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))):โ„•โŸถโ„‚)
102101ffvelcdmda 7055 . . . . . . 7 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))โ€˜๐‘˜) โˆˆ โ„‚)
103102adantlr 713 . . . . . 6 (((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))โ€˜๐‘˜) โˆˆ โ„‚)
10488adantl 482 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘› + 1) โˆˆ โ„•)
105104nnred 12192 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘› + 1) โˆˆ โ„)
10671adantr 481 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘š + 1) โˆˆ โ„•)
10784, 106nnaddcld 12229 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘› + (๐‘š + 1)) โˆˆ โ„•)
108105, 107nndivred 12231 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))) โˆˆ โ„)
109108recnd 11207 . . . . . . . . 9 ((๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•) โ†’ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))) โˆˆ โ„‚)
110109fmpttd 7083 . . . . . . . 8 (๐‘š โˆˆ โ„•0 โ†’ (๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1)))):โ„•โŸถโ„‚)
111110ffvelcdmda 7055 . . . . . . 7 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))โ€˜๐‘˜) โˆˆ โ„‚)
112111adantlr 713 . . . . . 6 (((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))โ€˜๐‘˜) โˆˆ โ„‚)
113 peano2nn 12189 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ โ„• โ†’ (๐‘˜ + 1) โˆˆ โ„•)
114113adantl 482 . . . . . . . . . . . . . 14 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + 1) โˆˆ โ„•)
115114nncnd 12193 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + 1) โˆˆ โ„‚)
116 simpl 483 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘š โˆˆ โ„•0)
117115, 116expp1d 14077 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘˜ + 1)โ†‘(๐‘š + 1)) = (((๐‘˜ + 1)โ†‘๐‘š) ยท (๐‘˜ + 1)))
118117oveq2d 7393 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))) = ((!โ€˜๐‘˜) ยท (((๐‘˜ + 1)โ†‘๐‘š) ยท (๐‘˜ + 1))))
119 simpr 485 . . . . . . . . . . . . . . 15 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„•)
120119nnnn0d 12497 . . . . . . . . . . . . . 14 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„•0)
121 faccl 14208 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ โ„•0 โ†’ (!โ€˜๐‘˜) โˆˆ โ„•)
122120, 121syl 17 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (!โ€˜๐‘˜) โˆˆ โ„•)
123122nncnd 12193 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (!โ€˜๐‘˜) โˆˆ โ„‚)
124 nnexpcl 14005 . . . . . . . . . . . . . . 15 (((๐‘˜ + 1) โˆˆ โ„• โˆง ๐‘š โˆˆ โ„•0) โ†’ ((๐‘˜ + 1)โ†‘๐‘š) โˆˆ โ„•)
125113, 124sylan 580 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„• โˆง ๐‘š โˆˆ โ„•0) โ†’ ((๐‘˜ + 1)โ†‘๐‘š) โˆˆ โ„•)
126125ancoms 459 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘˜ + 1)โ†‘๐‘š) โˆˆ โ„•)
127126nncnd 12193 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘˜ + 1)โ†‘๐‘š) โˆˆ โ„‚)
128123, 127, 115mulassd 11202 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) ยท (๐‘˜ + 1)) = ((!โ€˜๐‘˜) ยท (((๐‘˜ + 1)โ†‘๐‘š) ยท (๐‘˜ + 1))))
129118, 128eqtr4d 2774 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))) = (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) ยท (๐‘˜ + 1)))
130120, 116nn0addcld 12501 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + ๐‘š) โˆˆ โ„•0)
131 facp1 14203 . . . . . . . . . . . 12 ((๐‘˜ + ๐‘š) โˆˆ โ„•0 โ†’ (!โ€˜((๐‘˜ + ๐‘š) + 1)) = ((!โ€˜(๐‘˜ + ๐‘š)) ยท ((๐‘˜ + ๐‘š) + 1)))
132130, 131syl 17 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (!โ€˜((๐‘˜ + ๐‘š) + 1)) = ((!โ€˜(๐‘˜ + ๐‘š)) ยท ((๐‘˜ + ๐‘š) + 1)))
133119nncnd 12193 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„‚)
134116nn0cnd 12499 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘š โˆˆ โ„‚)
135 1cnd 11174 . . . . . . . . . . . . 13 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ 1 โˆˆ โ„‚)
136133, 134, 135addassd 11201 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘˜ + ๐‘š) + 1) = (๐‘˜ + (๐‘š + 1)))
137136fveq2d 6866 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (!โ€˜((๐‘˜ + ๐‘š) + 1)) = (!โ€˜(๐‘˜ + (๐‘š + 1))))
138136oveq2d 7393 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((!โ€˜(๐‘˜ + ๐‘š)) ยท ((๐‘˜ + ๐‘š) + 1)) = ((!โ€˜(๐‘˜ + ๐‘š)) ยท (๐‘˜ + (๐‘š + 1))))
139132, 137, 1383eqtr3d 2779 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (!โ€˜(๐‘˜ + (๐‘š + 1))) = ((!โ€˜(๐‘˜ + ๐‘š)) ยท (๐‘˜ + (๐‘š + 1))))
140129, 139oveq12d 7395 . . . . . . . . 9 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘˜ + (๐‘š + 1)))) = ((((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) ยท (๐‘˜ + 1)) / ((!โ€˜(๐‘˜ + ๐‘š)) ยท (๐‘˜ + (๐‘š + 1)))))
141122, 126nnmulcld 12230 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) โˆˆ โ„•)
142141nncnd 12193 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) โˆˆ โ„‚)
143 faccl 14208 . . . . . . . . . . . 12 ((๐‘˜ + ๐‘š) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘˜ + ๐‘š)) โˆˆ โ„•)
144130, 143syl 17 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (!โ€˜(๐‘˜ + ๐‘š)) โˆˆ โ„•)
145144nncnd 12193 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (!โ€˜(๐‘˜ + ๐‘š)) โˆˆ โ„‚)
14671adantr 481 . . . . . . . . . . . 12 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘š + 1) โˆˆ โ„•)
147119, 146nnaddcld 12229 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + (๐‘š + 1)) โˆˆ โ„•)
148147nncnd 12193 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + (๐‘š + 1)) โˆˆ โ„‚)
149144nnne0d 12227 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (!โ€˜(๐‘˜ + ๐‘š)) โ‰  0)
150147nnne0d 12227 . . . . . . . . . 10 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘˜ + (๐‘š + 1)) โ‰  0)
151142, 145, 115, 148, 149, 150divmuldivd 11996 . . . . . . . . 9 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) / (!โ€˜(๐‘˜ + ๐‘š))) ยท ((๐‘˜ + 1) / (๐‘˜ + (๐‘š + 1)))) = ((((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) ยท (๐‘˜ + 1)) / ((!โ€˜(๐‘˜ + ๐‘š)) ยท (๐‘˜ + (๐‘š + 1)))))
152140, 151eqtr4d 2774 . . . . . . . 8 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘˜ + (๐‘š + 1)))) = ((((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) / (!โ€˜(๐‘˜ + ๐‘š))) ยท ((๐‘˜ + 1) / (๐‘˜ + (๐‘š + 1)))))
153 fveq2 6862 . . . . . . . . . . . 12 (๐‘› = ๐‘˜ โ†’ (!โ€˜๐‘›) = (!โ€˜๐‘˜))
15475oveq1d 7392 . . . . . . . . . . . 12 (๐‘› = ๐‘˜ โ†’ ((๐‘› + 1)โ†‘(๐‘š + 1)) = ((๐‘˜ + 1)โ†‘(๐‘š + 1)))
155153, 154oveq12d 7395 . . . . . . . . . . 11 (๐‘› = ๐‘˜ โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) = ((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))))
156 fvoveq1 7400 . . . . . . . . . . 11 (๐‘› = ๐‘˜ โ†’ (!โ€˜(๐‘› + (๐‘š + 1))) = (!โ€˜(๐‘˜ + (๐‘š + 1))))
157155, 156oveq12d 7395 . . . . . . . . . 10 (๐‘› = ๐‘˜ โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1)))) = (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘˜ + (๐‘š + 1)))))
158 eqid 2731 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1))))) = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1)))))
159 ovex 7410 . . . . . . . . . 10 (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘˜ + (๐‘š + 1)))) โˆˆ V
160157, 158, 159fvmpt 6968 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1)))))โ€˜๐‘˜) = (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘˜ + (๐‘š + 1)))))
161160adantl 482 . . . . . . . 8 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1)))))โ€˜๐‘˜) = (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘˜ + (๐‘š + 1)))))
16275oveq1d 7392 . . . . . . . . . . . . 13 (๐‘› = ๐‘˜ โ†’ ((๐‘› + 1)โ†‘๐‘š) = ((๐‘˜ + 1)โ†‘๐‘š))
163153, 162oveq12d 7395 . . . . . . . . . . . 12 (๐‘› = ๐‘˜ โ†’ ((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) = ((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)))
164 fvoveq1 7400 . . . . . . . . . . . 12 (๐‘› = ๐‘˜ โ†’ (!โ€˜(๐‘› + ๐‘š)) = (!โ€˜(๐‘˜ + ๐‘š)))
165163, 164oveq12d 7395 . . . . . . . . . . 11 (๐‘› = ๐‘˜ โ†’ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))) = (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) / (!โ€˜(๐‘˜ + ๐‘š))))
166 eqid 2731 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) = (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))
167 ovex 7410 . . . . . . . . . . 11 (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) / (!โ€˜(๐‘˜ + ๐‘š))) โˆˆ V
168165, 166, 167fvmpt 6968 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))โ€˜๐‘˜) = (((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) / (!โ€˜(๐‘˜ + ๐‘š))))
169168, 80oveq12d 7395 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))โ€˜๐‘˜) ยท ((๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))โ€˜๐‘˜)) = ((((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) / (!โ€˜(๐‘˜ + ๐‘š))) ยท ((๐‘˜ + 1) / (๐‘˜ + (๐‘š + 1)))))
170169adantl 482 . . . . . . . 8 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ (((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))โ€˜๐‘˜) ยท ((๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))โ€˜๐‘˜)) = ((((!โ€˜๐‘˜) ยท ((๐‘˜ + 1)โ†‘๐‘š)) / (!โ€˜(๐‘˜ + ๐‘š))) ยท ((๐‘˜ + 1) / (๐‘˜ + (๐‘š + 1)))))
171152, 161, 1703eqtr4d 2781 . . . . . . 7 ((๐‘š โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1)))))โ€˜๐‘˜) = (((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))โ€˜๐‘˜) ยท ((๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))โ€˜๐‘˜)))
172171adantlr 713 . . . . . 6 (((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1)))))โ€˜๐‘˜) = (((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š))))โ€˜๐‘˜) ยท ((๐‘› โˆˆ โ„• โ†ฆ ((๐‘› + 1) / (๐‘› + (๐‘š + 1))))โ€˜๐‘˜)))
17330, 65, 66, 68, 83, 103, 112, 172climmul 15542 . . . . 5 ((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1))))) โ‡ (1 ยท 1))
174 1t1e1 12339 . . . . 5 (1 ยท 1) = 1
175173, 174breqtrdi 5166 . . . 4 ((๐‘š โˆˆ โ„•0 โˆง (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1) โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1))))) โ‡ 1)
176175ex 413 . . 3 (๐‘š โˆˆ โ„•0 โ†’ ((๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘š)) / (!โ€˜(๐‘› + ๐‘š)))) โ‡ 1 โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘(๐‘š + 1))) / (!โ€˜(๐‘› + (๐‘š + 1))))) โ‡ 1))
1778, 15, 22, 29, 64, 176nn0ind 12622 . 2 (๐‘€ โˆˆ โ„•0 โ†’ (๐‘› โˆˆ โ„• โ†ฆ (((!โ€˜๐‘›) ยท ((๐‘› + 1)โ†‘๐‘€)) / (!โ€˜(๐‘› + ๐‘€)))) โ‡ 1)
1781, 177eqbrtrid 5160 1 (๐‘€ โˆˆ โ„•0 โ†’ ๐น โ‡ 1)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 396   = wceq 1541  โŠคwtru 1542   โˆˆ wcel 2106  Vcvv 3459   class class class wbr 5125   โ†ฆ cmpt 5208  โ€˜cfv 6516  (class class class)co 7377  โ„‚cc 11073  0cc0 11075  1c1 11076   + caddc 11078   ยท cmul 11080   / cdiv 11836  โ„•cn 12177  โ„•0cn0 12437  โ†‘cexp 13992  !cfa 14198   โ‡ cli 15393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5262  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3364  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-pss 3947  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-iun 4976  df-br 5126  df-opab 5188  df-mpt 5209  df-tr 5243  df-id 5551  df-eprel 5557  df-po 5565  df-so 5566  df-fr 5608  df-we 5610  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-pred 6273  df-ord 6340  df-on 6341  df-lim 6342  df-suc 6343  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7333  df-ov 7380  df-oprab 7381  df-mpo 7382  df-om 7823  df-2nd 7942  df-frecs 8232  df-wrecs 8263  df-recs 8337  df-rdg 8376  df-er 8670  df-pm 8790  df-en 8906  df-dom 8907  df-sdom 8908  df-sup 9402  df-inf 9403  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11411  df-neg 11412  df-div 11837  df-nn 12178  df-2 12240  df-3 12241  df-n0 12438  df-z 12524  df-uz 12788  df-rp 12940  df-fl 13722  df-seq 13932  df-exp 13993  df-fac 14199  df-shft 14979  df-cj 15011  df-re 15012  df-im 15013  df-sqrt 15147  df-abs 15148  df-clim 15397  df-rlim 15398
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator