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

Theorem recexgt0sr 6661
Description: The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.)
Assertion
Ref Expression
recexgt0sr (0R <R Ax R (0R <R x (A ·R x) = 1R))
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.
StepHypRef Expression
1 ltrelsr 6626 . . . 4 <R ⊆ (R × R)
21brel 4335 . . 3 (0R <R A → (0R R A R))
32simprd 107 . 2 (0R <R AA R)
4 df-nr 6615 . . 3 R = ((P × P) / ~R )
5 breq2 3759 . . . 4 ([⟨y, z⟩] ~R = A → (0R <R [⟨y, z⟩] ~R ↔ 0R <R A))
6 oveq1 5462 . . . . . . 7 ([⟨y, z⟩] ~R = A → ([⟨y, z⟩] ~R ·R x) = (A ·R x))
76eqeq1d 2045 . . . . . 6 ([⟨y, z⟩] ~R = A → (([⟨y, z⟩] ~R ·R x) = 1R ↔ (A ·R x) = 1R))
87anbi2d 437 . . . . 5 ([⟨y, z⟩] ~R = A → ((0R <R x ([⟨y, z⟩] ~R ·R x) = 1R) ↔ (0R <R x (A ·R x) = 1R)))
98rexbidv 2321 . . . 4 ([⟨y, z⟩] ~R = A → (x R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R) ↔ x R (0R <R x (A ·R x) = 1R)))
105, 9imbi12d 223 . . 3 ([⟨y, z⟩] ~R = A → ((0R <R [⟨y, z⟩] ~Rx R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R)) ↔ (0R <R Ax R (0R <R x (A ·R x) = 1R))))
11 gt0srpr 6636 . . . . 5 (0R <R [⟨y, z⟩] ~Rz<P y)
12 ltexpri 6585 . . . . 5 (z<P yw P (z +P w) = y)
1311, 12sylbi 114 . . . 4 (0R <R [⟨y, z⟩] ~Rw P (z +P w) = y)
14 recexpr 6608 . . . . . . 7 (w Pv P (w ·P v) = 1P)
1514adantl 262 . . . . . 6 (((y P z P) w P) → v P (w ·P v) = 1P)
16 1pr 6534 . . . . . . . . . . . . . 14 1P P
17 addclpr 6520 . . . . . . . . . . . . . 14 ((v P 1P P) → (v +P 1P) P)
1816, 17mpan2 401 . . . . . . . . . . . . 13 (v P → (v +P 1P) P)
19 enrex 6625 . . . . . . . . . . . . . 14 ~R V
2019, 4ecopqsi 6097 . . . . . . . . . . . . 13 (((v +P 1P) P 1P P) → [⟨(v +P 1P), 1P⟩] ~R R)
2118, 16, 20sylancl 392 . . . . . . . . . . . 12 (v P → [⟨(v +P 1P), 1P⟩] ~R R)
2221adantl 262 . . . . . . . . . . 11 ((w P v P) → [⟨(v +P 1P), 1P⟩] ~R R)
2322ad2antlr 458 . . . . . . . . . 10 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → [⟨(v +P 1P), 1P⟩] ~R R)
24 simprr 484 . . . . . . . . . . . 12 (((y P z P) (w P v P)) → v P)
2524adantr 261 . . . . . . . . . . 11 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → v P)
26 ltaddpr 6569 . . . . . . . . . . . . . 14 ((1P P v P) → 1P<P (1P +P v))
2716, 26mpan 400 . . . . . . . . . . . . 13 (v P → 1P<P (1P +P v))
28 addcomprg 6552 . . . . . . . . . . . . . 14 ((1P P v P) → (1P +P v) = (v +P 1P))
2916, 28mpan 400 . . . . . . . . . . . . 13 (v P → (1P +P v) = (v +P 1P))
3027, 29breqtrd 3779 . . . . . . . . . . . 12 (v P → 1P<P (v +P 1P))
31 gt0srpr 6636 . . . . . . . . . . . 12 (0R <R [⟨(v +P 1P), 1P⟩] ~R ↔ 1P<P (v +P 1P))
3230, 31sylibr 137 . . . . . . . . . . 11 (v P → 0R <R [⟨(v +P 1P), 1P⟩] ~R )
3325, 32syl 14 . . . . . . . . . 10 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → 0R <R [⟨(v +P 1P), 1P⟩] ~R )
3418, 16jctir 296 . . . . . . . . . . . . . . . 16 (v P → ((v +P 1P) P 1P P))
3534anim2i 324 . . . . . . . . . . . . . . 15 (((y P z P) v P) → ((y P z P) ((v +P 1P) P 1P P)))
3635adantr 261 . . . . . . . . . . . . . 14 ((((y P z P) v P) ((w ·P v) = 1P (z +P w) = y)) → ((y P z P) ((v +P 1P) P 1P P)))
37 mulsrpr 6634 . . . . . . . . . . . . . 14 (((y P z P) ((v +P 1P) P 1P P)) → ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ) = [⟨((y ·P (v +P 1P)) +P (z ·P 1P)), ((y ·P 1P) +P (z ·P (v +P 1P)))⟩] ~R )
3836, 37syl 14 . . . . . . . . . . . . 13 ((((y P z P) v P) ((w ·P v) = 1P (z +P w) = y)) → ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ) = [⟨((y ·P (v +P 1P)) +P (z ·P 1P)), ((y ·P 1P) +P (z ·P (v +P 1P)))⟩] ~R )
3938adantlrl 451 . . . . . . . . . . . 12 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ) = [⟨((y ·P (v +P 1P)) +P (z ·P 1P)), ((y ·P 1P) +P (z ·P (v +P 1P)))⟩] ~R )
40 oveq1 5462 . . . . . . . . . . . . . . . . . . . . 21 ((z +P w) = y → ((z +P w) ·P v) = (y ·P v))
4140eqcomd 2042 . . . . . . . . . . . . . . . . . . . 20 ((z +P w) = y → (y ·P v) = ((z +P w) ·P v))
4241ad2antll 460 . . . . . . . . . . . . . . . . . . 19 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → (y ·P v) = ((z +P w) ·P v))
43 mulcomprg 6554 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((f P P) → (f ·P ) = ( ·P f))
44433adant2 922 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((f P g P P) → (f ·P ) = ( ·P f))
45 mulcomprg 6554 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((g P P) → (g ·P ) = ( ·P g))
46453adant1 921 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((f P g P P) → (g ·P ) = ( ·P g))
4744, 46oveq12d 5473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((f P g P P) → ((f ·P ) +P (g ·P )) = (( ·P f) +P ( ·P g)))
48 distrprg 6562 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( P f P g P) → ( ·P (f +P g)) = (( ·P f) +P ( ·P g)))
49483coml 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)
52513adant3 923 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((f P g P P) → (f +P g) P)
53 mulcomprg 6554 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( P (f +P g) P) → ( ·P (f +P g)) = ((f +P g) ·P ))
5450, 52, 53syl2anc 391 . . . . . . . . . . . . . . . . . . . . . . . 24 ((f P g P P) → ( ·P (f +P g)) = ((f +P g) ·P ))
5547, 49, 543eqtr2rd 2076 . . . . . . . . . . . . . . . . . . . . . . 23 ((f P g P P) → ((f +P g) ·P ) = ((f ·P ) +P (g ·P )))
5655adantl 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)
5956, 57, 58, 24caovdird 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) = 1P → ((z ·P v) +P (w ·P v)) = ((z ·P v) +P 1P))
6159, 60sylan9eq 2089 . . . . . . . . . . . . . . . . . . . 20 ((((y P z P) (w P v P)) (w ·P v) = 1P) → ((z +P w) ·P v) = ((z ·P v) +P 1P))
6261adantrr 448 . . . . . . . . . . . . . . . . . . 19 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ((z +P w) ·P v) = ((z ·P v) +P 1P))
6342, 62eqtrd 2069 . . . . . . . . . . . . . . . . . 18 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → (y ·P v) = ((z ·P v) +P 1P))
6463oveq1d 5470 . . . . . . . . . . . . . . . . 17 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))) = (((z ·P v) +P 1P) +P ((y ·P 1P) +P (z ·P 1P))))
65 mulclpr 6551 . . . . . . . . . . . . . . . . . . . 20 ((z P v P) → (z ·P v) P)
6657, 24, 65syl2anc 391 . . . . . . . . . . . . . . . . . . 19 (((y P z P) (w P v P)) → (z ·P v) P)
6716a1i 9 . . . . . . . . . . . . . . . . . . 19 (((y P z P) (w P v P)) → 1P P)
68 simpll 481 . . . . . . . . . . . . . . . . . . . . 21 (((y P z P) (w P v P)) → y P)
69 mulclpr 6551 . . . . . . . . . . . . . . . . . . . . 21 ((y P 1P P) → (y ·P 1P) P)
7068, 16, 69sylancl 392 . . . . . . . . . . . . . . . . . . . 20 (((y P z P) (w P v P)) → (y ·P 1P) P)
71 mulclpr 6551 . . . . . . . . . . . . . . . . . . . . 21 ((z P 1P P) → (z ·P 1P) P)
7257, 16, 71sylancl 392 . . . . . . . . . . . . . . . . . . . 20 (((y P z P) (w P v P)) → (z ·P 1P) P)
73 addclpr 6520 . . . . . . . . . . . . . . . . . . . 20 (((y ·P 1P) P (z ·P 1P) P) → ((y ·P 1P) +P (z ·P 1P)) P)
7470, 72, 73syl2anc 391 . . . . . . . . . . . . . . . . . . 19 (((y P z P) (w P v P)) → ((y ·P 1P) +P (z ·P 1P)) P)
75 addcomprg 6552 . . . . . . . . . . . . . . . . . . . 20 ((f P g P) → (f +P g) = (g +P f))
7675adantl 262 . . . . . . . . . . . . . . . . . . 19 ((((y P z P) (w P v P)) (f P g P)) → (f +P g) = (g +P f))
77 addassprg 6553 . . . . . . . . . . . . . . . . . . . 20 ((f P g P P) → ((f +P g) +P ) = (f +P (g +P )))
7877adantl 262 . . . . . . . . . . . . . . . . . . 19 ((((y P z P) (w P v P)) (f P g P P)) → ((f +P g) +P ) = (f +P (g +P )))
7966, 67, 74, 76, 78caov32d 5623 . . . . . . . . . . . . . . . . . 18 (((y P z P) (w P v P)) → (((z ·P v) +P 1P) +P ((y ·P 1P) +P (z ·P 1P))) = (((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P))
8079adantr 261 . . . . . . . . . . . . . . . . 17 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → (((z ·P v) +P 1P) +P ((y ·P 1P) +P (z ·P 1P))) = (((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P))
8164, 80eqtrd 2069 . . . . . . . . . . . . . . . 16 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))) = (((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P))
8281oveq1d 5470 . . . . . . . . . . . . . . 15 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → (((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P) = ((((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P) +P 1P))
83 addclpr 6520 . . . . . . . . . . . . . . . . . 18 (((z ·P v) P ((y ·P 1P) +P (z ·P 1P)) P) → ((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) P)
8466, 74, 83syl2anc 391 . . . . . . . . . . . . . . . . 17 (((y P z P) (w P v P)) → ((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) P)
8584adantr 261 . . . . . . . . . . . . . . . 16 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) P)
8616a1i 9 . . . . . . . . . . . . . . . 16 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → 1P P)
87 addassprg 6553 . . . . . . . . . . . . . . . 16 ((((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) P 1P P 1P P) → ((((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P) +P 1P) = (((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P (1P +P 1P)))
8885, 86, 86, 87syl3anc 1134 . . . . . . . . . . . . . . 15 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ((((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P) +P 1P) = (((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P (1P +P 1P)))
8982, 88eqtrd 2069 . . . . . . . . . . . . . 14 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → (((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P) = (((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P (1P +P 1P)))
90 distrprg 6562 . . . . . . . . . . . . . . . . . . 19 ((y P v P 1P P) → (y ·P (v +P 1P)) = ((y ·P v) +P (y ·P 1P)))
9168, 24, 67, 90syl3anc 1134 . . . . . . . . . . . . . . . . . 18 (((y P z P) (w P v P)) → (y ·P (v +P 1P)) = ((y ·P v) +P (y ·P 1P)))
9291oveq1d 5470 . . . . . . . . . . . . . . . . 17 (((y P z P) (w P v P)) → ((y ·P (v +P 1P)) +P (z ·P 1P)) = (((y ·P v) +P (y ·P 1P)) +P (z ·P 1P)))
93 mulclpr 6551 . . . . . . . . . . . . . . . . . . 19 ((y P v P) → (y ·P v) P)
9468, 24, 93syl2anc 391 . . . . . . . . . . . . . . . . . 18 (((y P z P) (w P v P)) → (y ·P v) P)
95 addassprg 6553 . . . . . . . . . . . . . . . . . 18 (((y ·P v) P (y ·P 1P) P (z ·P 1P) P) → (((y ·P v) +P (y ·P 1P)) +P (z ·P 1P)) = ((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))))
9694, 70, 72, 95syl3anc 1134 . . . . . . . . . . . . . . . . 17 (((y P z P) (w P v P)) → (((y ·P v) +P (y ·P 1P)) +P (z ·P 1P)) = ((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))))
9792, 96eqtrd 2069 . . . . . . . . . . . . . . . 16 (((y P z P) (w P v P)) → ((y ·P (v +P 1P)) +P (z ·P 1P)) = ((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))))
9897oveq1d 5470 . . . . . . . . . . . . . . 15 (((y P z P) (w P v P)) → (((y ·P (v +P 1P)) +P (z ·P 1P)) +P 1P) = (((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P))
9998adantr 261 . . . . . . . . . . . . . 14 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → (((y ·P (v +P 1P)) +P (z ·P 1P)) +P 1P) = (((y ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P 1P))
100 distrprg 6562 . . . . . . . . . . . . . . . . . . 19 ((z P v P 1P P) → (z ·P (v +P 1P)) = ((z ·P v) +P (z ·P 1P)))
10157, 24, 67, 100syl3anc 1134 . . . . . . . . . . . . . . . . . 18 (((y P z P) (w P v P)) → (z ·P (v +P 1P)) = ((z ·P v) +P (z ·P 1P)))
102101oveq2d 5471 . . . . . . . . . . . . . . . . 17 (((y P z P) (w P v P)) → ((y ·P 1P) +P (z ·P (v +P 1P))) = ((y ·P 1P) +P ((z ·P v) +P (z ·P 1P))))
10370, 66, 72, 76, 78caov12d 5624 . . . . . . . . . . . . . . . . 17 (((y P z P) (w P v P)) → ((y ·P 1P) +P ((z ·P v) +P (z ·P 1P))) = ((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))))
104102, 103eqtrd 2069 . . . . . . . . . . . . . . . 16 (((y P z P) (w P v P)) → ((y ·P 1P) +P (z ·P (v +P 1P))) = ((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))))
105104oveq1d 5470 . . . . . . . . . . . . . . 15 (((y P z P) (w P v P)) → (((y ·P 1P) +P (z ·P (v +P 1P))) +P (1P +P 1P)) = (((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P (1P +P 1P)))
106105adantr 261 . . . . . . . . . . . . . 14 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → (((y ·P 1P) +P (z ·P (v +P 1P))) +P (1P +P 1P)) = (((z ·P v) +P ((y ·P 1P) +P (z ·P 1P))) +P (1P +P 1P)))
10789, 99, 1063eqtr4d 2079 . . . . . . . . . . . . 13 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → (((y ·P (v +P 1P)) +P (z ·P 1P)) +P 1P) = (((y ·P 1P) +P (z ·P (v +P 1P))) +P (1P +P 1P)))
10824, 16, 17sylancl 392 . . . . . . . . . . . . . . . . 17 (((y P z P) (w P v P)) → (v +P 1P) P)
109 mulclpr 6551 . . . . . . . . . . . . . . . . 17 ((y P (v +P 1P) P) → (y ·P (v +P 1P)) P)
11068, 108, 109syl2anc 391 . . . . . . . . . . . . . . . 16 (((y P z P) (w P v P)) → (y ·P (v +P 1P)) P)
111 addclpr 6520 . . . . . . . . . . . . . . . 16 (((y ·P (v +P 1P)) P (z ·P 1P) P) → ((y ·P (v +P 1P)) +P (z ·P 1P)) P)
112110, 72, 111syl2anc 391 . . . . . . . . . . . . . . 15 (((y P z P) (w P v P)) → ((y ·P (v +P 1P)) +P (z ·P 1P)) P)
113104, 84eqeltrd 2111 . . . . . . . . . . . . . . 15 (((y P z P) (w P v P)) → ((y ·P 1P) +P (z ·P (v +P 1P))) P)
114 addclpr 6520 . . . . . . . . . . . . . . . . 17 ((1P P 1P P) → (1P +P 1P) P)
11516, 16, 114mp2an 402 . . . . . . . . . . . . . . . 16 (1P +P 1P) P
116115a1i 9 . . . . . . . . . . . . . . 15 (((y P z P) (w P v P)) → (1P +P 1P) P)
117 enreceq 6624 . . . . . . . . . . . . . . 15 (((((y ·P (v +P 1P)) +P (z ·P 1P)) P ((y ·P 1P) +P (z ·P (v +P 1P))) P) ((1P +P 1P) P 1P P)) → ([⟨((y ·P (v +P 1P)) +P (z ·P 1P)), ((y ·P 1P) +P (z ·P (v +P 1P)))⟩] ~R = [⟨(1P +P 1P), 1P⟩] ~R ↔ (((y ·P (v +P 1P)) +P (z ·P 1P)) +P 1P) = (((y ·P 1P) +P (z ·P (v +P 1P))) +P (1P +P 1P))))
118112, 113, 116, 67, 117syl22anc 1135 . . . . . . . . . . . . . 14 (((y P z P) (w P v P)) → ([⟨((y ·P (v +P 1P)) +P (z ·P 1P)), ((y ·P 1P) +P (z ·P (v +P 1P)))⟩] ~R = [⟨(1P +P 1P), 1P⟩] ~R ↔ (((y ·P (v +P 1P)) +P (z ·P 1P)) +P 1P) = (((y ·P 1P) +P (z ·P (v +P 1P))) +P (1P +P 1P))))
119118adantr 261 . . . . . . . . . . . . 13 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ([⟨((y ·P (v +P 1P)) +P (z ·P 1P)), ((y ·P 1P) +P (z ·P (v +P 1P)))⟩] ~R = [⟨(1P +P 1P), 1P⟩] ~R ↔ (((y ·P (v +P 1P)) +P (z ·P 1P)) +P 1P) = (((y ·P 1P) +P (z ·P (v +P 1P))) +P (1P +P 1P))))
120107, 119mpbird 156 . . . . . . . . . . . 12 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → [⟨((y ·P (v +P 1P)) +P (z ·P 1P)), ((y ·P 1P) +P (z ·P (v +P 1P)))⟩] ~R = [⟨(1P +P 1P), 1P⟩] ~R )
12139, 120eqtrd 2069 . . . . . . . . . . 11 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ) = [⟨(1P +P 1P), 1P⟩] ~R )
122 df-1r 6620 . . . . . . . . . . 11 1R = [⟨(1P +P 1P), 1P⟩] ~R
123121, 122syl6eqr 2087 . . . . . . . . . 10 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ) = 1R)
124 breq2 3759 . . . . . . . . . . . 12 (x = [⟨(v +P 1P), 1P⟩] ~R → (0R <R x ↔ 0R <R [⟨(v +P 1P), 1P⟩] ~R ))
125 oveq2 5463 . . . . . . . . . . . . 13 (x = [⟨(v +P 1P), 1P⟩] ~R → ([⟨y, z⟩] ~R ·R x) = ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ))
126125eqeq1d 2045 . . . . . . . . . . . 12 (x = [⟨(v +P 1P), 1P⟩] ~R → (([⟨y, z⟩] ~R ·R x) = 1R ↔ ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ) = 1R))
127124, 126anbi12d 442 . . . . . . . . . . 11 (x = [⟨(v +P 1P), 1P⟩] ~R → ((0R <R x ([⟨y, z⟩] ~R ·R x) = 1R) ↔ (0R <R [⟨(v +P 1P), 1P⟩] ~R ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ) = 1R)))
128127rspcev 2650 . . . . . . . . . 10 (([⟨(v +P 1P), 1P⟩] ~R R (0R <R [⟨(v +P 1P), 1P⟩] ~R ([⟨y, z⟩] ~R ·R [⟨(v +P 1P), 1P⟩] ~R ) = 1R)) → x R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R))
12923, 33, 123, 128syl12anc 1132 . . . . . . . . 9 ((((y P z P) (w P v P)) ((w ·P v) = 1P (z +P w) = y)) → x R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R))
130129exp32 347 . . . . . . . 8 (((y P z P) (w P v P)) → ((w ·P v) = 1P → ((z +P w) = yx R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R))))
131130anassrs 380 . . . . . . 7 ((((y P z P) w P) v P) → ((w ·P v) = 1P → ((z +P w) = yx R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R))))
132131rexlimdva 2427 . . . . . 6 (((y P z P) w P) → (v P (w ·P v) = 1P → ((z +P w) = yx R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R))))
13315, 132mpd 13 . . . . 5 (((y P z P) w P) → ((z +P w) = yx R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R)))
134133rexlimdva 2427 . . . 4 ((y P z P) → (w P (z +P w) = yx R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R)))
13513, 134syl5 28 . . 3 ((y P z P) → (0R <R [⟨y, z⟩] ~Rx R (0R <R x ([⟨y, z⟩] ~R ·R x) = 1R)))
1364, 10, 135ecoptocl 6129 . 2 (A R → (0R <R Ax R (0R <R x (A ·R x) = 1R)))
1373, 136mpcom 32 1 (0R <R Ax R (0R <R x (A ·R x) = 1R))
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  1Pc1p 6276   +P cpp 6277   ·P cmp 6278  <P cltp 6279   ~R cer 6280  Rcnr 6281  0Rc0r 6282  1Rc1r 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-bnd 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 6406  df-nq0 6407  df-0nq0 6408  df-plq0 6409  df-mq0 6410  df-inp 6448  df-i1p 6449  df-iplp 6450  df-imp 6451  df-iltp 6452  df-enr 6614  df-nr 6615  df-mr 6617  df-ltr 6618  df-0r 6619  df-1r 6620
This theorem is referenced by:  recexsrlem  6662  axprecex  6724
  Copyright terms: Public domain W3C validator