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	$$⊢\phi \to A\in ℝ$$
	pythagreim.2	$$⊢\phi \to B\in ℝ$$
Assertion	pythagreim	$$⊢\phi \to {\left|B-\mathrm{i}A\right|}^2=A^2+B^2$$

Proof

Step	Hyp	Ref	Expression
1		pythagreim.1	$$⊢\phi \to A\in ℝ$$
2		pythagreim.2	$$⊢\phi \to B\in ℝ$$
3		cjreim2	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \overline{B-\mathrm{i}A}=B+\mathrm{i}A$$
4	2 1 3	syl2anc	$$⊢\phi \to \overline{B-\mathrm{i}A}=B+\mathrm{i}A$$
5	4	oveq2d	$$⊢\phi \to \left(B-\mathrm{i}A\right)\overline{B-\mathrm{i}A}=\left(B-\mathrm{i}A\right)\left(B+\mathrm{i}A\right)$$
6	2	recnd	$$⊢\phi \to B\in ℂ$$
7		ax-icn	$$⊢\mathrm{i}\in ℂ$$
8	7	a1i	$$⊢\phi \to \mathrm{i}\in ℂ$$
9	1	recnd	$$⊢\phi \to A\in ℂ$$
10	8 9	mulcld	$$⊢\phi \to \mathrm{i}A\in ℂ$$
11	6 10	subcld	$$⊢\phi \to B-\mathrm{i}A\in ℂ$$
12	6 10	addcld	$$⊢\phi \to B+\mathrm{i}A\in ℂ$$
13	11 12	mulcomd	$$⊢\phi \to \left(B-\mathrm{i}A\right)\left(B+\mathrm{i}A\right)=\left(B+\mathrm{i}A\right)\left(B-\mathrm{i}A\right)$$
14	5 13	eqtrd	$$⊢\phi \to \left(B-\mathrm{i}A\right)\overline{B-\mathrm{i}A}=\left(B+\mathrm{i}A\right)\left(B-\mathrm{i}A\right)$$
15	11	absvalsqd	$$⊢\phi \to {\left|B-\mathrm{i}A\right|}^2=\left(B-\mathrm{i}A\right)\overline{B-\mathrm{i}A}$$
16	8 9	sqmuld	$$⊢\phi \to {\mathrm{i}A}^2={\mathrm{i}}^2{A}^2$$
17		i2	$$⊢{\mathrm{i}}^2=-1$$
18	17	oveq1i	$$⊢{\mathrm{i}}^2{A}^2=-1A^2$$
19	16 18	eqtrdi	$$⊢\phi \to {\mathrm{i}A}^2=-1A^2$$
20	9	sqcld	$$⊢\phi \to A^2\in ℂ$$
21	20	mulm1d	$$⊢\phi \to -1A^2=-A^2$$
22	19 21	eqtrd	$$⊢\phi \to {\mathrm{i}A}^2=-A^2$$
23	22	oveq2d	$$⊢\phi \to B^2-{\mathrm{i}A}^2=B^2-\left(-A^2\right)$$
24	6	sqcld	$$⊢\phi \to B^2\in ℂ$$
25	24 20	subnegd	$$⊢\phi \to B^2-\left(-A^2\right)=B^2+A^2$$
26	24 20	addcomd	$$⊢\phi \to B^2+A^2=A^2+B^2$$
27	23 25 26	3eqtrd	$$⊢\phi \to B^2-{\mathrm{i}A}^2=A^2+B^2$$
28		subsq	$$⊢\left(B\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to B^2-{\mathrm{i}A}^2=\left(B+\mathrm{i}A\right)\left(B-\mathrm{i}A\right)$$
29	6 10 28	syl2anc	$$⊢\phi \to B^2-{\mathrm{i}A}^2=\left(B+\mathrm{i}A\right)\left(B-\mathrm{i}A\right)$$
30	27 29	eqtr3d	$$⊢\phi \to A^2+B^2=\left(B+\mathrm{i}A\right)\left(B-\mathrm{i}A\right)$$
31	14 15 30	3eqtr4d	$$⊢\phi \to {\left|B-\mathrm{i}A\right|}^2=A^2+B^2$$