![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > facp1 | GIF version |
Description: The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Ref | Expression |
---|---|
facp1 | ⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnn0 8876 | . 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) | |
2 | elnnuz 9257 | . . . . . . 7 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1)) | |
3 | 2 | biimpi 119 | . . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ≥‘1)) |
4 | fvi 5430 | . . . . . . . 8 ⊢ (𝑓 ∈ (ℤ≥‘1) → ( I ‘𝑓) = 𝑓) | |
5 | eluzelcn 9232 | . . . . . . . 8 ⊢ (𝑓 ∈ (ℤ≥‘1) → 𝑓 ∈ ℂ) | |
6 | 4, 5 | eqeltrd 2189 | . . . . . . 7 ⊢ (𝑓 ∈ (ℤ≥‘1) → ( I ‘𝑓) ∈ ℂ) |
7 | 6 | adantl 273 | . . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ (ℤ≥‘1)) → ( I ‘𝑓) ∈ ℂ) |
8 | mulcl 7664 | . . . . . . 7 ⊢ ((𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ) → (𝑓 · 𝑔) ∈ ℂ) | |
9 | 8 | adantl 273 | . . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ)) → (𝑓 · 𝑔) ∈ ℂ) |
10 | 3, 7, 9 | seq3p1 10121 | . . . . 5 ⊢ (𝑁 ∈ ℕ → (seq1( · , I )‘(𝑁 + 1)) = ((seq1( · , I )‘𝑁) · ( I ‘(𝑁 + 1)))) |
11 | peano2nn 8635 | . . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ) | |
12 | fvi 5430 | . . . . . . 7 ⊢ ((𝑁 + 1) ∈ ℕ → ( I ‘(𝑁 + 1)) = (𝑁 + 1)) | |
13 | 11, 12 | syl 14 | . . . . . 6 ⊢ (𝑁 ∈ ℕ → ( I ‘(𝑁 + 1)) = (𝑁 + 1)) |
14 | 13 | oveq2d 5742 | . . . . 5 ⊢ (𝑁 ∈ ℕ → ((seq1( · , I )‘𝑁) · ( I ‘(𝑁 + 1))) = ((seq1( · , I )‘𝑁) · (𝑁 + 1))) |
15 | 10, 14 | eqtrd 2145 | . . . 4 ⊢ (𝑁 ∈ ℕ → (seq1( · , I )‘(𝑁 + 1)) = ((seq1( · , I )‘𝑁) · (𝑁 + 1))) |
16 | facnn 10359 | . . . . 5 ⊢ ((𝑁 + 1) ∈ ℕ → (!‘(𝑁 + 1)) = (seq1( · , I )‘(𝑁 + 1))) | |
17 | 11, 16 | syl 14 | . . . 4 ⊢ (𝑁 ∈ ℕ → (!‘(𝑁 + 1)) = (seq1( · , I )‘(𝑁 + 1))) |
18 | facnn 10359 | . . . . 5 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = (seq1( · , I )‘𝑁)) | |
19 | 18 | oveq1d 5741 | . . . 4 ⊢ (𝑁 ∈ ℕ → ((!‘𝑁) · (𝑁 + 1)) = ((seq1( · , I )‘𝑁) · (𝑁 + 1))) |
20 | 15, 17, 19 | 3eqtr4d 2155 | . . 3 ⊢ (𝑁 ∈ ℕ → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) |
21 | 0p1e1 8737 | . . . . . 6 ⊢ (0 + 1) = 1 | |
22 | 21 | fveq2i 5376 | . . . . 5 ⊢ (!‘(0 + 1)) = (!‘1) |
23 | fac1 10361 | . . . . 5 ⊢ (!‘1) = 1 | |
24 | 22, 23 | eqtri 2133 | . . . 4 ⊢ (!‘(0 + 1)) = 1 |
25 | fvoveq1 5749 | . . . 4 ⊢ (𝑁 = 0 → (!‘(𝑁 + 1)) = (!‘(0 + 1))) | |
26 | fveq2 5373 | . . . . . 6 ⊢ (𝑁 = 0 → (!‘𝑁) = (!‘0)) | |
27 | oveq1 5733 | . . . . . 6 ⊢ (𝑁 = 0 → (𝑁 + 1) = (0 + 1)) | |
28 | 26, 27 | oveq12d 5744 | . . . . 5 ⊢ (𝑁 = 0 → ((!‘𝑁) · (𝑁 + 1)) = ((!‘0) · (0 + 1))) |
29 | fac0 10360 | . . . . . . 7 ⊢ (!‘0) = 1 | |
30 | 29, 21 | oveq12i 5738 | . . . . . 6 ⊢ ((!‘0) · (0 + 1)) = (1 · 1) |
31 | 1t1e1 8769 | . . . . . 6 ⊢ (1 · 1) = 1 | |
32 | 30, 31 | eqtri 2133 | . . . . 5 ⊢ ((!‘0) · (0 + 1)) = 1 |
33 | 28, 32 | syl6eq 2161 | . . . 4 ⊢ (𝑁 = 0 → ((!‘𝑁) · (𝑁 + 1)) = 1) |
34 | 24, 25, 33 | 3eqtr4a 2171 | . . 3 ⊢ (𝑁 = 0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) |
35 | 20, 34 | jaoi 688 | . 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) |
36 | 1, 35 | sylbi 120 | 1 ⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∨ wo 680 = wceq 1312 ∈ wcel 1461 I cid 4168 ‘cfv 5079 (class class class)co 5726 ℂcc 7538 0cc0 7540 1c1 7541 + caddc 7543 · cmul 7545 ℕcn 8623 ℕ0cn0 8874 ℤ≥cuz 9221 seqcseq 10104 !cfa 10357 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-13 1472 ax-14 1473 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-coll 4001 ax-sep 4004 ax-nul 4012 ax-pow 4056 ax-pr 4089 ax-un 4313 ax-setind 4410 ax-iinf 4460 ax-cnex 7629 ax-resscn 7630 ax-1cn 7631 ax-1re 7632 ax-icn 7633 ax-addcl 7634 ax-addrcl 7635 ax-mulcl 7636 ax-addcom 7638 ax-mulcom 7639 ax-addass 7640 ax-mulass 7641 ax-distr 7642 ax-i2m1 7643 ax-0lt1 7644 ax-1rid 7645 ax-0id 7646 ax-rnegex 7647 ax-cnre 7649 ax-pre-ltirr 7650 ax-pre-ltwlin 7651 ax-pre-lttrn 7652 ax-pre-ltadd 7654 |
This theorem depends on definitions: df-bi 116 df-3or 944 df-3an 945 df-tru 1315 df-fal 1318 df-nf 1418 df-sb 1717 df-eu 1976 df-mo 1977 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-ne 2281 df-nel 2376 df-ral 2393 df-rex 2394 df-reu 2395 df-rab 2397 df-v 2657 df-sbc 2877 df-csb 2970 df-dif 3037 df-un 3039 df-in 3041 df-ss 3048 df-nul 3328 df-pw 3476 df-sn 3497 df-pr 3498 df-op 3500 df-uni 3701 df-int 3736 df-iun 3779 df-br 3894 df-opab 3948 df-mpt 3949 df-tr 3985 df-id 4173 df-iord 4246 df-on 4248 df-ilim 4249 df-suc 4251 df-iom 4463 df-xp 4503 df-rel 4504 df-cnv 4505 df-co 4506 df-dm 4507 df-rn 4508 df-res 4509 df-ima 4510 df-iota 5044 df-fun 5081 df-fn 5082 df-f 5083 df-f1 5084 df-fo 5085 df-f1o 5086 df-fv 5087 df-riota 5682 df-ov 5729 df-oprab 5730 df-mpo 5731 df-1st 5989 df-2nd 5990 df-recs 6153 df-frec 6239 df-pnf 7719 df-mnf 7720 df-xr 7721 df-ltxr 7722 df-le 7723 df-sub 7851 df-neg 7852 df-inn 8624 df-n0 8875 df-z 8952 df-uz 9222 df-seqfrec 10105 df-fac 10358 |
This theorem is referenced by: fac2 10363 fac3 10364 fac4 10365 facnn2 10366 faccl 10367 facdiv 10370 facwordi 10372 faclbnd 10373 faclbnd6 10376 facubnd 10377 bcm1k 10392 bcp1n 10393 4bc2eq6 10406 efcllemp 11208 ef01bndlem 11307 eirraplem 11324 dvdsfac 11399 prmfac1 11669 ex-fac 12620 |
Copyright terms: Public domain | W3C validator |