Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
โข
((!โ๐) /
((!โ(๐ โ ๐)) ยท (!โ๐))) = ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) |
2 | | simpl 484 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
3 | | prmnn 16555 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
4 | 3 | nnzd 12531 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โค) |
5 | | 1nn0 12434 |
. . . . . . . . 9
โข 1 โ
โ0 |
6 | | eluzmn 12775 |
. . . . . . . . 9
โข ((๐ โ โค โง 1 โ
โ0) โ ๐ โ (โคโฅโ(๐ โ 1))) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
(โคโฅโ(๐ โ 1))) |
8 | | fzss2 13487 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ(๐ โ 1)) โ (1...(๐ โ 1)) โ (1...๐)) |
9 | 7, 8 | syl 17 |
. . . . . . 7
โข (๐ โ โ โ
(1...(๐ โ 1)) โ
(1...๐)) |
10 | | fz1ssfz0 13543 |
. . . . . . 7
โข
(1...๐) โ
(0...๐) |
11 | 9, 10 | sstrdi 3957 |
. . . . . 6
โข (๐ โ โ โ
(1...(๐ โ 1)) โ
(0...๐)) |
12 | 11 | sselda 3945 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ (0...๐)) |
13 | | bcval2 14211 |
. . . . 5
โข (๐ โ (0...๐) โ (๐C๐) = ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
14 | 12, 13 | syl 17 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐C๐) = ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
15 | 3 | nnnn0d 12478 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ0) |
16 | 15 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ
โ0) |
17 | | elfzelz 13447 |
. . . . . . 7
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โค) |
18 | 17 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โค) |
19 | | bccl 14228 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โค)
โ (๐C๐) โ
โ0) |
20 | 16, 18, 19 | syl2anc 585 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐C๐) โ
โ0) |
21 | 20 | nn0zd 12530 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐C๐) โ โค) |
22 | 14, 21 | eqeltrrd 2835 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) โ โค) |
23 | | elfznn 13476 |
. . . . . . . . 9
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
24 | 23 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
25 | 24 | nnnn0d 12478 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ
โ0) |
26 | | 1zzd 12539 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ 1 โ
โค) |
27 | 4 | adantr 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โค) |
28 | | simpr 486 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ (1...(๐ โ 1))) |
29 | | elfzm11 13518 |
. . . . . . . . . 10
โข ((1
โ โค โง ๐
โ โค) โ (๐
โ (1...(๐ โ 1))
โ (๐ โ โค
โง 1 โค ๐ โง ๐ < ๐))) |
30 | 29 | biimpa 478 |
. . . . . . . . 9
โข (((1
โ โค โง ๐
โ โค) โง ๐
โ (1...(๐ โ 1)))
โ (๐ โ โค
โง 1 โค ๐ โง ๐ < ๐)) |
31 | 30 | simp3d 1145 |
. . . . . . . 8
โข (((1
โ โค โง ๐
โ โค) โง ๐
โ (1...(๐ โ 1)))
โ ๐ < ๐) |
32 | 26, 27, 28, 31 | syl21anc 837 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ < ๐) |
33 | | ltsubnn0 12469 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ < ๐ โ (๐ โ ๐) โ
โ0)) |
34 | 33 | imp 408 |
. . . . . . 7
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ๐ < ๐) โ (๐ โ ๐) โ
โ0) |
35 | 16, 25, 32, 34 | syl21anc 837 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โ ๐) โ
โ0) |
36 | 35 | faccld 14190 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (!โ(๐ โ ๐)) โ โ) |
37 | 36 | nnzd 12531 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (!โ(๐ โ ๐)) โ โค) |
38 | 25 | faccld 14190 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (!โ๐) โ
โ) |
39 | 38 | nnzd 12531 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (!โ๐) โ
โค) |
40 | 37, 39 | zmulcld 12618 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((!โ(๐ โ ๐)) ยท (!โ๐)) โ โค) |
41 | 37 | zcnd 12613 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (!โ(๐ โ ๐)) โ โ) |
42 | 39 | zcnd 12613 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (!โ๐) โ
โ) |
43 | | facne0 14192 |
. . . . 5
โข ((๐ โ ๐) โ โ0 โ
(!โ(๐ โ ๐)) โ 0) |
44 | 35, 43 | syl 17 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (!โ(๐ โ ๐)) โ 0) |
45 | | facne0 14192 |
. . . . 5
โข (๐ โ โ0
โ (!โ๐) โ
0) |
46 | 25, 45 | syl 17 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (!โ๐) โ 0) |
47 | 41, 42, 44, 46 | mulne0d 11812 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((!โ(๐ โ ๐)) ยท (!โ๐)) โ 0) |
48 | | uzid 12783 |
. . . . . 6
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
49 | 4, 48 | syl 17 |
. . . . 5
โข (๐ โ โ โ ๐ โ
(โคโฅโ๐)) |
50 | | dvdsfac 16213 |
. . . . 5
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โฅ (!โ๐)) |
51 | 3, 49, 50 | syl2anc 585 |
. . . 4
โข (๐ โ โ โ ๐ โฅ (!โ๐)) |
52 | 51 | adantr 482 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โฅ (!โ๐)) |
53 | 16 | nn0red 12479 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
54 | 24 | nnrpd 12960 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ
โ+) |
55 | 53, 54 | ltsubrpd 12994 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โ ๐) < ๐) |
56 | | prmndvdsfaclt 16606 |
. . . . . 6
โข ((๐ โ โ โง (๐ โ ๐) โ โ0) โ ((๐ โ ๐) < ๐ โ ยฌ ๐ โฅ (!โ(๐ โ ๐)))) |
57 | 56 | imp 408 |
. . . . 5
โข (((๐ โ โ โง (๐ โ ๐) โ โ0) โง (๐ โ ๐) < ๐) โ ยฌ ๐ โฅ (!โ(๐ โ ๐))) |
58 | 2, 35, 55, 57 | syl21anc 837 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ (!โ(๐ โ ๐))) |
59 | | prmndvdsfaclt 16606 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ < ๐ โ ยฌ ๐ โฅ (!โ๐))) |
60 | 59 | imp 408 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ < ๐) โ ยฌ ๐ โฅ (!โ๐)) |
61 | 2, 25, 32, 60 | syl21anc 837 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ (!โ๐)) |
62 | | ioran 983 |
. . . . . 6
โข (ยฌ
(๐ โฅ (!โ(๐ โ ๐)) โจ ๐ โฅ (!โ๐)) โ (ยฌ ๐ โฅ (!โ(๐ โ ๐)) โง ยฌ ๐ โฅ (!โ๐))) |
63 | | euclemma 16594 |
. . . . . . . 8
โข ((๐ โ โ โง
(!โ(๐ โ ๐)) โ โค โง
(!โ๐) โ โค)
โ (๐ โฅ
((!โ(๐ โ ๐)) ยท (!โ๐)) โ (๐ โฅ (!โ(๐ โ ๐)) โจ ๐ โฅ (!โ๐)))) |
64 | 63 | biimpd 228 |
. . . . . . 7
โข ((๐ โ โ โง
(!โ(๐ โ ๐)) โ โค โง
(!โ๐) โ โค)
โ (๐ โฅ
((!โ(๐ โ ๐)) ยท (!โ๐)) โ (๐ โฅ (!โ(๐ โ ๐)) โจ ๐ โฅ (!โ๐)))) |
65 | 64 | con3d 152 |
. . . . . 6
โข ((๐ โ โ โง
(!โ(๐ โ ๐)) โ โค โง
(!โ๐) โ โค)
โ (ยฌ (๐ โฅ
(!โ(๐ โ ๐)) โจ ๐ โฅ (!โ๐)) โ ยฌ ๐ โฅ ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
66 | 62, 65 | biimtrrid 242 |
. . . . 5
โข ((๐ โ โ โง
(!โ(๐ โ ๐)) โ โค โง
(!โ๐) โ โค)
โ ((ยฌ ๐ โฅ
(!โ(๐ โ ๐)) โง ยฌ ๐ โฅ (!โ๐)) โ ยฌ ๐ โฅ ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
67 | 66 | imp 408 |
. . . 4
โข (((๐ โ โ โง
(!โ(๐ โ ๐)) โ โค โง
(!โ๐) โ โค)
โง (ยฌ ๐ โฅ
(!โ(๐ โ ๐)) โง ยฌ ๐ โฅ (!โ๐))) โ ยฌ ๐ โฅ ((!โ(๐ โ ๐)) ยท (!โ๐))) |
68 | 2, 37, 39, 58, 61, 67 | syl32anc 1379 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ((!โ(๐ โ ๐)) ยท (!โ๐))) |
69 | 1, 2, 22, 40, 47, 52, 68 | dvdszzq 31760 |
. 2
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โฅ ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
70 | 69, 14 | breqtrrd 5134 |
1
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โฅ (๐C๐)) |