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

Theorem 4sqlem9 14336
 Description: Lemma for 4sq 14354. (Contributed by Mario Carneiro, 15-Jul-2014.)
Hypotheses
Ref Expression
4sqlem5.2
4sqlem5.3
4sqlem5.4
4sqlem9.5
Assertion
Ref Expression
4sqlem9

Proof of Theorem 4sqlem9
StepHypRef Expression
1 4sqlem9.5 . . . . . . . 8
2 4sqlem5.2 . . . . . . . . . . . . 13
3 4sqlem5.3 . . . . . . . . . . . . 13
4 4sqlem5.4 . . . . . . . . . . . . 13
52, 3, 44sqlem5 14332 . . . . . . . . . . . 12
65simpld 459 . . . . . . . . . . 11
76zcnd 10970 . . . . . . . . . 10
8 sqeq0 12206 . . . . . . . . . 10
97, 8syl 16 . . . . . . . . 9
109biimpa 484 . . . . . . . 8
111, 10syldan 470 . . . . . . 7
1211oveq2d 6293 . . . . . 6
132adantr 465 . . . . . . . 8
1413zcnd 10970 . . . . . . 7
1514subid1d 9920 . . . . . 6
1612, 15eqtrd 2482 . . . . 5
1716oveq1d 6292 . . . 4
185simprd 463 . . . . 5
1918adantr 465 . . . 4
2017, 19eqeltrrd 2530 . . 3
213nnzd 10968 . . . . 5
223nnne0d 10581 . . . . 5
23 dvdsval2 13861 . . . . 5
2421, 22, 2, 23syl3anc 1227 . . . 4