Metamath Proof Explorer

Theorem lcmfunsnlem2lem2

Description: Lemma 2 for lcmfunsnlem2 . (Contributed by AV, 26-Aug-2020)

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 ) )