Metamath Proof Explorer


Theorem efif1olem2

Description: Lemma for efif1o . (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Hypothesis efif1olem1.1 โŠข ๐ท = ( ๐ด (,] ( ๐ด + ( 2 ยท ฯ€ ) ) )
Assertion efif1olem2 ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ โˆƒ ๐‘ฆ โˆˆ ๐ท ( ( ๐‘ง โˆ’ ๐‘ฆ ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ค )

Proof

Step Hyp Ref Expression
1 efif1olem1.1 โŠข ๐ท = ( ๐ด (,] ( ๐ด + ( 2 ยท ฯ€ ) ) )
2 simpl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ๐ด โˆˆ โ„ )
3 2re โŠข 2 โˆˆ โ„
4 pire โŠข ฯ€ โˆˆ โ„
5 3 4 remulcli โŠข ( 2 ยท ฯ€ ) โˆˆ โ„
6 readdcl โŠข ( ( ๐ด โˆˆ โ„ โˆง ( 2 ยท ฯ€ ) โˆˆ โ„ ) โ†’ ( ๐ด + ( 2 ยท ฯ€ ) ) โˆˆ โ„ )
7 2 5 6 sylancl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐ด + ( 2 ยท ฯ€ ) ) โˆˆ โ„ )
8 resubcl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐ด โˆ’ ๐‘ง ) โˆˆ โ„ )
9 2pos โŠข 0 < 2
10 pipos โŠข 0 < ฯ€
11 3 4 9 10 mulgt0ii โŠข 0 < ( 2 ยท ฯ€ )
12 5 11 elrpii โŠข ( 2 ยท ฯ€ ) โˆˆ โ„+
13 modcl โŠข ( ( ( ๐ด โˆ’ ๐‘ง ) โˆˆ โ„ โˆง ( 2 ยท ฯ€ ) โˆˆ โ„+ ) โ†’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) โˆˆ โ„ )
14 8 12 13 sylancl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) โˆˆ โ„ )
15 7 14 resubcld โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆˆ โ„ )
16 5 a1i โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( 2 ยท ฯ€ ) โˆˆ โ„ )
17 modlt โŠข ( ( ( ๐ด โˆ’ ๐‘ง ) โˆˆ โ„ โˆง ( 2 ยท ฯ€ ) โˆˆ โ„+ ) โ†’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) < ( 2 ยท ฯ€ ) )
18 8 12 17 sylancl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) < ( 2 ยท ฯ€ ) )
19 14 16 2 18 ltadd2dd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐ด + ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) < ( ๐ด + ( 2 ยท ฯ€ ) ) )
20 2 14 7 ltaddsubd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) < ( ๐ด + ( 2 ยท ฯ€ ) ) โ†” ๐ด < ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) )
21 19 20 mpbid โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ๐ด < ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) )
22 modge0 โŠข ( ( ( ๐ด โˆ’ ๐‘ง ) โˆˆ โ„ โˆง ( 2 ยท ฯ€ ) โˆˆ โ„+ ) โ†’ 0 โ‰ค ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) )
23 8 12 22 sylancl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ 0 โ‰ค ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) )
24 7 14 subge02d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( 0 โ‰ค ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) โ†” ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โ‰ค ( ๐ด + ( 2 ยท ฯ€ ) ) ) )
25 23 24 mpbid โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โ‰ค ( ๐ด + ( 2 ยท ฯ€ ) ) )
26 rexr โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„* )
27 elioc2 โŠข ( ( ๐ด โˆˆ โ„* โˆง ( ๐ด + ( 2 ยท ฯ€ ) ) โˆˆ โ„ ) โ†’ ( ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆˆ ( ๐ด (,] ( ๐ด + ( 2 ยท ฯ€ ) ) ) โ†” ( ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆˆ โ„ โˆง ๐ด < ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆง ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โ‰ค ( ๐ด + ( 2 ยท ฯ€ ) ) ) ) )
28 26 7 27 syl2an2r โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆˆ ( ๐ด (,] ( ๐ด + ( 2 ยท ฯ€ ) ) ) โ†” ( ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆˆ โ„ โˆง ๐ด < ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆง ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โ‰ค ( ๐ด + ( 2 ยท ฯ€ ) ) ) ) )
29 15 21 25 28 mpbir3and โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆˆ ( ๐ด (,] ( ๐ด + ( 2 ยท ฯ€ ) ) ) )
30 29 1 eleqtrrdi โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆˆ ๐ท )
31 modval โŠข ( ( ( ๐ด โˆ’ ๐‘ง ) โˆˆ โ„ โˆง ( 2 ยท ฯ€ ) โˆˆ โ„+ ) โ†’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) = ( ( ๐ด โˆ’ ๐‘ง ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
32 8 12 31 sylancl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) = ( ( ๐ด โˆ’ ๐‘ง ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
33 32 oveq2d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) = ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) ) )
34 7 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐ด + ( 2 ยท ฯ€ ) ) โˆˆ โ„‚ )
35 8 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐ด โˆ’ ๐‘ง ) โˆˆ โ„‚ )
36 5 11 gt0ne0ii โŠข ( 2 ยท ฯ€ ) โ‰  0
37 redivcl โŠข ( ( ( ๐ด โˆ’ ๐‘ง ) โˆˆ โ„ โˆง ( 2 ยท ฯ€ ) โˆˆ โ„ โˆง ( 2 ยท ฯ€ ) โ‰  0 ) โ†’ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ )
38 5 36 37 mp3an23 โŠข ( ( ๐ด โˆ’ ๐‘ง ) โˆˆ โ„ โ†’ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ )
39 8 38 syl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ )
40 39 flcld โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) โˆˆ โ„ค )
41 40 zred โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) โˆˆ โ„ )
42 remulcl โŠข ( ( ( 2 ยท ฯ€ ) โˆˆ โ„ โˆง ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) โˆˆ โ„ ) โ†’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) โˆˆ โ„ )
43 5 41 42 sylancr โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) โˆˆ โ„ )
44 43 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) โˆˆ โ„‚ )
45 34 35 44 subsubd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) ) = ( ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ๐ด โˆ’ ๐‘ง ) ) + ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
46 2 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ๐ด โˆˆ โ„‚ )
47 5 recni โŠข ( 2 ยท ฯ€ ) โˆˆ โ„‚
48 47 a1i โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( 2 ยท ฯ€ ) โˆˆ โ„‚ )
49 simpr โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ๐‘ง โˆˆ โ„ )
50 49 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ๐‘ง โˆˆ โ„‚ )
51 46 48 50 pnncand โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ๐ด โˆ’ ๐‘ง ) ) = ( ( 2 ยท ฯ€ ) + ๐‘ง ) )
52 51 oveq1d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ๐ด โˆ’ ๐‘ง ) ) + ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) = ( ( ( 2 ยท ฯ€ ) + ๐‘ง ) + ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
53 33 45 52 3eqtrd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) = ( ( ( 2 ยท ฯ€ ) + ๐‘ง ) + ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
54 53 oveq2d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) = ( ๐‘ง โˆ’ ( ( ( 2 ยท ฯ€ ) + ๐‘ง ) + ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) ) )
55 addcl โŠข ( ( ( 2 ยท ฯ€ ) โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ ) โ†’ ( ( 2 ยท ฯ€ ) + ๐‘ง ) โˆˆ โ„‚ )
56 47 50 55 sylancr โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( 2 ยท ฯ€ ) + ๐‘ง ) โˆˆ โ„‚ )
57 50 56 44 subsub4d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐‘ง โˆ’ ( ( 2 ยท ฯ€ ) + ๐‘ง ) ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) = ( ๐‘ง โˆ’ ( ( ( 2 ยท ฯ€ ) + ๐‘ง ) + ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) ) )
58 56 50 negsubdi2d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ - ( ( ( 2 ยท ฯ€ ) + ๐‘ง ) โˆ’ ๐‘ง ) = ( ๐‘ง โˆ’ ( ( 2 ยท ฯ€ ) + ๐‘ง ) ) )
59 48 50 pncand โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ( 2 ยท ฯ€ ) + ๐‘ง ) โˆ’ ๐‘ง ) = ( 2 ยท ฯ€ ) )
60 59 negeqd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ - ( ( ( 2 ยท ฯ€ ) + ๐‘ง ) โˆ’ ๐‘ง ) = - ( 2 ยท ฯ€ ) )
61 58 60 eqtr3d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐‘ง โˆ’ ( ( 2 ยท ฯ€ ) + ๐‘ง ) ) = - ( 2 ยท ฯ€ ) )
62 neg1cn โŠข - 1 โˆˆ โ„‚
63 47 mulm1i โŠข ( - 1 ยท ( 2 ยท ฯ€ ) ) = - ( 2 ยท ฯ€ )
64 62 47 63 mulcomli โŠข ( ( 2 ยท ฯ€ ) ยท - 1 ) = - ( 2 ยท ฯ€ )
65 61 64 eqtr4di โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐‘ง โˆ’ ( ( 2 ยท ฯ€ ) + ๐‘ง ) ) = ( ( 2 ยท ฯ€ ) ยท - 1 ) )
66 65 oveq1d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐‘ง โˆ’ ( ( 2 ยท ฯ€ ) + ๐‘ง ) ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) = ( ( ( 2 ยท ฯ€ ) ยท - 1 ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
67 62 a1i โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ - 1 โˆˆ โ„‚ )
68 40 zcnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) โˆˆ โ„‚ )
69 48 67 68 subdid โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( 2 ยท ฯ€ ) ยท ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) = ( ( ( 2 ยท ฯ€ ) ยท - 1 ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
70 66 69 eqtr4d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐‘ง โˆ’ ( ( 2 ยท ฯ€ ) + ๐‘ง ) ) โˆ’ ( ( 2 ยท ฯ€ ) ยท ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) = ( ( 2 ยท ฯ€ ) ยท ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
71 54 57 70 3eqtr2d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) = ( ( 2 ยท ฯ€ ) ยท ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) )
72 71 oveq1d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) / ( 2 ยท ฯ€ ) ) = ( ( ( 2 ยท ฯ€ ) ยท ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) / ( 2 ยท ฯ€ ) ) )
73 neg1z โŠข - 1 โˆˆ โ„ค
74 zsubcl โŠข ( ( - 1 โˆˆ โ„ค โˆง ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) โˆˆ โ„ค ) โ†’ ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) โˆˆ โ„ค )
75 73 40 74 sylancr โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) โˆˆ โ„ค )
76 75 zcnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) โˆˆ โ„‚ )
77 divcan3 โŠข ( ( ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) โˆˆ โ„‚ โˆง ( 2 ยท ฯ€ ) โˆˆ โ„‚ โˆง ( 2 ยท ฯ€ ) โ‰  0 ) โ†’ ( ( ( 2 ยท ฯ€ ) ยท ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) / ( 2 ยท ฯ€ ) ) = ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) )
78 47 36 77 mp3an23 โŠข ( ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) โˆˆ โ„‚ โ†’ ( ( ( 2 ยท ฯ€ ) ยท ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) / ( 2 ยท ฯ€ ) ) = ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) )
79 76 78 syl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ( 2 ยท ฯ€ ) ยท ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) ) / ( 2 ยท ฯ€ ) ) = ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) )
80 72 79 eqtrd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) / ( 2 ยท ฯ€ ) ) = ( - 1 โˆ’ ( โŒŠ โ€˜ ( ( ๐ด โˆ’ ๐‘ง ) / ( 2 ยท ฯ€ ) ) ) ) )
81 80 75 eqeltrd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ ( ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ค )
82 oveq2 โŠข ( ๐‘ฆ = ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โ†’ ( ๐‘ง โˆ’ ๐‘ฆ ) = ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) )
83 82 oveq1d โŠข ( ๐‘ฆ = ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โ†’ ( ( ๐‘ง โˆ’ ๐‘ฆ ) / ( 2 ยท ฯ€ ) ) = ( ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) / ( 2 ยท ฯ€ ) ) )
84 83 eleq1d โŠข ( ๐‘ฆ = ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โ†’ ( ( ( ๐‘ง โˆ’ ๐‘ฆ ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ค โ†” ( ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ค ) )
85 84 rspcev โŠข ( ( ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) โˆˆ ๐ท โˆง ( ( ๐‘ง โˆ’ ( ( ๐ด + ( 2 ยท ฯ€ ) ) โˆ’ ( ( ๐ด โˆ’ ๐‘ง ) mod ( 2 ยท ฯ€ ) ) ) ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ค ) โ†’ โˆƒ ๐‘ฆ โˆˆ ๐ท ( ( ๐‘ง โˆ’ ๐‘ฆ ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ค )
86 30 81 85 syl2anc โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐‘ง โˆˆ โ„ ) โ†’ โˆƒ ๐‘ฆ โˆˆ ๐ท ( ( ๐‘ง โˆ’ ๐‘ฆ ) / ( 2 ยท ฯ€ ) ) โˆˆ โ„ค )