recexgt0sr - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > recexgt0sr		GIF version

Theorem recexgt0sr 6701

Description: The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.)

**Assertion**
Ref	Expression
recexgt0sr	⊢ (0_R <_R A → ∃x ∈ R (0_R <_R x ∧ (A ·_R x) = 1_R))

Distinct variable group: x,A

Proof of Theorem recexgt0sr Dummy variables y z w v f g ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelsr 6666	. . . 4 ⊢ <_R ⊆ (R × R)
2	1	brel 4335	. . 3 ⊢ (0_R <_R A → (0_R ∈ R ∧ A ∈ R))
3	2	simprd 107	. 2 ⊢ (0_R <_R A → A ∈ R)
4		df-nr 6655	. . 3 ⊢ R = ((P × P) / ~_R )
5		breq2 3759	. . . 4 ⊢ ([⟨y, z⟩] ~_R = A → (0_R <_R [⟨y, z⟩] ~_R ↔ 0_R <_R A))
6		oveq1 5462	. . . . . . 7 ⊢ ([⟨y, z⟩] ~_R = A → ([⟨y, z⟩] ~_R ·_R x) = (A ·_R x))
7	6	eqeq1d 2045	. . . . . 6 ⊢ ([⟨y, z⟩] ~_R = A → (([⟨y, z⟩] ~_R ·_R x) = 1_R ↔ (A ·_R x) = 1_R))
8	7	anbi2d 437	. . . . 5 ⊢ ([⟨y, z⟩] ~_R = A → ((0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R) ↔ (0_R <_R x ∧ (A ·_R x) = 1_R)))
9	8	rexbidv 2321	. . . 4 ⊢ ([⟨y, z⟩] ~_R = A → (∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R) ↔ ∃x ∈ R (0_R <_R x ∧ (A ·_R x) = 1_R)))
10	5, 9	imbi12d 223	. . 3 ⊢ ([⟨y, z⟩] ~_R = A → ((0_R <_R [⟨y, z⟩] ~_R → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R)) ↔ (0_R <_R A → ∃x ∈ R (0_R <_R x ∧ (A ·_R x) = 1_R))))
11		gt0srpr 6676	. . . . 5 ⊢ (0_R <_R [⟨y, z⟩] ~_R ↔ z<_P y)
12		ltexpri 6587	. . . . 5 ⊢ (z<_P y → ∃w ∈ P (z +_P w) = y)
13	11, 12	sylbi 114	. . . 4 ⊢ (0_R <_R [⟨y, z⟩] ~_R → ∃w ∈ P (z +_P w) = y)
14		recexpr 6610	. . . . . . 7 ⊢ (w ∈ P → ∃v ∈ P (w ·_P v) = 1_P)
15	14	adantl 262	. . . . . 6 ⊢ (((y ∈ P ∧ z ∈ P) ∧ w ∈ P) → ∃v ∈ P (w ·_P v) = 1_P)
16		1pr 6535	. . . . . . . . . . . . . 14 ⊢ 1_P ∈ P
17		addclpr 6520	. . . . . . . . . . . . . 14 ⊢ ((v ∈ P ∧ 1_P ∈ P) → (v +_P 1_P) ∈ P)
18	16, 17	mpan2 401	. . . . . . . . . . . . 13 ⊢ (v ∈ P → (v +_P 1_P) ∈ P)
19		enrex 6665	. . . . . . . . . . . . . 14 ⊢ ~_R ∈ V
20	19, 4	ecopqsi 6097	. . . . . . . . . . . . 13 ⊢ (((v +_P 1_P) ∈ P ∧ 1_P ∈ P) → [⟨(v +_P 1_P), 1_P⟩] ~_R ∈ R)
21	18, 16, 20	sylancl 392	. . . . . . . . . . . 12 ⊢ (v ∈ P → [⟨(v +_P 1_P), 1_P⟩] ~_R ∈ R)
22	21	adantl 262	. . . . . . . . . . 11 ⊢ ((w ∈ P ∧ v ∈ P) → [⟨(v +_P 1_P), 1_P⟩] ~_R ∈ R)
23	22	ad2antlr 458	. . . . . . . . . 10 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → [⟨(v +_P 1_P), 1_P⟩] ~_R ∈ R)
24		simprr 484	. . . . . . . . . . . 12 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → v ∈ P)
25	24	adantr 261	. . . . . . . . . . 11 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → v ∈ P)
26		ltaddpr 6571	. . . . . . . . . . . . . 14 ⊢ ((1_P ∈ P ∧ v ∈ P) → 1_P<_P (1_P +_P v))
27	16, 26	mpan 400	. . . . . . . . . . . . 13 ⊢ (v ∈ P → 1_P<_P (1_P +_P v))
28		addcomprg 6554	. . . . . . . . . . . . . 14 ⊢ ((1_P ∈ P ∧ v ∈ P) → (1_P +_P v) = (v +_P 1_P))
29	16, 28	mpan 400	. . . . . . . . . . . . 13 ⊢ (v ∈ P → (1_P +_P v) = (v +_P 1_P))
30	27, 29	breqtrd 3779	. . . . . . . . . . . 12 ⊢ (v ∈ P → 1_P<_P (v +_P 1_P))
31		gt0srpr 6676	. . . . . . . . . . . 12 ⊢ (0_R <_R [⟨(v +_P 1_P), 1_P⟩] ~_R ↔ 1_P<_P (v +_P 1_P))
32	30, 31	sylibr 137	. . . . . . . . . . 11 ⊢ (v ∈ P → 0_R <_R [⟨(v +_P 1_P), 1_P⟩] ~_R )
33	25, 32	syl 14	. . . . . . . . . 10 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → 0_R <_R [⟨(v +_P 1_P), 1_P⟩] ~_R )
34	18, 16	jctir 296	. . . . . . . . . . . . . . . 16 ⊢ (v ∈ P → ((v +_P 1_P) ∈ P ∧ 1_P ∈ P))
35	34	anim2i 324	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ P ∧ z ∈ P) ∧ v ∈ P) → ((y ∈ P ∧ z ∈ P) ∧ ((v +_P 1_P) ∈ P ∧ 1_P ∈ P)))
36	35	adantr 261	. . . . . . . . . . . . . 14 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ v ∈ P) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ((y ∈ P ∧ z ∈ P) ∧ ((v +_P 1_P) ∈ P ∧ 1_P ∈ P)))
37		mulsrpr 6674	. . . . . . . . . . . . . 14 ⊢ (((y ∈ P ∧ z ∈ P) ∧ ((v +_P 1_P) ∈ P ∧ 1_P ∈ P)) → ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ) = [⟨((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)), ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P)))⟩] ~_R )
38	36, 37	syl 14	. . . . . . . . . . . . 13 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ v ∈ P) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ) = [⟨((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)), ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P)))⟩] ~_R )
39	38	adantlrl 451	. . . . . . . . . . . 12 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ) = [⟨((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)), ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P)))⟩] ~_R )
40		oveq1 5462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((z +_P w) = y → ((z +_P w) ·_P v) = (y ·_P v))
41	40	eqcomd 2042	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z +_P w) = y → (y ·_P v) = ((z +_P w) ·_P v))
42	41	ad2antll 460	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → (y ·_P v) = ((z +_P w) ·_P v))
43		mulcomprg 6556	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f ∈ P ∧ ℎ ∈ P) → (f ·_P ℎ) = (ℎ ·_P f))
44	43	3adant2 922	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → (f ·_P ℎ) = (ℎ ·_P f))
45		mulcomprg 6556	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((g ∈ P ∧ ℎ ∈ P) → (g ·_P ℎ) = (ℎ ·_P g))
46	45	3adant1 921	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → (g ·_P ℎ) = (ℎ ·_P g))
47	44, 46	oveq12d 5473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → ((f ·_P ℎ) +_P (g ·_P ℎ)) = ((ℎ ·_P f) +_P (ℎ ·_P g)))
48		distrprg 6564	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∈ P ∧ f ∈ P ∧ g ∈ P) → (ℎ ·_P (f +_P g)) = ((ℎ ·_P f) +_P (ℎ ·_P g)))
49	48	3coml 1110	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → (ℎ ·_P (f +_P g)) = ((ℎ ·_P f) +_P (ℎ ·_P g)))
50		simp3 905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → ℎ ∈ P)
51		addclpr 6520	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f ∈ P ∧ g ∈ P) → (f +_P g) ∈ P)
52	51	3adant3 923	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → (f +_P g) ∈ P)
53		mulcomprg 6556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∈ P ∧ (f +_P g) ∈ P) → (ℎ ·_P (f +_P g)) = ((f +_P g) ·_P ℎ))
54	50, 52, 53	syl2anc 391	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → (ℎ ·_P (f +_P g)) = ((f +_P g) ·_P ℎ))
55	47, 49, 54	3eqtr2rd 2076	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → ((f +_P g) ·_P ℎ) = ((f ·_P ℎ) +_P (g ·_P ℎ)))
56	55	adantl 262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ (f ∈ P ∧ g ∈ P ∧ ℎ ∈ P)) → ((f +_P g) ·_P ℎ) = ((f ·_P ℎ) +_P (g ·_P ℎ)))
57		simplr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → z ∈ P)
58		simprl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → w ∈ P)
59	56, 57, 58, 24	caovdird 5621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((z +_P w) ·_P v) = ((z ·_P v) +_P (w ·_P v)))
60		oveq2 5463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((w ·_P v) = 1_P → ((z ·_P v) +_P (w ·_P v)) = ((z ·_P v) +_P 1_P))
61	59, 60	sylan9eq 2089	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ (w ·_P v) = 1_P) → ((z +_P w) ·_P v) = ((z ·_P v) +_P 1_P))
62	61	adantrr 448	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ((z +_P w) ·_P v) = ((z ·_P v) +_P 1_P))
63	42, 62	eqtrd 2069	. . . . . . . . . . . . . . . . . 18 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → (y ·_P v) = ((z ·_P v) +_P 1_P))
64	63	oveq1d 5470	. . . . . . . . . . . . . . . . 17 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) = (((z ·_P v) +_P 1_P) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))))
65		mulclpr 6553	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z ∈ P ∧ v ∈ P) → (z ·_P v) ∈ P)
66	57, 24, 65	syl2anc 391	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (z ·_P v) ∈ P)
67	16	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → 1_P ∈ P)
68		simpll 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → y ∈ P)
69		mulclpr 6553	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ P ∧ 1_P ∈ P) → (y ·_P 1_P) ∈ P)
70	68, 16, 69	sylancl 392	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (y ·_P 1_P) ∈ P)
71		mulclpr 6553	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((z ∈ P ∧ 1_P ∈ P) → (z ·_P 1_P) ∈ P)
72	57, 16, 71	sylancl 392	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (z ·_P 1_P) ∈ P)
73		addclpr 6520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((y ·_P 1_P) ∈ P ∧ (z ·_P 1_P) ∈ P) → ((y ·_P 1_P) +_P (z ·_P 1_P)) ∈ P)
74	70, 72, 73	syl2anc 391	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·_P 1_P) +_P (z ·_P 1_P)) ∈ P)
75		addcomprg 6554	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f ∈ P ∧ g ∈ P) → (f +_P g) = (g +_P f))
76	75	adantl 262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ (f ∈ P ∧ g ∈ P)) → (f +_P g) = (g +_P f))
77		addassprg 6555	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f ∈ P ∧ g ∈ P ∧ ℎ ∈ P) → ((f +_P g) +_P ℎ) = (f +_P (g +_P ℎ)))
78	77	adantl 262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ (f ∈ P ∧ g ∈ P ∧ ℎ ∈ P)) → ((f +_P g) +_P ℎ) = (f +_P (g +_P ℎ)))
79	66, 67, 74, 76, 78	caov32d 5623	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (((z ·_P v) +_P 1_P) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) = (((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P))
80	79	adantr 261	. . . . . . . . . . . . . . . . 17 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → (((z ·_P v) +_P 1_P) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) = (((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P))
81	64, 80	eqtrd 2069	. . . . . . . . . . . . . . . 16 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) = (((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P))
82	81	oveq1d 5470	. . . . . . . . . . . . . . 15 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → (((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P) = ((((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P) +_P 1_P))
83		addclpr 6520	. . . . . . . . . . . . . . . . . 18 ⊢ (((z ·_P v) ∈ P ∧ ((y ·_P 1_P) +_P (z ·_P 1_P)) ∈ P) → ((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) ∈ P)
84	66, 74, 83	syl2anc 391	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) ∈ P)
85	84	adantr 261	. . . . . . . . . . . . . . . 16 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) ∈ P)
86	16	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → 1_P ∈ P)
87		addassprg 6555	. . . . . . . . . . . . . . . 16 ⊢ ((((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) ∈ P ∧ 1_P ∈ P ∧ 1_P ∈ P) → ((((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P) +_P 1_P) = (((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P (1_P +_P 1_P)))
88	85, 86, 86, 87	syl3anc 1134	. . . . . . . . . . . . . . 15 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ((((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P) +_P 1_P) = (((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P (1_P +_P 1_P)))
89	82, 88	eqtrd 2069	. . . . . . . . . . . . . 14 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → (((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P) = (((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P (1_P +_P 1_P)))
90		distrprg 6564	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ P ∧ v ∈ P ∧ 1_P ∈ P) → (y ·_P (v +_P 1_P)) = ((y ·_P v) +_P (y ·_P 1_P)))
91	68, 24, 67, 90	syl3anc 1134	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (y ·_P (v +_P 1_P)) = ((y ·_P v) +_P (y ·_P 1_P)))
92	91	oveq1d 5470	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) = (((y ·_P v) +_P (y ·_P 1_P)) +_P (z ·_P 1_P)))
93		mulclpr 6553	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ P ∧ v ∈ P) → (y ·_P v) ∈ P)
94	68, 24, 93	syl2anc 391	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (y ·_P v) ∈ P)
95		addassprg 6555	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ·_P v) ∈ P ∧ (y ·_P 1_P) ∈ P ∧ (z ·_P 1_P) ∈ P) → (((y ·_P v) +_P (y ·_P 1_P)) +_P (z ·_P 1_P)) = ((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))))
96	94, 70, 72, 95	syl3anc 1134	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (((y ·_P v) +_P (y ·_P 1_P)) +_P (z ·_P 1_P)) = ((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))))
97	92, 96	eqtrd 2069	. . . . . . . . . . . . . . . 16 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) = ((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))))
98	97	oveq1d 5470	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) +_P 1_P) = (((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P))
99	98	adantr 261	. . . . . . . . . . . . . 14 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → (((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) +_P 1_P) = (((y ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P 1_P))
100		distrprg 6564	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ P ∧ v ∈ P ∧ 1_P ∈ P) → (z ·_P (v +_P 1_P)) = ((z ·_P v) +_P (z ·_P 1_P)))
101	57, 24, 67, 100	syl3anc 1134	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (z ·_P (v +_P 1_P)) = ((z ·_P v) +_P (z ·_P 1_P)))
102	101	oveq2d 5471	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) = ((y ·_P 1_P) +_P ((z ·_P v) +_P (z ·_P 1_P))))
103	70, 66, 72, 76, 78	caov12d 5624	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·_P 1_P) +_P ((z ·_P v) +_P (z ·_P 1_P))) = ((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))))
104	102, 103	eqtrd 2069	. . . . . . . . . . . . . . . 16 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) = ((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))))
105	104	oveq1d 5470	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) +_P (1_P +_P 1_P)) = (((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P (1_P +_P 1_P)))
106	105	adantr 261	. . . . . . . . . . . . . 14 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → (((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) +_P (1_P +_P 1_P)) = (((z ·_P v) +_P ((y ·_P 1_P) +_P (z ·_P 1_P))) +_P (1_P +_P 1_P)))
107	89, 99, 106	3eqtr4d 2079	. . . . . . . . . . . . 13 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → (((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) +_P 1_P) = (((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) +_P (1_P +_P 1_P)))
108	24, 16, 17	sylancl 392	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (v +_P 1_P) ∈ P)
109		mulclpr 6553	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ P ∧ (v +_P 1_P) ∈ P) → (y ·_P (v +_P 1_P)) ∈ P)
110	68, 108, 109	syl2anc 391	. . . . . . . . . . . . . . . 16 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (y ·_P (v +_P 1_P)) ∈ P)
111		addclpr 6520	. . . . . . . . . . . . . . . 16 ⊢ (((y ·_P (v +_P 1_P)) ∈ P ∧ (z ·_P 1_P) ∈ P) → ((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) ∈ P)
112	110, 72, 111	syl2anc 391	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) ∈ P)
113	104, 84	eqeltrd 2111	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) ∈ P)
114		addclpr 6520	. . . . . . . . . . . . . . . . 17 ⊢ ((1_P ∈ P ∧ 1_P ∈ P) → (1_P +_P 1_P) ∈ P)
115	16, 16, 114	mp2an 402	. . . . . . . . . . . . . . . 16 ⊢ (1_P +_P 1_P) ∈ P
116	115	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (1_P +_P 1_P) ∈ P)
117		enreceq 6664	. . . . . . . . . . . . . . 15 ⊢ (((((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) ∈ P ∧ ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) ∈ P) ∧ ((1_P +_P 1_P) ∈ P ∧ 1_P ∈ P)) → ([⟨((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)), ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P)))⟩] ~_R = [⟨(1_P +_P 1_P), 1_P⟩] ~_R ↔ (((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) +_P 1_P) = (((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) +_P (1_P +_P 1_P))))
118	112, 113, 116, 67, 117	syl22anc 1135	. . . . . . . . . . . . . 14 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ([⟨((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)), ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P)))⟩] ~_R = [⟨(1_P +_P 1_P), 1_P⟩] ~_R ↔ (((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) +_P 1_P) = (((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) +_P (1_P +_P 1_P))))
119	118	adantr 261	. . . . . . . . . . . . 13 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ([⟨((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)), ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P)))⟩] ~_R = [⟨(1_P +_P 1_P), 1_P⟩] ~_R ↔ (((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)) +_P 1_P) = (((y ·_P 1_P) +_P (z ·_P (v +_P 1_P))) +_P (1_P +_P 1_P))))
120	107, 119	mpbird 156	. . . . . . . . . . . 12 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → [⟨((y ·_P (v +_P 1_P)) +_P (z ·_P 1_P)), ((y ·_P 1_P) +_P (z ·_P (v +_P 1_P)))⟩] ~_R = [⟨(1_P +_P 1_P), 1_P⟩] ~_R )
121	39, 120	eqtrd 2069	. . . . . . . . . . 11 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ) = [⟨(1_P +_P 1_P), 1_P⟩] ~_R )
122		df-1r 6660	. . . . . . . . . . 11 ⊢ 1_R = [⟨(1_P +_P 1_P), 1_P⟩] ~_R
123	121, 122	syl6eqr 2087	. . . . . . . . . 10 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ) = 1_R)
124		breq2 3759	. . . . . . . . . . . 12 ⊢ (x = [⟨(v +_P 1_P), 1_P⟩] ~_R → (0_R <_R x ↔ 0_R <_R [⟨(v +_P 1_P), 1_P⟩] ~_R ))
125		oveq2 5463	. . . . . . . . . . . . 13 ⊢ (x = [⟨(v +_P 1_P), 1_P⟩] ~_R → ([⟨y, z⟩] ~_R ·_R x) = ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ))
126	125	eqeq1d 2045	. . . . . . . . . . . 12 ⊢ (x = [⟨(v +_P 1_P), 1_P⟩] ~_R → (([⟨y, z⟩] ~_R ·_R x) = 1_R ↔ ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ) = 1_R))
127	124, 126	anbi12d 442	. . . . . . . . . . 11 ⊢ (x = [⟨(v +_P 1_P), 1_P⟩] ~_R → ((0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R) ↔ (0_R <_R [⟨(v +_P 1_P), 1_P⟩] ~_R ∧ ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ) = 1_R)))
128	127	rspcev 2650	. . . . . . . . . 10 ⊢ (([⟨(v +_P 1_P), 1_P⟩] ~_R ∈ R ∧ (0_R <_R [⟨(v +_P 1_P), 1_P⟩] ~_R ∧ ([⟨y, z⟩] ~_R ·_R [⟨(v +_P 1_P), 1_P⟩] ~_R ) = 1_R)) → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R))
129	23, 33, 123, 128	syl12anc 1132	. . . . . . . . 9 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w ·_P v) = 1_P ∧ (z +_P w) = y)) → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R))
130	129	exp32 347	. . . . . . . 8 ⊢ (((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((w ·_P v) = 1_P → ((z +_P w) = y → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R))))
131	130	anassrs 380	. . . . . . 7 ⊢ ((((y ∈ P ∧ z ∈ P) ∧ w ∈ P) ∧ v ∈ P) → ((w ·_P v) = 1_P → ((z +_P w) = y → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R))))
132	131	rexlimdva 2427	. . . . . 6 ⊢ (((y ∈ P ∧ z ∈ P) ∧ w ∈ P) → (∃v ∈ P (w ·_P v) = 1_P → ((z +_P w) = y → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R))))
133	15, 132	mpd 13	. . . . 5 ⊢ (((y ∈ P ∧ z ∈ P) ∧ w ∈ P) → ((z +_P w) = y → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R)))
134	133	rexlimdva 2427	. . . 4 ⊢ ((y ∈ P ∧ z ∈ P) → (∃w ∈ P (z +_P w) = y → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R)))
135	13, 134	syl5 28	. . 3 ⊢ ((y ∈ P ∧ z ∈ P) → (0_R <_R [⟨y, z⟩] ~_R → ∃x ∈ R (0_R <_R x ∧ ([⟨y, z⟩] ~_R ·_R x) = 1_R)))
136	4, 10, 135	ecoptocl 6129	. 2 ⊢ (A ∈ R → (0_R <_R A → ∃x ∈ R (0_R <_R x ∧ (A ·_R x) = 1_R)))
137	3, 136	mpcom 32	1 ⊢ (0_R <_R A → ∃x ∈ R (0_R <_R x ∧ (A ·_R x) = 1_R))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 ∧ w3a 884 = wceq 1242 ∈ wcel 1390 ∃wrex 2301 ⟨cop 3370 class class class wbr 3755 (class class class)co 5455 [cec 6040 Pcnp 6275 1_Pc1p 6276 +_P cpp 6277 ·_P cmp 6278 <_P cltp 6279 ~_R cer 6280 Rcnr 6281 0_Rc0r 6282 1_Rc1r 6283 ·_R cmr 6286 <_R cltr 6287

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-13 1401 ax-14 1402 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-coll 3863 ax-sep 3866 ax-nul 3874 ax-pow 3918 ax-pr 3935 ax-un 4136 ax-setind 4220 ax-iinf 4254

This theorem depends on definitions: df-bi 110 df-dc 742 df-3or 885 df-3an 886 df-tru 1245 df-fal 1248 df-nf 1347 df-sb 1643 df-eu 1900 df-mo 1901 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ne 2203 df-ral 2305 df-rex 2306 df-reu 2307 df-rab 2309 df-v 2553 df-sbc 2759 df-csb 2847 df-dif 2914 df-un 2916 df-in 2918 df-ss 2925 df-nul 3219 df-pw 3353 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-int 3607 df-iun 3650 df-br 3756 df-opab 3810 df-mpt 3811 df-tr 3846 df-eprel 4017 df-id 4021 df-po 4024 df-iso 4025 df-iord 4069 df-on 4071 df-suc 4074 df-iom 4257 df-xp 4294 df-rel 4295 df-cnv 4296 df-co 4297 df-dm 4298 df-rn 4299 df-res 4300 df-ima 4301 df-iota 4810 df-fun 4847 df-fn 4848 df-f 4849 df-f1 4850 df-fo 4851 df-f1o 4852 df-fv 4853 df-ov 5458 df-oprab 5459 df-mpt2 5460 df-1st 5709 df-2nd 5710 df-recs 5861 df-irdg 5897 df-1o 5940 df-2o 5941 df-oadd 5944 df-omul 5945 df-er 6042 df-ec 6044 df-qs 6048 df-ni 6288 df-pli 6289 df-mi 6290 df-lti 6291 df-plpq 6328 df-mpq 6329 df-enq 6331 df-nqqs 6332 df-plqqs 6333 df-mqqs 6334 df-1nqqs 6335 df-rq 6336 df-ltnqqs 6337 df-enq0 6407 df-nq0 6408 df-0nq0 6409 df-plq0 6410 df-mq0 6411 df-inp 6449 df-i1p 6450 df-iplp 6451 df-imp 6452 df-iltp 6453 df-enr 6654 df-nr 6655 df-mr 6657 df-ltr 6658 df-0r 6659 df-1r 6660

This theorem is referenced by: recexsrlem 6702 axprecex 6764

W3C validator