Step | Hyp | Ref
| Expression |
1 | | prmuz2 16635 |
. . . . . . . 8
β’ (π β β β π β
(β€β₯β2)) |
2 | | uz2m1nn 12909 |
. . . . . . . 8
β’ (π β
(β€β₯β2) β (π β 1) β β) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (π β β β (π β 1) β
β) |
4 | | nnuz 12867 |
. . . . . . 7
β’ β =
(β€β₯β1) |
5 | 3, 4 | eleqtrdi 2843 |
. . . . . 6
β’ (π β β β (π β 1) β
(β€β₯β1)) |
6 | | eluzfz2 13511 |
. . . . . 6
β’ ((π β 1) β
(β€β₯β1) β (π β 1) β (1...(π β 1))) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π β β β (π β 1) β (1...(π β 1))) |
8 | | simpl 483 |
. . . . . . . 8
β’ ((π β β β§ π¦ β (1...(π β 1))) β π β β) |
9 | | elfzelz 13503 |
. . . . . . . . 9
β’ (π¦ β (1...(π β 1)) β π¦ β β€) |
10 | 9 | adantl 482 |
. . . . . . . 8
β’ ((π β β β§ π¦ β (1...(π β 1))) β π¦ β β€) |
11 | | prmnn 16613 |
. . . . . . . . 9
β’ (π β β β π β
β) |
12 | | fzm1ndvds 16267 |
. . . . . . . . 9
β’ ((π β β β§ π¦ β (1...(π β 1))) β Β¬ π β₯ π¦) |
13 | 11, 12 | sylan 580 |
. . . . . . . 8
β’ ((π β β β§ π¦ β (1...(π β 1))) β Β¬ π β₯ π¦) |
14 | | eqid 2732 |
. . . . . . . . 9
β’ ((π¦β(π β 2)) mod π) = ((π¦β(π β 2)) mod π) |
15 | 14 | prmdiv 16720 |
. . . . . . . 8
β’ ((π β β β§ π¦ β β€ β§ Β¬
π β₯ π¦) β (((π¦β(π β 2)) mod π) β (1...(π β 1)) β§ π β₯ ((π¦ Β· ((π¦β(π β 2)) mod π)) β 1))) |
16 | 8, 10, 13, 15 | syl3anc 1371 |
. . . . . . 7
β’ ((π β β β§ π¦ β (1...(π β 1))) β (((π¦β(π β 2)) mod π) β (1...(π β 1)) β§ π β₯ ((π¦ Β· ((π¦β(π β 2)) mod π)) β 1))) |
17 | 16 | simpld 495 |
. . . . . 6
β’ ((π β β β§ π¦ β (1...(π β 1))) β ((π¦β(π β 2)) mod π) β (1...(π β 1))) |
18 | 17 | ralrimiva 3146 |
. . . . 5
β’ (π β β β
βπ¦ β
(1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1))) |
19 | | ovex 7444 |
. . . . . . 7
β’
(1...(π β 1))
β V |
20 | 19 | pwid 4624 |
. . . . . 6
β’
(1...(π β 1))
β π« (1...(π
β 1)) |
21 | | eleq2 2822 |
. . . . . . . 8
β’ (π₯ = (1...(π β 1)) β ((π β 1) β π₯ β (π β 1) β (1...(π β 1)))) |
22 | | eleq2 2822 |
. . . . . . . . 9
β’ (π₯ = (1...(π β 1)) β (((π¦β(π β 2)) mod π) β π₯ β ((π¦β(π β 2)) mod π) β (1...(π β 1)))) |
23 | 22 | raleqbi1dv 3333 |
. . . . . . . 8
β’ (π₯ = (1...(π β 1)) β (βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯ β βπ¦ β (1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1)))) |
24 | 21, 23 | anbi12d 631 |
. . . . . . 7
β’ (π₯ = (1...(π β 1)) β (((π β 1) β π₯ β§ βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯) β ((π β 1) β (1...(π β 1)) β§ βπ¦ β (1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1))))) |
25 | | wilthlem.a |
. . . . . . 7
β’ π΄ = {π₯ β π« (1...(π β 1)) β£ ((π β 1) β π₯ β§ βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯)} |
26 | 24, 25 | elrab2 3686 |
. . . . . 6
β’
((1...(π β 1))
β π΄ β
((1...(π β 1)) β
π« (1...(π β
1)) β§ ((π β 1)
β (1...(π β 1))
β§ βπ¦ β
(1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1))))) |
27 | 20, 26 | mpbiran 707 |
. . . . 5
β’
((1...(π β 1))
β π΄ β ((π β 1) β (1...(π β 1)) β§ βπ¦ β (1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1)))) |
28 | 7, 18, 27 | sylanbrc 583 |
. . . 4
β’ (π β β β
(1...(π β 1)) β
π΄) |
29 | | fzfi 13939 |
. . . . 5
β’
(1...(π β 1))
β Fin |
30 | | eleq1 2821 |
. . . . . . . 8
β’ (π = π‘ β (π β π΄ β π‘ β π΄)) |
31 | | reseq2 5976 |
. . . . . . . . . . 11
β’ (π = π‘ β ( I βΎ π ) = ( I βΎ π‘)) |
32 | 31 | oveq2d 7427 |
. . . . . . . . . 10
β’ (π = π‘ β (π Ξ£g ( I βΎ
π )) = (π Ξ£g ( I βΎ
π‘))) |
33 | 32 | oveq1d 7426 |
. . . . . . . . 9
β’ (π = π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = ((π Ξ£g ( I βΎ
π‘)) mod π)) |
34 | 33 | eqeq1d 2734 |
. . . . . . . 8
β’ (π = π‘ β (((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π) β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π))) |
35 | 30, 34 | imbi12d 344 |
. . . . . . 7
β’ (π = π‘ β ((π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β (π‘ β π΄ β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π)))) |
36 | 35 | imbi2d 340 |
. . . . . 6
β’ (π = π‘ β ((π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))) β (π β β β (π‘ β π΄ β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π))))) |
37 | | eleq1 2821 |
. . . . . . . 8
β’ (π = (1...(π β 1)) β (π β π΄ β (1...(π β 1)) β π΄)) |
38 | | reseq2 5976 |
. . . . . . . . . . 11
β’ (π = (1...(π β 1)) β ( I βΎ π ) = ( I βΎ (1...(π β 1)))) |
39 | 38 | oveq2d 7427 |
. . . . . . . . . 10
β’ (π = (1...(π β 1)) β (π Ξ£g ( I βΎ
π )) = (π Ξ£g ( I βΎ
(1...(π β
1))))) |
40 | 39 | oveq1d 7426 |
. . . . . . . . 9
β’ (π = (1...(π β 1)) β ((π Ξ£g ( I βΎ
π )) mod π) = ((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π)) |
41 | 40 | eqeq1d 2734 |
. . . . . . . 8
β’ (π = (1...(π β 1)) β (((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π) β ((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π) = (-1 mod π))) |
42 | 37, 41 | imbi12d 344 |
. . . . . . 7
β’ (π = (1...(π β 1)) β ((π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β ((1...(π β 1)) β π΄ β ((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π) = (-1 mod π)))) |
43 | 42 | imbi2d 340 |
. . . . . 6
β’ (π = (1...(π β 1)) β ((π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))) β (π β β β ((1...(π β 1)) β π΄ β ((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π) = (-1 mod π))))) |
44 | | bi2.04 388 |
. . . . . . . . . . 11
β’ ((π β π‘ β (π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β (π β β β (π β π‘ β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))))) |
45 | | pm2.27 42 |
. . . . . . . . . . . 12
β’ (π β β β ((π β β β (π β π‘ β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β (π β π‘ β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))))) |
46 | 45 | com34 91 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β (π β π‘ β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β (π β π΄ β (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))))) |
47 | 44, 46 | biimtrid 241 |
. . . . . . . . . 10
β’ (π β β β ((π β π‘ β (π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β (π β π΄ β (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))))) |
48 | 47 | alimdv 1919 |
. . . . . . . . 9
β’ (π β β β
(βπ (π β π‘ β (π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β βπ (π β π΄ β (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))))) |
49 | | df-ral 3062 |
. . . . . . . . 9
β’
(βπ β
π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β βπ (π β π΄ β (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) |
50 | 48, 49 | imbitrrdi 251 |
. . . . . . . 8
β’ (π β β β
(βπ (π β π‘ β (π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) |
51 | | wilthlem.t |
. . . . . . . . . 10
β’ π =
(mulGrpββfld) |
52 | | simp1 1136 |
. . . . . . . . . 10
β’ ((π β β β§
βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β§ π‘ β π΄) β π β β) |
53 | | simp3 1138 |
. . . . . . . . . 10
β’ ((π β β β§
βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β§ π‘ β π΄) β π‘ β π΄) |
54 | | simp2 1137 |
. . . . . . . . . 10
β’ ((π β β β§
βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β§ π‘ β π΄) β βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))) |
55 | 51, 25, 52, 53, 54 | wilthlem2 26580 |
. . . . . . . . 9
β’ ((π β β β§
βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β§ π‘ β π΄) β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π)) |
56 | 55 | 3exp 1119 |
. . . . . . . 8
β’ (π β β β
(βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β (π‘ β π΄ β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π)))) |
57 | 50, 56 | syldc 48 |
. . . . . . 7
β’
(βπ (π β π‘ β (π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β (π β β β (π‘ β π΄ β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π)))) |
58 | 57 | a1i 11 |
. . . . . 6
β’ (π‘ β Fin β
(βπ (π β π‘ β (π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β (π β β β (π‘ β π΄ β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π))))) |
59 | 36, 43, 58 | findcard3 9287 |
. . . . 5
β’
((1...(π β 1))
β Fin β (π β
β β ((1...(π
β 1)) β π΄ β
((π
Ξ£g ( I βΎ (1...(π β 1)))) mod π) = (-1 mod π)))) |
60 | 29, 59 | ax-mp 5 |
. . . 4
β’ (π β β β
((1...(π β 1)) β
π΄ β ((π Ξ£g ( I
βΎ (1...(π β
1)))) mod π) = (-1 mod
π))) |
61 | 28, 60 | mpd 15 |
. . 3
β’ (π β β β ((π Ξ£g ( I
βΎ (1...(π β
1)))) mod π) = (-1 mod
π)) |
62 | | cnfld1 20976 |
. . . . . 6
β’ 1 =
(1rββfld) |
63 | 51, 62 | ringidval 20008 |
. . . . 5
β’ 1 =
(0gβπ) |
64 | | cncrng 20972 |
. . . . . 6
β’
βfld β CRing |
65 | 51 | crngmgp 20066 |
. . . . . 6
β’
(βfld β CRing β π β CMnd) |
66 | 64, 65 | mp1i 13 |
. . . . 5
β’ (π β β β π β CMnd) |
67 | 29 | a1i 11 |
. . . . 5
β’ (π β β β
(1...(π β 1)) β
Fin) |
68 | | zsubrg 21004 |
. . . . . 6
β’ β€
β (SubRingββfld) |
69 | 51 | subrgsubm 20336 |
. . . . . 6
β’ (β€
β (SubRingββfld) β β€ β
(SubMndβπ)) |
70 | 68, 69 | mp1i 13 |
. . . . 5
β’ (π β β β β€
β (SubMndβπ)) |
71 | | f1oi 6871 |
. . . . . . . 8
β’ ( I
βΎ (1...(π β
1))):(1...(π β
1))β1-1-ontoβ(1...(π β 1)) |
72 | | f1of 6833 |
. . . . . . . 8
β’ (( I
βΎ (1...(π β
1))):(1...(π β
1))β1-1-ontoβ(1...(π β 1)) β ( I βΎ (1...(π β 1))):(1...(π β 1))βΆ(1...(π β 1))) |
73 | 71, 72 | ax-mp 5 |
. . . . . . 7
β’ ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆ(1...(π β
1)) |
74 | | fzssz 13505 |
. . . . . . 7
β’
(1...(π β 1))
β β€ |
75 | | fss 6734 |
. . . . . . 7
β’ ((( I
βΎ (1...(π β
1))):(1...(π β
1))βΆ(1...(π β
1)) β§ (1...(π β
1)) β β€) β ( I βΎ (1...(π β 1))):(1...(π β
1))βΆβ€) |
76 | 73, 74, 75 | mp2an 690 |
. . . . . 6
β’ ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ€ |
77 | 76 | a1i 11 |
. . . . 5
β’ (π β β β ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ€) |
78 | | 1ex 11212 |
. . . . . . 7
β’ 1 β
V |
79 | 78 | a1i 11 |
. . . . . 6
β’ (π β β β 1 β
V) |
80 | 77, 67, 79 | fdmfifsupp 9375 |
. . . . 5
β’ (π β β β ( I
βΎ (1...(π β
1))) finSupp 1) |
81 | 63, 66, 67, 70, 77, 80 | gsumsubmcl 19789 |
. . . 4
β’ (π β β β (π Ξ£g ( I
βΎ (1...(π β
1)))) β β€) |
82 | | 1z 12594 |
. . . . 5
β’ 1 β
β€ |
83 | | znegcl 12599 |
. . . . 5
β’ (1 β
β€ β -1 β β€) |
84 | 82, 83 | mp1i 13 |
. . . 4
β’ (π β β β -1 β
β€) |
85 | | moddvds 16210 |
. . . 4
β’ ((π β β β§ (π Ξ£g ( I
βΎ (1...(π β
1)))) β β€ β§ -1 β β€) β (((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π) = (-1 mod π) β π β₯ ((π Ξ£g ( I βΎ
(1...(π β 1))))
β -1))) |
86 | 11, 81, 84, 85 | syl3anc 1371 |
. . 3
β’ (π β β β (((π Ξ£g ( I
βΎ (1...(π β
1)))) mod π) = (-1 mod
π) β π β₯ ((π Ξ£g ( I βΎ
(1...(π β 1))))
β -1))) |
87 | 61, 86 | mpbid 231 |
. 2
β’ (π β β β π β₯ ((π Ξ£g ( I βΎ
(1...(π β 1))))
β -1)) |
88 | | fcoi1 6765 |
. . . . . . . . . 10
β’ (( I
βΎ (1...(π β
1))):(1...(π β
1))βΆ(1...(π β
1)) β (( I βΎ (1...(π β 1))) β ( I βΎ
(1...(π β 1)))) = ( I
βΎ (1...(π β
1)))) |
89 | 73, 88 | ax-mp 5 |
. . . . . . . . 9
β’ (( I
βΎ (1...(π β
1))) β ( I βΎ (1...(π β 1)))) = ( I βΎ (1...(π β 1))) |
90 | 89 | fveq1i 6892 |
. . . . . . . 8
β’ ((( I
βΎ (1...(π β
1))) β ( I βΎ (1...(π β 1))))βπ) = (( I βΎ (1...(π β 1)))βπ) |
91 | | fvres 6910 |
. . . . . . . 8
β’ (π β (1...(π β 1)) β (( I βΎ (1...(π β 1)))βπ) = ( I βπ)) |
92 | 90, 91 | eqtrid 2784 |
. . . . . . 7
β’ (π β (1...(π β 1)) β ((( I βΎ
(1...(π β 1)))
β ( I βΎ (1...(π
β 1))))βπ) = (
I βπ)) |
93 | 92 | adantl 482 |
. . . . . 6
β’ ((π β β β§ π β (1...(π β 1))) β ((( I βΎ
(1...(π β 1)))
β ( I βΎ (1...(π
β 1))))βπ) = (
I βπ)) |
94 | 5, 93 | seqfveq 13994 |
. . . . 5
β’ (π β β β (seq1(
Β· , (( I βΎ (1...(π β 1))) β ( I βΎ
(1...(π β
1)))))β(π β 1))
= (seq1( Β· , I )β(π β 1))) |
95 | | cnfldbas 20954 |
. . . . . . 7
β’ β =
(Baseββfld) |
96 | 51, 95 | mgpbas 19995 |
. . . . . 6
β’ β =
(Baseβπ) |
97 | | cnfldmul 20956 |
. . . . . . 7
β’ Β·
= (.rββfld) |
98 | 51, 97 | mgpplusg 19993 |
. . . . . 6
β’ Β·
= (+gβπ) |
99 | | eqid 2732 |
. . . . . 6
β’
(Cntzβπ) =
(Cntzβπ) |
100 | | cnring 20973 |
. . . . . . 7
β’
βfld β Ring |
101 | 51 | ringmgp 20064 |
. . . . . . 7
β’
(βfld β Ring β π β Mnd) |
102 | 100, 101 | mp1i 13 |
. . . . . 6
β’ (π β β β π β Mnd) |
103 | | zsscn 12568 |
. . . . . . . 8
β’ β€
β β |
104 | | fss 6734 |
. . . . . . . 8
β’ ((( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ€ β§ β€ β β) β ( I βΎ
(1...(π β
1))):(1...(π β
1))βΆβ) |
105 | 76, 103, 104 | mp2an 690 |
. . . . . . 7
β’ ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ |
106 | 105 | a1i 11 |
. . . . . 6
β’ (π β β β ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ) |
107 | 96, 99, 66, 106 | cntzcmnf 19715 |
. . . . . 6
β’ (π β β β ran ( I
βΎ (1...(π β
1))) β ((Cntzβπ)βran ( I βΎ (1...(π β 1))))) |
108 | | f1of1 6832 |
. . . . . . 7
β’ (( I
βΎ (1...(π β
1))):(1...(π β
1))β1-1-ontoβ(1...(π β 1)) β ( I βΎ (1...(π β 1))):(1...(π β 1))β1-1β(1...(π β 1))) |
109 | 71, 108 | mp1i 13 |
. . . . . 6
β’ (π β β β ( I
βΎ (1...(π β
1))):(1...(π β
1))β1-1β(1...(π β 1))) |
110 | | suppssdm 8164 |
. . . . . . . . 9
β’ (( I
βΎ (1...(π β
1))) supp 1) β dom ( I βΎ (1...(π β 1))) |
111 | | dmresi 6051 |
. . . . . . . . 9
β’ dom ( I
βΎ (1...(π β
1))) = (1...(π β
1)) |
112 | 110, 111 | sseqtri 4018 |
. . . . . . . 8
β’ (( I
βΎ (1...(π β
1))) supp 1) β (1...(π β 1)) |
113 | | rnresi 6074 |
. . . . . . . 8
β’ ran ( I
βΎ (1...(π β
1))) = (1...(π β
1)) |
114 | 112, 113 | sseqtrri 4019 |
. . . . . . 7
β’ (( I
βΎ (1...(π β
1))) supp 1) β ran ( I βΎ (1...(π β 1))) |
115 | 114 | a1i 11 |
. . . . . 6
β’ (π β β β (( I
βΎ (1...(π β
1))) supp 1) β ran ( I βΎ (1...(π β 1)))) |
116 | | eqid 2732 |
. . . . . 6
β’ ((( I
βΎ (1...(π β
1))) β ( I βΎ (1...(π β 1)))) supp 1) = ((( I βΎ
(1...(π β 1)))
β ( I βΎ (1...(π
β 1)))) supp 1) |
117 | 96, 63, 98, 99, 102, 67, 106, 107, 3, 109, 115, 116 | gsumval3 19777 |
. . . . 5
β’ (π β β β (π Ξ£g ( I
βΎ (1...(π β
1)))) = (seq1( Β· , (( I βΎ (1...(π β 1))) β ( I βΎ
(1...(π β
1)))))β(π β
1))) |
118 | | facnn 14237 |
. . . . . 6
β’ ((π β 1) β β
β (!β(π β
1)) = (seq1( Β· , I )β(π β 1))) |
119 | 3, 118 | syl 17 |
. . . . 5
β’ (π β β β
(!β(π β 1)) =
(seq1( Β· , I )β(π β 1))) |
120 | 94, 117, 119 | 3eqtr4d 2782 |
. . . 4
β’ (π β β β (π Ξ£g ( I
βΎ (1...(π β
1)))) = (!β(π β
1))) |
121 | 120 | oveq1d 7426 |
. . 3
β’ (π β β β ((π Ξ£g ( I
βΎ (1...(π β
1)))) β -1) = ((!β(π β 1)) β -1)) |
122 | | nnm1nn0 12515 |
. . . . . . 7
β’ (π β β β (π β 1) β
β0) |
123 | 11, 122 | syl 17 |
. . . . . 6
β’ (π β β β (π β 1) β
β0) |
124 | 123 | faccld 14246 |
. . . . 5
β’ (π β β β
(!β(π β 1))
β β) |
125 | 124 | nncnd 12230 |
. . . 4
β’ (π β β β
(!β(π β 1))
β β) |
126 | | ax-1cn 11170 |
. . . 4
β’ 1 β
β |
127 | | subneg 11511 |
. . . 4
β’
(((!β(π
β 1)) β β β§ 1 β β) β ((!β(π β 1)) β -1) =
((!β(π β 1)) +
1)) |
128 | 125, 126,
127 | sylancl 586 |
. . 3
β’ (π β β β
((!β(π β 1))
β -1) = ((!β(π
β 1)) + 1)) |
129 | 121, 128 | eqtrd 2772 |
. 2
β’ (π β β β ((π Ξ£g ( I
βΎ (1...(π β
1)))) β -1) = ((!β(π β 1)) + 1)) |
130 | 87, 129 | breqtrd 5174 |
1
β’ (π β β β π β₯ ((!β(π β 1)) +
1)) |