Step | Hyp | Ref
| Expression |
1 | | elnn0 12473 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
2 | | nnre 12218 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
3 | 2 | adantr 481 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โ) |
4 | | nnge1 12239 |
. . . . . 6
โข (๐ โ โ โ 1 โค
๐) |
5 | 4 | adantr 481 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0)
โ 1 โค ๐) |
6 | | nn0z 12582 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โค) |
7 | 6 | adantl 482 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โค) |
8 | | uzid 12836 |
. . . . . 6
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
9 | | peano2uz 12884 |
. . . . . 6
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
10 | 7, 8, 9 | 3syl 18 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ + 1) โ
(โคโฅโ๐)) |
11 | 3, 5, 10 | leexp2ad 14216 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โค (๐โ(๐ + 1))) |
12 | | nnnn0 12478 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ0) |
13 | | faclbnd 14249 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐โ(๐ + 1)) โค ((๐โ๐) ยท (!โ๐))) |
14 | 12, 13 | sylan 580 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ(๐ + 1)) โค ((๐โ๐) ยท (!โ๐))) |
15 | | nn0re 12480 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โ) |
16 | | reexpcl 14043 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
17 | 15, 16 | sylan 580 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐โ๐) โ โ) |
18 | | peano2nn0 12511 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
19 | | reexpcl 14043 |
. . . . . . 7
โข ((๐ โ โ โง (๐ + 1) โ
โ0) โ (๐โ(๐ + 1)) โ โ) |
20 | 15, 18, 19 | syl2an 596 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐โ(๐ + 1)) โ โ) |
21 | | reexpcl 14043 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
22 | 15, 21 | mpancom 686 |
. . . . . . 7
โข (๐ โ โ0
โ (๐โ๐) โ
โ) |
23 | | faccl 14242 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
24 | 23 | nnred 12226 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
25 | | remulcl 11194 |
. . . . . . 7
โข (((๐โ๐) โ โ โง (!โ๐) โ โ) โ ((๐โ๐) ยท (!โ๐)) โ โ) |
26 | 22, 24, 25 | syl2an 596 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐โ๐) ยท (!โ๐)) โ โ) |
27 | | letr 11307 |
. . . . . 6
โข (((๐โ๐) โ โ โง (๐โ(๐ + 1)) โ โ โง ((๐โ๐) ยท (!โ๐)) โ โ) โ (((๐โ๐) โค (๐โ(๐ + 1)) โง (๐โ(๐ + 1)) โค ((๐โ๐) ยท (!โ๐))) โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐)))) |
28 | 17, 20, 26, 27 | syl3anc 1371 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐โ๐) โค (๐โ(๐ + 1)) โง (๐โ(๐ + 1)) โค ((๐โ๐) ยท (!โ๐))) โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐)))) |
29 | 12, 28 | sylan 580 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (((๐โ๐) โค (๐โ(๐ + 1)) โง (๐โ(๐ + 1)) โค ((๐โ๐) ยท (!โ๐))) โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐)))) |
30 | 11, 14, 29 | mp2and 697 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐))) |
31 | | elnn0 12473 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
32 | | 0exp 14062 |
. . . . . . . . 9
โข (๐ โ โ โ
(0โ๐) =
0) |
33 | | 0le1 11736 |
. . . . . . . . 9
โข 0 โค
1 |
34 | 32, 33 | eqbrtrdi 5187 |
. . . . . . . 8
โข (๐ โ โ โ
(0โ๐) โค
1) |
35 | | oveq2 7416 |
. . . . . . . . 9
โข (๐ = 0 โ (0โ๐) = (0โ0)) |
36 | | 0exp0e1 14031 |
. . . . . . . . . 10
โข
(0โ0) = 1 |
37 | | 1le1 11841 |
. . . . . . . . . 10
โข 1 โค
1 |
38 | 36, 37 | eqbrtri 5169 |
. . . . . . . . 9
โข
(0โ0) โค 1 |
39 | 35, 38 | eqbrtrdi 5187 |
. . . . . . . 8
โข (๐ = 0 โ (0โ๐) โค 1) |
40 | 34, 39 | jaoi 855 |
. . . . . . 7
โข ((๐ โ โ โจ ๐ = 0) โ (0โ๐) โค 1) |
41 | 31, 40 | sylbi 216 |
. . . . . 6
โข (๐ โ โ0
โ (0โ๐) โค
1) |
42 | | 1nn 12222 |
. . . . . . . 8
โข 1 โ
โ |
43 | | nnmulcl 12235 |
. . . . . . . 8
โข ((1
โ โ โง (!โ๐) โ โ) โ (1 ยท
(!โ๐)) โ
โ) |
44 | 42, 23, 43 | sylancr 587 |
. . . . . . 7
โข (๐ โ โ0
โ (1 ยท (!โ๐)) โ โ) |
45 | 44 | nnge1d 12259 |
. . . . . 6
โข (๐ โ โ0
โ 1 โค (1 ยท (!โ๐))) |
46 | | 0re 11215 |
. . . . . . . 8
โข 0 โ
โ |
47 | | reexpcl 14043 |
. . . . . . . 8
โข ((0
โ โ โง ๐
โ โ0) โ (0โ๐) โ โ) |
48 | 46, 47 | mpan 688 |
. . . . . . 7
โข (๐ โ โ0
โ (0โ๐) โ
โ) |
49 | | 1re 11213 |
. . . . . . . 8
โข 1 โ
โ |
50 | | remulcl 11194 |
. . . . . . . 8
โข ((1
โ โ โง (!โ๐) โ โ) โ (1 ยท
(!โ๐)) โ
โ) |
51 | 49, 24, 50 | sylancr 587 |
. . . . . . 7
โข (๐ โ โ0
โ (1 ยท (!โ๐)) โ โ) |
52 | | letr 11307 |
. . . . . . . 8
โข
(((0โ๐) โ
โ โง 1 โ โ โง (1 ยท (!โ๐)) โ โ) โ (((0โ๐) โค 1 โง 1 โค (1
ยท (!โ๐)))
โ (0โ๐) โค (1
ยท (!โ๐)))) |
53 | 49, 52 | mp3an2 1449 |
. . . . . . 7
โข
(((0โ๐) โ
โ โง (1 ยท (!โ๐)) โ โ) โ (((0โ๐) โค 1 โง 1 โค (1
ยท (!โ๐)))
โ (0โ๐) โค (1
ยท (!โ๐)))) |
54 | 48, 51, 53 | syl2anc 584 |
. . . . . 6
โข (๐ โ โ0
โ (((0โ๐) โค 1
โง 1 โค (1 ยท (!โ๐))) โ (0โ๐) โค (1 ยท (!โ๐)))) |
55 | 41, 45, 54 | mp2and 697 |
. . . . 5
โข (๐ โ โ0
โ (0โ๐) โค (1
ยท (!โ๐))) |
56 | 55 | adantl 482 |
. . . 4
โข ((๐ = 0 โง ๐ โ โ0) โ
(0โ๐) โค (1 ยท
(!โ๐))) |
57 | | oveq1 7415 |
. . . . . 6
โข (๐ = 0 โ (๐โ๐) = (0โ๐)) |
58 | | oveq12 7417 |
. . . . . . . . 9
โข ((๐ = 0 โง ๐ = 0) โ (๐โ๐) = (0โ0)) |
59 | 58 | anidms 567 |
. . . . . . . 8
โข (๐ = 0 โ (๐โ๐) = (0โ0)) |
60 | 59, 36 | eqtrdi 2788 |
. . . . . . 7
โข (๐ = 0 โ (๐โ๐) = 1) |
61 | 60 | oveq1d 7423 |
. . . . . 6
โข (๐ = 0 โ ((๐โ๐) ยท (!โ๐)) = (1 ยท (!โ๐))) |
62 | 57, 61 | breq12d 5161 |
. . . . 5
โข (๐ = 0 โ ((๐โ๐) โค ((๐โ๐) ยท (!โ๐)) โ (0โ๐) โค (1 ยท (!โ๐)))) |
63 | 62 | adantr 481 |
. . . 4
โข ((๐ = 0 โง ๐ โ โ0) โ ((๐โ๐) โค ((๐โ๐) ยท (!โ๐)) โ (0โ๐) โค (1 ยท (!โ๐)))) |
64 | 56, 63 | mpbird 256 |
. . 3
โข ((๐ = 0 โง ๐ โ โ0) โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐))) |
65 | 30, 64 | jaoian 955 |
. 2
โข (((๐ โ โ โจ ๐ = 0) โง ๐ โ โ0) โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐))) |
66 | 1, 65 | sylanb 581 |
1
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐))) |