Metamath Proof Explorer

Theorem pythagtriplem10

Description: Lemma for pythagtrip . Show that C - B is positive. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem10 
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C - B ) )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( A e. NN -> A e. RR )
2 1 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. RR )
3 nnne0 
 |-  ( A e. NN -> A =/= 0 )
4 3 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A =/= 0 )
5 2 4 sqgt0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( A ^ 2 ) )
6 2 resqcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. RR )
7 nnre 
 |-  ( B e. NN -> B e. RR )
8 7 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. RR )
9 8 resqcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. RR )
10 6 9 ltaddpos2d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( 0 < ( A ^ 2 ) <-> ( B ^ 2 ) < ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
11 5 10 mpbid 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) < ( ( A ^ 2 ) + ( B ^ 2 ) ) )
12 11 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( B ^ 2 ) < ( ( A ^ 2 ) + ( B ^ 2 ) ) )
13 simpr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
14 12 13 breqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( B ^ 2 ) < ( C ^ 2 ) )
15 8 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> B e. RR )
16 nnre 
 |-  ( C e. NN -> C e. RR )
17 16 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. RR )
18 17 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> C e. RR )
19 nnnn0 
 |-  ( B e. NN -> B e. NN0 )
20 19 nn0ge0d 
 |-  ( B e. NN -> 0 <_ B )
21 20 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 <_ B )
22 21 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 <_ B )
23 nnnn0 
 |-  ( C e. NN -> C e. NN0 )
24 23 nn0ge0d 
 |-  ( C e. NN -> 0 <_ C )
25 24 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 <_ C )
26 25 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 <_ C )
27 15 18 22 26 lt2sqd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( B < C <-> ( B ^ 2 ) < ( C ^ 2 ) ) )
28 14 27 mpbird 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> B < C )
29 15 18 posdifd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( B < C <-> 0 < ( C - B ) ) )
30 28 29 mpbid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C - B ) )