Step | Hyp | Ref
| Expression |
1 | | fveq2 6838 |
. . . . 5
โข (๐ฅ = ๐พ โ (!โ๐ฅ) = (!โ๐พ)) |
2 | 1 | breq2d 5116 |
. . . 4
โข (๐ฅ = ๐พ โ (๐พ โฅ (!โ๐ฅ) โ ๐พ โฅ (!โ๐พ))) |
3 | 2 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐พ โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฅ)) โ (๐พ โ โ โ ๐พ โฅ (!โ๐พ)))) |
4 | | fveq2 6838 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (!โ๐ฅ) = (!โ๐ฆ)) |
5 | 4 | breq2d 5116 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐พ โฅ (!โ๐ฅ) โ ๐พ โฅ (!โ๐ฆ))) |
6 | 5 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฅ)) โ (๐พ โ โ โ ๐พ โฅ (!โ๐ฆ)))) |
7 | | fveq2 6838 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ (!โ๐ฅ) = (!โ(๐ฆ + 1))) |
8 | 7 | breq2d 5116 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ (๐พ โฅ (!โ๐ฅ) โ ๐พ โฅ (!โ(๐ฆ + 1)))) |
9 | 8 | imbi2d 341 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฅ)) โ (๐พ โ โ โ ๐พ โฅ (!โ(๐ฆ + 1))))) |
10 | | fveq2 6838 |
. . . . 5
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
11 | 10 | breq2d 5116 |
. . . 4
โข (๐ฅ = ๐ โ (๐พ โฅ (!โ๐ฅ) โ ๐พ โฅ (!โ๐))) |
12 | 11 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฅ)) โ (๐พ โ โ โ ๐พ โฅ (!โ๐)))) |
13 | | nnm1nn0 12388 |
. . . . . . 7
โข (๐พ โ โ โ (๐พ โ 1) โ
โ0) |
14 | 13 | faccld 14112 |
. . . . . 6
โข (๐พ โ โ โ
(!โ(๐พ โ 1))
โ โ) |
15 | 14 | nnzd 12539 |
. . . . 5
โข (๐พ โ โ โ
(!โ(๐พ โ 1))
โ โค) |
16 | | nnz 12456 |
. . . . 5
โข (๐พ โ โ โ ๐พ โ
โค) |
17 | | dvdsmul2 16096 |
. . . . 5
โข
(((!โ(๐พ
โ 1)) โ โค โง ๐พ โ โค) โ ๐พ โฅ ((!โ(๐พ โ 1)) ยท ๐พ)) |
18 | 15, 16, 17 | syl2anc 585 |
. . . 4
โข (๐พ โ โ โ ๐พ โฅ ((!โ(๐พ โ 1)) ยท ๐พ)) |
19 | | facnn2 14110 |
. . . 4
โข (๐พ โ โ โ
(!โ๐พ) =
((!โ(๐พ โ 1))
ยท ๐พ)) |
20 | 18, 19 | breqtrrd 5132 |
. . 3
โข (๐พ โ โ โ ๐พ โฅ (!โ๐พ)) |
21 | 16 | adantl 483 |
. . . . . . 7
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐พ โ โค) |
22 | | elnnuz 12736 |
. . . . . . . . . . . 12
โข (๐พ โ โ โ ๐พ โ
(โคโฅโ1)) |
23 | | uztrn 12714 |
. . . . . . . . . . . 12
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ (โคโฅโ1))
โ ๐ฆ โ
(โคโฅโ1)) |
24 | 22, 23 | sylan2b 595 |
. . . . . . . . . . 11
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐ฆ โ
(โคโฅโ1)) |
25 | | elnnuz 12736 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ๐ฆ โ
(โคโฅโ1)) |
26 | 24, 25 | sylibr 233 |
. . . . . . . . . 10
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐ฆ โ โ) |
27 | 26 | nnnn0d 12407 |
. . . . . . . . 9
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐ฆ โ โ0) |
28 | 27 | faccld 14112 |
. . . . . . . 8
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (!โ๐ฆ) โ
โ) |
29 | 28 | nnzd 12539 |
. . . . . . 7
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (!โ๐ฆ) โ
โค) |
30 | 26 | nnzd 12539 |
. . . . . . . 8
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ ๐ฆ โ โค) |
31 | 30 | peano2zd 12543 |
. . . . . . 7
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (๐ฆ + 1) โ โค) |
32 | | dvdsmultr1 16113 |
. . . . . . 7
โข ((๐พ โ โค โง
(!โ๐ฆ) โ โค
โง (๐ฆ + 1) โ
โค) โ (๐พ โฅ
(!โ๐ฆ) โ ๐พ โฅ ((!โ๐ฆ) ยท (๐ฆ + 1)))) |
33 | 21, 29, 31, 32 | syl3anc 1372 |
. . . . . 6
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (๐พ โฅ (!โ๐ฆ) โ ๐พ โฅ ((!โ๐ฆ) ยท (๐ฆ + 1)))) |
34 | | facp1 14106 |
. . . . . . . 8
โข (๐ฆ โ โ0
โ (!โ(๐ฆ + 1)) =
((!โ๐ฆ) ยท
(๐ฆ + 1))) |
35 | 27, 34 | syl 17 |
. . . . . . 7
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (!โ(๐ฆ + 1)) = ((!โ๐ฆ) ยท (๐ฆ + 1))) |
36 | 35 | breq2d 5116 |
. . . . . 6
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (๐พ โฅ (!โ(๐ฆ + 1)) โ ๐พ โฅ ((!โ๐ฆ) ยท (๐ฆ + 1)))) |
37 | 33, 36 | sylibrd 259 |
. . . . 5
โข ((๐ฆ โ
(โคโฅโ๐พ) โง ๐พ โ โ) โ (๐พ โฅ (!โ๐ฆ) โ ๐พ โฅ (!โ(๐ฆ + 1)))) |
38 | 37 | ex 414 |
. . . 4
โข (๐ฆ โ
(โคโฅโ๐พ) โ (๐พ โ โ โ (๐พ โฅ (!โ๐ฆ) โ ๐พ โฅ (!โ(๐ฆ + 1))))) |
39 | 38 | a2d 29 |
. . 3
โข (๐ฆ โ
(โคโฅโ๐พ) โ ((๐พ โ โ โ ๐พ โฅ (!โ๐ฆ)) โ (๐พ โ โ โ ๐พ โฅ (!โ(๐ฆ + 1))))) |
40 | 3, 6, 9, 12, 20, 39 | uzind4i 12764 |
. 2
โข (๐ โ
(โคโฅโ๐พ) โ (๐พ โ โ โ ๐พ โฅ (!โ๐))) |
41 | 40 | impcom 409 |
1
โข ((๐พ โ โ โง ๐ โ
(โคโฅโ๐พ)) โ ๐พ โฅ (!โ๐)) |