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 ⊢0𝑹<𝑹A→∃x∈𝑹A⋅𝑹x=1𝑹

Proof

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