Metamath Proof Explorer

Theorem pythagreim

Description: A simplified version of the Pythagorean theorem, where the points A and B respectively lie on the imaginary and real axes, and the right angle is at the origin. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Hypotheses pythagreim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
pythagreim.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion pythagreim ( 𝜑 → ( ( abs ‘ ( 𝐵 − ( i · 𝐴 ) ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 pythagreim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 pythagreim.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 cjreim2 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ∗ ‘ ( 𝐵 − ( i · 𝐴 ) ) ) = ( 𝐵 + ( i · 𝐴 ) ) )
4 2 1 3 syl2anc ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − ( i · 𝐴 ) ) ) = ( 𝐵 + ( i · 𝐴 ) ) )
5 4 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 − ( i · 𝐴 ) ) · ( ∗ ‘ ( 𝐵 − ( i · 𝐴 ) ) ) ) = ( ( 𝐵 − ( i · 𝐴 ) ) · ( 𝐵 + ( i · 𝐴 ) ) ) )
6 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7 ax-icn ⊢ i ∈ ℂ
8 7 a1i ⊢ ( 𝜑 → i ∈ ℂ )
9 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
10 8 9 mulcld ⊢ ( 𝜑 → ( i · 𝐴 ) ∈ ℂ )
11 6 10 subcld ⊢ ( 𝜑 → ( 𝐵 − ( i · 𝐴 ) ) ∈ ℂ )
12 6 10 addcld ⊢ ( 𝜑 → ( 𝐵 + ( i · 𝐴 ) ) ∈ ℂ )
13 11 12 mulcomd ⊢ ( 𝜑 → ( ( 𝐵 − ( i · 𝐴 ) ) · ( 𝐵 + ( i · 𝐴 ) ) ) = ( ( 𝐵 + ( i · 𝐴 ) ) · ( 𝐵 − ( i · 𝐴 ) ) ) )
14 5 13 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 − ( i · 𝐴 ) ) · ( ∗ ‘ ( 𝐵 − ( i · 𝐴 ) ) ) ) = ( ( 𝐵 + ( i · 𝐴 ) ) · ( 𝐵 − ( i · 𝐴 ) ) ) )
15 11 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − ( i · 𝐴 ) ) ) ↑ 2 ) = ( ( 𝐵 − ( i · 𝐴 ) ) · ( ∗ ‘ ( 𝐵 − ( i · 𝐴 ) ) ) ) )
16 8 9 sqmuld ⊢ ( 𝜑 → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
17 i2 ⊢ ( i ↑ 2 ) = - 1
18 17 oveq1i ⊢ ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) )
19 16 18 eqtrdi ⊢ ( 𝜑 → ( ( i · 𝐴 ) ↑ 2 ) = ( - 1 · ( 𝐴 ↑ 2 ) ) )
20 9 sqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
21 20 mulm1d ⊢ ( 𝜑 → ( - 1 · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
22 19 21 eqtrd ⊢ ( 𝜑 → ( ( i · 𝐴 ) ↑ 2 ) = - ( 𝐴 ↑ 2 ) )
23 22 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) − - ( 𝐴 ↑ 2 ) ) )
24 6 sqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
25 24 20 subnegd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − - ( 𝐴 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
26 24 20 addcomd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
27 23 25 26 3eqtrd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
28 subsq ⊢ ( ( 𝐵 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ( 𝐵 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 𝐵 + ( i · 𝐴 ) ) · ( 𝐵 − ( i · 𝐴 ) ) ) )
29 6 10 28 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 𝐵 + ( i · 𝐴 ) ) · ( 𝐵 − ( i · 𝐴 ) ) ) )
30 27 29 eqtr3d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 + ( i · 𝐴 ) ) · ( 𝐵 − ( i · 𝐴 ) ) ) )
31 14 15 30 3eqtr4d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − ( i · 𝐴 ) ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )