Step | Hyp | Ref
| Expression |
1 | | breq2 5110 |
. . . . . 6
โข (๐ = 0 โ (๐ โค ๐ โ ๐ โค 0)) |
2 | 1 | anbi2d 630 |
. . . . 5
โข (๐ = 0 โ ((๐ โ โ0 โง ๐ โค ๐) โ (๐ โ โ0 โง ๐ โค 0))) |
3 | | fveq2 6843 |
. . . . . 6
โข (๐ = 0 โ (!โ๐) =
(!โ0)) |
4 | 3 | breq2d 5118 |
. . . . 5
โข (๐ = 0 โ ((!โ๐) โค (!โ๐) โ (!โ๐) โค
(!โ0))) |
5 | 2, 4 | imbi12d 345 |
. . . 4
โข (๐ = 0 โ (((๐ โ โ0 โง ๐ โค ๐) โ (!โ๐) โค (!โ๐)) โ ((๐ โ โ0 โง ๐ โค 0) โ (!โ๐) โค
(!โ0)))) |
6 | | breq2 5110 |
. . . . . 6
โข (๐ = ๐ โ (๐ โค ๐ โ ๐ โค ๐)) |
7 | 6 | anbi2d 630 |
. . . . 5
โข (๐ = ๐ โ ((๐ โ โ0 โง ๐ โค ๐) โ (๐ โ โ0 โง ๐ โค ๐))) |
8 | | fveq2 6843 |
. . . . . 6
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
9 | 8 | breq2d 5118 |
. . . . 5
โข (๐ = ๐ โ ((!โ๐) โค (!โ๐) โ (!โ๐) โค (!โ๐))) |
10 | 7, 9 | imbi12d 345 |
. . . 4
โข (๐ = ๐ โ (((๐ โ โ0 โง ๐ โค ๐) โ (!โ๐) โค (!โ๐)) โ ((๐ โ โ0 โง ๐ โค ๐) โ (!โ๐) โค (!โ๐)))) |
11 | | breq2 5110 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ โค ๐ โ ๐ โค (๐ + 1))) |
12 | 11 | anbi2d 630 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ โ โ0 โง ๐ โค ๐) โ (๐ โ โ0 โง ๐ โค (๐ + 1)))) |
13 | | fveq2 6843 |
. . . . . 6
โข (๐ = (๐ + 1) โ (!โ๐) = (!โ(๐ + 1))) |
14 | 13 | breq2d 5118 |
. . . . 5
โข (๐ = (๐ + 1) โ ((!โ๐) โค (!โ๐) โ (!โ๐) โค (!โ(๐ + 1)))) |
15 | 12, 14 | imbi12d 345 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ โ โ0 โง ๐ โค ๐) โ (!โ๐) โค (!โ๐)) โ ((๐ โ โ0 โง ๐ โค (๐ + 1)) โ (!โ๐) โค (!โ(๐ + 1))))) |
16 | | breq2 5110 |
. . . . . 6
โข (๐ = ๐ โ (๐ โค ๐ โ ๐ โค ๐)) |
17 | 16 | anbi2d 630 |
. . . . 5
โข (๐ = ๐ โ ((๐ โ โ0 โง ๐ โค ๐) โ (๐ โ โ0 โง ๐ โค ๐))) |
18 | | fveq2 6843 |
. . . . . 6
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
19 | 18 | breq2d 5118 |
. . . . 5
โข (๐ = ๐ โ ((!โ๐) โค (!โ๐) โ (!โ๐) โค (!โ๐))) |
20 | 17, 19 | imbi12d 345 |
. . . 4
โข (๐ = ๐ โ (((๐ โ โ0 โง ๐ โค ๐) โ (!โ๐) โค (!โ๐)) โ ((๐ โ โ0 โง ๐ โค ๐) โ (!โ๐) โค (!โ๐)))) |
21 | | nn0le0eq0 12446 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โค 0 โ
๐ = 0)) |
22 | 21 | biimpa 478 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โค 0) โ
๐ = 0) |
23 | 22 | fveq2d 6847 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โค 0) โ
(!โ๐) =
(!โ0)) |
24 | | fac0 14182 |
. . . . . . 7
โข
(!โ0) = 1 |
25 | | 1re 11160 |
. . . . . . 7
โข 1 โ
โ |
26 | 24, 25 | eqeltri 2830 |
. . . . . 6
โข
(!โ0) โ โ |
27 | 26 | leidi 11694 |
. . . . 5
โข
(!โ0) โค (!โ0) |
28 | 23, 27 | eqbrtrdi 5145 |
. . . 4
โข ((๐ โ โ0
โง ๐ โค 0) โ
(!โ๐) โค
(!โ0)) |
29 | | impexp 452 |
. . . . 5
โข (((๐ โ โ0
โง ๐ โค ๐) โ (!โ๐) โค (!โ๐)) โ (๐ โ โ0 โ (๐ โค ๐ โ (!โ๐) โค (!โ๐)))) |
30 | | nn0re 12427 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ) |
31 | | nn0re 12427 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ๐ โ
โ) |
32 | | peano2re 11333 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ + 1) โ
โ) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
34 | | leloe 11246 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ + 1) โ โ) โ
(๐ โค (๐ + 1) โ (๐ < (๐ + 1) โจ ๐ = (๐ + 1)))) |
35 | 30, 33, 34 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โค (๐ + 1) โ (๐ < (๐ + 1) โจ ๐ = (๐ + 1)))) |
36 | | nn0leltp1 12567 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
37 | | faccl 14189 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
38 | 37 | nnred 12173 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
39 | 37 | nnnn0d 12478 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ0
โ (!โ๐) โ
โ0) |
40 | 39 | nn0ge0d 12481 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ 0 โค (!โ๐)) |
41 | | nn0p1nn 12457 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
42 | 41 | nnge1d 12206 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ 1 โค (๐ +
1)) |
43 | 38, 33, 40, 42 | lemulge11d 12097 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (!โ๐) โค
((!โ๐) ยท
(๐ + 1))) |
44 | | facp1 14184 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
45 | 43, 44 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ (!โ๐) โค
(!โ(๐ +
1))) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โค (!โ(๐ + 1))) |
47 | | faccl 14189 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
48 | 47 | nnred 12173 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โ โ) |
50 | 38 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โ โ) |
51 | | peano2nn0 12458 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
52 | 51 | faccld 14190 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ (!โ(๐ + 1))
โ โ) |
53 | 52 | nnred 12173 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (!โ(๐ + 1))
โ โ) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(๐ + 1)) โ โ) |
55 | | letr 11254 |
. . . . . . . . . . . . . . . . 17
โข
(((!โ๐) โ
โ โง (!โ๐)
โ โ โง (!โ(๐ + 1)) โ โ) โ
(((!โ๐) โค
(!โ๐) โง
(!โ๐) โค
(!โ(๐ + 1))) โ
(!โ๐) โค
(!โ(๐ +
1)))) |
56 | 49, 50, 54, 55 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((!โ๐) โค (!โ๐) โง (!โ๐) โค (!โ(๐ + 1))) โ (!โ๐) โค (!โ(๐ + 1)))) |
57 | 46, 56 | mpan2d 693 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) โค (!โ๐) โ (!โ๐) โค (!โ(๐ + 1)))) |
58 | 57 | imim2d 57 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (๐ โค ๐ โ (!โ๐) โค (!โ(๐ + 1))))) |
59 | 58 | com23 86 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โค ๐ โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (!โ๐) โค (!โ(๐ + 1))))) |
60 | 36, 59 | sylbird 260 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ < (๐ + 1) โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (!โ๐) โค (!โ(๐ + 1))))) |
61 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ + 1) โ (!โ๐) = (!โ(๐ + 1))) |
62 | 48 | leidd 11726 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ (!โ๐) โค
(!โ๐)) |
63 | | breq2 5110 |
. . . . . . . . . . . . . . . 16
โข
((!โ๐) =
(!โ(๐ + 1)) โ
((!โ๐) โค
(!โ๐) โ
(!โ๐) โค
(!โ(๐ +
1)))) |
64 | 62, 63 | syl5ibcom 244 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ((!โ๐) =
(!โ(๐ + 1)) โ
(!โ๐) โค
(!โ(๐ +
1)))) |
65 | 61, 64 | syl5 34 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (๐ = (๐ + 1) โ (!โ๐) โค (!โ(๐ + 1)))) |
66 | 65 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ = (๐ + 1) โ (!โ๐) โค (!โ(๐ + 1)))) |
67 | 66 | a1dd 50 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ = (๐ + 1) โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (!โ๐) โค (!โ(๐ + 1))))) |
68 | 60, 67 | jaod 858 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ < (๐ + 1) โจ ๐ = (๐ + 1)) โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (!โ๐) โค (!โ(๐ + 1))))) |
69 | 35, 68 | sylbid 239 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โค (๐ + 1) โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (!โ๐) โค (!โ(๐ + 1))))) |
70 | 69 | ex 414 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ โ
โ0 โ (๐ โค (๐ + 1) โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (!โ๐) โค (!โ(๐ + 1)))))) |
71 | 70 | com13 88 |
. . . . . . . 8
โข (๐ โค (๐ + 1) โ (๐ โ โ0 โ (๐ โ โ0
โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (!โ๐) โค (!โ(๐ + 1)))))) |
72 | 71 | com4l 92 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ
โ0 โ ((๐ โค ๐ โ (!โ๐) โค (!โ๐)) โ (๐ โค (๐ + 1) โ (!โ๐) โค (!โ(๐ + 1)))))) |
73 | 72 | a2d 29 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ
โ0 โ (๐ โค ๐ โ (!โ๐) โค (!โ๐))) โ (๐ โ โ0 โ (๐ โค (๐ + 1) โ (!โ๐) โค (!โ(๐ + 1)))))) |
74 | 73 | imp4a 424 |
. . . . 5
โข (๐ โ โ0
โ ((๐ โ
โ0 โ (๐ โค ๐ โ (!โ๐) โค (!โ๐))) โ ((๐ โ โ0 โง ๐ โค (๐ + 1)) โ (!โ๐) โค (!โ(๐ + 1))))) |
75 | 29, 74 | biimtrid 241 |
. . . 4
โข (๐ โ โ0
โ (((๐ โ
โ0 โง ๐
โค ๐) โ
(!โ๐) โค
(!โ๐)) โ ((๐ โ โ0
โง ๐ โค (๐ + 1)) โ (!โ๐) โค (!โ(๐ + 1))))) |
76 | 5, 10, 15, 20, 28, 75 | nn0ind 12603 |
. . 3
โข (๐ โ โ0
โ ((๐ โ
โ0 โง ๐
โค ๐) โ
(!โ๐) โค
(!โ๐))) |
77 | 76 | 3impib 1117 |
. 2
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โค ๐) โ
(!โ๐) โค
(!โ๐)) |
78 | 77 | 3com12 1124 |
1
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โค ๐) โ
(!โ๐) โค
(!โ๐)) |