Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . . . 6
β’ (π β (0...(π β 1)) β Fin) |
2 | | 4sqlem11.5 |
. . . . . . . 8
β’ π΄ = {π’ β£ βπ β (0...π)π’ = ((πβ2) mod π)} |
3 | | elfzelz 13448 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β β€) |
4 | | zsqcl 14041 |
. . . . . . . . . . . . 13
β’ (π β β€ β (πβ2) β
β€) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (0...π) β (πβ2) β β€) |
6 | | 4sq.4 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
7 | | prmnn 16557 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β β) |
9 | | zmodfz 13805 |
. . . . . . . . . . . 12
β’ (((πβ2) β β€ β§
π β β) β
((πβ2) mod π) β (0...(π β 1))) |
10 | 5, 8, 9 | syl2anr 598 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β ((πβ2) mod π) β (0...(π β 1))) |
11 | | eleq1a 2833 |
. . . . . . . . . . 11
β’ (((πβ2) mod π) β (0...(π β 1)) β (π’ = ((πβ2) mod π) β π’ β (0...(π β 1)))) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (π’ = ((πβ2) mod π) β π’ β (0...(π β 1)))) |
13 | 12 | rexlimdva 3153 |
. . . . . . . . 9
β’ (π β (βπ β (0...π)π’ = ((πβ2) mod π) β π’ β (0...(π β 1)))) |
14 | 13 | abssdv 4030 |
. . . . . . . 8
β’ (π β {π’ β£ βπ β (0...π)π’ = ((πβ2) mod π)} β (0...(π β 1))) |
15 | 2, 14 | eqsstrid 3997 |
. . . . . . 7
β’ (π β π΄ β (0...(π β 1))) |
16 | | prmz 16558 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β€) |
17 | 6, 16 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β β€) |
18 | | peano2zm 12553 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β (π β 1) β
β€) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π β 1) β β€) |
20 | 19 | zcnd 12615 |
. . . . . . . . . . . . 13
β’ (π β (π β 1) β β) |
21 | 20 | addid2d 11363 |
. . . . . . . . . . . 12
β’ (π β (0 + (π β 1)) = (π β 1)) |
22 | 21 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π β ((0 + (π β 1)) β π£) = ((π β 1) β π£)) |
23 | 22 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π£ β π΄) β ((0 + (π β 1)) β π£) = ((π β 1) β π£)) |
24 | 15 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β§ π£ β π΄) β π£ β (0...(π β 1))) |
25 | | fzrev3i 13515 |
. . . . . . . . . . 11
β’ (π£ β (0...(π β 1)) β ((0 + (π β 1)) β π£) β (0...(π β 1))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π£ β π΄) β ((0 + (π β 1)) β π£) β (0...(π β 1))) |
27 | 23, 26 | eqeltrrd 2839 |
. . . . . . . . 9
β’ ((π β§ π£ β π΄) β ((π β 1) β π£) β (0...(π β 1))) |
28 | | 4sqlem11.6 |
. . . . . . . . 9
β’ πΉ = (π£ β π΄ β¦ ((π β 1) β π£)) |
29 | 27, 28 | fmptd 7067 |
. . . . . . . 8
β’ (π β πΉ:π΄βΆ(0...(π β 1))) |
30 | 29 | frnd 6681 |
. . . . . . 7
β’ (π β ran πΉ β (0...(π β 1))) |
31 | 15, 30 | unssd 4151 |
. . . . . 6
β’ (π β (π΄ βͺ ran πΉ) β (0...(π β 1))) |
32 | 1, 31 | ssfid 9218 |
. . . . 5
β’ (π β (π΄ βͺ ran πΉ) β Fin) |
33 | | hashcl 14263 |
. . . . 5
β’ ((π΄ βͺ ran πΉ) β Fin β (β―β(π΄ βͺ ran πΉ)) β
β0) |
34 | 32, 33 | syl 17 |
. . . 4
β’ (π β (β―β(π΄ βͺ ran πΉ)) β
β0) |
35 | 34 | nn0red 12481 |
. . 3
β’ (π β (β―β(π΄ βͺ ran πΉ)) β β) |
36 | 17 | zred 12614 |
. . 3
β’ (π β π β β) |
37 | | ssdomg 8947 |
. . . . . 6
β’
((0...(π β 1))
β Fin β ((π΄ βͺ
ran πΉ) β (0...(π β 1)) β (π΄ βͺ ran πΉ) βΌ (0...(π β 1)))) |
38 | 1, 31, 37 | sylc 65 |
. . . . 5
β’ (π β (π΄ βͺ ran πΉ) βΌ (0...(π β 1))) |
39 | | hashdom 14286 |
. . . . . 6
β’ (((π΄ βͺ ran πΉ) β Fin β§ (0...(π β 1)) β Fin) β
((β―β(π΄ βͺ
ran πΉ)) β€
(β―β(0...(π
β 1))) β (π΄
βͺ ran πΉ) βΌ
(0...(π β
1)))) |
40 | 32, 1, 39 | syl2anc 585 |
. . . . 5
β’ (π β ((β―β(π΄ βͺ ran πΉ)) β€ (β―β(0...(π β 1))) β (π΄ βͺ ran πΉ) βΌ (0...(π β 1)))) |
41 | 38, 40 | mpbird 257 |
. . . 4
β’ (π β (β―β(π΄ βͺ ran πΉ)) β€ (β―β(0...(π β 1)))) |
42 | | fz01en 13476 |
. . . . . . 7
β’ (π β β€ β
(0...(π β 1)) β
(1...π)) |
43 | 17, 42 | syl 17 |
. . . . . 6
β’ (π β (0...(π β 1)) β (1...π)) |
44 | | fzfid 13885 |
. . . . . . 7
β’ (π β (1...π) β Fin) |
45 | | hashen 14254 |
. . . . . . 7
β’
(((0...(π β
1)) β Fin β§ (1...π) β Fin) β
((β―β(0...(π
β 1))) = (β―β(1...π)) β (0...(π β 1)) β (1...π))) |
46 | 1, 44, 45 | syl2anc 585 |
. . . . . 6
β’ (π β
((β―β(0...(π
β 1))) = (β―β(1...π)) β (0...(π β 1)) β (1...π))) |
47 | 43, 46 | mpbird 257 |
. . . . 5
β’ (π β (β―β(0...(π β 1))) =
(β―β(1...π))) |
48 | 8 | nnnn0d 12480 |
. . . . . 6
β’ (π β π β
β0) |
49 | | hashfz1 14253 |
. . . . . 6
β’ (π β β0
β (β―β(1...π)) = π) |
50 | 48, 49 | syl 17 |
. . . . 5
β’ (π β (β―β(1...π)) = π) |
51 | 47, 50 | eqtrd 2777 |
. . . 4
β’ (π β (β―β(0...(π β 1))) = π) |
52 | 41, 51 | breqtrd 5136 |
. . 3
β’ (π β (β―β(π΄ βͺ ran πΉ)) β€ π) |
53 | 35, 36, 52 | lensymd 11313 |
. 2
β’ (π β Β¬ π < (β―β(π΄ βͺ ran πΉ))) |
54 | 36 | adantr 482 |
. . . . . 6
β’ ((π β§ (π΄ β© ran πΉ) = β
) β π β β) |
55 | 54 | ltp1d 12092 |
. . . . 5
β’ ((π β§ (π΄ β© ran πΉ) = β
) β π < (π + 1)) |
56 | | 4sq.2 |
. . . . . . . . . 10
β’ (π β π β β) |
57 | 56 | nncnd 12176 |
. . . . . . . . 9
β’ (π β π β β) |
58 | | 1cnd 11157 |
. . . . . . . . 9
β’ (π β 1 β
β) |
59 | 57, 57, 58, 58 | add4d 11390 |
. . . . . . . 8
β’ (π β ((π + π) + (1 + 1)) = ((π + 1) + (π + 1))) |
60 | | 4sq.3 |
. . . . . . . . . 10
β’ (π β π = ((2 Β· π) + 1)) |
61 | 60 | oveq1d 7377 |
. . . . . . . . 9
β’ (π β (π + 1) = (((2 Β· π) + 1) + 1)) |
62 | | 2cn 12235 |
. . . . . . . . . . 11
β’ 2 β
β |
63 | | mulcl 11142 |
. . . . . . . . . . 11
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
64 | 62, 57, 63 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (2 Β· π) β
β) |
65 | 64, 58, 58 | addassd 11184 |
. . . . . . . . 9
β’ (π β (((2 Β· π) + 1) + 1) = ((2 Β· π) + (1 + 1))) |
66 | 57 | 2timesd 12403 |
. . . . . . . . . 10
β’ (π β (2 Β· π) = (π + π)) |
67 | 66 | oveq1d 7377 |
. . . . . . . . 9
β’ (π β ((2 Β· π) + (1 + 1)) = ((π + π) + (1 + 1))) |
68 | 61, 65, 67 | 3eqtrd 2781 |
. . . . . . . 8
β’ (π β (π + 1) = ((π + π) + (1 + 1))) |
69 | 10 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (0...π) β ((πβ2) mod π) β (0...(π β 1)))) |
70 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β) |
71 | 3 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β€) |
72 | 71, 4 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (πβ2) β β€) |
73 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π’ β (0...π) β π’ β β€) |
74 | 73 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π’ β β€) |
75 | | zsqcl 14041 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ β β€ β (π’β2) β
β€) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π’β2) β β€) |
77 | | moddvds 16154 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ (πβ2) β β€ β§
(π’β2) β β€)
β (((πβ2) mod
π) = ((π’β2) mod π) β π β₯ ((πβ2) β (π’β2)))) |
78 | 70, 72, 76, 77 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (((πβ2) mod π) = ((π’β2) mod π) β π β₯ ((πβ2) β (π’β2)))) |
79 | 71 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β) |
80 | 74 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π’ β β) |
81 | | subsq 14121 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ π’ β β) β ((πβ2) β (π’β2)) = ((π + π’) Β· (π β π’))) |
82 | 79, 80, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β ((πβ2) β (π’β2)) = ((π + π’) Β· (π β π’))) |
83 | 82 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β₯ ((πβ2) β (π’β2)) β π β₯ ((π + π’) Β· (π β π’)))) |
84 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β) |
85 | 71, 74 | zaddcld 12618 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π + π’) β β€) |
86 | 71, 74 | zsubcld 12619 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β π’) β β€) |
87 | | euclemma 16596 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ (π + π’) β β€ β§ (π β π’) β β€) β (π β₯ ((π + π’) Β· (π β π’)) β (π β₯ (π + π’) β¨ π β₯ (π β π’)))) |
88 | 84, 85, 86, 87 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β₯ ((π + π’) Β· (π β π’)) β (π β₯ (π + π’) β¨ π β₯ (π β π’)))) |
89 | 78, 83, 88 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (((πβ2) mod π) = ((π’β2) mod π) β (π β₯ (π + π’) β¨ π β₯ (π β π’)))) |
90 | 85 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π + π’) β β) |
91 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 2 β
β |
92 | 56 | nnred 12175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β β) |
93 | | remulcl 11143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
94 | 91, 92, 93 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (2 Β· π) β
β) |
95 | 94 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (2 Β· π) β β) |
96 | 84, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β€) |
97 | 96 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β) |
98 | 71 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β) |
99 | 74 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π’ β β) |
100 | 92 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β) |
101 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (0...π) β π β€ π) |
102 | 101 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β€ π) |
103 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π’ β (0...π) β π’ β€ π) |
104 | 103 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π’ β€ π) |
105 | 98, 99, 100, 100, 102, 104 | le2addd 11781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π + π’) β€ (π + π)) |
106 | 57 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β π β β) |
107 | 106 | 2timesd 12403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (2 Β· π) = (π + π)) |
108 | 105, 107 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π + π’) β€ (2 Β· π)) |
109 | 94 | ltp1d 12092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (2 Β· π) < ((2 Β· π) + 1)) |
110 | 109, 60 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (2 Β· π) < π) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (2 Β· π) < π) |
112 | 90, 95, 97, 108, 111 | lelttrd 11320 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π + π’) < π) |
113 | 90, 97 | ltnled 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β ((π + π’) < π β Β¬ π β€ (π + π’))) |
114 | 112, 113 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β Β¬ π β€ (π + π’)) |
115 | 114 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β Β¬ π β€ (π + π’)) |
116 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β π β β€) |
117 | 85 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (π + π’) β β€) |
118 | | 1red 11163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β 1 β β) |
119 | | nn0abscl 15204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β π’) β β€ β (absβ(π β π’)) β
β0) |
120 | 86, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(π β π’)) β
β0) |
121 | 120 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(π β π’)) β β) |
122 | 121 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (absβ(π β π’)) β β) |
123 | 117 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (π + π’) β β) |
124 | 120 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (absβ(π β π’)) β
β0) |
125 | 124 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (absβ(π β π’)) β β€) |
126 | 86 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β π’) β β) |
127 | 126 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (π β π’) β β) |
128 | 79, 80 | subeq0ad 11529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β ((π β π’) = 0 β π = π’)) |
129 | 128 | necon3bid 2989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β ((π β π’) β 0 β π β π’)) |
130 | 129 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (π β π’) β 0) |
131 | 127, 130 | absrpcld 15340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (absβ(π β π’)) β
β+) |
132 | 131 | rpgt0d 12967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β 0 < (absβ(π β π’))) |
133 | | elnnz 12516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((absβ(π
β π’)) β β
β ((absβ(π
β π’)) β β€
β§ 0 < (absβ(π
β π’)))) |
134 | 125, 132,
133 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (absβ(π β π’)) β β) |
135 | 134 | nnge1d 12208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β 1 β€ (absβ(π β π’))) |
136 | | 0cnd 11155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β 0 β
β) |
137 | 79, 80, 136 | abs3difd 15352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(π β π’)) β€ ((absβ(π β 0)) + (absβ(0 β π’)))) |
138 | 79 | subid1d 11508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β 0) = π) |
139 | 138 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(π β 0)) = (absβπ)) |
140 | | elfzle1 13451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β (0...π) β 0 β€ π) |
141 | 140 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β 0 β€ π) |
142 | 98, 141 | absidd 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβπ) = π) |
143 | 139, 142 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(π β 0)) = π) |
144 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 0 β
β |
145 | | abssub 15218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((0
β β β§ π’
β β) β (absβ(0 β π’)) = (absβ(π’ β 0))) |
146 | 144, 80, 145 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(0 β π’)) = (absβ(π’ β 0))) |
147 | 80 | subid1d 11508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π’ β 0) = π’) |
148 | 147 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(π’ β 0)) = (absβπ’)) |
149 | | elfzle1 13451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π’ β (0...π) β 0 β€ π’) |
150 | 149 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β 0 β€ π’) |
151 | 99, 150 | absidd 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβπ’) = π’) |
152 | 146, 148,
151 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(0 β π’)) = π’) |
153 | 143, 152 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β ((absβ(π β 0)) + (absβ(0 β π’))) = (π + π’)) |
154 | 137, 153 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (absβ(π β π’)) β€ (π + π’)) |
155 | 154 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (absβ(π β π’)) β€ (π + π’)) |
156 | 118, 122,
123, 135, 155 | letrd 11319 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β 1 β€ (π + π’)) |
157 | | elnnz1 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π + π’) β β β ((π + π’) β β€ β§ 1 β€ (π + π’))) |
158 | 117, 156,
157 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (π + π’) β β) |
159 | | dvdsle 16199 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β€ β§ (π + π’) β β) β (π β₯ (π + π’) β π β€ (π + π’))) |
160 | 116, 158,
159 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (π β₯ (π + π’) β π β€ (π + π’))) |
161 | 115, 160 | mtod 197 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β Β¬ π β₯ (π + π’)) |
162 | 161 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β π’ β Β¬ π β₯ (π + π’))) |
163 | 162 | necon4ad 2963 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β₯ (π + π’) β π = π’)) |
164 | | dvdsabsb 16165 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β€ β§ (π β π’) β β€) β (π β₯ (π β π’) β π β₯ (absβ(π β π’)))) |
165 | 96, 86, 164 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β₯ (π β π’) β π β₯ (absβ(π β π’)))) |
166 | | letr 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β β§
(absβ(π β π’)) β β β§ (π + π’) β β) β ((π β€ (absβ(π β π’)) β§ (absβ(π β π’)) β€ (π + π’)) β π β€ (π + π’))) |
167 | 97, 121, 90, 166 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β ((π β€ (absβ(π β π’)) β§ (absβ(π β π’)) β€ (π + π’)) β π β€ (π + π’))) |
168 | 154, 167 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β€ (absβ(π β π’)) β π β€ (π + π’))) |
169 | 114, 168 | mtod 197 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β Β¬ π β€ (absβ(π β π’))) |
170 | 169 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β Β¬ π β€ (absβ(π β π’))) |
171 | 96 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β π β β€) |
172 | | dvdsle 16199 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β€ β§
(absβ(π β π’)) β β) β (π β₯ (absβ(π β π’)) β π β€ (absβ(π β π’)))) |
173 | 171, 134,
172 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β (π β₯ (absβ(π β π’)) β π β€ (absβ(π β π’)))) |
174 | 170, 173 | mtod 197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π β (0...π) β§ π’ β (0...π))) β§ π β π’) β Β¬ π β₯ (absβ(π β π’))) |
175 | 174 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β π’ β Β¬ π β₯ (absβ(π β π’)))) |
176 | 175 | necon4ad 2963 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β₯ (absβ(π β π’)) β π = π’)) |
177 | 165, 176 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (π β₯ (π β π’) β π = π’)) |
178 | 163, 177 | jaod 858 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β ((π β₯ (π + π’) β¨ π β₯ (π β π’)) β π = π’)) |
179 | 89, 178 | sylbid 239 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (((πβ2) mod π) = ((π’β2) mod π) β π = π’)) |
180 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π’ β (πβ2) = (π’β2)) |
181 | 180 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π’ β ((πβ2) mod π) = ((π’β2) mod π)) |
182 | 179, 181 | impbid1 224 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β (0...π) β§ π’ β (0...π))) β (((πβ2) mod π) = ((π’β2) mod π) β π = π’)) |
183 | 182 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π β (0...π) β§ π’ β (0...π)) β (((πβ2) mod π) = ((π’β2) mod π) β π = π’))) |
184 | 69, 183 | dom2lem 8939 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1β(0...(π β 1))) |
185 | | f1f1orn 6800 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1β(0...(π β 1)) β (π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1-ontoβran
(π β (0...π) β¦ ((πβ2) mod π))) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1-ontoβran
(π β (0...π) β¦ ((πβ2) mod π))) |
187 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β¦ ((πβ2) mod π)) = (π β (0...π) β¦ ((πβ2) mod π)) |
188 | 187 | rnmpt 5915 |
. . . . . . . . . . . . . . . . 17
β’ ran
(π β (0...π) β¦ ((πβ2) mod π)) = {π’ β£ βπ β (0...π)π’ = ((πβ2) mod π)} |
189 | 2, 188 | eqtr4i 2768 |
. . . . . . . . . . . . . . . 16
β’ π΄ = ran (π β (0...π) β¦ ((πβ2) mod π)) |
190 | | f1oeq3 6779 |
. . . . . . . . . . . . . . . 16
β’ (π΄ = ran (π β (0...π) β¦ ((πβ2) mod π)) β ((π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1-ontoβπ΄ β (π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1-ontoβran
(π β (0...π) β¦ ((πβ2) mod π)))) |
191 | 189, 190 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ((π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1-ontoβπ΄ β (π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1-ontoβran
(π β (0...π) β¦ ((πβ2) mod π))) |
192 | 186, 191 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (π β (π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1-ontoβπ΄) |
193 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’
(0...π) β
V |
194 | 193 | f1oen 8920 |
. . . . . . . . . . . . . 14
β’ ((π β (0...π) β¦ ((πβ2) mod π)):(0...π)β1-1-ontoβπ΄ β (0...π) β π΄) |
195 | 192, 194 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π΄) |
196 | 195 | ensymd 8952 |
. . . . . . . . . . . 12
β’ (π β π΄ β (0...π)) |
197 | | ax-1cn 11116 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
198 | | pncan 11414 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
199 | 57, 197, 198 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (π β ((π + 1) β 1) = π) |
200 | 199 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π β (0...((π + 1) β 1)) = (0...π)) |
201 | 56 | nnnn0d 12480 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
202 | | peano2nn0 12460 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π + 1) β
β0) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π + 1) β
β0) |
204 | 203 | nn0zd 12532 |
. . . . . . . . . . . . . 14
β’ (π β (π + 1) β β€) |
205 | | fz01en 13476 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β β€ β
(0...((π + 1) β 1))
β (1...(π +
1))) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (0...((π + 1) β 1)) β (1...(π + 1))) |
207 | 200, 206 | eqbrtrrd 5134 |
. . . . . . . . . . . 12
β’ (π β (0...π) β (1...(π + 1))) |
208 | | entr 8953 |
. . . . . . . . . . . 12
β’ ((π΄ β (0...π) β§ (0...π) β (1...(π + 1))) β π΄ β (1...(π + 1))) |
209 | 196, 207,
208 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β π΄ β (1...(π + 1))) |
210 | 1, 15 | ssfid 9218 |
. . . . . . . . . . . 12
β’ (π β π΄ β Fin) |
211 | | fzfid 13885 |
. . . . . . . . . . . 12
β’ (π β (1...(π + 1)) β Fin) |
212 | | hashen 14254 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ (1...(π + 1)) β Fin) β
((β―βπ΄) =
(β―β(1...(π +
1))) β π΄ β
(1...(π +
1)))) |
213 | 210, 211,
212 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ((β―βπ΄) = (β―β(1...(π + 1))) β π΄ β (1...(π + 1)))) |
214 | 209, 213 | mpbird 257 |
. . . . . . . . . 10
β’ (π β (β―βπ΄) = (β―β(1...(π + 1)))) |
215 | | hashfz1 14253 |
. . . . . . . . . . 11
β’ ((π + 1) β β0
β (β―β(1...(π + 1))) = (π + 1)) |
216 | 203, 215 | syl 17 |
. . . . . . . . . 10
β’ (π β (β―β(1...(π + 1))) = (π + 1)) |
217 | 214, 216 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β (β―βπ΄) = (π + 1)) |
218 | 27 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β (π£ β π΄ β ((π β 1) β π£) β (0...(π β 1)))) |
219 | 20 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π£ β π΄ β§ π β π΄)) β (π β 1) β β) |
220 | | fzssuz 13489 |
. . . . . . . . . . . . . . . . . . . 20
β’
(0...(π β 1))
β (β€β₯β0) |
221 | | uzssz 12791 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β€β₯β0) β β€ |
222 | | zsscn 12514 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β€
β β |
223 | 221, 222 | sstri 3958 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β€β₯β0) β β |
224 | 220, 223 | sstri 3958 |
. . . . . . . . . . . . . . . . . . 19
β’
(0...(π β 1))
β β |
225 | 15, 224 | sstrdi 3961 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β β) |
226 | 225 | sselda 3949 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π£ β π΄) β π£ β β) |
227 | 226 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π£ β π΄ β§ π β π΄)) β π£ β β) |
228 | 225 | sselda 3949 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΄) β π β β) |
229 | 228 | adantrl 715 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π£ β π΄ β§ π β π΄)) β π β β) |
230 | 219, 227,
229 | subcanad 11562 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π£ β π΄ β§ π β π΄)) β (((π β 1) β π£) = ((π β 1) β π) β π£ = π)) |
231 | 230 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β ((π£ β π΄ β§ π β π΄) β (((π β 1) β π£) = ((π β 1) β π) β π£ = π))) |
232 | 218, 231 | dom2lem 8939 |
. . . . . . . . . . . . 13
β’ (π β (π£ β π΄ β¦ ((π β 1) β π£)):π΄β1-1β(0...(π β 1))) |
233 | | f1eq1 6738 |
. . . . . . . . . . . . . 14
β’ (πΉ = (π£ β π΄ β¦ ((π β 1) β π£)) β (πΉ:π΄β1-1β(0...(π β 1)) β (π£ β π΄ β¦ ((π β 1) β π£)):π΄β1-1β(0...(π β 1)))) |
234 | 28, 233 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (πΉ:π΄β1-1β(0...(π β 1)) β (π£ β π΄ β¦ ((π β 1) β π£)):π΄β1-1β(0...(π β 1))) |
235 | 232, 234 | sylibr 233 |
. . . . . . . . . . . 12
β’ (π β πΉ:π΄β1-1β(0...(π β 1))) |
236 | | f1f1orn 6800 |
. . . . . . . . . . . 12
β’ (πΉ:π΄β1-1β(0...(π β 1)) β πΉ:π΄β1-1-ontoβran
πΉ) |
237 | 235, 236 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ:π΄β1-1-ontoβran
πΉ) |
238 | 210, 237 | hasheqf1od 14260 |
. . . . . . . . . 10
β’ (π β (β―βπ΄) = (β―βran πΉ)) |
239 | 238, 217 | eqtr3d 2779 |
. . . . . . . . 9
β’ (π β (β―βran πΉ) = (π + 1)) |
240 | 217, 239 | oveq12d 7380 |
. . . . . . . 8
β’ (π β ((β―βπ΄) + (β―βran πΉ)) = ((π + 1) + (π + 1))) |
241 | 59, 68, 240 | 3eqtr4d 2787 |
. . . . . . 7
β’ (π β (π + 1) = ((β―βπ΄) + (β―βran πΉ))) |
242 | 241 | adantr 482 |
. . . . . 6
β’ ((π β§ (π΄ β© ran πΉ) = β
) β (π + 1) = ((β―βπ΄) + (β―βran πΉ))) |
243 | 210 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π΄ β© ran πΉ) = β
) β π΄ β Fin) |
244 | 1, 30 | ssfid 9218 |
. . . . . . . 8
β’ (π β ran πΉ β Fin) |
245 | 244 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π΄ β© ran πΉ) = β
) β ran πΉ β Fin) |
246 | | simpr 486 |
. . . . . . 7
β’ ((π β§ (π΄ β© ran πΉ) = β
) β (π΄ β© ran πΉ) = β
) |
247 | | hashun 14289 |
. . . . . . 7
β’ ((π΄ β Fin β§ ran πΉ β Fin β§ (π΄ β© ran πΉ) = β
) β (β―β(π΄ βͺ ran πΉ)) = ((β―βπ΄) + (β―βran πΉ))) |
248 | 243, 245,
246, 247 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π΄ β© ran πΉ) = β
) β (β―β(π΄ βͺ ran πΉ)) = ((β―βπ΄) + (β―βran πΉ))) |
249 | 242, 248 | eqtr4d 2780 |
. . . . 5
β’ ((π β§ (π΄ β© ran πΉ) = β
) β (π + 1) = (β―β(π΄ βͺ ran πΉ))) |
250 | 55, 249 | breqtrd 5136 |
. . . 4
β’ ((π β§ (π΄ β© ran πΉ) = β
) β π < (β―β(π΄ βͺ ran πΉ))) |
251 | 250 | ex 414 |
. . 3
β’ (π β ((π΄ β© ran πΉ) = β
β π < (β―β(π΄ βͺ ran πΉ)))) |
252 | 251 | necon3bd 2958 |
. 2
β’ (π β (Β¬ π < (β―β(π΄ βͺ ran πΉ)) β (π΄ β© ran πΉ) β β
)) |
253 | 53, 252 | mpd 15 |
1
β’ (π β (π΄ β© ran πΉ) β β
) |