Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  abvrec Structured version   Unicode version

Theorem abvrec 17805
 Description: The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.)
Hypotheses
Ref Expression
abv0.a AbsVal
abvneg.b
abvrec.z
abvrec.p
Assertion
Ref Expression
abvrec

Proof of Theorem abvrec
StepHypRef Expression
1 simplr 754 . . . 4
2 simprl 756 . . . 4
3 abv0.a . . . . 5 AbsVal
4 abvneg.b . . . . 5
53, 4abvcl 17793 . . . 4
61, 2, 5syl2anc 659 . . 3
76recnd 9652 . 2
8 simpll 752 . . . . 5
9 simprr 758 . . . . 5
10 abvrec.z . . . . . 6
11 abvrec.p . . . . . 6
124, 10, 11drnginvrcl 17733 . . . . 5
138, 2, 9, 12syl3anc 1230 . . . 4
143, 4abvcl 17793 . . . 4
151, 13, 14syl2anc 659 . . 3
1615recnd 9652 . 2
173, 4, 10abvne0 17796 . . 3
181, 2, 9, 17syl3anc 1230 . 2
19 eqid 2402 . . . . . 6
20 eqid 2402 . . . . . 6
214, 10, 19, 20, 11drnginvrr 17736 . . . . 5
228, 2, 9, 21syl3anc 1230 . . . 4
2322fveq2d 5853 . . 3
243, 4, 19abvmul 17798 . . . 4
251, 2, 13, 24syl3anc 1230 . . 3
263, 20abv1 17802 . . . 4