This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> A e. RR )
pythagreim.2 
|- ( ph -> B e. RR )
Assertion pythagreim 
|- ( ph -> ( ( abs ` ( B - ( _i x. A ) ) ) ^ 2 ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 pythagreim.1 
 |-  ( ph -> A e. RR )
2 pythagreim.2 
 |-  ( ph -> B e. RR )
3 cjreim2 
 |-  ( ( B e. RR /\ A e. RR ) -> ( * ` ( B - ( _i x. A ) ) ) = ( B + ( _i x. A ) ) )
4 2 1 3 syl2anc 
 |-  ( ph -> ( * ` ( B - ( _i x. A ) ) ) = ( B + ( _i x. A ) ) )
5 4 oveq2d 
 |-  ( ph -> ( ( B - ( _i x. A ) ) x. ( * ` ( B - ( _i x. A ) ) ) ) = ( ( B - ( _i x. A ) ) x. ( B + ( _i x. A ) ) ) )
6 2 recnd 
 |-  ( ph -> B e. CC )
7 ax-icn 
 |-  _i e. CC
8 7 a1i 
 |-  ( ph -> _i e. CC )
9 1 recnd 
 |-  ( ph -> A e. CC )
10 8 9 mulcld 
 |-  ( ph -> ( _i x. A ) e. CC )
11 6 10 subcld 
 |-  ( ph -> ( B - ( _i x. A ) ) e. CC )
12 6 10 addcld 
 |-  ( ph -> ( B + ( _i x. A ) ) e. CC )
13 11 12 mulcomd 
 |-  ( ph -> ( ( B - ( _i x. A ) ) x. ( B + ( _i x. A ) ) ) = ( ( B + ( _i x. A ) ) x. ( B - ( _i x. A ) ) ) )
14 5 13 eqtrd 
 |-  ( ph -> ( ( B - ( _i x. A ) ) x. ( * ` ( B - ( _i x. A ) ) ) ) = ( ( B + ( _i x. A ) ) x. ( B - ( _i x. A ) ) ) )
15 11 absvalsqd 
 |-  ( ph -> ( ( abs ` ( B - ( _i x. A ) ) ) ^ 2 ) = ( ( B - ( _i x. A ) ) x. ( * ` ( B - ( _i x. A ) ) ) ) )
16 8 9 sqmuld 
 |-  ( ph -> ( ( _i x. A ) ^ 2 ) = ( ( _i ^ 2 ) x. ( A ^ 2 ) ) )
17 i2 
 |-  ( _i ^ 2 ) = -u 1
18 17 oveq1i 
 |-  ( ( _i ^ 2 ) x. ( A ^ 2 ) ) = ( -u 1 x. ( A ^ 2 ) )
19 16 18 eqtrdi 
 |-  ( ph -> ( ( _i x. A ) ^ 2 ) = ( -u 1 x. ( A ^ 2 ) ) )
20 9 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
21 20 mulm1d 
 |-  ( ph -> ( -u 1 x. ( A ^ 2 ) ) = -u ( A ^ 2 ) )
22 19 21 eqtrd 
 |-  ( ph -> ( ( _i x. A ) ^ 2 ) = -u ( A ^ 2 ) )
23 22 oveq2d 
 |-  ( ph -> ( ( B ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( ( B ^ 2 ) - -u ( A ^ 2 ) ) )
24 6 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
25 24 20 subnegd 
 |-  ( ph -> ( ( B ^ 2 ) - -u ( A ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) )
26 24 20 addcomd 
 |-  ( ph -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
27 23 25 26 3eqtrd 
 |-  ( ph -> ( ( B ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
28 subsq 
 |-  ( ( B e. CC /\ ( _i x. A ) e. CC ) -> ( ( B ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( ( B + ( _i x. A ) ) x. ( B - ( _i x. A ) ) ) )
29 6 10 28 syl2anc 
 |-  ( ph -> ( ( B ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( ( B + ( _i x. A ) ) x. ( B - ( _i x. A ) ) ) )
30 27 29 eqtr3d 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( B + ( _i x. A ) ) x. ( B - ( _i x. A ) ) ) )
31 14 15 30 3eqtr4d 
 |-  ( ph -> ( ( abs ` ( B - ( _i x. A ) ) ) ^ 2 ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )