Step | Hyp | Ref
| Expression |
1 | | eucrctshift.v |
. . . . 5
β’ π = (VtxβπΊ) |
2 | | eucrctshift.i |
. . . . 5
β’ πΌ = (iEdgβπΊ) |
3 | | eucrctshift.c |
. . . . 5
β’ (π β πΉ(CircuitsβπΊ)π) |
4 | | eucrctshift.n |
. . . . 5
β’ π = (β―βπΉ) |
5 | | eucrctshift.s |
. . . . 5
β’ (π β π β (0..^π)) |
6 | | eucrctshift.h |
. . . . 5
β’ π» = (πΉ cyclShift π) |
7 | | eucrctshift.q |
. . . . 5
β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) |
8 | 1, 2, 3, 4, 5, 6, 7 | crctcshtrl 29345 |
. . . 4
β’ (π β π»(TrailsβπΊ)π) |
9 | | simpr 484 |
. . . . 5
β’ ((π β§ π»(TrailsβπΊ)π) β π»(TrailsβπΊ)π) |
10 | | eucrctshift.e |
. . . . . . . 8
β’ (π β πΉ(EulerPathsβπΊ)π) |
11 | 2 | eupthf1o 29725 |
. . . . . . . 8
β’ (πΉ(EulerPathsβπΊ)π β πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ) |
12 | 10, 11 | syl 17 |
. . . . . . 7
β’ (π β πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ) |
13 | 12 | adantr 480 |
. . . . . 6
β’ ((π β§ π»(TrailsβπΊ)π) β πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ) |
14 | | trliswlk 29222 |
. . . . . . . . 9
β’ (π»(TrailsβπΊ)π β π»(WalksβπΊ)π) |
15 | 2 | wlkf 29139 |
. . . . . . . . 9
β’ (π»(WalksβπΊ)π β π» β Word dom πΌ) |
16 | | wrdf 14474 |
. . . . . . . . 9
β’ (π» β Word dom πΌ β π»:(0..^(β―βπ»))βΆdom πΌ) |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . 8
β’ (π»(TrailsβπΊ)π β π»:(0..^(β―βπ»))βΆdom πΌ) |
18 | | df-f1o 6550 |
. . . . . . . . . 10
β’ (πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ β (πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β§ πΉ:(0..^(β―βπΉ))βontoβdom πΌ)) |
19 | | dffo3 7103 |
. . . . . . . . . . 11
β’ (πΉ:(0..^(β―βπΉ))βontoβdom πΌ β (πΉ:(0..^(β―βπΉ))βΆdom πΌ β§ βπ β dom πΌβπ¦ β (0..^(β―βπΉ))π = (πΉβπ¦))) |
20 | | crctiswlk 29321 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΉ(CircuitsβπΊ)π β πΉ(WalksβπΊ)π) |
21 | 2 | wlkf 29139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΉ(WalksβπΊ)π β πΉ β Word dom πΌ) |
22 | | lencl 14488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΉ β Word dom πΌ β (β―βπΉ) β
β0) |
23 | 4 | oveq2i 7423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(0..^π) =
(0..^(β―βπΉ)) |
24 | 23 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0..^π) β π β (0..^(β―βπΉ))) |
25 | | elfzonn0 13682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β
(0..^(β―βπΉ))
β π β
β0) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β π β
β0) |
27 | | elfzonn0 13682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ β
(0..^(β―βπΉ))
β π¦ β
β0) |
28 | | nn0sub 12527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β0
β§ π¦ β
β0) β (π β€ π¦ β (π¦ β π) β
β0)) |
29 | 26, 27, 28 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β (π β€ π¦ β (π¦ β π) β
β0)) |
30 | 29 | biimpac 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (π¦ β π) β
β0) |
31 | | elfzo0 13678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ β
(0..^(β―βπΉ))
β (π¦ β
β0 β§ (β―βπΉ) β β β§ π¦ < (β―βπΉ))) |
32 | | simp2 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
(β―βπΉ) β
β) |
33 | 31, 32 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π¦ β
(0..^(β―βπΉ))
β (β―βπΉ)
β β) |
34 | 33 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (β―βπΉ)
β β) |
35 | | nn0re 12486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π¦ β β0
β π¦ β
β) |
36 | 35 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π¦ β β0
β§ (β―βπΉ)
β β) β§ π
β (0..^(β―βπΉ))) β π¦ β β) |
37 | | nnre 12224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’
((β―βπΉ)
β β β (β―βπΉ) β β) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π¦ β β0
β§ (β―βπΉ)
β β) β (β―βπΉ) β β) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π¦ β β0
β§ (β―βπΉ)
β β) β§ π
β (0..^(β―βπΉ))) β (β―βπΉ) β β) |
40 | | elfzoelz 13637 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ (π β
(0..^(β―βπΉ))
β π β
β€) |
41 | 40 | zred 12671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π β
(0..^(β―βπΉ))
β π β
β) |
42 | | readdcl 11197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
(((β―βπΉ)
β β β§ π
β β) β ((β―βπΉ) + π) β β) |
43 | 38, 41, 42 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π¦ β β0
β§ (β―βπΉ)
β β) β§ π
β (0..^(β―βπΉ))) β ((β―βπΉ) + π) β β) |
44 | 36, 39, 43 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ (β―βπΉ)
β β) β§ π
β (0..^(β―βπΉ))) β (π¦ β β β§ (β―βπΉ) β β β§
((β―βπΉ) + π) β
β)) |
45 | | elfzole1 13645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π β
(0..^(β―βπΉ))
β 0 β€ π) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π¦ β β0
β§ (β―βπΉ)
β β) β§ π
β (0..^(β―βπΉ))) β 0 β€ π) |
47 | | addge01 11729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
(((β―βπΉ)
β β β§ π
β β) β (0 β€ π β (β―βπΉ) β€ ((β―βπΉ) + π))) |
48 | 38, 41, 47 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π¦ β β0
β§ (β―βπΉ)
β β) β§ π
β (0..^(β―βπΉ))) β (0 β€ π β (β―βπΉ) β€ ((β―βπΉ) + π))) |
49 | 46, 48 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ (β―βπΉ)
β β) β§ π
β (0..^(β―βπΉ))) β (β―βπΉ) β€ ((β―βπΉ) + π)) |
50 | 44, 49 | lelttrdi 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (((π¦ β β0
β§ (β―βπΉ)
β β) β§ π
β (0..^(β―βπΉ))) β (π¦ < (β―βπΉ) β π¦ < ((β―βπΉ) + π))) |
51 | 50 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π¦ β β0
β§ (β―βπΉ)
β β) β (π
β (0..^(β―βπΉ)) β (π¦ < (β―βπΉ) β π¦ < ((β―βπΉ) + π)))) |
52 | 51 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π¦ β β0
β§ (β―βπΉ)
β β) β (π¦
< (β―βπΉ)
β (π β
(0..^(β―βπΉ))
β π¦ <
((β―βπΉ) + π)))) |
53 | 52 | 3impia 1116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
(π β
(0..^(β―βπΉ))
β π¦ <
((β―βπΉ) + π))) |
54 | 53 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
(((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ))) β π¦ < ((β―βπΉ) + π))) |
55 | 54 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β§
((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ)))) β π¦ < ((β―βπΉ) + π)) |
56 | 35 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
π¦ β
β) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β§
((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ)))) β π¦ β β) |
58 | 41 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β§
((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ)))) β π β β) |
59 | | elfzoel2 13636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β
(0..^(β―βπΉ))
β (β―βπΉ)
β β€) |
60 | 59 | zred 12671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β
(0..^(β―βπΉ))
β (β―βπΉ)
β β) |
61 | 60 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β§
((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ)))) β (β―βπΉ) β β) |
62 | 57, 58, 61 | ltsubaddd 11815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β§
((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ)))) β ((π¦ β π) < (β―βπΉ) β π¦ < ((β―βπΉ) + π))) |
63 | 55, 62 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β§
((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ)))) β (π¦ β π) < (β―βπΉ)) |
64 | 63 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
(((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ))) β (π¦ β π) < (β―βπΉ))) |
65 | 31, 64 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ β
(0..^(β―βπΉ))
β (((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β (π¦ β π) < (β―βπΉ))) |
66 | 65 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β (π¦ β π) < (β―βπΉ)) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (π¦ β π) < (β―βπΉ)) |
68 | | elfzo0 13678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π¦ β π) β (0..^(β―βπΉ)) β ((π¦ β π) β β0 β§
(β―βπΉ) β
β β§ (π¦ β
π) <
(β―βπΉ))) |
69 | 30, 34, 67, 68 | syl3anbrc 1342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (π¦ β π) β
(0..^(β―βπΉ))) |
70 | | oveq1 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π§ = (π¦ β π) β (π§ + π) = ((π¦ β π) + π)) |
71 | 70 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π§ = (π¦ β π) β ((π§ + π) mod (β―βπΉ)) = (((π¦ β π) + π) mod (β―βπΉ))) |
72 | 40 | zcnd 12672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β
(0..^(β―βπΉ))
β π β
β) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β π β β) |
74 | | elfzoelz 13637 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π¦ β
(0..^(β―βπΉ))
β π¦ β
β€) |
75 | 74 | zcnd 12672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π¦ β
(0..^(β―βπΉ))
β π¦ β
β) |
76 | 73, 75 | anim12ci 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β (π¦ β β β§ π β β)) |
77 | 76 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (π¦ β β
β§ π β
β)) |
78 | | npcan 11474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π¦ β β β§ π β β) β ((π¦ β π) + π) = π¦) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β ((π¦ β π) + π) = π¦) |
80 | 79 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (((π¦ β π) + π) mod (β―βπΉ)) = (π¦ mod (β―βπΉ))) |
81 | | zmodidfzoimp 13871 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π¦ β
(0..^(β―βπΉ))
β (π¦ mod
(β―βπΉ)) = π¦) |
82 | 81 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (π¦ mod
(β―βπΉ)) = π¦) |
83 | 80, 82 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (((π¦ β π) + π) mod (β―βπΉ)) = π¦) |
84 | 71, 83 | sylan9eqr 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β§ π§ = (π¦ β π)) β ((π§ + π) mod (β―βπΉ)) = π¦) |
85 | 84 | eqcomd 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β§ π§ = (π¦ β π)) β π¦ = ((π§ + π) mod (β―βπΉ))) |
86 | 69, 85 | rspcedeq2vd 3619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β βπ§ β
(0..^(β―βπΉ))π¦ = ((π§ + π) mod (β―βπΉ))) |
87 | | elfzo0 13678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β
(0..^(β―βπΉ))
β (π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) |
88 | | nn0cn 12487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π¦ β β0
β π¦ β
β) |
89 | 88 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β π¦ β β) |
90 | | nn0cn 12487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π β β0
β π β
β) |
91 | 90 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π β β0
β§ (β―βπΉ)
β β β§ π <
(β―βπΉ)) β
π β
β) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β π β β) |
93 | | nncn 12225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
((β―βπΉ)
β β β (β―βπΉ) β β) |
94 | 93 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π β β0
β§ (β―βπΉ)
β β β§ π <
(β―βπΉ)) β
(β―βπΉ) β
β) |
95 | 94 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β (β―βπΉ) β β) |
96 | 89, 92, 95 | subadd23d 11598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β ((π¦ β π) + (β―βπΉ)) = (π¦ + ((β―βπΉ) β π))) |
97 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β π¦ β β0) |
98 | | nn0z 12588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ (π β β0
β π β
β€) |
99 | | nnz 12584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’
((β―βπΉ)
β β β (β―βπΉ) β β€) |
100 | | znnsub 12613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((π β β€ β§
(β―βπΉ) β
β€) β (π <
(β―βπΉ) β
((β―βπΉ) β
π) β
β)) |
101 | 98, 99, 100 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((π β β0
β§ (β―βπΉ)
β β) β (π
< (β―βπΉ)
β ((β―βπΉ)
β π) β
β)) |
102 | 101 | biimp3a 1468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π β β0
β§ (β―βπΉ)
β β β§ π <
(β―βπΉ)) β
((β―βπΉ) β
π) β
β) |
103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β ((β―βπΉ) β π) β β) |
104 | 103 | nnnn0d 12537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β ((β―βπΉ) β π) β
β0) |
105 | 97, 104 | nn0addcld 12541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β (π¦ + ((β―βπΉ) β π)) β
β0) |
106 | 96, 105 | eqeltrd 2832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β ((π¦ β π) + (β―βπΉ)) β
β0) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β ((π¦ β π) + (β―βπΉ)) β
β0) |
108 | | simplr2 1215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β (β―βπΉ) β β) |
109 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π¦ β β0
β§ π¦ <
(β―βπΉ)) β
π¦ β
β) |
110 | | subcl 11464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π¦ β β β§ π β β) β (π¦ β π) β β) |
111 | 109, 91, 110 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β (π¦ β π) β β) |
112 | 95, 111 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β ((β―βπΉ) β β β§ (π¦ β π) β β)) |
113 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β ((β―βπΉ) β β β§ (π¦ β π) β β)) |
114 | | addcom 11405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(((β―βπΉ)
β β β§ (π¦
β π) β β)
β ((β―βπΉ) +
(π¦ β π)) = ((π¦ β π) + (β―βπΉ))) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β ((β―βπΉ) + (π¦ β π)) = ((π¦ β π) + (β―βπΉ))) |
116 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π¦ β β0
β§ π¦ <
(β―βπΉ)) β
π¦ β
β) |
117 | | nn0re 12486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (π β β0
β π β
β) |
118 | 117 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π β β0
β§ (β―βπΉ)
β β β§ π <
(β―βπΉ)) β
π β
β) |
119 | | ltnle 11298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π¦ β β β§ π β β) β (π¦ < π β Β¬ π β€ π¦)) |
120 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((π¦ β β β§ π β β) β π¦ β
β) |
121 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((π¦ β β β§ π β β) β π β
β) |
122 | 120, 121 | sublt0d 11845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((π¦ β β β§ π β β) β ((π¦ β π) < 0 β π¦ < π)) |
123 | 122 | biimprd 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π¦ β β β§ π β β) β (π¦ < π β (π¦ β π) < 0)) |
124 | 119, 123 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π¦ β β β§ π β β) β (Β¬
π β€ π¦ β (π¦ β π) < 0)) |
125 | 116, 118,
124 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β (Β¬ π β€ π¦ β (π¦ β π) < 0)) |
126 | 125 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β (π¦ β π) < 0) |
127 | | resubcl 11529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((π¦ β β β§ π β β) β (π¦ β π) β β) |
128 | 116, 118,
127 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β (π¦ β π) β β) |
129 | 37 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((π β β0
β§ (β―βπΉ)
β β β§ π <
(β―βπΉ)) β
(β―βπΉ) β
β) |
130 | 129 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β (β―βπΉ) β β) |
131 | 128, 130 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β ((π¦ β π) β β β§ (β―βπΉ) β
β)) |
132 | 131 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β ((π¦ β π) β β β§ (β―βπΉ) β
β)) |
133 | | ltaddneg 11434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π¦ β π) β β β§ (β―βπΉ) β β) β ((π¦ β π) < 0 β ((β―βπΉ) + (π¦ β π)) < (β―βπΉ))) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β ((π¦ β π) < 0 β ((β―βπΉ) + (π¦ β π)) < (β―βπΉ))) |
135 | 126, 134 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β ((β―βπΉ) + (π¦ β π)) < (β―βπΉ)) |
136 | 115, 135 | eqbrtrrd 5172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β ((π¦ β π) + (β―βπΉ)) < (β―βπΉ)) |
137 | 107, 108,
136 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((((π¦ β β0
β§ π¦ <
(β―βπΉ)) β§
(π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ))) β§ Β¬ π β€ π¦) β (((π¦ β π) + (β―βπΉ)) β β0 β§
(β―βπΉ) β
β β§ ((π¦ β
π) + (β―βπΉ)) < (β―βπΉ))) |
138 | 137 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π¦ β β0
β§ π¦ <
(β―βπΉ)) β
((π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ)) β (Β¬ π β€ π¦ β (((π¦ β π) + (β―βπΉ)) β β0 β§
(β―βπΉ) β
β β§ ((π¦ β
π) + (β―βπΉ)) < (β―βπΉ))))) |
139 | 138 | 3adant2 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
((π β
β0 β§ (β―βπΉ) β β β§ π < (β―βπΉ)) β (Β¬ π β€ π¦ β (((π¦ β π) + (β―βπΉ)) β β0 β§
(β―βπΉ) β
β β§ ((π¦ β
π) + (β―βπΉ)) < (β―βπΉ))))) |
140 | 87, 139 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
(π β
(0..^(β―βπΉ))
β (Β¬ π β€ π¦ β (((π¦ β π) + (β―βπΉ)) β β0 β§
(β―βπΉ) β
β β§ ((π¦ β
π) + (β―βπΉ)) < (β―βπΉ))))) |
141 | 140 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
(((β―βπΉ) β
β0 β§ π
β (0..^(β―βπΉ))) β (Β¬ π β€ π¦ β (((π¦ β π) + (β―βπΉ)) β β0 β§
(β―βπΉ) β
β β§ ((π¦ β
π) + (β―βπΉ)) < (β―βπΉ))))) |
142 | 31, 141 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ β
(0..^(β―βπΉ))
β (((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β (Β¬ π β€ π¦ β (((π¦ β π) + (β―βπΉ)) β β0 β§
(β―βπΉ) β
β β§ ((π¦ β
π) + (β―βπΉ)) < (β―βπΉ))))) |
143 | 142 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β (Β¬ π β€ π¦ β (((π¦ β π) + (β―βπΉ)) β β0 β§
(β―βπΉ) β
β β§ ((π¦ β
π) + (β―βπΉ)) < (β―βπΉ)))) |
144 | 143 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (((π¦ β π) + (β―βπΉ)) β β0
β§ (β―βπΉ)
β β β§ ((π¦
β π) +
(β―βπΉ)) <
(β―βπΉ))) |
145 | | elfzo0 13678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π¦ β π) + (β―βπΉ)) β (0..^(β―βπΉ)) β (((π¦ β π) + (β―βπΉ)) β β0 β§
(β―βπΉ) β
β β§ ((π¦ β
π) + (β―βπΉ)) < (β―βπΉ))) |
146 | 144, 145 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β ((π¦ β π) + (β―βπΉ)) β
(0..^(β―βπΉ))) |
147 | | oveq1 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π§ = ((π¦ β π) + (β―βπΉ)) β (π§ + π) = (((π¦ β π) + (β―βπΉ)) + π)) |
148 | 147 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π§ = ((π¦ β π) + (β―βπΉ)) β ((π§ + π) mod (β―βπΉ)) = ((((π¦ β π) + (β―βπΉ)) + π) mod (β―βπΉ))) |
149 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β π β β) |
150 | 75 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β π¦ β β) |
151 | | nn0cn 12487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((β―βπΉ)
β β0 β (β―βπΉ) β β) |
152 | 151 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β (β―βπΉ) β β) |
153 | 149, 150,
152 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β (π β β β§ π¦ β β β§ (β―βπΉ) β
β)) |
154 | 153 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (π β β
β§ π¦ β β
β§ (β―βπΉ)
β β)) |
155 | | simp2 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β β β§ π¦ β β β§
(β―βπΉ) β
β) β π¦ β
β) |
156 | | simp3 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β β β§ π¦ β β β§
(β―βπΉ) β
β) β (β―βπΉ) β β) |
157 | | simp1 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β β β§ π¦ β β β§
(β―βπΉ) β
β) β π β
β) |
158 | 155, 157,
156 | nppcand 11601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β β β§ π¦ β β β§
(β―βπΉ) β
β) β (((π¦
β π) +
(β―βπΉ)) + π) = (π¦ + (β―βπΉ))) |
159 | 155, 156,
158 | comraddd 11433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β β β§ π¦ β β β§
(β―βπΉ) β
β) β (((π¦
β π) +
(β―βπΉ)) + π) = ((β―βπΉ) + π¦)) |
160 | 154, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (((π¦ β π) + (β―βπΉ)) + π) = ((β―βπΉ) + π¦)) |
161 | 160 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β ((((π¦ β π) + (β―βπΉ)) + π) mod (β―βπΉ)) = (((β―βπΉ) + π¦) mod (β―βπΉ))) |
162 | 31 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π¦ β
(0..^(β―βπΉ))
β (π¦ β
β0 β§ (β―βπΉ) β β β§ π¦ < (β―βπΉ))) |
163 | 162 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (π¦ β
β0 β§ (β―βπΉ) β β β§ π¦ < (β―βπΉ))) |
164 | | addmodid 13889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π¦ β β0
β§ (β―βπΉ)
β β β§ π¦ <
(β―βπΉ)) β
(((β―βπΉ) + π¦) mod (β―βπΉ)) = π¦) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β (((β―βπΉ)
+ π¦) mod
(β―βπΉ)) = π¦) |
166 | 161, 165 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β ((((π¦ β π) + (β―βπΉ)) + π) mod (β―βπΉ)) = π¦) |
167 | 148, 166 | sylan9eqr 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β§ π§ = ((π¦ β π) + (β―βπΉ))) β ((π§ + π) mod (β―βπΉ)) = π¦) |
168 | 167 | eqcomd 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β§ π§ = ((π¦ β π) + (β―βπΉ))) β π¦ = ((π§ + π) mod (β―βπΉ))) |
169 | 146, 168 | rspcedeq2vd 3619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((Β¬
π β€ π¦ β§ (((β―βπΉ) β β0 β§ π β
(0..^(β―βπΉ)))
β§ π¦ β
(0..^(β―βπΉ))))
β βπ§ β
(0..^(β―βπΉ))π¦ = ((π§ + π) mod (β―βπΉ))) |
170 | 86, 169 | pm2.61ian 809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β βπ§ β (0..^(β―βπΉ))π¦ = ((π§ + π) mod (β―βπΉ))) |
171 | 23 | rexeqi 3323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(βπ§ β
(0..^π)π¦ = ((π§ + π) mod (β―βπΉ)) β βπ§ β (0..^(β―βπΉ))π¦ = ((π§ + π) mod (β―βπΉ))) |
172 | 170, 171 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((β―βπΉ)
β β0 β§ π β (0..^(β―βπΉ))) β§ π¦ β (0..^(β―βπΉ))) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ))) |
173 | 172 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β―βπΉ)
β β0 β (π β (0..^(β―βπΉ)) β (π¦ β (0..^(β―βπΉ)) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ))))) |
174 | 24, 173 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπΉ)
β β0 β (π β (0..^π) β (π¦ β (0..^(β―βπΉ)) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ))))) |
175 | 22, 174 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΉ β Word dom πΌ β (π β (0..^π) β (π¦ β (0..^(β―βπΉ)) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ))))) |
176 | 20, 21, 175 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΉ(CircuitsβπΊ)π β (π β (0..^π) β (π¦ β (0..^(β―βπΉ)) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ))))) |
177 | 3, 5, 176 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π¦ β (0..^(β―βπΉ)) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ)))) |
178 | 177 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β dom πΌ) β (π¦ β (0..^(β―βπΉ)) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ)))) |
179 | 178 | imp 406 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ))) |
180 | 179 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β βπ§ β (0..^π)π¦ = ((π§ + π) mod (β―βπΉ))) |
181 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = ((π§ + π) mod (β―βπΉ)) β (πΉβπ¦) = (πΉβ((π§ + π) mod (β―βπΉ)))) |
182 | 181 | reximi 3083 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ§ β
(0..^π)π¦ = ((π§ + π) mod (β―βπΉ)) β βπ§ β (0..^π)(πΉβπ¦) = (πΉβ((π§ + π) mod (β―βπΉ)))) |
183 | 180, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β βπ§ β (0..^π)(πΉβπ¦) = (πΉβ((π§ + π) mod (β―βπΉ)))) |
184 | 3, 20, 21 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΉ β Word dom πΌ) |
185 | 184 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β πΉ β Word dom πΌ) |
186 | | elfzoelz 13637 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0..^π) β π β β€) |
187 | 5, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β€) |
188 | 187 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β π β β€) |
189 | 23 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ β (0..^π) β π§ β (0..^(β―βπΉ))) |
190 | 189 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ β (0..^π) β π§ β (0..^(β―βπΉ))) |
191 | | cshwidxmod 14758 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉ β Word dom πΌ β§ π β β€ β§ π§ β (0..^(β―βπΉ))) β ((πΉ cyclShift π)βπ§) = (πΉβ((π§ + π) mod (β―βπΉ)))) |
192 | 185, 188,
190, 191 | syl2an3an 1421 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β§ π§ β (0..^π)) β ((πΉ cyclShift π)βπ§) = (πΉβ((π§ + π) mod (β―βπΉ)))) |
193 | 192 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β§ π§ β (0..^π)) β ((πΉβπ¦) = ((πΉ cyclShift π)βπ§) β (πΉβπ¦) = (πΉβ((π§ + π) mod (β―βπΉ))))) |
194 | 193 | rexbidva 3175 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β (βπ§ β (0..^π)(πΉβπ¦) = ((πΉ cyclShift π)βπ§) β βπ§ β (0..^π)(πΉβπ¦) = (πΉβ((π§ + π) mod (β―βπΉ))))) |
195 | 183, 194 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β βπ§ β (0..^π)(πΉβπ¦) = ((πΉ cyclShift π)βπ§)) |
196 | 1, 2, 3, 4, 5, 6 | crctcshlem2 29340 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β―βπ») = π) |
197 | 196 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^(β―βπ»)) = (0..^π)) |
198 | 197 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β (0..^(β―βπ»)) = (0..^π)) |
199 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β π = (πΉβπ¦)) |
200 | 6 | fveq1i 6892 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π»βπ§) = ((πΉ cyclShift π)βπ§) |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β (π»βπ§) = ((πΉ cyclShift π)βπ§)) |
202 | 199, 201 | eqeq12d 2747 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β (π = (π»βπ§) β (πΉβπ¦) = ((πΉ cyclShift π)βπ§))) |
203 | 198, 202 | rexeqbidv 3342 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β (βπ§ β (0..^(β―βπ»))π = (π»βπ§) β βπ§ β (0..^π)(πΉβπ¦) = ((πΉ cyclShift π)βπ§))) |
204 | 195, 203 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β dom πΌ) β§ π¦ β (0..^(β―βπΉ))) β§ π = (πΉβπ¦)) β βπ§ β (0..^(β―βπ»))π = (π»βπ§)) |
205 | 204 | rexlimdva2 3156 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β dom πΌ) β (βπ¦ β (0..^(β―βπΉ))π = (πΉβπ¦) β βπ§ β (0..^(β―βπ»))π = (π»βπ§))) |
206 | 205 | ralimdva 3166 |
. . . . . . . . . . . . . . 15
β’ (π β (βπ β dom πΌβπ¦ β (0..^(β―βπΉ))π = (πΉβπ¦) β βπ β dom πΌβπ§ β (0..^(β―βπ»))π = (π»βπ§))) |
207 | 206 | impcom 407 |
. . . . . . . . . . . . . 14
β’
((βπ β
dom πΌβπ¦ β
(0..^(β―βπΉ))π = (πΉβπ¦) β§ π) β βπ β dom πΌβπ§ β (0..^(β―βπ»))π = (π»βπ§)) |
208 | 207 | anim1ci 615 |
. . . . . . . . . . . . 13
β’
(((βπ β
dom πΌβπ¦ β
(0..^(β―βπΉ))π = (πΉβπ¦) β§ π) β§ π»:(0..^(β―βπ»))βΆdom πΌ) β (π»:(0..^(β―βπ»))βΆdom πΌ β§ βπ β dom πΌβπ§ β (0..^(β―βπ»))π = (π»βπ§))) |
209 | | dffo3 7103 |
. . . . . . . . . . . . 13
β’ (π»:(0..^(β―βπ»))βontoβdom πΌ β (π»:(0..^(β―βπ»))βΆdom πΌ β§ βπ β dom πΌβπ§ β (0..^(β―βπ»))π = (π»βπ§))) |
210 | 208, 209 | sylibr 233 |
. . . . . . . . . . . 12
β’
(((βπ β
dom πΌβπ¦ β
(0..^(β―βπΉ))π = (πΉβπ¦) β§ π) β§ π»:(0..^(β―βπ»))βΆdom πΌ) β π»:(0..^(β―βπ»))βontoβdom πΌ) |
211 | 210 | exp31 419 |
. . . . . . . . . . 11
β’
(βπ β
dom πΌβπ¦ β
(0..^(β―βπΉ))π = (πΉβπ¦) β (π β (π»:(0..^(β―βπ»))βΆdom πΌ β π»:(0..^(β―βπ»))βontoβdom πΌ))) |
212 | 19, 211 | simplbiim 504 |
. . . . . . . . . 10
β’ (πΉ:(0..^(β―βπΉ))βontoβdom πΌ β (π β (π»:(0..^(β―βπ»))βΆdom πΌ β π»:(0..^(β―βπ»))βontoβdom πΌ))) |
213 | 18, 212 | simplbiim 504 |
. . . . . . . . 9
β’ (πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ β (π β (π»:(0..^(β―βπ»))βΆdom πΌ β π»:(0..^(β―βπ»))βontoβdom πΌ))) |
214 | 213 | com13 88 |
. . . . . . . 8
β’ (π»:(0..^(β―βπ»))βΆdom πΌ β (π β (πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ β π»:(0..^(β―βπ»))βontoβdom πΌ))) |
215 | 17, 214 | syl 17 |
. . . . . . 7
β’ (π»(TrailsβπΊ)π β (π β (πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ β π»:(0..^(β―βπ»))βontoβdom πΌ))) |
216 | 215 | impcom 407 |
. . . . . 6
β’ ((π β§ π»(TrailsβπΊ)π) β (πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ β π»:(0..^(β―βπ»))βontoβdom πΌ)) |
217 | 13, 216 | mpd 15 |
. . . . 5
β’ ((π β§ π»(TrailsβπΊ)π) β π»:(0..^(β―βπ»))βontoβdom πΌ) |
218 | 9, 217 | jca 511 |
. . . 4
β’ ((π β§ π»(TrailsβπΊ)π) β (π»(TrailsβπΊ)π β§ π»:(0..^(β―βπ»))βontoβdom πΌ)) |
219 | 8, 218 | mpdan 684 |
. . 3
β’ (π β (π»(TrailsβπΊ)π β§ π»:(0..^(β―βπ»))βontoβdom πΌ)) |
220 | 2 | iseupth 29722 |
. . 3
β’ (π»(EulerPathsβπΊ)π β (π»(TrailsβπΊ)π β§ π»:(0..^(β―βπ»))βontoβdom πΌ)) |
221 | 219, 220 | sylibr 233 |
. 2
β’ (π β π»(EulerPathsβπΊ)π) |
222 | 1, 2, 3, 4, 5, 6, 7 | crctcsh 29346 |
. 2
β’ (π β π»(CircuitsβπΊ)π) |
223 | 221, 222 | jca 511 |
1
β’ (π β (π»(EulerPathsβπΊ)π β§ π»(CircuitsβπΊ)π)) |