This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem redivvald

Description: Value of real division, which is the (unique) real x such that ( B x. x ) = A . (Contributed by SN, 25-Nov-2025)

Ref Expression
Hypotheses redivvald.a 
|- ( ph -> A e. RR )
redivvald.b 
|- ( ph -> B e. RR )
redivvald.z 
|- ( ph -> B =/= 0 )
Assertion redivvald 
|- ( ph -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) )

Proof

Step Hyp Ref Expression
1 redivvald.a 
 |-  ( ph -> A e. RR )
2 redivvald.b 
 |-  ( ph -> B e. RR )
3 redivvald.z 
 |-  ( ph -> B =/= 0 )
4 2 3 eldifsnd 
 |-  ( ph -> B e. ( RR \ { 0 } ) )
5 eqeq2 
 |-  ( z = A -> ( ( y x. x ) = z <-> ( y x. x ) = A ) )
6 5 riotabidv 
 |-  ( z = A -> ( iota_ x e. RR ( y x. x ) = z ) = ( iota_ x e. RR ( y x. x ) = A ) )
7 oveq1 
 |-  ( y = B -> ( y x. x ) = ( B x. x ) )
8 7 eqeq1d 
 |-  ( y = B -> ( ( y x. x ) = A <-> ( B x. x ) = A ) )
9 8 riotabidv 
 |-  ( y = B -> ( iota_ x e. RR ( y x. x ) = A ) = ( iota_ x e. RR ( B x. x ) = A ) )
10 df-rediv 
 |-  /R = ( z e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ x e. RR ( y x. x ) = z ) )
11 riotaex 
 |-  ( iota_ x e. RR ( B x. x ) = A ) e. _V
12 6 9 10 11 ovmpo 
 |-  ( ( A e. RR /\ B e. ( RR \ { 0 } ) ) -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) )
13 1 4 12 syl2anc 
 |-  ( ph -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) )