Step | Hyp | Ref
| Expression |
1 | | breq2 5110 |
. . . . 5
โข (๐ = 0 โ (๐ โค ๐ โ ๐ โค 0)) |
2 | | fveq2 6843 |
. . . . . . 7
โข (๐ = 0 โ (!โ๐) =
(!โ0)) |
3 | 2 | oveq1d 7373 |
. . . . . 6
โข (๐ = 0 โ ((!โ๐) / ๐) = ((!โ0) / ๐)) |
4 | 3 | eleq1d 2819 |
. . . . 5
โข (๐ = 0 โ (((!โ๐) / ๐) โ โ โ ((!โ0) / ๐) โ
โ)) |
5 | 1, 4 | imbi12d 345 |
. . . 4
โข (๐ = 0 โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (๐ โค 0 โ ((!โ0) / ๐) โ
โ))) |
6 | 5 | imbi2d 341 |
. . 3
โข (๐ = 0 โ ((๐ โ โ โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ)) โ (๐ โ โ โ (๐ โค 0 โ ((!โ0) / ๐) โ
โ)))) |
7 | | breq2 5110 |
. . . . 5
โข (๐ = ๐ โ (๐ โค ๐ โ ๐ โค ๐)) |
8 | | fveq2 6843 |
. . . . . . 7
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
9 | 8 | oveq1d 7373 |
. . . . . 6
โข (๐ = ๐ โ ((!โ๐) / ๐) = ((!โ๐) / ๐)) |
10 | 9 | eleq1d 2819 |
. . . . 5
โข (๐ = ๐ โ (((!โ๐) / ๐) โ โ โ ((!โ๐) / ๐) โ โ)) |
11 | 7, 10 | imbi12d 345 |
. . . 4
โข (๐ = ๐ โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ))) |
12 | 11 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ)) โ (๐ โ โ โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ)))) |
13 | | breq2 5110 |
. . . . 5
โข (๐ = (๐ + 1) โ (๐ โค ๐ โ ๐ โค (๐ + 1))) |
14 | | fveq2 6843 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (!โ๐) = (!โ(๐ + 1))) |
15 | 14 | oveq1d 7373 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((!โ๐) / ๐) = ((!โ(๐ + 1)) / ๐)) |
16 | 15 | eleq1d 2819 |
. . . . 5
โข (๐ = (๐ + 1) โ (((!โ๐) / ๐) โ โ โ ((!โ(๐ + 1)) / ๐) โ โ)) |
17 | 13, 16 | imbi12d 345 |
. . . 4
โข (๐ = (๐ + 1) โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (๐ โค (๐ + 1) โ ((!โ(๐ + 1)) / ๐) โ โ))) |
18 | 17 | imbi2d 341 |
. . 3
โข (๐ = (๐ + 1) โ ((๐ โ โ โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ)) โ (๐ โ โ โ (๐ โค (๐ + 1) โ ((!โ(๐ + 1)) / ๐) โ โ)))) |
19 | | breq2 5110 |
. . . . 5
โข (๐ = ๐ โ (๐ โค ๐ โ ๐ โค ๐)) |
20 | | fveq2 6843 |
. . . . . . 7
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
21 | 20 | oveq1d 7373 |
. . . . . 6
โข (๐ = ๐ โ ((!โ๐) / ๐) = ((!โ๐) / ๐)) |
22 | 21 | eleq1d 2819 |
. . . . 5
โข (๐ = ๐ โ (((!โ๐) / ๐) โ โ โ ((!โ๐) / ๐) โ โ)) |
23 | 19, 22 | imbi12d 345 |
. . . 4
โข (๐ = ๐ โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ))) |
24 | 23 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ)) โ (๐ โ โ โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ)))) |
25 | | nnnle0 12191 |
. . . 4
โข (๐ โ โ โ ยฌ
๐ โค 0) |
26 | 25 | pm2.21d 121 |
. . 3
โข (๐ โ โ โ (๐ โค 0 โ ((!โ0) /
๐) โ
โ)) |
27 | | nnre 12165 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
28 | | peano2nn0 12458 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
29 | 28 | nn0red 12479 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
30 | | leloe 11246 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ + 1) โ โ) โ
(๐ โค (๐ + 1) โ (๐ < (๐ + 1) โจ ๐ = (๐ + 1)))) |
31 | 27, 29, 30 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ โค (๐ + 1) โ (๐ < (๐ + 1) โจ ๐ = (๐ + 1)))) |
32 | | nnnn0 12425 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ0) |
33 | | nn0leltp1 12567 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
34 | 32, 33 | sylan 581 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
35 | | nn0p1nn 12457 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
36 | | nnmulcl 12182 |
. . . . . . . . . . . . . . . . . . 19
โข
((((!โ๐) /
๐) โ โ โง
(๐ + 1) โ โ)
โ (((!โ๐) /
๐) ยท (๐ + 1)) โ
โ) |
37 | 35, 36 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
โข
((((!โ๐) /
๐) โ โ โง
๐ โ
โ0) โ (((!โ๐) / ๐) ยท (๐ + 1)) โ โ) |
38 | 37 | expcom 415 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ (((!โ๐) /
๐) โ โ โ
(((!โ๐) / ๐) ยท (๐ + 1)) โ โ)) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ0)
โ (((!โ๐) /
๐) โ โ โ
(((!โ๐) / ๐) ยท (๐ + 1)) โ โ)) |
40 | | faccl 14189 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
41 | 40 | nncnd 12174 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
42 | 28 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
43 | | nncn 12166 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
44 | | nnne0 12192 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ 0) |
45 | 43, 44 | jca 513 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ (๐ โ โ โง ๐ โ 0)) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ โ โ
โง ๐ โ
0)) |
47 | | div23 11837 |
. . . . . . . . . . . . . . . . . 18
โข
(((!โ๐) โ
โ โง (๐ + 1)
โ โ โง (๐
โ โ โง ๐ โ
0)) โ (((!โ๐)
ยท (๐ + 1)) / ๐) = (((!โ๐) / ๐) ยท (๐ + 1))) |
48 | 41, 42, 46, 47 | syl2an23an 1424 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ0)
โ (((!โ๐)
ยท (๐ + 1)) / ๐) = (((!โ๐) / ๐) ยท (๐ + 1))) |
49 | 48 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ0)
โ ((((!โ๐)
ยท (๐ + 1)) / ๐) โ โ โ
(((!โ๐) / ๐) ยท (๐ + 1)) โ โ)) |
50 | 39, 49 | sylibrd 259 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ0)
โ (((!โ๐) /
๐) โ โ โ
(((!โ๐) ยท
(๐ + 1)) / ๐) โ
โ)) |
51 | 50 | imim2d 57 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (๐ โค ๐ โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ))) |
52 | 51 | com23 86 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ โค ๐ โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ))) |
53 | 34, 52 | sylbird 260 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ < (๐ + 1) โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ))) |
54 | 41 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ0)
โ (!โ๐) โ
โ) |
55 | 43 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โ) |
56 | 44 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
0) |
57 | 54, 55, 56 | divcan4d 11942 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ0)
โ (((!โ๐)
ยท ๐) / ๐) = (!โ๐)) |
58 | 40 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ0)
โ (!โ๐) โ
โ) |
59 | 57, 58 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ (((!โ๐)
ยท ๐) / ๐) โ
โ) |
60 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ + 1) โ ((!โ๐) ยท ๐) = ((!โ๐) ยท (๐ + 1))) |
61 | 60 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ + 1) โ (((!โ๐) ยท ๐) / ๐) = (((!โ๐) ยท (๐ + 1)) / ๐)) |
62 | 61 | eleq1d 2819 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ + 1) โ ((((!โ๐) ยท ๐) / ๐) โ โ โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ)) |
63 | 59, 62 | syl5ibcom 244 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ = (๐ + 1) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ)) |
64 | 63 | a1dd 50 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ = (๐ + 1) โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ))) |
65 | 53, 64 | jaod 858 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ0)
โ ((๐ < (๐ + 1) โจ ๐ = (๐ + 1)) โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ))) |
66 | 31, 65 | sylbid 239 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ โค (๐ + 1) โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ))) |
67 | 66 | ex 414 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ โ0
โ (๐ โค (๐ + 1) โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ)))) |
68 | 67 | com34 91 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ โ0
โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (๐ โค (๐ + 1) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ)))) |
69 | 68 | com12 32 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ โ
โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (๐ โค (๐ + 1) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ)))) |
70 | 69 | imp4d 426 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ โ
โง ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โง ๐ โค (๐ + 1))) โ (((!โ๐) ยท (๐ + 1)) / ๐) โ โ)) |
71 | | facp1 14184 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
72 | 71 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ โ0
โ ((!โ(๐ + 1)) /
๐) = (((!โ๐) ยท (๐ + 1)) / ๐)) |
73 | 72 | eleq1d 2819 |
. . . . . 6
โข (๐ โ โ0
โ (((!โ(๐ + 1))
/ ๐) โ โ โ
(((!โ๐) ยท
(๐ + 1)) / ๐) โ
โ)) |
74 | 70, 73 | sylibrd 259 |
. . . . 5
โข (๐ โ โ0
โ ((๐ โ โ
โง ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โง ๐ โค (๐ + 1))) โ ((!โ(๐ + 1)) / ๐) โ โ)) |
75 | 74 | exp4d 435 |
. . . 4
โข (๐ โ โ0
โ (๐ โ โ
โ ((๐ โค ๐ โ ((!โ๐) / ๐) โ โ) โ (๐ โค (๐ + 1) โ ((!โ(๐ + 1)) / ๐) โ โ)))) |
76 | 75 | a2d 29 |
. . 3
โข (๐ โ โ0
โ ((๐ โ โ
โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ)) โ (๐ โ โ โ (๐ โค (๐ + 1) โ ((!โ(๐ + 1)) / ๐) โ โ)))) |
77 | 6, 12, 18, 24, 26, 76 | nn0ind 12603 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โ (๐ โค ๐ โ ((!โ๐) / ๐) โ โ))) |
78 | 77 | 3imp 1112 |
1
โข ((๐ โ โ0
โง ๐ โ โ
โง ๐ โค ๐) โ ((!โ๐) / ๐) โ โ) |