Metamath Proof Explorer


Theorem recextlem2

Description: Lemma for recex . (Contributed by Eric Schmidt, 23-May-2007)

Ref Expression
Assertion recextlem2 A B A + i B 0 A A + B B 0

Proof

Step Hyp Ref Expression
1 oveq2 B = 0 i B = i 0
2 ax-icn i
3 2 mul01i i 0 = 0
4 1 3 eqtrdi B = 0 i B = 0
5 oveq12 A = 0 i B = 0 A + i B = 0 + 0
6 4 5 sylan2 A = 0 B = 0 A + i B = 0 + 0
7 00id 0 + 0 = 0
8 6 7 eqtrdi A = 0 B = 0 A + i B = 0
9 8 necon3ai A + i B 0 ¬ A = 0 B = 0
10 neorian A 0 B 0 ¬ A = 0 B = 0
11 9 10 sylibr A + i B 0 A 0 B 0
12 remulcl A A A A
13 12 anidms A A A
14 remulcl B B B B
15 14 anidms B B B
16 13 15 anim12i A B A A B B
17 msqgt0 A A 0 0 < A A
18 msqge0 B 0 B B
19 17 18 anim12i A A 0 B 0 < A A 0 B B
20 19 an32s A B A 0 0 < A A 0 B B
21 addgtge0 A A B B 0 < A A 0 B B 0 < A A + B B
22 16 20 21 syl2an2r A B A 0 0 < A A + B B
23 msqge0 A 0 A A
24 msqgt0 B B 0 0 < B B
25 23 24 anim12i A B B 0 0 A A 0 < B B
26 25 anassrs A B B 0 0 A A 0 < B B
27 addgegt0 A A B B 0 A A 0 < B B 0 < A A + B B
28 16 26 27 syl2an2r A B B 0 0 < A A + B B
29 22 28 jaodan A B A 0 B 0 0 < A A + B B
30 11 29 sylan2 A B A + i B 0 0 < A A + B B
31 30 3impa A B A + i B 0 0 < A A + B B
32 31 gt0ne0d A B A + i B 0 A A + B B 0