Theorem axlowdimlem17 27049

Description: Lemma for axlowdim 27052. Establish a congruence result. (Contributed by Scott Fenton, 22-Apr-2013.) (Proof shortened by Mario Carneiro, 22-May-2014.)

Hypotheses

Ref	Expression
axlowdimlem16.1	⊢ 𝑃 = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
axlowdimlem16.2	⊢ 𝑄 = ({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))
axlowdimlem17.3	⊢ 𝐴 = ({⟨1, 𝑋⟩, ⟨2, 𝑌⟩} ∪ ((3...𝑁) × {0}))
axlowdimlem17.4	⊢ 𝑋 ∈ ℝ
axlowdimlem17.5	⊢ 𝑌 ∈ ℝ

Assertion

Ref	Expression
axlowdimlem17	⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → ⟨𝑃, 𝐴⟩Cgr⟨𝑄, 𝐴⟩)

Proof of Theorem axlowdimlem17

Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		uzuzle23 12485	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ (ℤ≥‘2))
2	1	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑁 ∈ (ℤ≥‘2))
3		fzss2 13152	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ≥‘2) → (1...2) ⊆ (1...𝑁))
4	2, 3	syl 17	. . . . . . . . . 10 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (1...2) ⊆ (1...𝑁))
5		simpr 488	. . . . . . . . . 10 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑖 ∈ (1...2))
6	4, 5	sseldd 3902	. . . . . . . . 9 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑖 ∈ (1...𝑁))
7		fznuz 13194	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...2) → ¬ 𝑖 ∈ (ℤ≥‘(2 + 1)))
8	7	adantl 485	. . . . . . . . . 10 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → ¬ 𝑖 ∈ (ℤ≥‘(2 + 1)))
9		3z 12210	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℤ
10		uzid 12453	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℤ → 3 ∈ (ℤ≥‘3))
11	9, 10	ax-mp 5	. . . . . . . . . . . . 13 ⊢ 3 ∈ (ℤ≥‘3)
12		df-3 11894	. . . . . . . . . . . . . 14 ⊢ 3 = (2 + 1)
13	12	fveq2i 6720	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘3) = (ℤ≥‘(2 + 1))
14	11, 13	eleqtri 2836	. . . . . . . . . . . 12 ⊢ 3 ∈ (ℤ≥‘(2 + 1))
15		eleq1 2825	. . . . . . . . . . . 12 ⊢ (𝑖 = 3 → (𝑖 ∈ (ℤ≥‘(2 + 1)) ↔ 3 ∈ (ℤ≥‘(2 + 1))))
16	14, 15	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑖 = 3 → 𝑖 ∈ (ℤ≥‘(2 + 1)))
17	16	necon3bi 2967	. . . . . . . . . 10 ⊢ (¬ 𝑖 ∈ (ℤ≥‘(2 + 1)) → 𝑖 ≠ 3)
18	8, 17	syl 17	. . . . . . . . 9 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑖 ≠ 3)
19		axlowdimlem16.1	. . . . . . . . . 10 ⊢ 𝑃 = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
20	19	axlowdimlem9 27041	. . . . . . . . 9 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ 3) → (𝑃‘𝑖) = 0)
21	6, 18, 20	syl2anc 587	. . . . . . . 8 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝑃‘𝑖) = 0)
22		elfzuz 13108	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ (ℤ≥‘2))
23	22	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝐼 ∈ (ℤ≥‘2))
24		eluzp1p1 12466	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ (ℤ≥‘2) → (𝐼 + 1) ∈ (ℤ≥‘(2 + 1)))
25	23, 24	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝐼 + 1) ∈ (ℤ≥‘(2 + 1)))
26		uzss 12461	. . . . . . . . . . . 12 ⊢ ((𝐼 + 1) ∈ (ℤ≥‘(2 + 1)) → (ℤ≥‘(𝐼 + 1)) ⊆ (ℤ≥‘(2 + 1)))
27	25, 26	syl 17	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (ℤ≥‘(𝐼 + 1)) ⊆ (ℤ≥‘(2 + 1)))
28	27, 8	ssneldd 3904	. . . . . . . . . 10 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → ¬ 𝑖 ∈ (ℤ≥‘(𝐼 + 1)))
29		eluzelz 12448	. . . . . . . . . . . . . 14 ⊢ ((𝐼 + 1) ∈ (ℤ≥‘(2 + 1)) → (𝐼 + 1) ∈ ℤ)
30	25, 29	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝐼 + 1) ∈ ℤ)
31		uzid 12453	. . . . . . . . . . . . 13 ⊢ ((𝐼 + 1) ∈ ℤ → (𝐼 + 1) ∈ (ℤ≥‘(𝐼 + 1)))
32	30, 31	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝐼 + 1) ∈ (ℤ≥‘(𝐼 + 1)))
33		eleq1 2825	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝐼 + 1) → (𝑖 ∈ (ℤ≥‘(𝐼 + 1)) ↔ (𝐼 + 1) ∈ (ℤ≥‘(𝐼 + 1))))
34	32, 33	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝑖 = (𝐼 + 1) → 𝑖 ∈ (ℤ≥‘(𝐼 + 1))))
35	34	necon3bd 2954	. . . . . . . . . 10 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (¬ 𝑖 ∈ (ℤ≥‘(𝐼 + 1)) → 𝑖 ≠ (𝐼 + 1)))
36	28, 35	mpd 15	. . . . . . . . 9 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → 𝑖 ≠ (𝐼 + 1))
37		axlowdimlem16.2	. . . . . . . . . 10 ⊢ 𝑄 = ({⟨(𝐼 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))
38	37	axlowdimlem12 27044	. . . . . . . . 9 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑖 ≠ (𝐼 + 1)) → (𝑄‘𝑖) = 0)
39	6, 36, 38	syl2anc 587	. . . . . . . 8 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝑄‘𝑖) = 0)
40	21, 39	eqtr4d 2780	. . . . . . 7 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (𝑃‘𝑖) = (𝑄‘𝑖))
41	40	oveq1d 7228	. . . . . 6 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → ((𝑃‘𝑖) − (𝐴‘𝑖)) = ((𝑄‘𝑖) − (𝐴‘𝑖)))
42	41	oveq1d 7228	. . . . 5 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...2)) → (((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = (((𝑄‘𝑖) − (𝐴‘𝑖))↑2))
43	42	sumeq2dv 15267	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (1...2)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (1...2)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2))
44	19, 37	axlowdimlem16 27048	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2))
45		axlowdimlem17.3	. . . . . . . . . . . . 13 ⊢ 𝐴 = ({⟨1, 𝑋⟩, ⟨2, 𝑌⟩} ∪ ((3...𝑁) × {0}))
46	45	fveq1i 6718	. . . . . . . . . . . 12 ⊢ (𝐴‘𝑖) = (({⟨1, 𝑋⟩, ⟨2, 𝑌⟩} ∪ ((3...𝑁) × {0}))‘𝑖)
47		axlowdimlem2 27034	. . . . . . . . . . . . 13 ⊢ ((1...2) ∩ (3...𝑁)) = ∅
48		axlowdimlem17.4	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ∈ ℝ
49		axlowdimlem17.5	. . . . . . . . . . . . . . . 16 ⊢ 𝑌 ∈ ℝ
50	48, 49	axlowdimlem4 27036	. . . . . . . . . . . . . . 15 ⊢ {⟨1, 𝑋⟩, ⟨2, 𝑌⟩}:(1...2)⟶ℝ
51		ffn 6545	. . . . . . . . . . . . . . 15 ⊢ ({⟨1, 𝑋⟩, ⟨2, 𝑌⟩}:(1...2)⟶ℝ → {⟨1, 𝑋⟩, ⟨2, 𝑌⟩} Fn (1...2))
52	50, 51	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ {⟨1, 𝑋⟩, ⟨2, 𝑌⟩} Fn (1...2)
53		axlowdimlem1 27033	. . . . . . . . . . . . . . 15 ⊢ ((3...𝑁) × {0}):(3...𝑁)⟶ℝ
54		ffn 6545	. . . . . . . . . . . . . . 15 ⊢ (((3...𝑁) × {0}):(3...𝑁)⟶ℝ → ((3...𝑁) × {0}) Fn (3...𝑁))
55	53, 54	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((3...𝑁) × {0}) Fn (3...𝑁)
56		fvun2 6803	. . . . . . . . . . . . . 14 ⊢ (({⟨1, 𝑋⟩, ⟨2, 𝑌⟩} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩ (3...𝑁)) = ∅ ∧ 𝑖 ∈ (3...𝑁))) → (({⟨1, 𝑋⟩, ⟨2, 𝑌⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = (((3...𝑁) × {0})‘𝑖))
57	52, 55, 56	mp3an12 1453	. . . . . . . . . . . . 13 ⊢ ((((1...2) ∩ (3...𝑁)) = ∅ ∧ 𝑖 ∈ (3...𝑁)) → (({⟨1, 𝑋⟩, ⟨2, 𝑌⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = (((3...𝑁) × {0})‘𝑖))
58	47, 57	mpan 690	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (3...𝑁) → (({⟨1, 𝑋⟩, ⟨2, 𝑌⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = (((3...𝑁) × {0})‘𝑖))
59	46, 58	syl5eq 2790	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (3...𝑁) → (𝐴‘𝑖) = (((3...𝑁) × {0})‘𝑖))
60		c0ex 10827	. . . . . . . . . . . 12 ⊢ 0 ∈ V
61	60	fvconst2 7019	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (3...𝑁) → (((3...𝑁) × {0})‘𝑖) = 0)
62	59, 61	eqtrd 2777	. . . . . . . . . 10 ⊢ (𝑖 ∈ (3...𝑁) → (𝐴‘𝑖) = 0)
63	62	adantl 485	. . . . . . . . 9 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝐴‘𝑖) = 0)
64	63	oveq2d 7229	. . . . . . . 8 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃‘𝑖) − (𝐴‘𝑖)) = ((𝑃‘𝑖) − 0))
65	19	axlowdimlem7 27039	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑃 ∈ (𝔼‘𝑁))
66	65	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
67		3nn 11909	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℕ
68		nnuz 12477	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ≥‘1)
69	67, 68	eleqtri 2836	. . . . . . . . . . . . 13 ⊢ 3 ∈ (ℤ≥‘1)
70		fzss1 13151	. . . . . . . . . . . . 13 ⊢ (3 ∈ (ℤ≥‘1) → (3...𝑁) ⊆ (1...𝑁))
71	69, 70	ax-mp 5	. . . . . . . . . . . 12 ⊢ (3...𝑁) ⊆ (1...𝑁)
72	71	sseli 3896	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (3...𝑁) → 𝑖 ∈ (1...𝑁))
73	72	adantl 485	. . . . . . . . . 10 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → 𝑖 ∈ (1...𝑁))
74		fveecn 26993	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ ℂ)
75	66, 73, 74	syl2anc 587	. . . . . . . . 9 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝑃‘𝑖) ∈ ℂ)
76	75	subid1d 11178	. . . . . . . 8 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃‘𝑖) − 0) = (𝑃‘𝑖))
77	64, 76	eqtrd 2777	. . . . . . 7 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑃‘𝑖) − (𝐴‘𝑖)) = (𝑃‘𝑖))
78	77	oveq1d 7228	. . . . . 6 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = ((𝑃‘𝑖)↑2))
79	78	sumeq2dv 15267	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (3...𝑁)((𝑃‘𝑖)↑2))
80	63	oveq2d 7229	. . . . . . . 8 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄‘𝑖) − (𝐴‘𝑖)) = ((𝑄‘𝑖) − 0))
81		eluzge3nn 12486	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ ℕ)
82		2eluzge1 12490	. . . . . . . . . . . . 13 ⊢ 2 ∈ (ℤ≥‘1)
83		fzss1 13151	. . . . . . . . . . . . 13 ⊢ (2 ∈ (ℤ≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
84	82, 83	ax-mp 5	. . . . . . . . . . . 12 ⊢ (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))
85	84	sseli 3896	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (2...(𝑁 − 1)) → 𝐼 ∈ (1...(𝑁 − 1)))
86	37	axlowdimlem10 27042	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁))
87	81, 85, 86	syl2an 599	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁))
88		fveecn 26993	. . . . . . . . . 10 ⊢ ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑄‘𝑖) ∈ ℂ)
89	87, 72, 88	syl2an 599	. . . . . . . . 9 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (𝑄‘𝑖) ∈ ℂ)
90	89	subid1d 11178	. . . . . . . 8 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄‘𝑖) − 0) = (𝑄‘𝑖))
91	80, 90	eqtrd 2777	. . . . . . 7 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → ((𝑄‘𝑖) − (𝐴‘𝑖)) = (𝑄‘𝑖))
92	91	oveq1d 7228	. . . . . 6 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (3...𝑁)) → (((𝑄‘𝑖) − (𝐴‘𝑖))↑2) = ((𝑄‘𝑖)↑2))
93	92	sumeq2dv 15267	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (3...𝑁)((𝑄‘𝑖)↑2))
94	44, 79, 93	3eqtr4d 2787	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (3...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (3...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2))
95	43, 94	oveq12d 7231	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (Σ𝑖 ∈ (1...2)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) + Σ𝑖 ∈ (3...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2)) = (Σ𝑖 ∈ (1...2)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2) + Σ𝑖 ∈ (3...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2)))
96	47	a1i 11	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → ((1...2) ∩ (3...𝑁)) = ∅)
97		eluzelre 12449	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ ℝ)
98		eluzle 12451	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘3) → 3 ≤ 𝑁)
99		2re 11904	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
100		3re 11910	. . . . . . . . . . . 12 ⊢ 3 ∈ ℝ
101		2lt3 12002	. . . . . . . . . . . 12 ⊢ 2 < 3
102	99, 100, 101	ltleii 10955	. . . . . . . . . . 11 ⊢ 2 ≤ 3
103		letr 10926	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 ≤ 3 ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁))
104	99, 100, 103	mp3an12 1453	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → ((2 ≤ 3 ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁))
105	102, 104	mpani 696	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ → (3 ≤ 𝑁 → 2 ≤ 𝑁))
106	97, 98, 105	sylc 65	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘3) → 2 ≤ 𝑁)
107		1le2 12039	. . . . . . . . 9 ⊢ 1 ≤ 2
108	106, 107	jctil 523	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘3) → (1 ≤ 2 ∧ 2 ≤ 𝑁))
109	108	adantr 484	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1 ≤ 2 ∧ 2 ≤ 𝑁))
110		eluzelz 12448	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ ℤ)
111	110	adantr 484	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑁 ∈ ℤ)
112		2z 12209	. . . . . . . . 9 ⊢ 2 ∈ ℤ
113		1z 12207	. . . . . . . . 9 ⊢ 1 ∈ ℤ
114		elfz 13101	. . . . . . . . 9 ⊢ ((2 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
115	112, 113, 114	mp3an12 1453	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
116	111, 115	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (2 ∈ (1...𝑁) ↔ (1 ≤ 2 ∧ 2 ≤ 𝑁)))
117	109, 116	mpbird 260	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 2 ∈ (1...𝑁))
118		fzsplit 13138	. . . . . 6 ⊢ (2 ∈ (1...𝑁) → (1...𝑁) = ((1...2) ∪ ((2 + 1)...𝑁)))
119	117, 118	syl 17	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1...𝑁) = ((1...2) ∪ ((2 + 1)...𝑁)))
120	12	oveq1i 7223	. . . . . 6 ⊢ (3...𝑁) = ((2 + 1)...𝑁)
121	120	uneq2i 4074	. . . . 5 ⊢ ((1...2) ∪ (3...𝑁)) = ((1...2) ∪ ((2 + 1)...𝑁))
122	119, 121	eqtr4di 2796	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1...𝑁) = ((1...2) ∪ (3...𝑁)))
123		fzfid 13546	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (1...𝑁) ∈ Fin)
124	65	ad2antrr 726	. . . . . . 7 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑃 ∈ (𝔼‘𝑁))
125	124, 74	sylancom 591	. . . . . 6 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ ℂ)
126	48, 49	axlowdimlem5 27037	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘2) → ({⟨1, 𝑋⟩, ⟨2, 𝑌⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
127	45, 126	eqeltrid 2842	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘2) → 𝐴 ∈ (𝔼‘𝑁))
128	1, 127	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝐴 ∈ (𝔼‘𝑁))
129	128	ad2antrr 726	. . . . . . 7 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
130		fveecn 26993	. . . . . . 7 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
131	129, 130	sylancom 591	. . . . . 6 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
132	125, 131	subcld 11189	. . . . 5 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑃‘𝑖) − (𝐴‘𝑖)) ∈ ℂ)
133	132	sqcld 13714	. . . 4 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑃‘𝑖) − (𝐴‘𝑖))↑2) ∈ ℂ)
134	96, 122, 123, 133	fsumsplit 15305	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (1...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = (Σ𝑖 ∈ (1...2)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) + Σ𝑖 ∈ (3...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2)))
135	87, 88	sylan 583	. . . . . 6 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑄‘𝑖) ∈ ℂ)
136	135, 131	subcld 11189	. . . . 5 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑄‘𝑖) − (𝐴‘𝑖)) ∈ ℂ)
137	136	sqcld 13714	. . . 4 ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑄‘𝑖) − (𝐴‘𝑖))↑2) ∈ ℂ)
138	96, 122, 123, 137	fsumsplit 15305	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (1...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2) = (Σ𝑖 ∈ (1...2)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2) + Σ𝑖 ∈ (3...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2)))
139	95, 134, 138	3eqtr4d 2787	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → Σ𝑖 ∈ (1...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2))
140	65	adantr 484	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝑃 ∈ (𝔼‘𝑁))
141	128	adantr 484	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → 𝐴 ∈ (𝔼‘𝑁))
142		brcgr 26991	. . 3 ⊢ (((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))) → (⟨𝑃, 𝐴⟩Cgr⟨𝑄, 𝐴⟩ ↔ Σ𝑖 ∈ (1...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2)))
143	140, 141, 87, 141, 142	syl22anc 839	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → (⟨𝑃, 𝐴⟩Cgr⟨𝑄, 𝐴⟩ ↔ Σ𝑖 ∈ (1...𝑁)(((𝑃‘𝑖) − (𝐴‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝑄‘𝑖) − (𝐴‘𝑖))↑2)))
144	139, 143	mpbird 260	1 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐼 ∈ (2...(𝑁 − 1))) → ⟨𝑃, 𝐴⟩Cgr⟨𝑄, 𝐴⟩)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110   ≠ wne 2940   ∖ cdif 3863   ∪ cun 3864   ∩ cin 3865   ⊆ wss 3866  ∅c0 4237  {csn 4541  {cpr 4543  ⟨cop 4547   class class class wbr 5053   × cxp 5549   Fn wfn 6375  ⟶wf 6376  ‘cfv 6380  (class class class)co 7213  ℂcc 10727  ℝcr 10728  0cc0 10729  1c1 10730   + caddc 10732   ≤ cle 10868   − cmin 11062  -cneg 11063  ℕcn 11830  2c2 11885  3c3 11886  ℤcz 12176  ℤ_≥cuz 12438  ...cfz 13095  ↑cexp 13635  Σcsu 15249  𝔼cee 26979  Cgrccgr 26981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-sup 9058  df-oi 9126  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-rp 12587  df-fz 13096  df-fzo 13239  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-clim 15049  df-sum 15250  df-ee 26982  df-cgr 26984

This theorem is referenced by:  axlowdim  27052