Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = 0 โ (!โ๐ฅ) =
(!โ0)) |
2 | 1 | breq2d 5122 |
. . . . 5
โข (๐ฅ = 0 โ (๐ โฅ (!โ๐ฅ) โ ๐ โฅ (!โ0))) |
3 | | breq2 5114 |
. . . . 5
โข (๐ฅ = 0 โ (๐ โค ๐ฅ โ ๐ โค 0)) |
4 | 2, 3 | imbi12d 345 |
. . . 4
โข (๐ฅ = 0 โ ((๐ โฅ (!โ๐ฅ) โ ๐ โค ๐ฅ) โ (๐ โฅ (!โ0) โ ๐ โค 0))) |
5 | 4 | imbi2d 341 |
. . 3
โข (๐ฅ = 0 โ ((๐ โ โ โ (๐ โฅ (!โ๐ฅ) โ ๐ โค ๐ฅ)) โ (๐ โ โ โ (๐ โฅ (!โ0) โ ๐ โค 0)))) |
6 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
7 | 6 | breq2d 5122 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ โฅ (!โ๐ฅ) โ ๐ โฅ (!โ๐))) |
8 | | breq2 5114 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ โค ๐ฅ โ ๐ โค ๐)) |
9 | 7, 8 | imbi12d 345 |
. . . 4
โข (๐ฅ = ๐ โ ((๐ โฅ (!โ๐ฅ) โ ๐ โค ๐ฅ) โ (๐ โฅ (!โ๐) โ ๐ โค ๐))) |
10 | 9 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ โ ((๐ โ โ โ (๐ โฅ (!โ๐ฅ) โ ๐ โค ๐ฅ)) โ (๐ โ โ โ (๐ โฅ (!โ๐) โ ๐ โค ๐)))) |
11 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = (๐ + 1) โ (!โ๐ฅ) = (!โ(๐ + 1))) |
12 | 11 | breq2d 5122 |
. . . . 5
โข (๐ฅ = (๐ + 1) โ (๐ โฅ (!โ๐ฅ) โ ๐ โฅ (!โ(๐ + 1)))) |
13 | | breq2 5114 |
. . . . 5
โข (๐ฅ = (๐ + 1) โ (๐ โค ๐ฅ โ ๐ โค (๐ + 1))) |
14 | 12, 13 | imbi12d 345 |
. . . 4
โข (๐ฅ = (๐ + 1) โ ((๐ โฅ (!โ๐ฅ) โ ๐ โค ๐ฅ) โ (๐ โฅ (!โ(๐ + 1)) โ ๐ โค (๐ + 1)))) |
15 | 14 | imbi2d 341 |
. . 3
โข (๐ฅ = (๐ + 1) โ ((๐ โ โ โ (๐ โฅ (!โ๐ฅ) โ ๐ โค ๐ฅ)) โ (๐ โ โ โ (๐ โฅ (!โ(๐ + 1)) โ ๐ โค (๐ + 1))))) |
16 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
17 | 16 | breq2d 5122 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ โฅ (!โ๐ฅ) โ ๐ โฅ (!โ๐))) |
18 | | breq2 5114 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ โค ๐ฅ โ ๐ โค ๐)) |
19 | 17, 18 | imbi12d 345 |
. . . 4
โข (๐ฅ = ๐ โ ((๐ โฅ (!โ๐ฅ) โ ๐ โค ๐ฅ) โ (๐ โฅ (!โ๐) โ ๐ โค ๐))) |
20 | 19 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ โ ((๐ โ โ โ (๐ โฅ (!โ๐ฅ) โ ๐ โค ๐ฅ)) โ (๐ โ โ โ (๐ โฅ (!โ๐) โ ๐ โค ๐)))) |
21 | | fac0 14183 |
. . . . 5
โข
(!โ0) = 1 |
22 | 21 | breq2i 5118 |
. . . 4
โข (๐ โฅ (!โ0) โ
๐ โฅ
1) |
23 | | nprmdvds1 16589 |
. . . . 5
โข (๐ โ โ โ ยฌ
๐ โฅ
1) |
24 | 23 | pm2.21d 121 |
. . . 4
โข (๐ โ โ โ (๐ โฅ 1 โ ๐ โค 0)) |
25 | 22, 24 | biimtrid 241 |
. . 3
โข (๐ โ โ โ (๐ โฅ (!โ0) โ
๐ โค 0)) |
26 | | facp1 14185 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
27 | 26 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
28 | 27 | breq2d 5122 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โฅ
(!โ(๐ + 1)) โ
๐ โฅ ((!โ๐) ยท (๐ + 1)))) |
29 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
30 | | faccl 14190 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
31 | 30 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ๐) โ
โ) |
32 | 31 | nnzd 12533 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (!โ๐) โ
โค) |
33 | | nn0p1nn 12459 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
34 | 33 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โ) |
35 | 34 | nnzd 12533 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โค) |
36 | | euclemma 16596 |
. . . . . . . . 9
โข ((๐ โ โ โง
(!โ๐) โ โค
โง (๐ + 1) โ
โค) โ (๐ โฅ
((!โ๐) ยท
(๐ + 1)) โ (๐ โฅ (!โ๐) โจ ๐ โฅ (๐ + 1)))) |
37 | 29, 32, 35, 36 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โฅ
((!โ๐) ยท
(๐ + 1)) โ (๐ โฅ (!โ๐) โจ ๐ โฅ (๐ + 1)))) |
38 | 28, 37 | bitrd 279 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โฅ
(!โ(๐ + 1)) โ
(๐ โฅ (!โ๐) โจ ๐ โฅ (๐ + 1)))) |
39 | | nn0re 12429 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ๐ โ
โ) |
40 | 39 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
41 | 40 | lep1d 12093 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โค (๐ + 1)) |
42 | | prmz 16558 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โค) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โค) |
44 | 43 | zred 12614 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
45 | 34 | nnred 12175 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
โ) |
46 | | letr 11256 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ โง (๐ + 1) โ โ) โ
((๐ โค ๐ โง ๐ โค (๐ + 1)) โ ๐ โค (๐ + 1))) |
47 | 44, 40, 45, 46 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โค ๐ โง ๐ โค (๐ + 1)) โ ๐ โค (๐ + 1))) |
48 | 41, 47 | mpan2d 693 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โค ๐ โ ๐ โค (๐ + 1))) |
49 | 48 | imim2d 57 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โฅ
(!โ๐) โ ๐ โค ๐) โ (๐ โฅ (!โ๐) โ ๐ โค (๐ + 1)))) |
50 | 49 | com23 86 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โฅ
(!โ๐) โ ((๐ โฅ (!โ๐) โ ๐ โค ๐) โ ๐ โค (๐ + 1)))) |
51 | | dvdsle 16199 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ + 1) โ โ) โ
(๐ โฅ (๐ + 1) โ ๐ โค (๐ + 1))) |
52 | 43, 34, 51 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โฅ (๐ + 1) โ ๐ โค (๐ + 1))) |
53 | 52 | a1dd 50 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โฅ (๐ + 1) โ ((๐ โฅ (!โ๐) โ ๐ โค ๐) โ ๐ โค (๐ + 1)))) |
54 | 50, 53 | jaod 858 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โฅ
(!โ๐) โจ ๐ โฅ (๐ + 1)) โ ((๐ โฅ (!โ๐) โ ๐ โค ๐) โ ๐ โค (๐ + 1)))) |
55 | 38, 54 | sylbid 239 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โฅ
(!โ(๐ + 1)) โ
((๐ โฅ (!โ๐) โ ๐ โค ๐) โ ๐ โค (๐ + 1)))) |
56 | 55 | com23 86 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โฅ
(!โ๐) โ ๐ โค ๐) โ (๐ โฅ (!โ(๐ + 1)) โ ๐ โค (๐ + 1)))) |
57 | 56 | ex 414 |
. . . 4
โข (๐ โ โ0
โ (๐ โ โ
โ ((๐ โฅ
(!โ๐) โ ๐ โค ๐) โ (๐ โฅ (!โ(๐ + 1)) โ ๐ โค (๐ + 1))))) |
58 | 57 | a2d 29 |
. . 3
โข (๐ โ โ0
โ ((๐ โ โ
โ (๐ โฅ
(!โ๐) โ ๐ โค ๐)) โ (๐ โ โ โ (๐ โฅ (!โ(๐ + 1)) โ ๐ โค (๐ + 1))))) |
59 | 5, 10, 15, 20, 25, 58 | nn0ind 12605 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โ (๐ โฅ
(!โ๐) โ ๐ โค ๐))) |
60 | 59 | 3imp 1112 |
1
โข ((๐ โ โ0
โง ๐ โ โ
โง ๐ โฅ
(!โ๐)) โ ๐ โค ๐) |