Step | Hyp | Ref
| Expression |
1 | | prmuz2 16633 |
. . . . . . . 8
β’ (π β β β π β
(β€β₯β2)) |
2 | | uz2m1nn 12907 |
. . . . . . . 8
β’ (π β
(β€β₯β2) β (π β 1) β β) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (π β β β (π β 1) β
β) |
4 | | nnuz 12865 |
. . . . . . 7
β’ β =
(β€β₯β1) |
5 | 3, 4 | eleqtrdi 2844 |
. . . . . 6
β’ (π β β β (π β 1) β
(β€β₯β1)) |
6 | | eluzfz2 13509 |
. . . . . 6
β’ ((π β 1) β
(β€β₯β1) β (π β 1) β (1...(π β 1))) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π β β β (π β 1) β (1...(π β 1))) |
8 | | simpl 484 |
. . . . . . . 8
β’ ((π β β β§ π¦ β (1...(π β 1))) β π β β) |
9 | | elfzelz 13501 |
. . . . . . . . 9
β’ (π¦ β (1...(π β 1)) β π¦ β β€) |
10 | 9 | adantl 483 |
. . . . . . . 8
β’ ((π β β β§ π¦ β (1...(π β 1))) β π¦ β β€) |
11 | | prmnn 16611 |
. . . . . . . . 9
β’ (π β β β π β
β) |
12 | | fzm1ndvds 16265 |
. . . . . . . . 9
β’ ((π β β β§ π¦ β (1...(π β 1))) β Β¬ π β₯ π¦) |
13 | 11, 12 | sylan 581 |
. . . . . . . 8
β’ ((π β β β§ π¦ β (1...(π β 1))) β Β¬ π β₯ π¦) |
14 | | eqid 2733 |
. . . . . . . . 9
β’ ((π¦β(π β 2)) mod π) = ((π¦β(π β 2)) mod π) |
15 | 14 | prmdiv 16718 |
. . . . . . . 8
β’ ((π β β β§ π¦ β β€ β§ Β¬
π β₯ π¦) β (((π¦β(π β 2)) mod π) β (1...(π β 1)) β§ π β₯ ((π¦ Β· ((π¦β(π β 2)) mod π)) β 1))) |
16 | 8, 10, 13, 15 | syl3anc 1372 |
. . . . . . 7
β’ ((π β β β§ π¦ β (1...(π β 1))) β (((π¦β(π β 2)) mod π) β (1...(π β 1)) β§ π β₯ ((π¦ Β· ((π¦β(π β 2)) mod π)) β 1))) |
17 | 16 | simpld 496 |
. . . . . 6
β’ ((π β β β§ π¦ β (1...(π β 1))) β ((π¦β(π β 2)) mod π) β (1...(π β 1))) |
18 | 17 | ralrimiva 3147 |
. . . . 5
β’ (π β β β
βπ¦ β
(1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1))) |
19 | | ovex 7442 |
. . . . . . 7
β’
(1...(π β 1))
β V |
20 | 19 | pwid 4625 |
. . . . . 6
β’
(1...(π β 1))
β π« (1...(π
β 1)) |
21 | | eleq2 2823 |
. . . . . . . 8
β’ (π₯ = (1...(π β 1)) β ((π β 1) β π₯ β (π β 1) β (1...(π β 1)))) |
22 | | eleq2 2823 |
. . . . . . . . 9
β’ (π₯ = (1...(π β 1)) β (((π¦β(π β 2)) mod π) β π₯ β ((π¦β(π β 2)) mod π) β (1...(π β 1)))) |
23 | 22 | raleqbi1dv 3334 |
. . . . . . . 8
β’ (π₯ = (1...(π β 1)) β (βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯ β βπ¦ β (1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1)))) |
24 | 21, 23 | anbi12d 632 |
. . . . . . 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 3687 |
. . . . . 6
β’
((1...(π β 1))
β π΄ β
((1...(π β 1)) β
π« (1...(π β
1)) β§ ((π β 1)
β (1...(π β 1))
β§ βπ¦ β
(1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1))))) |
27 | 20, 26 | mpbiran 708 |
. . . . 5
β’
((1...(π β 1))
β π΄ β ((π β 1) β (1...(π β 1)) β§ βπ¦ β (1...(π β 1))((π¦β(π β 2)) mod π) β (1...(π β 1)))) |
28 | 7, 18, 27 | sylanbrc 584 |
. . . 4
β’ (π β β β
(1...(π β 1)) β
π΄) |
29 | | fzfi 13937 |
. . . . 5
β’
(1...(π β 1))
β Fin |
30 | | eleq1 2822 |
. . . . . . . 8
β’ (π = π‘ β (π β π΄ β π‘ β π΄)) |
31 | | reseq2 5977 |
. . . . . . . . . . 11
β’ (π = π‘ β ( I βΎ π ) = ( I βΎ π‘)) |
32 | 31 | oveq2d 7425 |
. . . . . . . . . 10
β’ (π = π‘ β (π Ξ£g ( I βΎ
π )) = (π Ξ£g ( I βΎ
π‘))) |
33 | 32 | oveq1d 7424 |
. . . . . . . . 9
β’ (π = π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = ((π Ξ£g ( I βΎ
π‘)) mod π)) |
34 | 33 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = π‘ β (((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π) β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π))) |
35 | 30, 34 | imbi12d 345 |
. . . . . . 7
β’ (π = π‘ β ((π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β (π‘ β π΄ β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π)))) |
36 | 35 | imbi2d 341 |
. . . . . 6
β’ (π = π‘ β ((π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))) β (π β β β (π‘ β π΄ β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π))))) |
37 | | eleq1 2822 |
. . . . . . . 8
β’ (π = (1...(π β 1)) β (π β π΄ β (1...(π β 1)) β π΄)) |
38 | | reseq2 5977 |
. . . . . . . . . . 11
β’ (π = (1...(π β 1)) β ( I βΎ π ) = ( I βΎ (1...(π β 1)))) |
39 | 38 | oveq2d 7425 |
. . . . . . . . . 10
β’ (π = (1...(π β 1)) β (π Ξ£g ( I βΎ
π )) = (π Ξ£g ( I βΎ
(1...(π β
1))))) |
40 | 39 | oveq1d 7424 |
. . . . . . . . 9
β’ (π = (1...(π β 1)) β ((π Ξ£g ( I βΎ
π )) mod π) = ((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π)) |
41 | 40 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = (1...(π β 1)) β (((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π) β ((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π) = (-1 mod π))) |
42 | 37, 41 | imbi12d 345 |
. . . . . . 7
β’ (π = (1...(π β 1)) β ((π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β ((1...(π β 1)) β π΄ β ((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π) = (-1 mod π)))) |
43 | 42 | imbi2d 341 |
. . . . . 6
β’ (π = (1...(π β 1)) β ((π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))) β (π β β β ((1...(π β 1)) β π΄ β ((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π) = (-1 mod π))))) |
44 | | bi2.04 389 |
. . . . . . . . . . 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 1920 |
. . . . . . . . 9
β’ (π β β β
(βπ (π β π‘ β (π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β βπ (π β π΄ β (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))))) |
49 | | df-ral 3063 |
. . . . . . . . 9
β’
(βπ β
π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β βπ (π β π΄ β (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) |
50 | 48, 49 | syl6ibr 252 |
. . . . . . . 8
β’ (π β β β
(βπ (π β π‘ β (π β β β (π β π΄ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) β βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)))) |
51 | | wilthlem.t |
. . . . . . . . . 10
β’ π =
(mulGrpββfld) |
52 | | simp1 1137 |
. . . . . . . . . 10
β’ ((π β β β§
βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β§ π‘ β π΄) β π β β) |
53 | | simp3 1139 |
. . . . . . . . . 10
β’ ((π β β β§
βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β§ π‘ β π΄) β π‘ β π΄) |
54 | | simp2 1138 |
. . . . . . . . . 10
β’ ((π β β β§
βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β§ π‘ β π΄) β βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))) |
55 | 51, 25, 52, 53, 54 | wilthlem2 26573 |
. . . . . . . . 9
β’ ((π β β β§
βπ β π΄ (π β π‘ β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β§ π‘ β π΄) β ((π Ξ£g ( I βΎ
π‘)) mod π) = (-1 mod π)) |
56 | 55 | 3exp 1120 |
. . . . . . . 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 9285 |
. . . . 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 20970 |
. . . . . 6
β’ 1 =
(1rββfld) |
63 | 51, 62 | ringidval 20006 |
. . . . 5
β’ 1 =
(0gβπ) |
64 | | cncrng 20966 |
. . . . . 6
β’
βfld β CRing |
65 | 51 | crngmgp 20064 |
. . . . . 6
β’
(βfld β CRing β π β CMnd) |
66 | 64, 65 | mp1i 13 |
. . . . 5
β’ (π β β β π β CMnd) |
67 | 29 | a1i 11 |
. . . . 5
β’ (π β β β
(1...(π β 1)) β
Fin) |
68 | | zsubrg 20998 |
. . . . . 6
β’ β€
β (SubRingββfld) |
69 | 51 | subrgsubm 20332 |
. . . . . 6
β’ (β€
β (SubRingββfld) β β€ β
(SubMndβπ)) |
70 | 68, 69 | mp1i 13 |
. . . . 5
β’ (π β β β β€
β (SubMndβπ)) |
71 | | f1oi 6872 |
. . . . . . . 8
β’ ( I
βΎ (1...(π β
1))):(1...(π β
1))β1-1-ontoβ(1...(π β 1)) |
72 | | f1of 6834 |
. . . . . . . 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 13503 |
. . . . . . 7
β’
(1...(π β 1))
β β€ |
75 | | fss 6735 |
. . . . . . 7
β’ ((( I
βΎ (1...(π β
1))):(1...(π β
1))βΆ(1...(π β
1)) β§ (1...(π β
1)) β β€) β ( I βΎ (1...(π β 1))):(1...(π β
1))βΆβ€) |
76 | 73, 74, 75 | mp2an 691 |
. . . . . 6
β’ ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ€ |
77 | 76 | a1i 11 |
. . . . 5
β’ (π β β β ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ€) |
78 | | 1ex 11210 |
. . . . . . 7
β’ 1 β
V |
79 | 78 | a1i 11 |
. . . . . 6
β’ (π β β β 1 β
V) |
80 | 77, 67, 79 | fdmfifsupp 9373 |
. . . . 5
β’ (π β β β ( I
βΎ (1...(π β
1))) finSupp 1) |
81 | 63, 66, 67, 70, 77, 80 | gsumsubmcl 19787 |
. . . 4
β’ (π β β β (π Ξ£g ( I
βΎ (1...(π β
1)))) β β€) |
82 | | 1z 12592 |
. . . . 5
β’ 1 β
β€ |
83 | | znegcl 12597 |
. . . . 5
β’ (1 β
β€ β -1 β β€) |
84 | 82, 83 | mp1i 13 |
. . . 4
β’ (π β β β -1 β
β€) |
85 | | moddvds 16208 |
. . . 4
β’ ((π β β β§ (π Ξ£g ( I
βΎ (1...(π β
1)))) β β€ β§ -1 β β€) β (((π Ξ£g ( I βΎ
(1...(π β 1)))) mod
π) = (-1 mod π) β π β₯ ((π Ξ£g ( I βΎ
(1...(π β 1))))
β -1))) |
86 | 11, 81, 84, 85 | syl3anc 1372 |
. . 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 6766 |
. . . . . . . . . 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 6893 |
. . . . . . . 8
β’ ((( I
βΎ (1...(π β
1))) β ( I βΎ (1...(π β 1))))βπ) = (( I βΎ (1...(π β 1)))βπ) |
91 | | fvres 6911 |
. . . . . . . 8
β’ (π β (1...(π β 1)) β (( I βΎ (1...(π β 1)))βπ) = ( I βπ)) |
92 | 90, 91 | eqtrid 2785 |
. . . . . . 7
β’ (π β (1...(π β 1)) β ((( I βΎ
(1...(π β 1)))
β ( I βΎ (1...(π
β 1))))βπ) = (
I βπ)) |
93 | 92 | adantl 483 |
. . . . . 6
β’ ((π β β β§ π β (1...(π β 1))) β ((( I βΎ
(1...(π β 1)))
β ( I βΎ (1...(π
β 1))))βπ) = (
I βπ)) |
94 | 5, 93 | seqfveq 13992 |
. . . . 5
β’ (π β β β (seq1(
Β· , (( I βΎ (1...(π β 1))) β ( I βΎ
(1...(π β
1)))))β(π β 1))
= (seq1( Β· , I )β(π β 1))) |
95 | | cnfldbas 20948 |
. . . . . . 7
β’ β =
(Baseββfld) |
96 | 51, 95 | mgpbas 19993 |
. . . . . 6
β’ β =
(Baseβπ) |
97 | | cnfldmul 20950 |
. . . . . . 7
β’ Β·
= (.rββfld) |
98 | 51, 97 | mgpplusg 19991 |
. . . . . 6
β’ Β·
= (+gβπ) |
99 | | eqid 2733 |
. . . . . 6
β’
(Cntzβπ) =
(Cntzβπ) |
100 | | cnring 20967 |
. . . . . . 7
β’
βfld β Ring |
101 | 51 | ringmgp 20062 |
. . . . . . 7
β’
(βfld β Ring β π β Mnd) |
102 | 100, 101 | mp1i 13 |
. . . . . 6
β’ (π β β β π β Mnd) |
103 | | zsscn 12566 |
. . . . . . . 8
β’ β€
β β |
104 | | fss 6735 |
. . . . . . . 8
β’ ((( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ€ β§ β€ β β) β ( I βΎ
(1...(π β
1))):(1...(π β
1))βΆβ) |
105 | 76, 103, 104 | mp2an 691 |
. . . . . . 7
β’ ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ |
106 | 105 | a1i 11 |
. . . . . 6
β’ (π β β β ( I
βΎ (1...(π β
1))):(1...(π β
1))βΆβ) |
107 | 96, 99, 66, 106 | cntzcmnf 19713 |
. . . . . 6
β’ (π β β β ran ( I
βΎ (1...(π β
1))) β ((Cntzβπ)βran ( I βΎ (1...(π β 1))))) |
108 | | f1of1 6833 |
. . . . . . 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 8162 |
. . . . . . . . 9
β’ (( I
βΎ (1...(π β
1))) supp 1) β dom ( I βΎ (1...(π β 1))) |
111 | | dmresi 6052 |
. . . . . . . . 9
β’ dom ( I
βΎ (1...(π β
1))) = (1...(π β
1)) |
112 | 110, 111 | sseqtri 4019 |
. . . . . . . 8
β’ (( I
βΎ (1...(π β
1))) supp 1) β (1...(π β 1)) |
113 | | rnresi 6075 |
. . . . . . . 8
β’ ran ( I
βΎ (1...(π β
1))) = (1...(π β
1)) |
114 | 112, 113 | sseqtrri 4020 |
. . . . . . 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 2733 |
. . . . . 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 19775 |
. . . . 5
β’ (π β β β (π Ξ£g ( I
βΎ (1...(π β
1)))) = (seq1( Β· , (( I βΎ (1...(π β 1))) β ( I βΎ
(1...(π β
1)))))β(π β
1))) |
118 | | facnn 14235 |
. . . . . 6
β’ ((π β 1) β β
β (!β(π β
1)) = (seq1( Β· , I )β(π β 1))) |
119 | 3, 118 | syl 17 |
. . . . 5
β’ (π β β β
(!β(π β 1)) =
(seq1( Β· , I )β(π β 1))) |
120 | 94, 117, 119 | 3eqtr4d 2783 |
. . . 4
β’ (π β β β (π Ξ£g ( I
βΎ (1...(π β
1)))) = (!β(π β
1))) |
121 | 120 | oveq1d 7424 |
. . 3
β’ (π β β β ((π Ξ£g ( I
βΎ (1...(π β
1)))) β -1) = ((!β(π β 1)) β -1)) |
122 | | nnm1nn0 12513 |
. . . . . . 7
β’ (π β β β (π β 1) β
β0) |
123 | 11, 122 | syl 17 |
. . . . . 6
β’ (π β β β (π β 1) β
β0) |
124 | 123 | faccld 14244 |
. . . . 5
β’ (π β β β
(!β(π β 1))
β β) |
125 | 124 | nncnd 12228 |
. . . 4
β’ (π β β β
(!β(π β 1))
β β) |
126 | | ax-1cn 11168 |
. . . 4
β’ 1 β
β |
127 | | subneg 11509 |
. . . 4
β’
(((!β(π
β 1)) β β β§ 1 β β) β ((!β(π β 1)) β -1) =
((!β(π β 1)) +
1)) |
128 | 125, 126,
127 | sylancl 587 |
. . 3
β’ (π β β β
((!β(π β 1))
β -1) = ((!β(π
β 1)) + 1)) |
129 | 121, 128 | eqtrd 2773 |
. 2
β’ (π β β β ((π Ξ£g ( I
βΎ (1...(π β
1)))) β -1) = ((!β(π β 1)) + 1)) |
130 | 87, 129 | breqtrd 5175 |
1
β’ (π β β β π β₯ ((!β(π β 1)) +
1)) |