Metamath Proof Explorer

Theorem m1expaddsub

Description: Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion m1expaddsub ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ( ๐‘‹ โˆ’ ๐‘Œ ) ) = ( - 1 โ†‘ ( ๐‘‹ + ๐‘Œ ) ) )

Proof

Step Hyp Ref Expression
1 m1expcl โŠข ( ๐‘‹ โˆˆ โ„ค โ†’ ( - 1 โ†‘ ๐‘‹ ) โˆˆ โ„ค )
2 1 zcnd โŠข ( ๐‘‹ โˆˆ โ„ค โ†’ ( - 1 โ†‘ ๐‘‹ ) โˆˆ โ„‚ )
3 2 adantr โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ๐‘‹ ) โˆˆ โ„‚ )
4 m1expcl โŠข ( ๐‘Œ โˆˆ โ„ค โ†’ ( - 1 โ†‘ ๐‘Œ ) โˆˆ โ„ค )
5 4 zcnd โŠข ( ๐‘Œ โˆˆ โ„ค โ†’ ( - 1 โ†‘ ๐‘Œ ) โˆˆ โ„‚ )
6 5 adantl โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ๐‘Œ ) โˆˆ โ„‚ )
7 neg1cn โŠข - 1 โˆˆ โ„‚
8 neg1ne0 โŠข - 1 โ‰  0
9 expne0i โŠข ( ( - 1 โˆˆ โ„‚ โˆง - 1 โ‰  0 โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ๐‘Œ ) โ‰  0 )
10 7 8 9 mp3an12 โŠข ( ๐‘Œ โˆˆ โ„ค โ†’ ( - 1 โ†‘ ๐‘Œ ) โ‰  0 )
11 10 adantl โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ๐‘Œ ) โ‰  0 )
12 3 6 11 divrecd โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( ( - 1 โ†‘ ๐‘‹ ) / ( - 1 โ†‘ ๐‘Œ ) ) = ( ( - 1 โ†‘ ๐‘‹ ) ยท ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) ) )
13 m1expcl2 โŠข ( ๐‘Œ โˆˆ โ„ค โ†’ ( - 1 โ†‘ ๐‘Œ ) โˆˆ { - 1 , 1 } )
14 elpri โŠข ( ( - 1 โ†‘ ๐‘Œ ) โˆˆ { - 1 , 1 } โ†’ ( ( - 1 โ†‘ ๐‘Œ ) = - 1 โˆจ ( - 1 โ†‘ ๐‘Œ ) = 1 ) )
15 ax-1cn โŠข 1 โˆˆ โ„‚
16 ax-1ne0 โŠข 1 โ‰  0
17 divneg2 โŠข ( ( 1 โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง 1 โ‰  0 ) โ†’ - ( 1 / 1 ) = ( 1 / - 1 ) )
18 15 15 16 17 mp3an โŠข - ( 1 / 1 ) = ( 1 / - 1 )
19 1div1e1 โŠข ( 1 / 1 ) = 1
20 19 negeqi โŠข - ( 1 / 1 ) = - 1
21 18 20 eqtr3i โŠข ( 1 / - 1 ) = - 1
22 oveq2 โŠข ( ( - 1 โ†‘ ๐‘Œ ) = - 1 โ†’ ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) = ( 1 / - 1 ) )
23 id โŠข ( ( - 1 โ†‘ ๐‘Œ ) = - 1 โ†’ ( - 1 โ†‘ ๐‘Œ ) = - 1 )
24 21 22 23 3eqtr4a โŠข ( ( - 1 โ†‘ ๐‘Œ ) = - 1 โ†’ ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) = ( - 1 โ†‘ ๐‘Œ ) )
25 oveq2 โŠข ( ( - 1 โ†‘ ๐‘Œ ) = 1 โ†’ ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) = ( 1 / 1 ) )
26 id โŠข ( ( - 1 โ†‘ ๐‘Œ ) = 1 โ†’ ( - 1 โ†‘ ๐‘Œ ) = 1 )
27 19 25 26 3eqtr4a โŠข ( ( - 1 โ†‘ ๐‘Œ ) = 1 โ†’ ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) = ( - 1 โ†‘ ๐‘Œ ) )
28 24 27 jaoi โŠข ( ( ( - 1 โ†‘ ๐‘Œ ) = - 1 โˆจ ( - 1 โ†‘ ๐‘Œ ) = 1 ) โ†’ ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) = ( - 1 โ†‘ ๐‘Œ ) )
29 13 14 28 3syl โŠข ( ๐‘Œ โˆˆ โ„ค โ†’ ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) = ( - 1 โ†‘ ๐‘Œ ) )
30 29 adantl โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) = ( - 1 โ†‘ ๐‘Œ ) )
31 30 oveq2d โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( ( - 1 โ†‘ ๐‘‹ ) ยท ( 1 / ( - 1 โ†‘ ๐‘Œ ) ) ) = ( ( - 1 โ†‘ ๐‘‹ ) ยท ( - 1 โ†‘ ๐‘Œ ) ) )
32 12 31 eqtrd โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( ( - 1 โ†‘ ๐‘‹ ) / ( - 1 โ†‘ ๐‘Œ ) ) = ( ( - 1 โ†‘ ๐‘‹ ) ยท ( - 1 โ†‘ ๐‘Œ ) ) )
33 expsub โŠข ( ( ( - 1 โˆˆ โ„‚ โˆง - 1 โ‰  0 ) โˆง ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) ) โ†’ ( - 1 โ†‘ ( ๐‘‹ โˆ’ ๐‘Œ ) ) = ( ( - 1 โ†‘ ๐‘‹ ) / ( - 1 โ†‘ ๐‘Œ ) ) )
34 7 8 33 mpanl12 โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ( ๐‘‹ โˆ’ ๐‘Œ ) ) = ( ( - 1 โ†‘ ๐‘‹ ) / ( - 1 โ†‘ ๐‘Œ ) ) )
35 expaddz โŠข ( ( ( - 1 โˆˆ โ„‚ โˆง - 1 โ‰  0 ) โˆง ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) ) โ†’ ( - 1 โ†‘ ( ๐‘‹ + ๐‘Œ ) ) = ( ( - 1 โ†‘ ๐‘‹ ) ยท ( - 1 โ†‘ ๐‘Œ ) ) )
36 7 8 35 mpanl12 โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ( ๐‘‹ + ๐‘Œ ) ) = ( ( - 1 โ†‘ ๐‘‹ ) ยท ( - 1 โ†‘ ๐‘Œ ) ) )
37 32 34 36 3eqtr4d โŠข ( ( ๐‘‹ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ( ๐‘‹ โˆ’ ๐‘Œ ) ) = ( - 1 โ†‘ ( ๐‘‹ + ๐‘Œ ) ) )