Theorem veronesevrowd

Description: The Veronese map at a point, expressed explicitly as a piecewise maps-to function on the six coordinates. (Contributed by Jiamin Zhao, 17-Aug-2026)

	Ref	Expression
Hypothesis	veronesevrow.1	$$⊢\phi \to P\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	veronesevrowd	Could not format assertion : No typesetting found for |- ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		veronesevrow.1	$$⊢\phi \to P\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		ovex	$$⊢\left(if\left(k=1,{P\left(1\right)}^2,0\right)+if\left(k=2,{P\left(2\right)}^2,0\right)\right)+if\left(k=3,{P\left(3\right)}^2,0\right)+\left(if\left(k=4,P\left(1\right)P\left(2\right),0\right)+if\left(k=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(k=6,P\left(3\right)P\left(1\right),0\right)\in \mathrm{V}$$
3		eqid	$$⊢\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{P\left(1\right)}^2,0\right)+if\left(k=2,{P\left(2\right)}^2,0\right)\right)+if\left(k=3,{P\left(3\right)}^2,0\right)+\left(if\left(k=4,P\left(1\right)P\left(2\right),0\right)+if\left(k=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(k=6,P\left(3\right)P\left(1\right),0\right)\right)=\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{P\left(1\right)}^2,0\right)+if\left(k=2,{P\left(2\right)}^2,0\right)\right)+if\left(k=3,{P\left(3\right)}^2,0\right)+\left(if\left(k=4,P\left(1\right)P\left(2\right),0\right)+if\left(k=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(k=6,P\left(3\right)P\left(1\right),0\right)\right)$$
4	2 3	fnmpti	$$⊢\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{P\left(1\right)}^2,0\right)+if\left(k=2,{P\left(2\right)}^2,0\right)\right)+if\left(k=3,{P\left(3\right)}^2,0\right)+\left(if\left(k=4,P\left(1\right)P\left(2\right),0\right)+if\left(k=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(k=6,P\left(3\right)P\left(1\right),0\right)\right)Fn\left(1\dots 6\right)$$
5	1	veronesevald	Could not format ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) : No typesetting found for |- ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) with typecode |-
6	5	fneq1d	Could not format ( ph -> ( ( veronese ` P ) Fn ( 1 ... 6 ) <-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) Fn ( 1 ... 6 ) ) ) : No typesetting found for |- ( ph -> ( ( veronese ` P ) Fn ( 1 ... 6 ) <-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) Fn ( 1 ... 6 ) ) ) with typecode |-
7	4 6	mpbiri	Could not format ( ph -> ( veronese ` P ) Fn ( 1 ... 6 ) ) : No typesetting found for |- ( ph -> ( veronese ` P ) Fn ( 1 ... 6 ) ) with typecode |-
8		ovex	$$⊢{P\left(1\right)}^2\in \mathrm{V}$$
9		ovex	$$⊢{P\left(2\right)}^2\in \mathrm{V}$$
10		ovex	$$⊢{P\left(3\right)}^2\in \mathrm{V}$$
11		ovex	$$⊢P\left(1\right)P\left(2\right)\in \mathrm{V}$$
12		ovex	$$⊢P\left(2\right)P\left(3\right)\in \mathrm{V}$$
13		ovex	$$⊢P\left(3\right)P\left(1\right)\in \mathrm{V}$$
14	12 13	ifex	$$⊢if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\in \mathrm{V}$$
15	11 14	ifex	$$⊢if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\in \mathrm{V}$$
16	10 15	ifex	$$⊢if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\in \mathrm{V}$$
17	9 16	ifex	$$⊢if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\in \mathrm{V}$$
18	8 17	ifex	$$⊢if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\in \mathrm{V}$$
19		eqid	$$⊢\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)=\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)$$
20	18 19	fnmpti	$$⊢\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)Fn\left(1\dots 6\right)$$
21	20	a1i	$$⊢\phi \to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)Fn\left(1\dots 6\right)$$
22	1	veronesev1lem	Could not format ( ph -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) ) : No typesetting found for |- ( ph -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) ) with typecode |-
23	22	ad2antrr	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) ) with typecode |-
24		simpr	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=1\right)\to x=1$$
25	24	fveq2d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 1 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 1 ) ) with typecode |-
26	24	fveq2d	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=1\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(1\right)$$
27		1nn	$$⊢1\in \mathbb{N}$$
28		6nn	$$⊢6\in \mathbb{N}$$
29		1re	$$⊢1\in ℝ$$
30		6re	$$⊢6\in ℝ$$
31		1lt6	$$⊢1<6$$
32	29 30 31	ltleii	$$⊢1\le 6$$
33		elfz1b	$$⊢1\in \left(1\dots 6\right)\leftrightarrow \left(1\in \mathbb{N}\wedge 6\in \mathbb{N}\wedge 1\le 6\right)$$
34	27 28 32 33	mpbir3an	$$⊢1\in \left(1\dots 6\right)$$
35		iftrue	$$⊢k=1\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)={P\left(1\right)}^2$$
36	35 19 18	fvmpt3i	$$⊢1\in \left(1\dots 6\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(1\right)={P\left(1\right)}^2$$
37	34 36	ax-mp	$$⊢\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(1\right)={P\left(1\right)}^2$$
38	26 37	eqtrdi	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=1\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)={P\left(1\right)}^2$$
39	23 25 38	3eqtr4d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 1 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
40	1	veronesev2lem	Could not format ( ph -> ( ( veronese ` P ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) ) : No typesetting found for |- ( ph -> ( ( veronese ` P ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) ) with typecode |-
41	40	ad2antrr	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` 2 ) = ( ( P ` 2 ) ^ 2 ) ) with typecode |-
42		simpr	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=2\right)\to x=2$$
43	42	fveq2d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 2 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 2 ) ) with typecode |-
44	42	fveq2d	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=2\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(2\right)$$
45		2nn	$$⊢2\in \mathbb{N}$$
46		2re	$$⊢2\in ℝ$$
47		2lt6	$$⊢2<6$$
48	46 30 47	ltleii	$$⊢2\le 6$$
49		elfz1b	$$⊢2\in \left(1\dots 6\right)\leftrightarrow \left(2\in \mathbb{N}\wedge 6\in \mathbb{N}\wedge 2\le 6\right)$$
50	45 28 48 49	mpbir3an	$$⊢2\in \left(1\dots 6\right)$$
51		1ne2	$$⊢1\ne 2$$
52	51	necomi	$$⊢2\ne 1$$
53		neeq1	$$⊢k=2\to \left(k\ne 1\leftrightarrow 2\ne 1\right)$$
54	52 53	mpbiri	$$⊢k=2\to k\ne 1$$
55	54	neneqd	$$⊢k=2\to \neg k=1$$
56	55	iffalsed	$$⊢k=2\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)$$
57		iftrue	$$⊢k=2\to if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)={P\left(2\right)}^2$$
58	56 57	eqtrd	$$⊢k=2\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)={P\left(2\right)}^2$$
59	58 19 18	fvmpt3i	$$⊢2\in \left(1\dots 6\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(2\right)={P\left(2\right)}^2$$
60	50 59	ax-mp	$$⊢\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(2\right)={P\left(2\right)}^2$$
61	44 60	eqtrdi	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=2\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)={P\left(2\right)}^2$$
62	41 43 61	3eqtr4d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 2 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
63	39 62	jaodan	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( x = 1 \/ x = 2 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( x = 1 \/ x = 2 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
64	1	veronesev3lem	Could not format ( ph -> ( ( veronese ` P ) ` 3 ) = ( ( P ` 3 ) ^ 2 ) ) : No typesetting found for |- ( ph -> ( ( veronese ` P ) ` 3 ) = ( ( P ` 3 ) ^ 2 ) ) with typecode |-
65	64	ad2antrr	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` 3 ) = ( ( P ` 3 ) ^ 2 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` 3 ) = ( ( P ` 3 ) ^ 2 ) ) with typecode |-
66		simpr	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=3\right)\to x=3$$
67	66	fveq2d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 3 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 3 ) ) with typecode |-
68	66	fveq2d	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=3\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(3\right)$$
69		3nn	$$⊢3\in \mathbb{N}$$
70		3re	$$⊢3\in ℝ$$
71		3lt6	$$⊢3<6$$
72	70 30 71	ltleii	$$⊢3\le 6$$
73		elfz1b	$$⊢3\in \left(1\dots 6\right)\leftrightarrow \left(3\in \mathbb{N}\wedge 6\in \mathbb{N}\wedge 3\le 6\right)$$
74	69 28 72 73	mpbir3an	$$⊢3\in \left(1\dots 6\right)$$
75		1ne3	$$⊢1\ne 3$$
76	75	necomi	$$⊢3\ne 1$$
77		neeq1	$$⊢k=3\to \left(k\ne 1\leftrightarrow 3\ne 1\right)$$
78	76 77	mpbiri	$$⊢k=3\to k\ne 1$$
79	78	neneqd	$$⊢k=3\to \neg k=1$$
80	79	iffalsed	$$⊢k=3\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)$$
81		2ne3	$$⊢2\ne 3$$
82	81	necomi	$$⊢3\ne 2$$
83		neeq1	$$⊢k=3\to \left(k\ne 2\leftrightarrow 3\ne 2\right)$$
84	82 83	mpbiri	$$⊢k=3\to k\ne 2$$
85	84	neneqd	$$⊢k=3\to \neg k=2$$
86	85	iffalsed	$$⊢k=3\to if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)=if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)$$
87		iftrue	$$⊢k=3\to if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)={P\left(3\right)}^2$$
88	80 86 87	3eqtrd	$$⊢k=3\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)={P\left(3\right)}^2$$
89	88 19 18	fvmpt3i	$$⊢3\in \left(1\dots 6\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(3\right)={P\left(3\right)}^2$$
90	74 89	ax-mp	$$⊢\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(3\right)={P\left(3\right)}^2$$
91	68 90	eqtrdi	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=3\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)={P\left(3\right)}^2$$
92	65 67 91	3eqtr4d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 3 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
93	63 92	jaodan	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( x = 1 \/ x = 2 ) \/ x = 3 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( x = 1 \/ x = 2 ) \/ x = 3 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
94	1	veronesev4lem	Could not format ( ph -> ( ( veronese ` P ) ` 4 ) = ( ( P ` 1 ) x. ( P ` 2 ) ) ) : No typesetting found for |- ( ph -> ( ( veronese ` P ) ` 4 ) = ( ( P ` 1 ) x. ( P ` 2 ) ) ) with typecode |-
95	94	ad2antrr	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` 4 ) = ( ( P ` 1 ) x. ( P ` 2 ) ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` 4 ) = ( ( P ` 1 ) x. ( P ` 2 ) ) ) with typecode |-
96		simpr	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=4\right)\to x=4$$
97	96	fveq2d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 4 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 4 ) ) with typecode |-
98	96	fveq2d	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=4\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(4\right)$$
99		4nn	$$⊢4\in \mathbb{N}$$
100		4re	$$⊢4\in ℝ$$
101		4lt6	$$⊢4<6$$
102	100 30 101	ltleii	$$⊢4\le 6$$
103		elfz1b	$$⊢4\in \left(1\dots 6\right)\leftrightarrow \left(4\in \mathbb{N}\wedge 6\in \mathbb{N}\wedge 4\le 6\right)$$
104	99 28 102 103	mpbir3an	$$⊢4\in \left(1\dots 6\right)$$
105		1lt4	$$⊢1<4$$
106	29 105	gtneii	$$⊢4\ne 1$$
107		neeq1	$$⊢k=4\to \left(k\ne 1\leftrightarrow 4\ne 1\right)$$
108	106 107	mpbiri	$$⊢k=4\to k\ne 1$$
109	108	neneqd	$$⊢k=4\to \neg k=1$$
110	109	iffalsed	$$⊢k=4\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)$$
111		2lt4	$$⊢2<4$$
112	46 111	gtneii	$$⊢4\ne 2$$
113		neeq1	$$⊢k=4\to \left(k\ne 2\leftrightarrow 4\ne 2\right)$$
114	112 113	mpbiri	$$⊢k=4\to k\ne 2$$
115	114	neneqd	$$⊢k=4\to \neg k=2$$
116	115	iffalsed	$$⊢k=4\to if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)=if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)$$
117	110 116	eqtrd	$$⊢k=4\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)$$
118		3lt4	$$⊢3<4$$
119	70 118	gtneii	$$⊢4\ne 3$$
120		neeq1	$$⊢k=4\to \left(k\ne 3\leftrightarrow 4\ne 3\right)$$
121	119 120	mpbiri	$$⊢k=4\to k\ne 3$$
122	121	neneqd	$$⊢k=4\to \neg k=3$$
123	122	iffalsed	$$⊢k=4\to if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)=if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)$$
124		iftrue	$$⊢k=4\to if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)=P\left(1\right)P\left(2\right)$$
125	117 123 124	3eqtrd	$$⊢k=4\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=P\left(1\right)P\left(2\right)$$
126	125 19 18	fvmpt3i	$$⊢4\in \left(1\dots 6\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(4\right)=P\left(1\right)P\left(2\right)$$
127	104 126	ax-mp	$$⊢\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(4\right)=P\left(1\right)P\left(2\right)$$
128	98 127	eqtrdi	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=4\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=P\left(1\right)P\left(2\right)$$
129	95 97 128	3eqtr4d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 4 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
130	93 129	jaodan	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
131	1	veronesev5lem	Could not format ( ph -> ( ( veronese ` P ) ` 5 ) = ( ( P ` 2 ) x. ( P ` 3 ) ) ) : No typesetting found for |- ( ph -> ( ( veronese ` P ) ` 5 ) = ( ( P ` 2 ) x. ( P ` 3 ) ) ) with typecode |-
132	131	ad2antrr	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` 5 ) = ( ( P ` 2 ) x. ( P ` 3 ) ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` 5 ) = ( ( P ` 2 ) x. ( P ` 3 ) ) ) with typecode |-
133		simpr	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=5\right)\to x=5$$
134	133	fveq2d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 5 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 5 ) ) with typecode |-
135	133	fveq2d	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=5\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(5\right)$$
136		5nn	$$⊢5\in \mathbb{N}$$
137		5re	$$⊢5\in ℝ$$
138		5lt6	$$⊢5<6$$
139	137 30 138	ltleii	$$⊢5\le 6$$
140		elfz1b	$$⊢5\in \left(1\dots 6\right)\leftrightarrow \left(5\in \mathbb{N}\wedge 6\in \mathbb{N}\wedge 5\le 6\right)$$
141	136 28 139 140	mpbir3an	$$⊢5\in \left(1\dots 6\right)$$
142		1lt5	$$⊢1<5$$
143	29 142	gtneii	$$⊢5\ne 1$$
144		neeq1	$$⊢k=5\to \left(k\ne 1\leftrightarrow 5\ne 1\right)$$
145	143 144	mpbiri	$$⊢k=5\to k\ne 1$$
146	145	neneqd	$$⊢k=5\to \neg k=1$$
147	146	iffalsed	$$⊢k=5\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)$$
148		2lt5	$$⊢2<5$$
149	46 148	gtneii	$$⊢5\ne 2$$
150		neeq1	$$⊢k=5\to \left(k\ne 2\leftrightarrow 5\ne 2\right)$$
151	149 150	mpbiri	$$⊢k=5\to k\ne 2$$
152	151	neneqd	$$⊢k=5\to \neg k=2$$
153	152	iffalsed	$$⊢k=5\to if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)=if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)$$
154		3lt5	$$⊢3<5$$
155	70 154	gtneii	$$⊢5\ne 3$$
156		neeq1	$$⊢k=5\to \left(k\ne 3\leftrightarrow 5\ne 3\right)$$
157	155 156	mpbiri	$$⊢k=5\to k\ne 3$$
158	157	neneqd	$$⊢k=5\to \neg k=3$$
159	158	iffalsed	$$⊢k=5\to if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)=if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)$$
160	147 153 159	3eqtrd	$$⊢k=5\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)$$
161		4lt5	$$⊢4<5$$
162	100 161	gtneii	$$⊢5\ne 4$$
163		neeq1	$$⊢k=5\to \left(k\ne 4\leftrightarrow 5\ne 4\right)$$
164	162 163	mpbiri	$$⊢k=5\to k\ne 4$$
165	164	neneqd	$$⊢k=5\to \neg k=4$$
166	165	iffalsed	$$⊢k=5\to if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)=if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)$$
167		iftrue	$$⊢k=5\to if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)=P\left(2\right)P\left(3\right)$$
168	160 166 167	3eqtrd	$$⊢k=5\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=P\left(2\right)P\left(3\right)$$
169	168 19 18	fvmpt3i	$$⊢5\in \left(1\dots 6\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(5\right)=P\left(2\right)P\left(3\right)$$
170	141 169	ax-mp	$$⊢\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(5\right)=P\left(2\right)P\left(3\right)$$
171	135 170	eqtrdi	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=5\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=P\left(2\right)P\left(3\right)$$
172	132 134 171	3eqtr4d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 5 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
173	130 172	jaodan	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) \/ x = 5 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ ( ( ( ( x = 1 \/ x = 2 ) \/ x = 3 ) \/ x = 4 ) \/ x = 5 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
174	1	veronesev6lem	Could not format ( ph -> ( ( veronese ` P ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) ) ) : No typesetting found for |- ( ph -> ( ( veronese ` P ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) ) ) with typecode |-
175	174	ad2antrr	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` 6 ) = ( ( P ` 3 ) x. ( P ` 1 ) ) ) with typecode |-
176		simpr	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=6\right)\to x=6$$
177	176	fveq2d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 6 ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` x ) = ( ( veronese ` P ) ` 6 ) ) with typecode |-
178	176	fveq2d	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=6\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(6\right)$$
179	30	leidi	$$⊢6\le 6$$
180		elfz1b	$$⊢6\in \left(1\dots 6\right)\leftrightarrow \left(6\in \mathbb{N}\wedge 6\in \mathbb{N}\wedge 6\le 6\right)$$
181	28 28 179 180	mpbir3an	$$⊢6\in \left(1\dots 6\right)$$
182	29 31	gtneii	$$⊢6\ne 1$$
183		neeq1	$$⊢k=6\to \left(k\ne 1\leftrightarrow 6\ne 1\right)$$
184	182 183	mpbiri	$$⊢k=6\to k\ne 1$$
185	184	neneqd	$$⊢k=6\to \neg k=1$$
186	185	iffalsed	$$⊢k=6\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)$$
187	46 47	gtneii	$$⊢6\ne 2$$
188		neeq1	$$⊢k=6\to \left(k\ne 2\leftrightarrow 6\ne 2\right)$$
189	187 188	mpbiri	$$⊢k=6\to k\ne 2$$
190	189	neneqd	$$⊢k=6\to \neg k=2$$
191	190	iffalsed	$$⊢k=6\to if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)=if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)$$
192	70 71	gtneii	$$⊢6\ne 3$$
193		neeq1	$$⊢k=6\to \left(k\ne 3\leftrightarrow 6\ne 3\right)$$
194	192 193	mpbiri	$$⊢k=6\to k\ne 3$$
195	194	neneqd	$$⊢k=6\to \neg k=3$$
196	195	iffalsed	$$⊢k=6\to if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)=if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)$$
197	186 191 196	3eqtrd	$$⊢k=6\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)$$
198	100 101	gtneii	$$⊢6\ne 4$$
199		neeq1	$$⊢k=6\to \left(k\ne 4\leftrightarrow 6\ne 4\right)$$
200	198 199	mpbiri	$$⊢k=6\to k\ne 4$$
201	200	neneqd	$$⊢k=6\to \neg k=4$$
202	201	iffalsed	$$⊢k=6\to if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)=if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)$$
203	137 138	gtneii	$$⊢6\ne 5$$
204		neeq1	$$⊢k=6\to \left(k\ne 5\leftrightarrow 6\ne 5\right)$$
205	203 204	mpbiri	$$⊢k=6\to k\ne 5$$
206	205	neneqd	$$⊢k=6\to \neg k=5$$
207	206	iffalsed	$$⊢k=6\to if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)=P\left(3\right)P\left(1\right)$$
208	197 202 207	3eqtrd	$$⊢k=6\to if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)=P\left(3\right)P\left(1\right)$$
209	208 19 18	fvmpt3i	$$⊢6\in \left(1\dots 6\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(6\right)=P\left(3\right)P\left(1\right)$$
210	181 209	ax-mp	$$⊢\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(6\right)=P\left(3\right)P\left(1\right)$$
211	178 210	eqtrdi	$$⊢\left(\left(\phi \wedge x\in \left(1\dots 6\right)\right)\wedge x=6\right)\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{P\left(1\right)}^2,if\left(k=2,{P\left(2\right)}^2,if\left(k=3,{P\left(3\right)}^2,if\left(k=4,P\left(1\right)P\left(2\right),if\left(k=5,P\left(2\right)P\left(3\right),P\left(3\right)P\left(1\right)\right)\right)\right)\right)\right)\right)\left(x\right)=P\left(3\right)P\left(1\right)$$
212	175 177 211	3eqtr4d	Could not format ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( 1 ... 6 ) ) /\ x = 6 ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
213		simpr	$$⊢\left(\phi \wedge x\in \left(1\dots 6\right)\right)\to x\in \left(1\dots 6\right)$$
214		elnnuz	$$⊢5\in \mathbb{N}\leftrightarrow 5\in {\mathbb{Z}}_{\ge 1}$$
215	136 214	mpbi	$$⊢5\in {\mathbb{Z}}_{\ge 1}$$
216		elfzp1	$$⊢5\in {\mathbb{Z}}_{\ge 1}\to \left(x\in \left(1\dots 5+1\right)\leftrightarrow \left(x\in \left(1\dots 5\right)\vee x=5+1\right)\right)$$
217	215 216	ax-mp	$$⊢x\in \left(1\dots 5+1\right)\leftrightarrow \left(x\in \left(1\dots 5\right)\vee x=5+1\right)$$
218		5p1e6	$$⊢5+1=6$$
219	218	oveq2i	$$⊢\left(1\dots 5+1\right)=\left(1\dots 6\right)$$
220	219	eleq2i	$$⊢x\in \left(1\dots 5+1\right)\leftrightarrow x\in \left(1\dots 6\right)$$
221	218	eqeq2i	$$⊢x=5+1\leftrightarrow x=6$$
222	221	orbi2i	$$⊢\left(x\in \left(1\dots 5\right)\vee x=5+1\right)\leftrightarrow \left(x\in \left(1\dots 5\right)\vee x=6\right)$$
223	217 220 222	3bitr3i	$$⊢x\in \left(1\dots 6\right)\leftrightarrow \left(x\in \left(1\dots 5\right)\vee x=6\right)$$
224		elnnuz	$$⊢4\in \mathbb{N}\leftrightarrow 4\in {\mathbb{Z}}_{\ge 1}$$
225	99 224	mpbi	$$⊢4\in {\mathbb{Z}}_{\ge 1}$$
226		elfzp1	$$⊢4\in {\mathbb{Z}}_{\ge 1}\to \left(x\in \left(1\dots 4+1\right)\leftrightarrow \left(x\in \left(1\dots 4\right)\vee x=4+1\right)\right)$$
227	225 226	ax-mp	$$⊢x\in \left(1\dots 4+1\right)\leftrightarrow \left(x\in \left(1\dots 4\right)\vee x=4+1\right)$$
228		4p1e5	$$⊢4+1=5$$
229	228	oveq2i	$$⊢\left(1\dots 4+1\right)=\left(1\dots 5\right)$$
230	229	eleq2i	$$⊢x\in \left(1\dots 4+1\right)\leftrightarrow x\in \left(1\dots 5\right)$$
231	228	eqeq2i	$$⊢x=4+1\leftrightarrow x=5$$
232	231	orbi2i	$$⊢\left(x\in \left(1\dots 4\right)\vee x=4+1\right)\leftrightarrow \left(x\in \left(1\dots 4\right)\vee x=5\right)$$
233	227 230 232	3bitr3i	$$⊢x\in \left(1\dots 5\right)\leftrightarrow \left(x\in \left(1\dots 4\right)\vee x=5\right)$$
234		elnnuz	$$⊢3\in \mathbb{N}\leftrightarrow 3\in {\mathbb{Z}}_{\ge 1}$$
235	69 234	mpbi	$$⊢3\in {\mathbb{Z}}_{\ge 1}$$
236		elfzp1	$$⊢3\in {\mathbb{Z}}_{\ge 1}\to \left(x\in \left(1\dots 3+1\right)\leftrightarrow \left(x\in \left(1\dots 3\right)\vee x=3+1\right)\right)$$
237	235 236	ax-mp	$$⊢x\in \left(1\dots 3+1\right)\leftrightarrow \left(x\in \left(1\dots 3\right)\vee x=3+1\right)$$
238		3p1e4	$$⊢3+1=4$$
239	238	oveq2i	$$⊢\left(1\dots 3+1\right)=\left(1\dots 4\right)$$
240	239	eleq2i	$$⊢x\in \left(1\dots 3+1\right)\leftrightarrow x\in \left(1\dots 4\right)$$
241	238	eqeq2i	$$⊢x=3+1\leftrightarrow x=4$$
242	241	orbi2i	$$⊢\left(x\in \left(1\dots 3\right)\vee x=3+1\right)\leftrightarrow \left(x\in \left(1\dots 3\right)\vee x=4\right)$$
243	237 240 242	3bitr3i	$$⊢x\in \left(1\dots 4\right)\leftrightarrow \left(x\in \left(1\dots 3\right)\vee x=4\right)$$
244		2eluzge1	$$⊢2\in {\mathbb{Z}}_{\ge 1}$$
245		elfzp1	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to \left(x\in \left(1\dots 2+1\right)\leftrightarrow \left(x\in \left(1\dots 2\right)\vee x=2+1\right)\right)$$
246	244 245	ax-mp	$$⊢x\in \left(1\dots 2+1\right)\leftrightarrow \left(x\in \left(1\dots 2\right)\vee x=2+1\right)$$
247		2p1e3	$$⊢2+1=3$$
248	247	oveq2i	$$⊢\left(1\dots 2+1\right)=\left(1\dots 3\right)$$
249	248	eleq2i	$$⊢x\in \left(1\dots 2+1\right)\leftrightarrow x\in \left(1\dots 3\right)$$
250	247	eqeq2i	$$⊢x=2+1\leftrightarrow x=3$$
251	250	orbi2i	$$⊢\left(x\in \left(1\dots 2\right)\vee x=2+1\right)\leftrightarrow \left(x\in \left(1\dots 2\right)\vee x=3\right)$$
252	246 249 251	3bitr3i	$$⊢x\in \left(1\dots 3\right)\leftrightarrow \left(x\in \left(1\dots 2\right)\vee x=3\right)$$
253		elnnuz	$$⊢1\in \mathbb{N}\leftrightarrow 1\in {\mathbb{Z}}_{\ge 1}$$
254	27 253	mpbi	$$⊢1\in {\mathbb{Z}}_{\ge 1}$$
255		elfzp1	$$⊢1\in {\mathbb{Z}}_{\ge 1}\to \left(x\in \left(1\dots 1+1\right)\leftrightarrow \left(x\in \left(1\dots 1\right)\vee x=1+1\right)\right)$$
256	254 255	ax-mp	$$⊢x\in \left(1\dots 1+1\right)\leftrightarrow \left(x\in \left(1\dots 1\right)\vee x=1+1\right)$$
257		1p1e2	$$⊢1+1=2$$
258	257	oveq2i	$$⊢\left(1\dots 1+1\right)=\left(1\dots 2\right)$$
259	258	eleq2i	$$⊢x\in \left(1\dots 1+1\right)\leftrightarrow x\in \left(1\dots 2\right)$$
260	257	eqeq2i	$$⊢x=1+1\leftrightarrow x=2$$
261	260	orbi2i	$$⊢\left(x\in \left(1\dots 1\right)\vee x=1+1\right)\leftrightarrow \left(x\in \left(1\dots 1\right)\vee x=2\right)$$
262	256 259 261	3bitr3i	$$⊢x\in \left(1\dots 2\right)\leftrightarrow \left(x\in \left(1\dots 1\right)\vee x=2\right)$$
263		elfz1eq	$$⊢x\in \left(1\dots 1\right)\to x=1$$
264	263	orim1i	$$⊢\left(x\in \left(1\dots 1\right)\vee x=2\right)\to \left(x=1\vee x=2\right)$$
265	262 264	sylbi	$$⊢x\in \left(1\dots 2\right)\to \left(x=1\vee x=2\right)$$
266	265	orim1i	$$⊢\left(x\in \left(1\dots 2\right)\vee x=3\right)\to \left(\left(x=1\vee x=2\right)\vee x=3\right)$$
267	252 266	sylbi	$$⊢x\in \left(1\dots 3\right)\to \left(\left(x=1\vee x=2\right)\vee x=3\right)$$
268	267	orim1i	$$⊢\left(x\in \left(1\dots 3\right)\vee x=4\right)\to \left(\left(\left(x=1\vee x=2\right)\vee x=3\right)\vee x=4\right)$$
269	243 268	sylbi	$$⊢x\in \left(1\dots 4\right)\to \left(\left(\left(x=1\vee x=2\right)\vee x=3\right)\vee x=4\right)$$
270	269	orim1i	$$⊢\left(x\in \left(1\dots 4\right)\vee x=5\right)\to \left(\left(\left(\left(x=1\vee x=2\right)\vee x=3\right)\vee x=4\right)\vee x=5\right)$$
271	233 270	sylbi	$$⊢x\in \left(1\dots 5\right)\to \left(\left(\left(\left(x=1\vee x=2\right)\vee x=3\right)\vee x=4\right)\vee x=5\right)$$
272	271	orim1i	$$⊢\left(x\in \left(1\dots 5\right)\vee x=6\right)\to \left(\left(\left(\left(\left(x=1\vee x=2\right)\vee x=3\right)\vee x=4\right)\vee x=5\right)\vee x=6\right)$$
273	223 272	sylbi	$$⊢x\in \left(1\dots 6\right)\to \left(\left(\left(\left(\left(x=1\vee x=2\right)\vee x=3\right)\vee x=4\right)\vee x=5\right)\vee x=6\right)$$
274	213 273	syl	$$⊢\left(\phi \wedge x\in \left(1\dots 6\right)\right)\to \left(\left(\left(\left(\left(x=1\vee x=2\right)\vee x=3\right)\vee x=4\right)\vee x=5\right)\vee x=6\right)$$
275	173 212 274	mpjaodan	Could not format ( ( ph /\ x e. ( 1 ... 6 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) : No typesetting found for |- ( ( ph /\ x e. ( 1 ... 6 ) ) -> ( ( veronese ` P ) ` x ) = ( ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ` x ) ) with typecode |-
276	7 21 275	eqfnfvd	Could not format ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , ( ( P ` 3 ) x. ( P ` 1 ) ) ) ) ) ) ) ) ) with typecode |-