Step | Hyp | Ref
| Expression |
1 | | faclim2.1 |
. 2
โข ๐น = (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) |
2 | | oveq2 7385 |
. . . . . . 7
โข (๐ = 0 โ ((๐ + 1)โ๐) = ((๐ + 1)โ0)) |
3 | 2 | oveq2d 7393 |
. . . . . 6
โข (๐ = 0 โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ0))) |
4 | | oveq2 7385 |
. . . . . . 7
โข (๐ = 0 โ (๐ + ๐) = (๐ + 0)) |
5 | 4 | fveq2d 6866 |
. . . . . 6
โข (๐ = 0 โ (!โ(๐ + ๐)) = (!โ(๐ + 0))) |
6 | 3, 5 | oveq12d 7395 |
. . . . 5
โข (๐ = 0 โ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))) = (((!โ๐) ยท ((๐ + 1)โ0)) / (!โ(๐ + 0)))) |
7 | 6 | mpteq2dv 5227 |
. . . 4
โข (๐ = 0 โ (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) = (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ0)) / (!โ(๐ + 0))))) |
8 | 7 | breq1d 5135 |
. . 3
โข (๐ = 0 โ ((๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) โ 1 โ (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ0)) / (!โ(๐ + 0)))) โ 1)) |
9 | | oveq2 7385 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ + 1)โ๐) = ((๐ + 1)โ๐)) |
10 | 9 | oveq2d 7393 |
. . . . . 6
โข (๐ = ๐ โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ๐))) |
11 | | oveq2 7385 |
. . . . . . 7
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
12 | 11 | fveq2d 6866 |
. . . . . 6
โข (๐ = ๐ โ (!โ(๐ + ๐)) = (!โ(๐ + ๐))) |
13 | 10, 12 | oveq12d 7395 |
. . . . 5
โข (๐ = ๐ โ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))) = (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) |
14 | 13 | mpteq2dv 5227 |
. . . 4
โข (๐ = ๐ โ (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) = (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))))) |
15 | 14 | breq1d 5135 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) โ 1 โ (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) โ 1)) |
16 | | oveq2 7385 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ + 1)โ๐) = ((๐ + 1)โ(๐ + 1))) |
17 | 16 | oveq2d 7393 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ(๐ + 1)))) |
18 | | oveq2 7385 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ + ๐) = (๐ + (๐ + 1))) |
19 | 18 | fveq2d 6866 |
. . . . . 6
โข (๐ = (๐ + 1) โ (!โ(๐ + ๐)) = (!โ(๐ + (๐ + 1)))) |
20 | 17, 19 | oveq12d 7395 |
. . . . 5
โข (๐ = (๐ + 1) โ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))) = (((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1))))) |
21 | 20 | mpteq2dv 5227 |
. . . 4
โข (๐ = (๐ + 1) โ (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) = (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1)))))) |
22 | 21 | breq1d 5135 |
. . 3
โข (๐ = (๐ + 1) โ ((๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) โ 1 โ (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1))))) โ 1)) |
23 | | oveq2 7385 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ + 1)โ๐) = ((๐ + 1)โ๐)) |
24 | 23 | oveq2d 7393 |
. . . . . 6
โข (๐ = ๐ โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ๐))) |
25 | | oveq2 7385 |
. . . . . . 7
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
26 | 25 | fveq2d 6866 |
. . . . . 6
โข (๐ = ๐ โ (!โ(๐ + ๐)) = (!โ(๐ + ๐))) |
27 | 24, 26 | oveq12d 7395 |
. . . . 5
โข (๐ = ๐ โ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))) = (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) |
28 | 27 | mpteq2dv 5227 |
. . . 4
โข (๐ = ๐ โ (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) = (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))))) |
29 | 28 | breq1d 5135 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) โ 1 โ (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) โ 1)) |
30 | | nnuz 12830 |
. . . . 5
โข โ =
(โคโฅโ1) |
31 | | 1zzd 12558 |
. . . . 5
โข (โค
โ 1 โ โค) |
32 | | nnex 12183 |
. . . . . . 7
โข โ
โ V |
33 | 32 | mptex 7193 |
. . . . . 6
โข (๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ0)) /
(!โ(๐ + 0)))) โ
V |
34 | 33 | a1i 11 |
. . . . 5
โข (โค
โ (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ + 1)โ0))
/ (!โ(๐ + 0))))
โ V) |
35 | | 1cnd 11174 |
. . . . 5
โข (โค
โ 1 โ โ) |
36 | | fveq2 6862 |
. . . . . . . . . 10
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
37 | | oveq1 7384 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
38 | 37 | oveq1d 7392 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ + 1)โ0) = ((๐ + 1)โ0)) |
39 | 36, 38 | oveq12d 7395 |
. . . . . . . . 9
โข (๐ = ๐ โ ((!โ๐) ยท ((๐ + 1)โ0)) = ((!โ๐) ยท ((๐ + 1)โ0))) |
40 | | fvoveq1 7400 |
. . . . . . . . 9
โข (๐ = ๐ โ (!โ(๐ + 0)) = (!โ(๐ + 0))) |
41 | 39, 40 | oveq12d 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 |
44 | 41, 42, 43 | fvmpt 6968 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ0)) /
(!โ(๐ +
0))))โ๐) =
(((!โ๐) ยท
((๐ + 1)โ0)) /
(!โ(๐ +
0)))) |
45 | | peano2nn 12189 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ + 1) โ
โ) |
46 | 45 | nncnd 12193 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ + 1) โ
โ) |
47 | 46 | exp0d 14070 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ + 1)โ0) =
1) |
48 | 47 | oveq2d 7393 |
. . . . . . . . 9
โข (๐ โ โ โ
((!โ๐) ยท
((๐ + 1)โ0)) =
((!โ๐) ยท
1)) |
49 | | nnnn0 12444 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ0) |
50 | | faccl 14208 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(!โ๐) โ
โ) |
52 | 51 | nncnd 12193 |
. . . . . . . . . 10
โข (๐ โ โ โ
(!โ๐) โ
โ) |
53 | 52 | mulridd 11196 |
. . . . . . . . 9
โข (๐ โ โ โ
((!โ๐) ยท 1) =
(!โ๐)) |
54 | 48, 53 | eqtrd 2771 |
. . . . . . . 8
โข (๐ โ โ โ
((!โ๐) ยท
((๐ + 1)โ0)) =
(!โ๐)) |
55 | | nncn 12185 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
56 | 55 | addridd 11379 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ + 0) = ๐) |
57 | 56 | fveq2d 6866 |
. . . . . . . 8
โข (๐ โ โ โ
(!โ(๐ + 0)) =
(!โ๐)) |
58 | 54, 57 | oveq12d 7395 |
. . . . . . 7
โข (๐ โ โ โ
(((!โ๐) ยท
((๐ + 1)โ0)) /
(!โ(๐ + 0))) =
((!โ๐) /
(!โ๐))) |
59 | 51 | nnne0d 12227 |
. . . . . . . 8
โข (๐ โ โ โ
(!โ๐) โ
0) |
60 | 52, 59 | dividd 11953 |
. . . . . . 7
โข (๐ โ โ โ
((!โ๐) /
(!โ๐)) =
1) |
61 | 44, 58, 60 | 3eqtrd 2775 |
. . . . . 6
โข (๐ โ โ โ ((๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ0)) /
(!โ(๐ +
0))))โ๐) =
1) |
62 | 61 | adantl 482 |
. . . . 5
โข
((โค โง ๐
โ โ) โ ((๐
โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ0)) / (!โ(๐ + 0))))โ๐) = 1) |
63 | 30, 31, 34, 35, 62 | climconst 15452 |
. . . 4
โข (โค
โ (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ + 1)โ0))
/ (!โ(๐ + 0))))
โ 1) |
64 | 63 | mptru 1548 |
. . 3
โข (๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ0)) /
(!โ(๐ + 0)))) โ
1 |
65 | | 1zzd 12558 |
. . . . . 6
โข ((๐ โ โ0
โง (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) โ 1 โ
โค) |
66 | | simpr 485 |
. . . . . 6
โข ((๐ โ โ0
โง (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) โ (๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) โ 1) |
67 | 32 | mptex 7193 |
. . . . . . 7
โข (๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1))))) โ V |
68 | 67 | a1i 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) โ
โ) |
72 | 71 | nnzd 12550 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ + 1) โ
โค) |
73 | 32 | mptex 7193 |
. . . . . . . . 9
โข (๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1)))) โ V |
74 | 73 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ โ โ
โฆ ((๐ + 1) / (๐ + (๐ + 1)))) โ V) |
75 | | oveq1 7384 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
76 | | oveq1 7384 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ + (๐ + 1)) = (๐ + (๐ + 1))) |
77 | 75, 76 | oveq12d 7395 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ + 1) / (๐ + (๐ + 1))) = ((๐ + 1) / (๐ + (๐ + 1)))) |
78 | | eqid 2731 |
. . . . . . . . . 10
โข (๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1)))) = (๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1)))) |
79 | | ovex 7410 |
. . . . . . . . . 10
โข ((๐ + 1) / (๐ + (๐ + 1))) โ V |
80 | 77, 78, 79 | fvmpt 6968 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1))))โ๐) = ((๐ + 1) / (๐ + (๐ + 1)))) |
81 | 80 | adantl 482 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โ โ
โฆ ((๐ + 1) / (๐ + (๐ + 1))))โ๐) = ((๐ + 1) / (๐ + (๐ + 1)))) |
82 | 30, 69, 70, 72, 74, 81 | divcnvlin 34425 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ โ
โฆ ((๐ + 1) / (๐ + (๐ + 1)))) โ 1) |
83 | 82 | adantr 481 |
. . . . . 6
โข ((๐ โ โ0
โง (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) โ (๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1)))) โ 1) |
84 | | simpr 485 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
85 | 84 | nnnn0d 12497 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ0) |
86 | | faccl 14208 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ๐) โ
โ) |
88 | | peano2nn 12189 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ + 1) โ
โ) |
89 | | nnexpcl 14005 |
. . . . . . . . . . . . . . 15
โข (((๐ + 1) โ โ โง ๐ โ โ0)
โ ((๐ + 1)โ๐) โ
โ) |
90 | 88, 89 | sylan 580 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ ((๐ + 1)โ๐) โ
โ) |
91 | 90 | ancoms 459 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ + 1)โ๐) โ
โ) |
92 | 87, 91 | nnmulcld 12230 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((!โ๐)
ยท ((๐ +
1)โ๐)) โ
โ) |
93 | 92 | nnred 12192 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((!โ๐)
ยท ((๐ +
1)โ๐)) โ
โ) |
94 | | nnnn0addcl 12467 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ + ๐) โ
โ) |
95 | 94 | ancoms 459 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + ๐) โ
โ) |
96 | 95 | nnnn0d 12497 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + ๐) โ
โ0) |
97 | | faccl 14208 |
. . . . . . . . . . . 12
โข ((๐ + ๐) โ โ0 โ
(!โ(๐ + ๐)) โ
โ) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ(๐ + ๐)) โ
โ) |
99 | 93, 98 | nndivred 12231 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐))) โ
โ) |
100 | 99 | recnd 11207 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐))) โ
โ) |
101 | 100 | fmpttd 7083 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))):โโถโ) |
102 | 101 | ffvelcdmda 7055 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐))))โ๐) โ โ) |
103 | 102 | adantlr 713 |
. . . . . 6
โข (((๐ โ โ0
โง (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) โง ๐ โ โ) โ ((๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ๐)) / (!โ(๐ + ๐))))โ๐) โ โ) |
104 | 88 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โ) |
105 | 104 | nnred 12192 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โ) |
106 | 71 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โ) |
107 | 84, 106 | nnaddcld 12229 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + (๐ + 1)) โ
โ) |
108 | 105, 107 | nndivred 12231 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ + 1) / (๐ + (๐ + 1))) โ โ) |
109 | 108 | recnd 11207 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ + 1) / (๐ + (๐ + 1))) โ โ) |
110 | 109 | fmpttd 7083 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ โ โ
โฆ ((๐ + 1) / (๐ + (๐ +
1)))):โโถโ) |
111 | 110 | ffvelcdmda 7055 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โ โ
โฆ ((๐ + 1) / (๐ + (๐ + 1))))โ๐) โ โ) |
112 | 111 | adantlr 713 |
. . . . . 6
โข (((๐ โ โ0
โง (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) โง ๐ โ โ) โ ((๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1))))โ๐) โ โ) |
113 | | peano2nn 12189 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ + 1) โ
โ) |
114 | 113 | adantl 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โ) |
115 | 114 | nncnd 12193 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โ) |
116 | | simpl 483 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ0) |
117 | 115, 116 | expp1d 14077 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ + 1)โ(๐ + 1)) = (((๐ + 1)โ๐) ยท (๐ + 1))) |
118 | 117 | oveq2d 7393 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((!โ๐)
ยท ((๐ +
1)โ(๐ + 1))) =
((!โ๐) ยท
(((๐ + 1)โ๐) ยท (๐ + 1)))) |
119 | | simpr 485 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
120 | 119 | nnnn0d 12497 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ0) |
121 | | faccl 14208 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ๐) โ
โ) |
123 | 122 | nncnd 12193 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ๐) โ
โ) |
124 | | nnexpcl 14005 |
. . . . . . . . . . . . . . 15
โข (((๐ + 1) โ โ โง ๐ โ โ0)
โ ((๐ + 1)โ๐) โ
โ) |
125 | 113, 124 | sylan 580 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ ((๐ + 1)โ๐) โ
โ) |
126 | 125 | ancoms 459 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ + 1)โ๐) โ
โ) |
127 | 126 | nncnd 12193 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ + 1)โ๐) โ
โ) |
128 | 123, 127,
115 | mulassd 11202 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ (((!โ๐)
ยท ((๐ +
1)โ๐)) ยท (๐ + 1)) = ((!โ๐) ยท (((๐ + 1)โ๐) ยท (๐ + 1)))) |
129 | 118, 128 | eqtr4d 2774 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((!โ๐)
ยท ((๐ +
1)โ(๐ + 1))) =
(((!โ๐) ยท
((๐ + 1)โ๐)) ยท (๐ + 1))) |
130 | 120, 116 | nn0addcld 12501 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + ๐) โ
โ0) |
131 | | facp1 14203 |
. . . . . . . . . . . 12
โข ((๐ + ๐) โ โ0 โ
(!โ((๐ + ๐) + 1)) = ((!โ(๐ + ๐)) ยท ((๐ + ๐) + 1))) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ((๐ + ๐) + 1)) = ((!โ(๐ + ๐)) ยท ((๐ + ๐) + 1))) |
133 | 119 | nncnd 12193 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
134 | 116 | nn0cnd 12499 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
135 | | 1cnd 11174 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ 1 โ โ) |
136 | 133, 134,
135 | addassd 11201 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
137 | 136 | fveq2d 6866 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ((๐ + ๐) + 1)) = (!โ(๐ + (๐ + 1)))) |
138 | 136 | oveq2d 7393 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((!โ(๐ + ๐)) ยท ((๐ + ๐) + 1)) = ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1)))) |
139 | 132, 137,
138 | 3eqtr3d 2779 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ(๐ + (๐ + 1))) = ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1)))) |
140 | 129, 139 | oveq12d 7395 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (((!โ๐)
ยท ((๐ +
1)โ(๐ + 1))) /
(!โ(๐ + (๐ + 1)))) = ((((!โ๐) ยท ((๐ + 1)โ๐)) ยท (๐ + 1)) / ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1))))) |
141 | 122, 126 | nnmulcld 12230 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((!โ๐)
ยท ((๐ +
1)โ๐)) โ
โ) |
142 | 141 | nncnd 12193 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((!โ๐)
ยท ((๐ +
1)โ๐)) โ
โ) |
143 | | faccl 14208 |
. . . . . . . . . . . 12
โข ((๐ + ๐) โ โ0 โ
(!โ(๐ + ๐)) โ
โ) |
144 | 130, 143 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ(๐ + ๐)) โ
โ) |
145 | 144 | nncnd 12193 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ(๐ + ๐)) โ
โ) |
146 | 71 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โ) |
147 | 119, 146 | nnaddcld 12229 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + (๐ + 1)) โ
โ) |
148 | 147 | nncnd 12193 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + (๐ + 1)) โ
โ) |
149 | 144 | nnne0d 12227 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ(๐ + ๐)) โ 0) |
150 | 147 | nnne0d 12227 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + (๐ + 1)) โ 0) |
151 | 142, 145,
115, 148, 149, 150 | divmuldivd 11996 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐))) ยท ((๐ + 1) / (๐ + (๐ + 1)))) = ((((!โ๐) ยท ((๐ + 1)โ๐)) ยท (๐ + 1)) / ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1))))) |
152 | 140, 151 | eqtr4d 2774 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (((!โ๐)
ยท ((๐ +
1)โ(๐ + 1))) /
(!โ(๐ + (๐ + 1)))) = ((((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))) ยท ((๐ + 1) / (๐ + (๐ + 1))))) |
153 | | fveq2 6862 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
154 | 75 | oveq1d 7392 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ + 1)โ(๐ + 1)) = ((๐ + 1)โ(๐ + 1))) |
155 | 153, 154 | oveq12d 7395 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) = ((!โ๐) ยท ((๐ + 1)โ(๐ + 1)))) |
156 | | fvoveq1 7400 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (!โ(๐ + (๐ + 1))) = (!โ(๐ + (๐ + 1)))) |
157 | 155, 156 | oveq12d 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 |
160 | 157, 158,
159 | fvmpt 6968 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1)))))โ๐) = (((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1))))) |
161 | 160 | adantl 482 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ(๐ + 1))) /
(!โ(๐ + (๐ + 1)))))โ๐) = (((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1))))) |
162 | 75 | oveq1d 7392 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐ + 1)โ๐) = ((๐ + 1)โ๐)) |
163 | 153, 162 | oveq12d 7395 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ๐))) |
164 | | fvoveq1 7400 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (!โ(๐ + ๐)) = (!โ(๐ + ๐))) |
165 | 163, 164 | oveq12d 7395 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))) = (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) |
166 | | eqid 2731 |
. . . . . . . . . . 11
โข (๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) = (๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) |
167 | | ovex 7410 |
. . . . . . . . . . 11
โข
(((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐))) โ V |
168 | 165, 166,
167 | fvmpt 6968 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ๐)) / (!โ(๐ + ๐))))โ๐) = (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐)))) |
169 | 168, 80 | oveq12d 7395 |
. . . . . . . . 9
โข (๐ โ โ โ (((๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ๐)) / (!โ(๐ + ๐))))โ๐) ยท ((๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1))))โ๐)) = ((((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))) ยท ((๐ + 1) / (๐ + (๐ + 1))))) |
170 | 169 | adantl 482 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (((๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐))))โ๐) ยท ((๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1))))โ๐)) = ((((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))) ยท ((๐ + 1) / (๐ + (๐ + 1))))) |
171 | 152, 161,
170 | 3eqtr4d 2781 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ(๐ + 1))) /
(!โ(๐ + (๐ + 1)))))โ๐) = (((๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))))โ๐) ยท ((๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1))))โ๐))) |
172 | 171 | adantlr 713 |
. . . . . 6
โข (((๐ โ โ0
โง (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) โง ๐ โ โ) โ ((๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1)))))โ๐) = (((๐ โ โ โฆ (((!โ๐) ยท ((๐ + 1)โ๐)) / (!โ(๐ + ๐))))โ๐) ยท ((๐ โ โ โฆ ((๐ + 1) / (๐ + (๐ + 1))))โ๐))) |
173 | 30, 65, 66, 68, 83, 103, 112, 172 | climmul 15542 |
. . . . 5
โข ((๐ โ โ0
โง (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) โ (๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1))))) โ (1 ยท
1)) |
174 | | 1t1e1 12339 |
. . . . 5
โข (1
ยท 1) = 1 |
175 | 173, 174 | breqtrdi 5166 |
. . . 4
โข ((๐ โ โ0
โง (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) โ (๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1))))) โ 1) |
176 | 175 | ex 413 |
. . 3
โข (๐ โ โ0
โ ((๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1 โ (๐ โ โ โฆ
(((!โ๐) ยท
((๐ + 1)โ(๐ + 1))) / (!โ(๐ + (๐ + 1))))) โ 1)) |
177 | 8, 15, 22, 29, 64, 176 | nn0ind 12622 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โฆ (((!โ๐)
ยท ((๐ +
1)โ๐)) /
(!โ(๐ + ๐)))) โ 1) |
178 | 1, 177 | eqbrtrid 5160 |
1
โข (๐ โ โ0
โ ๐น โ
1) |