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 ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → 0 < C − B

Proof

Step Hyp Ref Expression
1 nnre ⊢ A ∈ ℕ → A ∈ ℝ
2 1 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A ∈ ℝ
3 nnne0 ⊢ A ∈ ℕ → A ≠ 0
4 3 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A ≠ 0
5 2 4 sqgt0d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → 0 < A 2
6 2 resqcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A 2 ∈ ℝ
7 nnre ⊢ B ∈ ℕ → B ∈ ℝ
8 7 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B ∈ ℝ
9 8 resqcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B 2 ∈ ℝ
10 6 9 ltaddpos2d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → 0 < A 2 ↔ B 2 < A 2 + B 2
11 5 10 mpbid ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → B 2 < A 2 + B 2
12 11 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → B 2 < A 2 + B 2
13 simpr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → A 2 + B 2 = C 2
14 12 13 breqtrd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → B 2 < C 2
15 8 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → B ∈ ℝ
16 nnre ⊢ C ∈ ℕ → C ∈ ℝ
17 16 3ad2ant3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C ∈ ℝ
18 17 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → C ∈ ℝ
19 nnnn0 ⊢ B ∈ ℕ → B ∈ ℕ 0
20 19 nn0ge0d ⊢ B ∈ ℕ → 0 ≤ B
21 20 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → 0 ≤ B
22 21 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → 0 ≤ B
23 nnnn0 ⊢ C ∈ ℕ → C ∈ ℕ 0
24 23 nn0ge0d ⊢ C ∈ ℕ → 0 ≤ C
25 24 3ad2ant3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → 0 ≤ C
26 25 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → 0 ≤ C
27 15 18 22 26 lt2sqd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → B < C ↔ B 2 < C 2
28 14 27 mpbird ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → B < C
29 15 18 posdifd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → B < C ↔ 0 < C − B
30 28 29 mpbid ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 → 0 < C − B