lcmfunsnlem2lem2

		Ref	Expression
	Assertion	lcmfunsnlem2lem2	\|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )

Proof

Step	Hyp	Ref	Expression
1		elun	\|- ( i e. ( ( y u. { z } ) u. { n } ) <-> ( i e. ( y u. { z } ) \/ i e. { n } ) )
2		elun	\|- ( i e. ( y u. { z } ) <-> ( i e. y \/ i e. { z } ) )
3		simp1	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> z e. ZZ )
4	3	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> z e. ZZ )
5	4	adantl	\|- ( ( ( i e. y \/ i e. { z } ) /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> z e. ZZ )
6		sneq	\|- ( n = z -> { n } = { z } )
7	6	uneq2d	\|- ( n = z -> ( y u. { n } ) = ( y u. { z } ) )
8	7	fveq2d	\|- ( n = z -> ( _lcm ` ( y u. { n } ) ) = ( _lcm ` ( y u. { z } ) ) )
9		oveq2	\|- ( n = z -> ( ( _lcm ` y ) lcm n ) = ( ( _lcm ` y ) lcm z ) )
10	8 9	eqeq12d	\|- ( n = z -> ( ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) <-> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
11	10	rspcv	\|- ( z e. ZZ -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
12	5 11	syl	\|- ( ( ( i e. y \/ i e. { z } ) /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
13		ssel	\|- ( y C_ ZZ -> ( i e. y -> i e. ZZ ) )
14	13	3ad2ant2	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( i e. y -> i e. ZZ ) )
15	14	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( i e. y -> i e. ZZ ) )
16	15	impcom	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> i e. ZZ )
17		lcmfcl	\|- ( ( y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. NN0 )
18	17	nn0zd	\|- ( ( y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. ZZ )
19	18	3adant1	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. ZZ )
20	19	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( _lcm ` y ) e. ZZ )
21	20	adantl	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( _lcm ` y ) e. ZZ )
22		lcmcl	\|- ( ( z e. ZZ /\ n e. ZZ ) -> ( z lcm n ) e. NN0 )
23	3 22	sylan	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( z lcm n ) e. NN0 )
24	23	nn0zd	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( z lcm n ) e. ZZ )
25	24	adantl	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( z lcm n ) e. ZZ )
26		lcmcl	\|- ( ( ( _lcm ` y ) e. ZZ /\ ( z lcm n ) e. ZZ ) -> ( ( _lcm ` y ) lcm ( z lcm n ) ) e. NN0 )
27	21 25 26	syl2anc	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( ( _lcm ` y ) lcm ( z lcm n ) ) e. NN0 )
28	27	nn0zd	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( ( _lcm ` y ) lcm ( z lcm n ) ) e. ZZ )
29		breq1	\|- ( k = i -> ( k \|\| ( _lcm ` y ) <-> i \|\| ( _lcm ` y ) ) )
30	29	rspcv	\|- ( i e. y -> ( A. k e. y k \|\| ( _lcm ` y ) -> i \|\| ( _lcm ` y ) ) )
31		dvdslcmf	\|- ( ( y C_ ZZ /\ y e. Fin ) -> A. k e. y k \|\| ( _lcm ` y ) )
32	31	3adant1	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> A. k e. y k \|\| ( _lcm ` y ) )
33	32	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> A. k e. y k \|\| ( _lcm ` y ) )
34	30 33	impel	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> i \|\| ( _lcm ` y ) )
35	20 24	jca	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( _lcm ` y ) e. ZZ /\ ( z lcm n ) e. ZZ ) )
36	35	adantl	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( ( _lcm ` y ) e. ZZ /\ ( z lcm n ) e. ZZ ) )
37		dvdslcm	\|- ( ( ( _lcm ` y ) e. ZZ /\ ( z lcm n ) e. ZZ ) -> ( ( _lcm ` y ) \|\| ( ( _lcm ` y ) lcm ( z lcm n ) ) /\ ( z lcm n ) \|\| ( ( _lcm ` y ) lcm ( z lcm n ) ) ) )
38	37	simpld	\|- ( ( ( _lcm ` y ) e. ZZ /\ ( z lcm n ) e. ZZ ) -> ( _lcm ` y ) \|\| ( ( _lcm ` y ) lcm ( z lcm n ) ) )
39	36 38	syl	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( _lcm ` y ) \|\| ( ( _lcm ` y ) lcm ( z lcm n ) ) )
40	16 21 28 34 39	dvdstrd	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> i \|\| ( ( _lcm ` y ) lcm ( z lcm n ) ) )
41	4	adantl	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> z e. ZZ )
42		simprr	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> n e. ZZ )
43		lcmass	\|- ( ( ( _lcm ` y ) e. ZZ /\ z e. ZZ /\ n e. ZZ ) -> ( ( ( _lcm ` y ) lcm z ) lcm n ) = ( ( _lcm ` y ) lcm ( z lcm n ) ) )
44	21 41 42 43	syl3anc	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( ( ( _lcm ` y ) lcm z ) lcm n ) = ( ( _lcm ` y ) lcm ( z lcm n ) ) )
45	40 44	breqtrrd	\|- ( ( i e. y /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> i \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) )
46	45	ex	\|- ( i e. y -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> i \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) ) )
47		elsni	\|- ( i e. { z } -> i = z )
48	17	3adant1	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. NN0 )
49	48	nn0zd	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. ZZ )
50		lcmcl	\|- ( ( ( _lcm ` y ) e. ZZ /\ z e. ZZ ) -> ( ( _lcm ` y ) lcm z ) e. NN0 )
51	49 3 50	syl2anc	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( ( _lcm ` y ) lcm z ) e. NN0 )
52	51	nn0zd	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( ( _lcm ` y ) lcm z ) e. ZZ )
53	52	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( _lcm ` y ) lcm z ) e. ZZ )
54		lcmcl	\|- ( ( ( ( _lcm ` y ) lcm z ) e. ZZ /\ n e. ZZ ) -> ( ( ( _lcm ` y ) lcm z ) lcm n ) e. NN0 )
55	52 54	sylan	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( ( _lcm ` y ) lcm z ) lcm n ) e. NN0 )
56	55	nn0zd	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( ( _lcm ` y ) lcm z ) lcm n ) e. ZZ )
57	19 3	jca	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( ( _lcm ` y ) e. ZZ /\ z e. ZZ ) )
58	57	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( _lcm ` y ) e. ZZ /\ z e. ZZ ) )
59		dvdslcm	\|- ( ( ( _lcm ` y ) e. ZZ /\ z e. ZZ ) -> ( ( _lcm ` y ) \|\| ( ( _lcm ` y ) lcm z ) /\ z \|\| ( ( _lcm ` y ) lcm z ) ) )
60	59	simprd	\|- ( ( ( _lcm ` y ) e. ZZ /\ z e. ZZ ) -> z \|\| ( ( _lcm ` y ) lcm z ) )
61	58 60	syl	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> z \|\| ( ( _lcm ` y ) lcm z ) )
62		dvdslcm	\|- ( ( ( ( _lcm ` y ) lcm z ) e. ZZ /\ n e. ZZ ) -> ( ( ( _lcm ` y ) lcm z ) \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) /\ n \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) ) )
63	62	simpld	\|- ( ( ( ( _lcm ` y ) lcm z ) e. ZZ /\ n e. ZZ ) -> ( ( _lcm ` y ) lcm z ) \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) )
64	52 63	sylan	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( _lcm ` y ) lcm z ) \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) )
65	4 53 56 61 64	dvdstrd	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> z \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) )
66		breq1	\|- ( i = z -> ( i \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) <-> z \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) ) )
67	65 66	imbitrrid	\|- ( i = z -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> i \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) ) )
68	47 67	syl	\|- ( i e. { z } -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> i \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) ) )
69	46 68	jaoi	\|- ( ( i e. y \/ i e. { z } ) -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> i \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) ) )
70	69	imp	\|- ( ( ( i e. y \/ i e. { z } ) /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> i \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) )
71		oveq1	\|- ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) = ( ( ( _lcm ` y ) lcm z ) lcm n ) )
72	71	breq2d	\|- ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) <-> i \|\| ( ( ( _lcm ` y ) lcm z ) lcm n ) ) )
73	70 72	syl5ibrcom	\|- ( ( ( i e. y \/ i e. { z } ) /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
74	12 73	syld	\|- ( ( ( i e. y \/ i e. { z } ) /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
75	74	ex	\|- ( ( i e. y \/ i e. { z } ) -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
76	2 75	sylbi	\|- ( i e. ( y u. { z } ) -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
77		elsni	\|- ( i e. { n } -> i = n )
78		simp2	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> y C_ ZZ )
79		snssi	\|- ( z e. ZZ -> { z } C_ ZZ )
80	79	3ad2ant1	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> { z } C_ ZZ )
81	78 80	unssd	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( y u. { z } ) C_ ZZ )
82		simp3	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> y e. Fin )
83		snfi	\|- { z } e. Fin
84		unfi	\|- ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
85	82 83 84	sylancl	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( y u. { z } ) e. Fin )
86		lcmfcl	\|- ( ( ( y u. { z } ) C_ ZZ /\ ( y u. { z } ) e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. NN0 )
87	81 85 86	syl2anc	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. NN0 )
88	87	nn0zd	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. ZZ )
89	88	anim1i	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) )
90	89	adantr	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) -> ( ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) )
91		dvdslcm	\|- ( ( ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) -> ( ( _lcm ` ( y u. { z } ) ) \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) /\ n \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
92	90 91	syl	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) -> ( ( _lcm ` ( y u. { z } ) ) \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) /\ n \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
93	92	simprd	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) -> n \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) )
94		breq1	\|- ( i = n -> ( i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) <-> n \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
95	93 94	imbitrrid	\|- ( i = n -> ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
96	95	expd	\|- ( i = n -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
97	77 96	syl	\|- ( i e. { n } -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
98	76 97	jaoi	\|- ( ( i e. ( y u. { z } ) \/ i e. { n } ) -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
99	1 98	sylbi	\|- ( i e. ( ( y u. { z } ) u. { n } ) -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
100	99	com13	\|- ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( i e. ( ( y u. { z } ) u. { n } ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
101	100	expd	\|- ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( n e. ZZ -> ( i e. ( ( y u. { z } ) u. { n } ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) )
102	101	adantl	\|- ( ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) -> ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( n e. ZZ -> ( i e. ( ( y u. { z } ) u. { n } ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) )
103	102	impcom	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) -> ( n e. ZZ -> ( i e. ( ( y u. { z } ) u. { n } ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
104	103	impcom	\|- ( ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) -> ( i e. ( ( y u. { z } ) u. { n } ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
105	104	adantl	\|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( i e. ( ( y u. { z } ) u. { n } ) -> i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
106	105	ralrimiv	\|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> A. i e. ( ( y u. { z } ) u. { n } ) i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) )
107		lcmfunsnlem2lem1	\|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> A. k e. NN ( A. i e. ( ( y u. { z } ) u. { n } ) i \|\| k -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) <_ k ) )
108	89	adantr	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) )
109	81	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( y u. { z } ) C_ ZZ )
110	85	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( y u. { z } ) e. Fin )
111		df-nel	\|- ( 0 e/ y <-> -. 0 e. y )
112	111	biimpi	\|- ( 0 e/ y -> -. 0 e. y )
113	112	3ad2ant1	\|- ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> -. 0 e. y )
114		elsni	\|- ( 0 e. { z } -> 0 = z )
115	114	eqcomd	\|- ( 0 e. { z } -> z = 0 )
116	115	necon3ai	\|- ( z =/= 0 -> -. 0 e. { z } )
117	116	3ad2ant2	\|- ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> -. 0 e. { z } )
118		ioran	\|- ( -. ( 0 e. y \/ 0 e. { z } ) <-> ( -. 0 e. y /\ -. 0 e. { z } ) )
119	113 117 118	sylanbrc	\|- ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> -. ( 0 e. y \/ 0 e. { z } ) )
120		elun	\|- ( 0 e. ( y u. { z } ) <-> ( 0 e. y \/ 0 e. { z } ) )
121	119 120	sylnibr	\|- ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> -. 0 e. ( y u. { z } ) )
122		df-nel	\|- ( 0 e/ ( y u. { z } ) <-> -. 0 e. ( y u. { z } ) )
123	121 122	sylibr	\|- ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> 0 e/ ( y u. { z } ) )
124		lcmfn0cl	\|- ( ( ( y u. { z } ) C_ ZZ /\ ( y u. { z } ) e. Fin /\ 0 e/ ( y u. { z } ) ) -> ( _lcm ` ( y u. { z } ) ) e. NN )
125	109 110 123 124	syl2an3an	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( _lcm ` ( y u. { z } ) ) e. NN )
126	125	nnne0d	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( _lcm ` ( y u. { z } ) ) =/= 0 )
127	126	neneqd	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> -. ( _lcm ` ( y u. { z } ) ) = 0 )
128		neneq	\|- ( n =/= 0 -> -. n = 0 )
129	128	3ad2ant3	\|- ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> -. n = 0 )
130	129	adantl	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> -. n = 0 )
131		ioran	\|- ( -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) <-> ( -. ( _lcm ` ( y u. { z } ) ) = 0 /\ -. n = 0 ) )
132	127 130 131	sylanbrc	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) )
133		lcmn0cl	\|- ( ( ( ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN )
134	108 132 133	syl2anc	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN )
135		snssi	\|- ( n e. ZZ -> { n } C_ ZZ )
136	135	adantl	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> { n } C_ ZZ )
137	109 136	unssd	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( y u. { z } ) u. { n } ) C_ ZZ )
138	137	adantr	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( ( y u. { z } ) u. { n } ) C_ ZZ )
139	83 84	mpan2	\|- ( y e. Fin -> ( y u. { z } ) e. Fin )
140		snfi	\|- { n } e. Fin
141		unfi	\|- ( ( ( y u. { z } ) e. Fin /\ { n } e. Fin ) -> ( ( y u. { z } ) u. { n } ) e. Fin )
142	139 140 141	sylancl	\|- ( y e. Fin -> ( ( y u. { z } ) u. { n } ) e. Fin )
143	142	3ad2ant3	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( ( y u. { z } ) u. { n } ) e. Fin )
144	143	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( y u. { z } ) u. { n } ) e. Fin )
145	144	adantr	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( ( y u. { z } ) u. { n } ) e. Fin )
146		elun	\|- ( 0 e. ( ( y u. { z } ) u. { n } ) <-> ( 0 e. ( y u. { z } ) \/ 0 e. { n } ) )
147		nnel	\|- ( -. 0 e/ y <-> 0 e. y )
148	147	biimpri	\|- ( 0 e. y -> -. 0 e/ y )
149	148	3mix1d	\|- ( 0 e. y -> ( -. 0 e/ y \/ -. z =/= 0 \/ -. n =/= 0 ) )
150		nne	\|- ( -. z =/= 0 <-> z = 0 )
151	115 150	sylibr	\|- ( 0 e. { z } -> -. z =/= 0 )
152	151	3mix2d	\|- ( 0 e. { z } -> ( -. 0 e/ y \/ -. z =/= 0 \/ -. n =/= 0 ) )
153	149 152	jaoi	\|- ( ( 0 e. y \/ 0 e. { z } ) -> ( -. 0 e/ y \/ -. z =/= 0 \/ -. n =/= 0 ) )
154	120 153	sylbi	\|- ( 0 e. ( y u. { z } ) -> ( -. 0 e/ y \/ -. z =/= 0 \/ -. n =/= 0 ) )
155		elsni	\|- ( 0 e. { n } -> 0 = n )
156	155	eqcomd	\|- ( 0 e. { n } -> n = 0 )
157		nne	\|- ( -. n =/= 0 <-> n = 0 )
158	156 157	sylibr	\|- ( 0 e. { n } -> -. n =/= 0 )
159	158	3mix3d	\|- ( 0 e. { n } -> ( -. 0 e/ y \/ -. z =/= 0 \/ -. n =/= 0 ) )
160	154 159	jaoi	\|- ( ( 0 e. ( y u. { z } ) \/ 0 e. { n } ) -> ( -. 0 e/ y \/ -. z =/= 0 \/ -. n =/= 0 ) )
161	146 160	sylbi	\|- ( 0 e. ( ( y u. { z } ) u. { n } ) -> ( -. 0 e/ y \/ -. z =/= 0 \/ -. n =/= 0 ) )
162		3ianor	\|- ( -. ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) <-> ( -. 0 e/ y \/ -. z =/= 0 \/ -. n =/= 0 ) )
163	161 162	sylibr	\|- ( 0 e. ( ( y u. { z } ) u. { n } ) -> -. ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) )
164	163	con2i	\|- ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> -. 0 e. ( ( y u. { z } ) u. { n } ) )
165		df-nel	\|- ( 0 e/ ( ( y u. { z } ) u. { n } ) <-> -. 0 e. ( ( y u. { z } ) u. { n } ) )
166	164 165	sylibr	\|- ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> 0 e/ ( ( y u. { z } ) u. { n } ) )
167	166	adantl	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> 0 e/ ( ( y u. { z } ) u. { n } ) )
168	138 145 167	3jca	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ ( ( y u. { z } ) u. { n } ) e. Fin /\ 0 e/ ( ( y u. { z } ) u. { n } ) ) )
169	134 168	jca	\|- ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN /\ ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ ( ( y u. { z } ) u. { n } ) e. Fin /\ 0 e/ ( ( y u. { z } ) u. { n } ) ) ) )
170	169	ex	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n e. ZZ ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN /\ ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ ( ( y u. { z } ) u. { n } ) e. Fin /\ 0 e/ ( ( y u. { z } ) u. { n } ) ) ) ) )
171	170	ex	\|- ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( n e. ZZ -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN /\ ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ ( ( y u. { z } ) u. { n } ) e. Fin /\ 0 e/ ( ( y u. { z } ) u. { n } ) ) ) ) ) )
172	171	adantr	\|- ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) -> ( n e. ZZ -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN /\ ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ ( ( y u. { z } ) u. { n } ) e. Fin /\ 0 e/ ( ( y u. { z } ) u. { n } ) ) ) ) ) )
173	172	impcom	\|- ( ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN /\ ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ ( ( y u. { z } ) u. { n } ) e. Fin /\ 0 e/ ( ( y u. { z } ) u. { n } ) ) ) ) )
174	173	impcom	\|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN /\ ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ ( ( y u. { z } ) u. { n } ) e. Fin /\ 0 e/ ( ( y u. { z } ) u. { n } ) ) ) )
175		lcmf	\|- ( ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) e. NN /\ ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ ( ( y u. { z } ) u. { n } ) e. Fin /\ 0 e/ ( ( y u. { z } ) u. { n } ) ) ) -> ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) = ( _lcm ` ( ( y u. { z } ) u. { n } ) ) <-> ( A. i e. ( ( y u. { z } ) u. { n } ) i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) /\ A. k e. NN ( A. i e. ( ( y u. { z } ) u. { n } ) i \|\| k -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) <_ k ) ) ) )
176	174 175	syl	\|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( ( ( _lcm ` ( y u. { z } ) ) lcm n ) = ( _lcm ` ( ( y u. { z } ) u. { n } ) ) <-> ( A. i e. ( ( y u. { z } ) u. { n } ) i \|\| ( ( _lcm ` ( y u. { z } ) ) lcm n ) /\ A. k e. NN ( A. i e. ( ( y u. { z } ) u. { n } ) i \|\| k -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) <_ k ) ) ) )
177	106 107 176	mpbir2and	\|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) = ( _lcm ` ( ( y u. { z } ) u. { n } ) ) )
178	177	eqcomd	\|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m \|\| k -> ( _lcm ` y ) \|\| k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )

Metamath Proof Explorer

Theorem lcmfunsnlem2lem2

Proof