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

Metamath Proof Explorer

Theorem rediveud

Description: Existential uniqueness of real quotients. (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 rediveud 
|- ( ph -> E! 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 ax-rrecex 
 |-  ( ( B e. RR /\ B =/= 0 ) -> E. y e. RR ( B x. y ) = 1 )
5 2 3 4 syl2anc 
 |-  ( ph -> E. y e. RR ( B x. y ) = 1 )
6 oveq2 
 |-  ( x = ( y x. A ) -> ( B x. x ) = ( B x. ( y x. A ) ) )
7 6 eqeq1d 
 |-  ( x = ( y x. A ) -> ( ( B x. x ) = A <-> ( B x. ( y x. A ) ) = A ) )
8 simprl 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> y e. RR )
9 1 adantr 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> A e. RR )
10 8 9 remulcld 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> ( y x. A ) e. RR )
11 simprr 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> ( B x. y ) = 1 )
12 11 oveq1d 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> ( ( B x. y ) x. A ) = ( 1 x. A ) )
13 2 recnd 
 |-  ( ph -> B e. CC )
14 13 adantr 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> B e. CC )
15 8 recnd 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> y e. CC )
16 1 recnd 
 |-  ( ph -> A e. CC )
17 16 adantr 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> A e. CC )
18 14 15 17 mulassd 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> ( ( B x. y ) x. A ) = ( B x. ( y x. A ) ) )
19 remullid 
 |-  ( A e. RR -> ( 1 x. A ) = A )
20 1 19 syl 
 |-  ( ph -> ( 1 x. A ) = A )
21 20 adantr 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> ( 1 x. A ) = A )
22 12 18 21 3eqtr3d 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> ( B x. ( y x. A ) ) = A )
23 7 10 22 rspcedvdw 
 |-  ( ( ph /\ ( y e. RR /\ ( B x. y ) = 1 ) ) -> E. x e. RR ( B x. x ) = A )
24 5 23 rexlimddv 
 |-  ( ph -> E. x e. RR ( B x. x ) = A )
25 eqtr3 
 |-  ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> ( B x. x ) = ( B x. y ) )
26 simprl 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> x e. RR )
27 simprr 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> y e. RR )
28 2 adantr 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> B e. RR )
29 3 adantr 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> B =/= 0 )
30 26 27 28 29 remulcand 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( ( B x. x ) = ( B x. y ) <-> x = y ) )
31 25 30 imbitrid 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) )
32 31 ralrimivva 
 |-  ( ph -> A. x e. RR A. y e. RR ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) )
33 oveq2 
 |-  ( x = y -> ( B x. x ) = ( B x. y ) )
34 33 eqeq1d 
 |-  ( x = y -> ( ( B x. x ) = A <-> ( B x. y ) = A ) )
35 34 reu4 
 |-  ( E! x e. RR ( B x. x ) = A <-> ( E. x e. RR ( B x. x ) = A /\ A. x e. RR A. y e. RR ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) ) )
36 24 32 35 sylanbrc 
 |-  ( ph -> E! x e. RR ( B x. x ) = A )