Metamath Proof Explorer

Theorem 2sqreulem3

Description: Lemma 3 for 2sqreu etc. (Contributed by AV, 25-Jun-2023)

Ref Expression
Assertion 2sqreulem3 ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ) → ( ( ( 𝜑 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 ) ∧ ( 𝜓 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ) ) → 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( 𝑃 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
2 1 eqcoms ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
3 2 adantl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
4 eqcom ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) )
5 2sqreulem2 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) → 𝐵 = 𝐶 ) )
6 4 5 syl5bi ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) → 𝐵 = 𝐶 ) )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) → 𝐵 = 𝐶 ) )
8 3 7 sylbid ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 → 𝐵 = 𝐶 ) )
9 8 adantld ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 ) → ( ( 𝜓 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ) → 𝐵 = 𝐶 ) )
10 9 ex ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 → ( ( 𝜓 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ) → 𝐵 = 𝐶 ) ) )
11 10 adantld ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝜑 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 ) → ( ( 𝜓 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ) → 𝐵 = 𝐶 ) ) )
12 11 impd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( 𝜑 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 ) ∧ ( 𝜓 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ) ) → 𝐵 = 𝐶 ) )
13 12 3expb ⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ) → ( ( ( 𝜑 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 ) ∧ ( 𝜓 ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 ) ) → 𝐵 = 𝐶 ) )