Metamath Proof Explorer


Theorem sqr0lem

Description: Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqr0lem A A 2 = 0 0 A i A + A = 0

Proof

Step Hyp Ref Expression
1 sqeq0 A A 2 = 0 A = 0
2 1 biimpa A A 2 = 0 A = 0
3 2 3ad2antr1 A A 2 = 0 0 A i A + A = 0
4 0re 0
5 eleq1 A = 0 A 0
6 4 5 mpbiri A = 0 A
7 6 recnd A = 0 A
8 sq0i A = 0 A 2 = 0
9 0le0 0 0
10 fveq2 A = 0 A = 0
11 re0 0 = 0
12 10 11 syl6eq A = 0 A = 0
13 9 12 breqtrrid A = 0 0 A
14 rennim A i A +
15 6 14 syl A = 0 i A +
16 8 13 15 3jca A = 0 A 2 = 0 0 A i A +
17 7 16 jca A = 0 A A 2 = 0 0 A i A +
18 3 17 impbii A A 2 = 0 0 A i A + A = 0