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

Metamath Proof Explorer

Theorem recexsrlem

Description: The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 15-May-1996) (New usage is discouraged.)

Ref Expression
Assertion recexsrlem ( 0R <R 𝐴 → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )

Proof

Step Hyp Ref Expression
1 ltrelsr ⊢ <R ⊆ ( R × R )
2 1 brel ⊢ ( 0R <R 𝐴 → ( 0R ∈ R ∧ 𝐴 ∈ R ) )
3 2 simprd ⊢ ( 0R <R 𝐴 → 𝐴 ∈ R )
4 df-nr ⊢ R = ( ( P × P ) / ~R )
5 breq2 ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ 0R <R 𝐴 ) )
6 oveq1 ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = ( 𝐴 ·R 𝑥 ) )
7 6 eqeq1d ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ↔ ( 𝐴 ·R 𝑥 ) = 1R ) )
8 7 rexbidv ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ↔ ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R ) )
9 5 8 imbi12d ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) ↔ ( 0R <R 𝐴 → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R ) ) )
10 gt0srpr ⊢ ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ 𝑧 <P 𝑦 )
11 ltexpri ⊢ ( 𝑧 <P 𝑦 → ∃ 𝑤 ∈ P ( 𝑧 +P 𝑤 ) = 𝑦 )
12 10 11 sylbi ⊢ ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑤 ∈ P ( 𝑧 +P 𝑤 ) = 𝑦 )
13 recexpr ⊢ ( 𝑤 ∈ P → ∃ 𝑣 ∈ P ( 𝑤 ·P 𝑣 ) = 1P )
14 1pr ⊢ 1P ∈ P
15 addclpr ⊢ ( ( 𝑣 ∈ P ∧ 1P ∈ P ) → ( 𝑣 +P 1P ) ∈ P )
16 14 15 mpan2 ⊢ ( 𝑣 ∈ P → ( 𝑣 +P 1P ) ∈ P )
17 enrex ⊢ ~R ∈ V
18 17 4 ecopqsi ⊢ ( ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) → [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ∈ R )
19 16 14 18 sylancl ⊢ ( 𝑣 ∈ P → [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ∈ R )
20 19 ad2antlr ⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ∈ R )
21 16 14 jctir ⊢ ( 𝑣 ∈ P → ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) )
22 21 anim2i ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) ) )
23 22 adantr ⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) ) )
24 mulsrpr ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R )
25 23 24 syl ⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R )
26 oveq1 ⊢ ( ( 𝑧 +P 𝑤 ) = 𝑦 → ( ( 𝑧 +P 𝑤 ) ·P 𝑣 ) = ( 𝑦 ·P 𝑣 ) )
27 26 eqcomd ⊢ ( ( 𝑧 +P 𝑤 ) = 𝑦 → ( 𝑦 ·P 𝑣 ) = ( ( 𝑧 +P 𝑤 ) ·P 𝑣 ) )
28 vex ⊢ 𝑧 ∈ V
29 vex ⊢ 𝑤 ∈ V
30 vex ⊢ 𝑣 ∈ V
31 mulcompr ⊢ ( 𝑢 ·P 𝑓 ) = ( 𝑓 ·P 𝑢 )
32 distrpr ⊢ ( 𝑢 ·P ( 𝑓 +P 𝑥 ) ) = ( ( 𝑢 ·P 𝑓 ) +P ( 𝑢 ·P 𝑥 ) )
33 28 29 30 31 32 caovdir ⊢ ( ( 𝑧 +P 𝑤 ) ·P 𝑣 ) = ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑣 ) )
34 oveq2 ⊢ ( ( 𝑤 ·P 𝑣 ) = 1P → ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑣 ) ) = ( ( 𝑧 ·P 𝑣 ) +P 1P ) )
35 33 34 eqtrid ⊢ ( ( 𝑤 ·P 𝑣 ) = 1P → ( ( 𝑧 +P 𝑤 ) ·P 𝑣 ) = ( ( 𝑧 ·P 𝑣 ) +P 1P ) )
36 27 35 sylan9eqr ⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( 𝑦 ·P 𝑣 ) = ( ( 𝑧 ·P 𝑣 ) +P 1P ) )
37 36 oveq1d ⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) = ( ( ( 𝑧 ·P 𝑣 ) +P 1P ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) )
38 ovex ⊢ ( 𝑧 ·P 𝑣 ) ∈ V
39 14 elexi ⊢ 1P ∈ V
40 ovex ⊢ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ∈ V
41 addcompr ⊢ ( 𝑢 +P 𝑓 ) = ( 𝑓 +P 𝑢 )
42 addasspr ⊢ ( ( 𝑢 +P 𝑓 ) +P 𝑥 ) = ( 𝑢 +P ( 𝑓 +P 𝑥 ) )
43 38 39 40 41 42 caov32 ⊢ ( ( ( 𝑧 ·P 𝑣 ) +P 1P ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P )
44 37 43 eqtrdi ⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) )
45 44 oveq1d ⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) = ( ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) +P 1P ) )
46 addasspr ⊢ ( ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) +P 1P ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P ( 1P +P 1P ) )
47 45 46 eqtrdi ⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P ( 1P +P 1P ) ) )
48 distrpr ⊢ ( 𝑦 ·P ( 𝑣 +P 1P ) ) = ( ( 𝑦 ·P 𝑣 ) +P ( 𝑦 ·P 1P ) )
49 48 oveq1i ⊢ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) = ( ( ( 𝑦 ·P 𝑣 ) +P ( 𝑦 ·P 1P ) ) +P ( 𝑧 ·P 1P ) )
50 addasspr ⊢ ( ( ( 𝑦 ·P 𝑣 ) +P ( 𝑦 ·P 1P ) ) +P ( 𝑧 ·P 1P ) ) = ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) )
51 49 50 eqtri ⊢ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) = ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) )
52 51 oveq1i ⊢ ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) +P 1P ) = ( ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P )
53 distrpr ⊢ ( 𝑧 ·P ( 𝑣 +P 1P ) ) = ( ( 𝑧 ·P 𝑣 ) +P ( 𝑧 ·P 1P ) )
54 53 oveq2i ⊢ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) = ( ( 𝑦 ·P 1P ) +P ( ( 𝑧 ·P 𝑣 ) +P ( 𝑧 ·P 1P ) ) )
55 ovex ⊢ ( 𝑦 ·P 1P ) ∈ V
56 ovex ⊢ ( 𝑧 ·P 1P ) ∈ V
57 55 38 56 41 42 caov12 ⊢ ( ( 𝑦 ·P 1P ) +P ( ( 𝑧 ·P 𝑣 ) +P ( 𝑧 ·P 1P ) ) ) = ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) )
58 54 57 eqtri ⊢ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) = ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) )
59 58 oveq1i ⊢ ( ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) +P ( 1P +P 1P ) ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P ( 1P +P 1P ) )
60 47 52 59 3eqtr4g ⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) +P 1P ) = ( ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) +P ( 1P +P 1P ) ) )
61 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ ( 𝑣 +P 1P ) ∈ P ) → ( 𝑦 ·P ( 𝑣 +P 1P ) ) ∈ P )
62 16 61 sylan2 ⊢ ( ( 𝑦 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑦 ·P ( 𝑣 +P 1P ) ) ∈ P )
63 mulclpr ⊢ ( ( 𝑧 ∈ P ∧ 1P ∈ P ) → ( 𝑧 ·P 1P ) ∈ P )
64 14 63 mpan2 ⊢ ( 𝑧 ∈ P → ( 𝑧 ·P 1P ) ∈ P )
65 addclpr ⊢ ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) ∈ P ∧ ( 𝑧 ·P 1P ) ∈ P ) → ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P )
66 62 64 65 syl2an ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑣 ∈ P ) ∧ 𝑧 ∈ P ) → ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P )
67 66 an32s ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P )
68 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 1P ∈ P ) → ( 𝑦 ·P 1P ) ∈ P )
69 14 68 mpan2 ⊢ ( 𝑦 ∈ P → ( 𝑦 ·P 1P ) ∈ P )
70 mulclpr ⊢ ( ( 𝑧 ∈ P ∧ ( 𝑣 +P 1P ) ∈ P ) → ( 𝑧 ·P ( 𝑣 +P 1P ) ) ∈ P )
71 16 70 sylan2 ⊢ ( ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑧 ·P ( 𝑣 +P 1P ) ) ∈ P )
72 addclpr ⊢ ( ( ( 𝑦 ·P 1P ) ∈ P ∧ ( 𝑧 ·P ( 𝑣 +P 1P ) ) ∈ P ) → ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P )
73 69 71 72 syl2an ⊢ ( ( 𝑦 ∈ P ∧ ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) ) → ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P )
74 73 anassrs ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P )
75 67 74 jca ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P ∧ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P ) )
76 addclpr ⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) ∈ P )
77 14 14 76 mp2an ⊢ ( 1P +P 1P ) ∈ P
78 77 14 pm3.2i ⊢ ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P )
79 enreceq ⊢ ( ( ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P ∧ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P ) ∧ ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ↔ ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) +P 1P ) = ( ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) +P ( 1P +P 1P ) ) ) )
80 75 78 79 sylancl ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ↔ ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) +P 1P ) = ( ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) +P ( 1P +P 1P ) ) ) )
81 60 80 imbitrrid ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ) )
82 81 imp ⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R )
83 25 82 eqtrd ⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R )
84 df-1r ⊢ 1R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R
85 83 84 eqtr4di ⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = 1R )
86 oveq2 ⊢ ( 𝑥 = [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) )
87 86 eqeq1d ⊢ ( 𝑥 = [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R → ( ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ↔ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = 1R ) )
88 87 rspcev ⊢ ( ( [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ∈ R ∧ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = 1R ) → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R )
89 20 85 88 syl2anc ⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R )
90 89 exp43 ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑣 ∈ P → ( ( 𝑤 ·P 𝑣 ) = 1P → ( ( 𝑧 +P 𝑤 ) = 𝑦 → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) ) ) )
91 90 rexlimdv ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ∃ 𝑣 ∈ P ( 𝑤 ·P 𝑣 ) = 1P → ( ( 𝑧 +P 𝑤 ) = 𝑦 → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) ) )
92 13 91 syl5 ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑤 ∈ P → ( ( 𝑧 +P 𝑤 ) = 𝑦 → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) ) )
93 92 rexlimdv ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ∃ 𝑤 ∈ P ( 𝑧 +P 𝑤 ) = 𝑦 → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) )
94 12 93 syl5 ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) )
95 4 9 94 ecoptocl ⊢ ( 𝐴 ∈ R → ( 0R <R 𝐴 → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R ) )
96 3 95 mpcom ⊢ ( 0R <R 𝐴 → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )