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 \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 < C - B$

Proof

Step	Hyp	Ref	Expression
1		nnre	$⊢ A \in ℕ \to A \in ℝ$
2	1	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℝ$
3		nnne0	$⊢ A \in ℕ \to A \neq 0$
4	3	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \neq 0$
5	2 4	sqgt0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < A^{2}$
6	2	resqcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} \in ℝ$
7		nnre	$⊢ B \in ℕ \to B \in ℝ$
8	7	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℝ$
9	8	resqcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \in ℝ$
10	6 9	ltaddpos2d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (0 < A^{2} \leftrightarrow B^{2} < A^{2} + B^{2})$
11	5 10	mpbid	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} < A^{2} + B^{2}$
12	11	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B^{2} < A^{2} + B^{2}$
13		simpr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to A^{2} + B^{2} = C^{2}$
14	12 13	breqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B^{2} < C^{2}$
15	8	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B \in ℝ$
16		nnre	$⊢ C \in ℕ \to C \in ℝ$
17	16	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℝ$
18	17	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to C \in ℝ$
19		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
20	19	nn0ge0d	$⊢ B \in ℕ \to 0 \leq B$
21	20	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 \leq B$
22	21	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 \leq B$
23		nnnn0	$⊢ C \in ℕ \to C \in ℕ_{0}$
24	23	nn0ge0d	$⊢ C \in ℕ \to 0 \leq C$
25	24	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 \leq C$
26	25	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 \leq C$
27	15 18 22 26	lt2sqd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to (B < C \leftrightarrow B^{2} < C^{2})$
28	14 27	mpbird	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B < C$
29	15 18	posdifd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to (B < C \leftrightarrow 0 < C - B)$
30	28 29	mpbid	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 < C - B$

Metamath Proof Explorer

Theorem pythagtriplem10

Proof