Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ipasslem4 Unicode version

Theorem ipasslem4 21428
 Description: Lemma for ipassi 21435. Show the inner product associative law for positive integer reciprocals. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
Hypotheses
Ref Expression
ip1i.1
ip1i.2
ip1i.4
ip1i.7
ip1i.9
ipasslem1.b
Assertion
Ref Expression
ipasslem4

Proof of Theorem ipasslem4
StepHypRef Expression
1 nncn 9770 . . . . . . 7
2 nnne0 9794 . . . . . . 7
31, 2recidd 9547 . . . . . 6
43oveq1d 5889 . . . . 5
5 ip1i.9 . . . . . . . 8
65phnvi 21410 . . . . . . 7
7 ipasslem1.b . . . . . . 7
8 ip1i.1 . . . . . . . 8
9 ip1i.7 . . . . . . . 8
108, 9dipcl 21304 . . . . . . 7
116, 7, 10mp3an13 1268 . . . . . 6
1211mulid2d 8869 . . . . 5
134, 12sylan9eq 2348 . . . 4
143oveq1d 5889 . . . . . . 7
15 ip1i.4 . . . . . . . . 9
168, 15nvsid 21201 . . . . . . . 8
176, 16mpan 651 . . . . . . 7
1814, 17sylan9eq 2348 . . . . . 6
191adantr 451 . . . . . . 7
20 nnrecre 9798 . . . . . . . . 9
2120recnd 8877 . . . . . . . 8
2221adantr 451 . . . . . . 7
23 simpr 447 . . . . . . 7
248, 15nvsass 21202 . . . . . . . 8
256, 24mpan 651 . . . . . . 7
2619, 22, 23, 25syl3anc 1182 . . . . . 6
2718, 26eqtr3d 2330 . . . . 5
2827oveq1d 5889 . . . 4
29 nnnn0 9988 . . . . . 6
3029adantr 451 . . . . 5
318, 15nvscl 21200 . . . . . . 7
326, 31mp3an1 1264 . . . . . 6
3321, 32sylan 457 . . . . 5
34 ip1i.2 . . . . . 6
358, 34, 15, 9, 5, 7ipasslem1 21425 . . . . 5
3630, 33, 35syl2anc 642 . . . 4
3713, 28, 363eqtrd 2332 . . 3
3811adantl 452 . . . 4
3919, 22, 38mulassd 8874 . . 3
4037, 39eqtr3d 2330 . 2
418, 9dipcl 21304 . . . . 5
426, 7, 41mp3an13 1268 . . . 4
4333, 42syl 15 . . 3
44 mulcl 8837 . . . 4
4521, 11, 44syl2an 463 . . 3