Step | Hyp | Ref
| Expression |
1 | | fveq2 5515 |
. . . . 5
โข (๐ฅ = ๐พ โ (!โ๐ฅ) = (!โ๐พ)) |
2 | 1 | breq2d 4015 |
. . . 4
โข (๐ฅ = ๐พ โ (๐พ โฅ (!โ๐ฅ) โ ๐พ โฅ (!โ๐พ))) |
3 | 2 | imbi2d 230 |
. . 3
โข (๐ฅ = ๐พ โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฅ)) โ (๐พ โ โ โ ๐พ โฅ (!โ๐พ)))) |
4 | | fveq2 5515 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (!โ๐ฅ) = (!โ๐ฆ)) |
5 | 4 | breq2d 4015 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐พ โฅ (!โ๐ฅ) โ ๐พ โฅ (!โ๐ฆ))) |
6 | 5 | imbi2d 230 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฅ)) โ (๐พ โ โ โ ๐พ โฅ (!โ๐ฆ)))) |
7 | | fveq2 5515 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ (!โ๐ฅ) = (!โ(๐ฆ + 1))) |
8 | 7 | breq2d 4015 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ (๐พ โฅ (!โ๐ฅ) โ ๐พ โฅ (!โ(๐ฆ + 1)))) |
9 | 8 | imbi2d 230 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฅ)) โ (๐พ โ โ โ ๐พ โฅ (!โ(๐ฆ + 1))))) |
10 | | fveq2 5515 |
. . . . 5
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
11 | 10 | breq2d 4015 |
. . . 4
โข (๐ฅ = ๐ โ (๐พ โฅ (!โ๐ฅ) โ ๐พ โฅ (!โ๐))) |
12 | 11 | imbi2d 230 |
. . 3
โข (๐ฅ = ๐ โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฅ)) โ (๐พ โ โ โ ๐พ โฅ (!โ๐)))) |
13 | | nnm1nn0 9216 |
. . . . . . . 8
โข (๐พ โ โ โ (๐พ โ 1) โ
โ0) |
14 | | faccl 10714 |
. . . . . . . 8
โข ((๐พ โ 1) โ
โ0 โ (!โ(๐พ โ 1)) โ
โ) |
15 | 13, 14 | syl 14 |
. . . . . . 7
โข (๐พ โ โ โ
(!โ(๐พ โ 1))
โ โ) |
16 | 15 | nnzd 9373 |
. . . . . 6
โข (๐พ โ โ โ
(!โ(๐พ โ 1))
โ โค) |
17 | | nnz 9271 |
. . . . . 6
โข (๐พ โ โ โ ๐พ โ
โค) |
18 | | dvdsmul2 11820 |
. . . . . 6
โข
(((!โ(๐พ
โ 1)) โ โค โง ๐พ โ โค) โ ๐พ โฅ ((!โ(๐พ โ 1)) ยท ๐พ)) |
19 | 16, 17, 18 | syl2anc 411 |
. . . . 5
โข (๐พ โ โ โ ๐พ โฅ ((!โ(๐พ โ 1)) ยท ๐พ)) |
20 | | facnn2 10713 |
. . . . 5
โข (๐พ โ โ โ
(!โ๐พ) =
((!โ(๐พ โ 1))
ยท ๐พ)) |
21 | 19, 20 | breqtrrd 4031 |
. . . 4
โข (๐พ โ โ โ ๐พ โฅ (!โ๐พ)) |
22 | 21 | a1i 9 |
. . 3
โข (๐พ โ โค โ (๐พ โ โ โ ๐พ โฅ (!โ๐พ))) |
23 | 17 | adantl 277 |
. . . . . . 7
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐พ โ โค) |
24 | | elnnuz 9563 |
. . . . . . . . . . . 12
โข (๐พ โ โ โ ๐พ โ
(โคโฅโ1)) |
25 | | uztrn 9543 |
. . . . . . . . . . . 12
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ (โคโฅโ1))
โ ๐ฆ โ
(โคโฅโ1)) |
26 | 24, 25 | sylan2b 287 |
. . . . . . . . . . 11
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐ฆ โ
(โคโฅโ1)) |
27 | | elnnuz 9563 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ๐ฆ โ
(โคโฅโ1)) |
28 | 26, 27 | sylibr 134 |
. . . . . . . . . 10
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐ฆ โ โ) |
29 | 28 | nnnn0d 9228 |
. . . . . . . . 9
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐ฆ โ โ0) |
30 | | faccl 10714 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ (!โ๐ฆ) โ
โ) |
31 | 29, 30 | syl 14 |
. . . . . . . 8
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (!โ๐ฆ) โ
โ) |
32 | 31 | nnzd 9373 |
. . . . . . 7
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (!โ๐ฆ) โ
โค) |
33 | 28 | nnzd 9373 |
. . . . . . . 8
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐ฆ โ โค) |
34 | 33 | peano2zd 9377 |
. . . . . . 7
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (๐ฆ + 1) โ โค) |
35 | | dvdsmultr1 11837 |
. . . . . . 7
โข ((๐พ โ โค โง
(!โ๐ฆ) โ โค
โง (๐ฆ + 1) โ
โค) โ (๐พ โฅ
(!โ๐ฆ) โ ๐พ โฅ ((!โ๐ฆ) ยท (๐ฆ + 1)))) |
36 | 23, 32, 34, 35 | syl3anc 1238 |
. . . . . 6
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (๐พ โฅ (!โ๐ฆ) โ ๐พ โฅ ((!โ๐ฆ) ยท (๐ฆ + 1)))) |
37 | | facp1 10709 |
. . . . . . . 8
โข (๐ฆ โ โ0
โ (!โ(๐ฆ + 1)) =
((!โ๐ฆ) ยท
(๐ฆ + 1))) |
38 | 29, 37 | syl 14 |
. . . . . . 7
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (!โ(๐ฆ + 1)) = ((!โ๐ฆ) ยท (๐ฆ + 1))) |
39 | 38 | breq2d 4015 |
. . . . . 6
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (๐พ โฅ (!โ(๐ฆ + 1)) โ ๐พ โฅ ((!โ๐ฆ) ยท (๐ฆ + 1)))) |
40 | 36, 39 | sylibrd 169 |
. . . . 5
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (๐พ โฅ (!โ๐ฆ) โ ๐พ โฅ (!โ(๐ฆ + 1)))) |
41 | 40 | ex 115 |
. . . 4
โข (๐ฆ โ
(โคโฅโ๐พ) โ (๐พ โ โ โ (๐พ โฅ (!โ๐ฆ) โ ๐พ โฅ (!โ(๐ฆ + 1))))) |
42 | 41 | a2d 26 |
. . 3
โข (๐ฆ โ
(โคโฅโ๐พ) โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฆ)) โ (๐พ โ โ โ ๐พ โฅ (!โ(๐ฆ + 1))))) |
43 | 3, 6, 9, 12, 22, 42 | uzind4 9587 |
. 2
โข (๐ โ
(โคโฅโ๐พ) โ (๐พ โ โ โ ๐พ โฅ (!โ๐))) |
44 | 43 | impcom 125 |
1
โข ((๐พ โ โ โง ๐ โ
(โคโฅโ๐พ)) โ ๐พ โฅ (!โ๐)) |