Metamath Proof Explorer


Theorem ofdivrec

Description: Function analogue of divrec , a division analogue of ofnegsub . (Contributed by Steve Rodriguez, 3-Nov-2015)

Ref Expression
Assertion ofdivrec AVF:AG:A0F×fA×1÷fG=F÷fG

Proof

Step Hyp Ref Expression
1 simp1 AVF:AG:A0AV
2 simp2 AVF:AG:A0F:A
3 2 ffnd AVF:AG:A0FFnA
4 ax-1cn 1
5 fnconstg 1A×1FnA
6 4 5 mp1i AVF:AG:A0A×1FnA
7 simp3 AVF:AG:A0G:A0
8 7 ffnd AVF:AG:A0GFnA
9 inidm AA=A
10 6 8 1 1 9 offn AVF:AG:A0A×1÷fGFnA
11 3 8 1 1 9 offn AVF:AG:A0F÷fGFnA
12 eqidd AVF:AG:A0xAFx=Fx
13 1cnd AVF:AG:A01
14 eqidd AVF:AG:A0xAGx=Gx
15 1 13 8 14 ofc1 AVF:AG:A0xAA×1÷fGx=1Gx
16 ffvelcdm F:AxAFx
17 2 16 sylan AVF:AG:A0xAFx
18 ffvelcdm G:A0xAGx0
19 eldifsn Gx0GxGx0
20 18 19 sylib G:A0xAGxGx0
21 7 20 sylan AVF:AG:A0xAGxGx0
22 divrec FxGxGx0FxGx=Fx1Gx
23 22 eqcomd FxGxGx0Fx1Gx=FxGx
24 23 3expb FxGxGx0Fx1Gx=FxGx
25 17 21 24 syl2anc AVF:AG:A0xAFx1Gx=FxGx
26 3 8 1 1 9 12 14 ofval AVF:AG:A0xAF÷fGx=FxGx
27 25 26 eqtr4d AVF:AG:A0xAFx1Gx=F÷fGx
28 1 3 10 11 12 15 27 offveq AVF:AG:A0F×fA×1÷fG=F÷fG