ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  recexre Unicode version
Theorem recexre 8906
Description: Existence of reciprocal of real number. (Contributed by Jim Kingdon, 29-Jan-2020.)
Assertion
Ref Expression
recexre |- ( ( A e. RR /\ A #ℝ 0 ) -> E. x e. RR ( A x. x ) = 1 )
Distinct variable group:   x, A
Proof of Theorem recexre
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 0re 8326 . . . 4 |- 0 e. RR
2 reapval 8904 . . . 4 |- ( ( A e. RR /\ 0 e. RR ) -> ( A #ℝ 0 <-> ( A < 0 \/ 0 < A ) ) )
31, 2mpan2 429 . . 3 |- ( A e. RR -> ( A #ℝ 0 <-> ( A < 0 \/ 0 < A ) ) )
4 lt0neg1 8796 . . . . . . . . . 10 |- ( A e. RR -> ( A < 0 <-> 0 < -u A ) )
5 renegcl 8587 . . . . . . . . . . 11 |- ( A e. RR -> -u A e. RR )
6 ltxrlt 8391 . . . . . . . . . . 11 |- ( ( 0 e. RR /\ -u A e. RR ) -> ( 0 < -u A <-> 0 <RR -u A ) )
71, 5, 6sylancr 418 . . . . . . . . . 10 |- ( A e. RR -> ( 0 < -u A <-> 0 <RR -u A ) )
84, 7bitrd 188 . . . . . . . . 9 |- ( A e. RR -> ( A < 0 <-> 0 <RR -u A ) )
98pm5.32i 458 . . . . . . . 8 |- ( ( A e. RR /\ A < 0 ) <-> ( A e. RR /\ 0 <RR -u A ) )
10 ax-precex 8289 . . . . . . . . . 10 |- ( ( -u A e. RR /\ 0 <RR -u A ) -> E. y e. RR ( 0 <RR y /\ ( -u A x. y ) = 1 ) )
11 simpr 110 . . . . . . . . . . 11 |- ( ( 0 <RR y /\ ( -u A x. y ) = 1 ) -> ( -u A x. y ) = 1 )
1211reximi 2647 . . . . . . . . . 10 |- ( E. y e. RR ( 0 <RR y /\ ( -u A x. y ) = 1 ) -> E. y e. RR ( -u A x. y ) = 1 )
1310, 12syl 14 . . . . . . . . 9 |- ( ( -u A e. RR /\ 0 <RR -u A ) -> E. y e. RR ( -u A x. y ) = 1 )
145, 13sylan 283 . . . . . . . 8 |- ( ( A e. RR /\ 0 <RR -u A ) -> E. y e. RR ( -u A x. y ) = 1 )
159, 14sylbi 121 . . . . . . 7 |- ( ( A e. RR /\ A < 0 ) -> E. y e. RR ( -u A x. y ) = 1 )
16 recn 8312 . . . . . . . . . . . . 13 |- ( y e. RR -> y e. CC )
1716negnegd 8628 . . . . . . . . . . . 12 |- ( y e. RR -> -u -u y = y )
1817oveq2d 6101 . . . . . . . . . . 11 |- ( y e. RR -> ( -u A x. -u -u y ) = ( -u A x. y ) )
1918eqeq1d 2247 . . . . . . . . . 10 |- ( y e. RR -> ( ( -u A x. -u -u y ) = 1 <-> ( -u A x. y ) = 1 ) )
2019pm5.32i 458 . . . . . . . . 9 |- ( ( y e. RR /\ ( -u A x. -u -u y ) = 1 ) <-> ( y e. RR /\ ( -u A x. y ) = 1 ) )
21 renegcl 8587 . . . . . . . . . 10 |- ( y e. RR -> -u y e. RR )
22 negeq 8519 . . . . . . . . . . . . 13 |- ( x = -u y -> -u x = -u -u y )
2322oveq2d 6101 . . . . . . . . . . . 12 |- ( x = -u y -> ( -u A x. -u x ) = ( -u A x. -u -u y ) )
2423eqeq1d 2247 . . . . . . . . . . 11 |- ( x = -u y -> ( ( -u A x. -u x ) = 1 <-> ( -u A x. -u -u y ) = 1 ) )
2524rspcev 2929 . . . . . . . . . 10 |- ( ( -u y e. RR /\ ( -u A x. -u -u y ) = 1 ) -> E. x e. RR ( -u A x. -u x ) = 1 )
2621, 25sylan 283 . . . . . . . . 9 |- ( ( y e. RR /\ ( -u A x. -u -u y ) = 1 ) -> E. x e. RR ( -u A x. -u x ) = 1 )
2720, 26sylbir 135 . . . . . . . 8 |- ( ( y e. RR /\ ( -u A x. y ) = 1 ) -> E. x e. RR ( -u A x. -u x ) = 1 )
2827adantl 277 . . . . . . 7 |- ( ( ( A e. RR /\ A < 0 ) /\ ( y e. RR /\ ( -u A x. y ) = 1 ) ) -> E. x e. RR ( -u A x. -u x ) = 1 )
2915, 28rexlimddv 2673 . . . . . 6 |- ( ( A e. RR /\ A < 0 ) -> E. x e. RR ( -u A x. -u x ) = 1 )
30 recn 8312 . . . . . . . . . 10 |- ( A e. RR -> A e. CC )
31 recn 8312 . . . . . . . . . 10 |- ( x e. RR -> x e. CC )
32 mul2neg 8725 . . . . . . . . . 10 |- ( ( A e. CC /\ x e. CC ) -> ( -u A x. -u x ) = ( A x. x ) )
3330, 31, 32syl2an 289 . . . . . . . . 9 |- ( ( A e. RR /\ x e. RR ) -> ( -u A x. -u x ) = ( A x. x ) )
3433eqeq1d 2247 . . . . . . . 8 |- ( ( A e. RR /\ x e. RR ) -> ( ( -u A x. -u x ) = 1 <-> ( A x. x ) = 1 ) )
3534rexbidva 2547 . . . . . . 7 |- ( A e. RR -> ( E. x e. RR ( -u A x. -u x ) = 1 <-> E. x e. RR ( A x. x ) = 1 ) )
3635adantr 276 . . . . . 6 |- ( ( A e. RR /\ A < 0 ) -> ( E. x e. RR ( -u A x. -u x ) = 1 <-> E. x e. RR ( A x. x ) = 1 ) )
3729, 36mpbid 147 . . . . 5 |- ( ( A e. RR /\ A < 0 ) -> E. x e. RR ( A x. x ) = 1 )
3837ex 115 . . . 4 |- ( A e. RR -> ( A < 0 -> E. x e. RR ( A x. x ) = 1 ) )
39 ltxrlt 8391 . . . . . . . 8 |- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A <-> 0 <RR A ) )
401, 39mpan 428 . . . . . . 7 |- ( A e. RR -> ( 0 < A <-> 0 <RR A ) )
4140pm5.32i 458 . . . . . 6 |- ( ( A e. RR /\ 0 < A ) <-> ( A e. RR /\ 0 <RR A ) )
42 ax-precex 8289 . . . . . . 7 |- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
43 simpr 110 . . . . . . . 8 |- ( ( 0 <RR x /\ ( A x. x ) = 1 ) -> ( A x. x ) = 1 )
4443reximi 2647 . . . . . . 7 |- ( E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) -> E. x e. RR ( A x. x ) = 1 )
4542, 44syl 14 . . . . . 6 |- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( A x. x ) = 1 )
4641, 45sylbi 121 . . . . 5 |- ( ( A e. RR /\ 0 < A ) -> E. x e. RR ( A x. x ) = 1 )
4746ex 115 . . . 4 |- ( A e. RR -> ( 0 < A -> E. x e. RR ( A x. x ) = 1 ) )
4838, 47jaod 729 . . 3 |- ( A e. RR -> ( ( A < 0 \/ 0 < A ) -> E. x e. RR ( A x. x ) = 1 ) )
493, 48sylbid 150 . 2 |- ( A e. RR -> ( A #ℝ 0 -> E. x e. RR ( A x. x ) = 1 ) )
5049imp 124 1 |- ( ( A e. RR /\ A #ℝ 0 ) -> E. x e. RR ( A x. x ) = 1 )
Colors of variables:    wff set class
This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720   = wceq 1402   e. wcel 2209   E.wrex 2529   class class class wbr 4130  (class class class)co 6085   CCcc 8177   RRcr 8178   0cc0 8179   1c1 8180   <RR cltrr 8183   x. cmul 8184   < clt 8360   -ucneg 8498   #ℝ creap 8902
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-addcom 8279  ax-mulcom 8280  ax-addass 8281  ax-distr 8283  ax-i2m1 8284  ax-0id 8287  ax-rnegex 8288  ax-precex 8289  ax-cnre 8290  ax-pre-ltadd 8295
This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-pnf 8362  df-mnf 8363  df-ltxr 8365  df-sub 8499  df-neg 8500  df-reap 8903
This theorem is used by:  rimul  8913  recexap  8981  rerecclap  9060
  Copyright terms: Public domain W3C validator