ip1ilem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ip1ilem		Structured version Visualization version GIF version

Theorem ip1ilem 31455

Description: Lemma for ip1i 31456. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
ip1i.1	⊢ 𝑋 = (BaseSet‘𝑈)
ip1i.2	⊢ 𝐺 = ( +_𝑣 ‘𝑈)
ip1i.4	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
ip1i.7	⊢ 𝑃 = (·_𝑖OLD‘𝑈)
ip1i.9	⊢ 𝑈 ∈ CPreHil_OLD
ip1i.a	⊢ 𝐴 ∈ 𝑋
ip1i.b	⊢ 𝐵 ∈ 𝑋
ip1i.c	⊢ 𝐶 ∈ 𝑋
ip1i.6	⊢ 𝑁 = (norm_CV‘𝑈)
ip0i.j	⊢ 𝐽 ∈ ℂ

**Assertion**
Ref	Expression
ip1ilem	⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))

**Proof of Theorem ip1ilem**
Step	Hyp	Ref	Expression
1		ip1i.9	. . . . . . 7 ⊢ 𝑈 ∈ CPreHil_OLD
2	1	phnvi 31445	. . . . . 6 ⊢ 𝑈 ∈ NrmCVec
3		ip1i.a	. . . . . 6 ⊢ 𝐴 ∈ 𝑋
4		ip1i.c	. . . . . 6 ⊢ 𝐶 ∈ 𝑋
5		ip1i.1	. . . . . . 7 ⊢ 𝑋 = (BaseSet‘𝑈)
6		ip1i.2	. . . . . . 7 ⊢ 𝐺 = ( +_𝑣 ‘𝑈)
7		ip1i.4	. . . . . . 7 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
8		ip1i.6	. . . . . . 7 ⊢ 𝑁 = (norm_CV‘𝑈)
9		ip1i.7	. . . . . . 7 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
10	5, 6, 7, 8, 9	4ipval2 31337	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2)))))
11	2, 3, 4, 10	mp3an 1491	. . . . 5 ⊢ (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2))))
12	11	oveq2i 7451	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2)))))
13		2cn 12442	. . . . 5 ⊢ 2 ∈ ℂ
14		4cn 12452	. . . . 5 ⊢ 4 ∈ ℂ
15	5, 9	dipcl 31341	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑃𝐶) ∈ ℂ)
16	2, 3, 4, 15	mp3an 1491	. . . . 5 ⊢ (𝐴𝑃𝐶) ∈ ℂ
17	13, 14, 16	mul12i 11529	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
18	5, 6	nvgcl 31249	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝐺𝐶) ∈ 𝑋)
19	2, 3, 4, 18	mp3an 1491	. . . . . . . . . . 11 ⊢ (𝐴𝐺𝐶) ∈ 𝑋
20	5, 8, 2, 19	nvcli 31291	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺𝐶)) ∈ ℝ
21	20	resqcli 14353	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℝ
22	21	recni 11347	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℂ
23		ax-1cn 11282	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
24	23	negcli 11650	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℂ
25	5, 7	nvscl 31255	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐶 ∈ 𝑋) → ( -1𝑆𝐶) ∈ 𝑋)
26	2, 24, 4, 25	mp3an 1491	. . . . . . . . . . . 12 ⊢ ( -1𝑆𝐶) ∈ 𝑋
27	5, 6	nvgcl 31249	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( -1𝑆𝐶) ∈ 𝑋) → (𝐴𝐺( -1𝑆𝐶)) ∈ 𝑋)
28	2, 3, 26, 27	mp3an 1491	. . . . . . . . . . 11 ⊢ (𝐴𝐺( -1𝑆𝐶)) ∈ 𝑋
29	5, 8, 2, 28	nvcli 31291	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺( -1𝑆𝐶))) ∈ ℝ
30	29	resqcli 14353	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2) ∈ ℝ
31	30	recni 11347	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2) ∈ ℂ
32	22, 31	subcli 11658	. . . . . . 7 ⊢ (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)) ∈ ℂ
33		ax-icn 11283	. . . . . . . 8 ⊢ i ∈ ℂ
34	5, 7	nvscl 31255	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (i𝑆𝐶) ∈ 𝑋)
35	2, 33, 4, 34	mp3an 1491	. . . . . . . . . . . . 13 ⊢ (i𝑆𝐶) ∈ 𝑋
36	5, 6	nvgcl 31249	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋)
37	2, 3, 35, 36	mp3an 1491	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋
38	5, 8, 2, 37	nvcli 31291	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(i𝑆𝐶))) ∈ ℝ
39	38	resqcli 14353	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℝ
40	39	recni 11347	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℂ
41	33	negcli 11650	. . . . . . . . . . . . . 14 ⊢ -i ∈ ℂ
42	5, 7	nvscl 31255	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → ( -i𝑆𝐶) ∈ 𝑋)
43	2, 41, 4, 42	mp3an 1491	. . . . . . . . . . . . 13 ⊢ ( -i𝑆𝐶) ∈ 𝑋
44	5, 6	nvgcl 31249	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( -i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺( -i𝑆𝐶)) ∈ 𝑋)
45	2, 3, 43, 44	mp3an 1491	. . . . . . . . . . . 12 ⊢ (𝐴𝐺( -i𝑆𝐶)) ∈ 𝑋
46	5, 8, 2, 45	nvcli 31291	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺( -i𝑆𝐶))) ∈ ℝ
47	46	resqcli 14353	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2) ∈ ℝ
48	47	recni 11347	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2) ∈ ℂ
49	40, 48	subcli 11658	. . . . . . . 8 ⊢ (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2)) ∈ ℂ
50	33, 49	mulcli 11340	. . . . . . 7 ⊢ (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2))) ∈ ℂ
51	13, 32, 50	adddii 11345	. . . . . 6 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2))))) = ((2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2))) + (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2)))))
52		ip1i.b	. . . . . . . . 9 ⊢ 𝐵 ∈ 𝑋
53	5, 6, 7, 9, 1, 3, 52, 4, 8, 23	ip0i 31454	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)))
54	5, 7	nvsid 31256	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋) → (1𝑆𝐶) = 𝐶)
55	2, 4, 54	mp2an 705	. . . . . . . . . . . . 13 ⊢ (1𝑆𝐶) = 𝐶
56	55	oveq2i 7451	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺𝐵)𝐺(1𝑆𝐶)) = ((𝐴𝐺𝐵)𝐺𝐶)
57	56	fveq2i 6908	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺𝐵)𝐺𝐶))
58	57	oveq1i 7450	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2)
59	58	oveq1i 7450	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2))
60	55	oveq2i 7451	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺( -1𝑆𝐵))𝐺(1𝑆𝐶)) = ((𝐴𝐺( -1𝑆𝐵))𝐺𝐶)
61	60	fveq2i 6908	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))
62	61	oveq1i 7450	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2)
63	62	oveq1i 7450	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2))
64	59, 63	oveq12i 7452	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2))) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2)))
65	55	oveq2i 7451	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(1𝑆𝐶)) = (𝐴𝐺𝐶)
66	65	fveq2i 6908	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(1𝑆𝐶))) = (𝑁‘(𝐴𝐺𝐶))
67	66	oveq1i 7450	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) = ((𝑁‘(𝐴𝐺𝐶))↑2)
68	67	oveq1i 7450	. . . . . . . . 9 ⊢ (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)) = (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2))
69	68	oveq2i 7451	. . . . . . . 8 ⊢ (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)))
70	53, 64, 69	3eqtr3i 2794	. . . . . . 7 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)))
71	5, 6, 7, 9, 1, 3, 52, 4, 8, 33	ip0i 31454	. . . . . . . . 9 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2)))
72	71	oveq2i 7451	. . . . . . . 8 ⊢ (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2)))) = (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2))))
73	5, 6	nvgcl 31249	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
74	2, 3, 52, 73	mp3an 1491	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺𝐵) ∈ 𝑋
75	5, 6	nvgcl 31249	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋)
76	2, 74, 35, 75	mp3an 1491	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋
77	5, 8, 2, 76	nvcli 31291	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶))) ∈ ℝ
78	77	resqcli 14353	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℝ
79	78	recni 11347	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℂ
80	5, 6	nvgcl 31249	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ( -i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)) ∈ 𝑋)
81	2, 74, 43, 80	mp3an 1491	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)) ∈ 𝑋
82	5, 8, 2, 81	nvcli 31291	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶))) ∈ ℝ
83	82	resqcli 14353	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2) ∈ ℝ
84	83	recni 11347	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2) ∈ ℂ
85	79, 84	subcli 11658	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2)) ∈ ℂ
86	5, 7	nvscl 31255	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → ( -1𝑆𝐵) ∈ 𝑋)
87	2, 24, 52, 86	mp3an 1491	. . . . . . . . . . . . . . 15 ⊢ ( -1𝑆𝐵) ∈ 𝑋
88	5, 6	nvgcl 31249	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( -1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺( -1𝑆𝐵)) ∈ 𝑋)
89	2, 3, 87, 88	mp3an 1491	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺( -1𝑆𝐵)) ∈ 𝑋
90	5, 6	nvgcl 31249	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺( -1𝑆𝐵)) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋)
91	2, 89, 35, 90	mp3an 1491	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋
92	5, 8, 2, 91	nvcli 31291	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶))) ∈ ℝ
93	92	resqcli 14353	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℝ
94	93	recni 11347	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℂ
95	5, 6	nvgcl 31249	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺( -1𝑆𝐵)) ∈ 𝑋 ∧ ( -i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)) ∈ 𝑋)
96	2, 89, 43, 95	mp3an 1491	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)) ∈ 𝑋
97	5, 8, 2, 96	nvcli 31291	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶))) ∈ ℝ
98	97	resqcli 14353	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2) ∈ ℝ
99	98	recni 11347	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2) ∈ ℂ
100	94, 99	subcli 11658	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2)) ∈ ℂ
101	33, 85, 100	adddii 11345	. . . . . . . 8 ⊢ (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2)))) = ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2))))
102	33, 13, 49	mul12i 11529	. . . . . . . 8 ⊢ (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2))))
103	72, 101, 102	3eqtr3i 2794	. . . . . . 7 ⊢ ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2))))
104	70, 103	oveq12i 7452	. . . . . 6 ⊢ (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2))))) = ((2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2))) + (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2)))))
105	51, 104	eqtr4i 2789	. . . . 5 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2))))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2)))))
106	5, 6	nvgcl 31249	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋)
107	2, 74, 4, 106	mp3an 1491	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋
108	5, 8, 2, 107	nvcli 31291	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺𝐶)) ∈ ℝ
109	108	resqcli 14353	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℝ
110	109	recni 11347	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℂ
111	5, 6	nvgcl 31249	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ( -1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)) ∈ 𝑋)
112	2, 74, 26, 111	mp3an 1491	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)) ∈ 𝑋
113	5, 8, 2, 112	nvcli 31291	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶))) ∈ ℝ
114	113	resqcli 14353	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2) ∈ ℝ
115	114	recni 11347	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2) ∈ ℂ
116	110, 115	subcli 11658	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) ∈ ℂ
117	5, 6	nvgcl 31249	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺( -1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺( -1𝑆𝐵))𝐺𝐶) ∈ 𝑋)
118	2, 89, 4, 117	mp3an 1491	. . . . . . . . . 10 ⊢ ((𝐴𝐺( -1𝑆𝐵))𝐺𝐶) ∈ 𝑋
119	5, 8, 2, 118	nvcli 31291	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶)) ∈ ℝ
120	119	resqcli 14353	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) ∈ ℝ
121	120	recni 11347	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) ∈ ℂ
122	5, 6	nvgcl 31249	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺( -1𝑆𝐵)) ∈ 𝑋 ∧ ( -1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)) ∈ 𝑋)
123	2, 89, 26, 122	mp3an 1491	. . . . . . . . . 10 ⊢ ((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)) ∈ 𝑋
124	5, 8, 2, 123	nvcli 31291	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶))) ∈ ℝ
125	124	resqcli 14353	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2) ∈ ℝ
126	125	recni 11347	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2) ∈ ℂ
127	121, 126	subcli 11658	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2)) ∈ ℂ
128	33, 85	mulcli 11340	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2))) ∈ ℂ
129	33, 100	mulcli 11340	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2))) ∈ ℂ
130	116, 127, 128, 129	add4i 11559	. . . . 5 ⊢ (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2))))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2)))))
131	5, 9	dipcl 31341	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ)
132	2, 74, 4, 131	mp3an 1491	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ
133	5, 9	dipcl 31341	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺( -1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶) ∈ ℂ)
134	2, 89, 4, 133	mp3an 1491	. . . . . . 7 ⊢ ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶) ∈ ℂ
135	14, 132, 134	adddii 11345	. . . . . 6 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶))) = ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)))
136	5, 6, 7, 8, 9	4ipval2 31337	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2)))))
137	2, 74, 4, 136	mp3an 1491	. . . . . . 7 ⊢ (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2))))
138	5, 6, 7, 8, 9	4ipval2 31337	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺( -1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2)))))
139	2, 89, 4, 138	mp3an 1491	. . . . . . 7 ⊢ (4 · ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2))))
140	137, 139	oveq12i 7452	. . . . . 6 ⊢ ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2)))))
141	135, 140	eqtr2i 2787	. . . . 5 ⊢ (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)))
142	105, 130, 141	3eqtri 2790	. . . 4 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)))
143	12, 17, 142	3eqtr3ri 2795	. . 3 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
144	143	oveq1i 7450	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶))) / 4) = ((4 · (2 · (𝐴𝑃𝐶))) / 4)
145	132, 134	addcli 11339	. . 3 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)) ∈ ℂ
146		4ne0 12478	. . 3 ⊢ 4 ≠ 0
147	145, 14, 146	divcan3i 12087	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶))) / 4) = (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶))
148	13, 16	mulcli 11340	. . 3 ⊢ (2 · (𝐴𝑃𝐶)) ∈ ℂ
149	148, 14, 146	divcan3i 12087	. 2 ⊢ ((4 · (2 · (𝐴𝑃𝐶))) / 4) = (2 · (𝐴𝑃𝐶))
150	144, 147, 149	3eqtr3i 2794	1 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 ∈ wcel 2147 ‘cfv 6555 (class class class)co 7440 ℂcc 11222 1c1 11225 ici 11226 + caddc 11227 · cmul 11229 − cmin 11565 -cneg 11566 / cdiv 11997 2c2 12421 4c4 12423 ↑cexp 14228 NrmCVeccnv 31213 +_𝑣 cpv 31214 BaseSetcba 31215 ·_𝑠OLD cns 31216 norm_CVcnmcv 31219 ·_𝑖OLDcdip 31329 CPreHil_OLDccphlo 31441

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-inf2 9666 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-er 8742 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-sup 9458 df-oi 9528 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-n0 12631 df-z 12718 df-uz 12990 df-rp 13145 df-fz 13664 df-fzo 13813 df-seq 14169 df-exp 14229 df-hash 14499 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-clim 15681 df-sum 15880 df-grpo 31122 df-ablo 31174 df-vc 31188 df-nv 31221 df-va 31224 df-ba 31225 df-sm 31226 df-0v 31227 df-nmcv 31229 df-dip 31330 df-ph 31442

This theorem is used by: ip1i 31456

W3C validator