Metamath Proof Explorer

Theorem lcmfunsnlem2

Description: Lemma for lcmfunsn and lcmfunsnlem (Induction step part 2). (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion lcmfunsnlem2 
|- ( ( ( 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. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ n ( z e. ZZ /\ y C_ ZZ /\ y e. Fin )
2 nfv 
 |-  F/ n A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k )
3 nfra1 
 |-  F/ n A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n )
4 2 3 nfan 
 |-  F/ n ( 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 ) )
5 1 4 nfan 
 |-  F/ n ( ( 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 ) ) )
6 0z 
 |-  0 e. ZZ
7 eqoreldif 
 |-  ( 0 e. ZZ -> ( n e. ZZ <-> ( n = 0 \/ n e. ( ZZ \ { 0 } ) ) ) )
8 6 7 ax-mp 
 |-  ( n e. ZZ <-> ( n = 0 \/ n e. ( ZZ \ { 0 } ) ) )
9 simp2 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> y C_ ZZ )
10 snssi 
 |-  ( z e. ZZ -> { z } C_ ZZ )
11 10 3ad2ant1 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> { z } C_ ZZ )
12 9 11 unssd 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( y u. { z } ) C_ ZZ )
13 snssi 
 |-  ( 0 e. ZZ -> { 0 } C_ ZZ )
14 6 13 mp1i 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> { 0 } C_ ZZ )
15 12 14 unssd 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( ( y u. { z } ) u. { 0 } ) C_ ZZ )
16 c0ex 
 |-  0 e. _V
17 16 snid 
 |-  0 e. { 0 }
18 17 olci 
 |-  ( 0 e. ( y u. { z } ) \/ 0 e. { 0 } )
19 elun 
 |-  ( 0 e. ( ( y u. { z } ) u. { 0 } ) <-> ( 0 e. ( y u. { z } ) \/ 0 e. { 0 } ) )
20 18 19 mpbir 
 |-  0 e. ( ( y u. { z } ) u. { 0 } )
21 lcmf0val 
 |-  ( ( ( ( y u. { z } ) u. { 0 } ) C_ ZZ /\ 0 e. ( ( y u. { z } ) u. { 0 } ) ) -> ( _lcm ` ( ( y u. { z } ) u. { 0 } ) ) = 0 )
22 15 20 21 sylancl 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( ( y u. { z } ) u. { 0 } ) ) = 0 )
23 22 adantr 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n = 0 ) -> ( _lcm ` ( ( y u. { z } ) u. { 0 } ) ) = 0 )
24 sneq 
 |-  ( n = 0 -> { n } = { 0 } )
25 24 adantl 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n = 0 ) -> { n } = { 0 } )
26 25 uneq2d 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n = 0 ) -> ( ( y u. { z } ) u. { n } ) = ( ( y u. { z } ) u. { 0 } ) )
27 26 fveq2d 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n = 0 ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( _lcm ` ( ( y u. { z } ) u. { 0 } ) ) )
28 oveq2 
 |-  ( n = 0 -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) = ( ( _lcm ` ( y u. { z } ) ) lcm 0 ) )
29 snfi 
 |-  { z } e. Fin
30 unfi 
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
31 29 30 mpan2 
 |-  ( y e. Fin -> ( y u. { z } ) e. Fin )
32 31 3ad2ant3 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( y u. { z } ) e. Fin )
33 lcmfcl 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( y u. { z } ) e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. NN0 )
34 12 32 33 syl2anc 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. NN0 )
35 34 nn0zd 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. ZZ )
36 lcm0val 
 |-  ( ( _lcm ` ( y u. { z } ) ) e. ZZ -> ( ( _lcm ` ( y u. { z } ) ) lcm 0 ) = 0 )
37 35 36 syl 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( ( _lcm ` ( y u. { z } ) ) lcm 0 ) = 0 )
38 28 37 sylan9eqr 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n = 0 ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) = 0 )
39 23 27 38 3eqtr4d 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ n = 0 ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )
40 39 ex 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( n = 0 -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
41 40 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 = 0 -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
42 41 com12 
 |-  ( n = 0 -> ( ( ( 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 ) ) )
43 9 adantl 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> y C_ ZZ )
44 11 adantl 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> { z } C_ ZZ )
45 43 44 unssd 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( y u. { z } ) C_ ZZ )
46 elun1 
 |-  ( 0 e. y -> 0 e. ( y u. { z } ) )
47 46 ad2antrr 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> 0 e. ( y u. { z } ) )
48 lcmf0val 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ 0 e. ( y u. { z } ) ) -> ( _lcm ` ( y u. { z } ) ) = 0 )
49 45 47 48 syl2anc 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( _lcm ` ( y u. { z } ) ) = 0 )
50 49 oveq2d 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( n lcm ( _lcm ` ( y u. { z } ) ) ) = ( n lcm 0 ) )
51 eldifi 
 |-  ( n e. ( ZZ \ { 0 } ) -> n e. ZZ )
52 lcm0val 
 |-  ( n e. ZZ -> ( n lcm 0 ) = 0 )
53 51 52 syl 
 |-  ( n e. ( ZZ \ { 0 } ) -> ( n lcm 0 ) = 0 )
54 53 ad2antlr 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( n lcm 0 ) = 0 )
55 50 54 eqtrd 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( n lcm ( _lcm ` ( y u. { z } ) ) ) = 0 )
56 simp3 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> y e. Fin )
57 56 29 30 sylancl 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( y u. { z } ) e. Fin )
58 12 57 33 syl2anc 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. NN0 )
59 58 nn0zd 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. ZZ )
60 51 adantl 
 |-  ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) -> n e. ZZ )
61 lcmcom 
 |-  ( ( ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) = ( n lcm ( _lcm ` ( y u. { z } ) ) ) )
62 59 60 61 syl2anr 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) = ( n lcm ( _lcm ` ( y u. { z } ) ) ) )
63 12 adantl 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( y u. { z } ) C_ ZZ )
64 51 snssd 
 |-  ( n e. ( ZZ \ { 0 } ) -> { n } C_ ZZ )
65 64 ad2antlr 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> { n } C_ ZZ )
66 63 65 unssd 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( ( y u. { z } ) u. { n } ) C_ ZZ )
67 46 orcd 
 |-  ( 0 e. y -> ( 0 e. ( y u. { z } ) \/ 0 e. { n } ) )
68 elun 
 |-  ( 0 e. ( ( y u. { z } ) u. { n } ) <-> ( 0 e. ( y u. { z } ) \/ 0 e. { n } ) )
69 67 68 sylibr 
 |-  ( 0 e. y -> 0 e. ( ( y u. { z } ) u. { n } ) )
70 69 ad2antrr 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> 0 e. ( ( y u. { z } ) u. { n } ) )
71 lcmf0val 
 |-  ( ( ( ( y u. { z } ) u. { n } ) C_ ZZ /\ 0 e. ( ( y u. { z } ) u. { n } ) ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = 0 )
72 66 70 71 syl2anc 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = 0 )
73 55 62 72 3eqtr4rd 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )
74 73 a1d 
 |-  ( ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) /\ ( 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 ) ) )
75 74 expimpd 
 |-  ( ( 0 e. y /\ n e. ( ZZ \ { 0 } ) ) -> ( ( ( 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 ) ) )
76 75 ex 
 |-  ( 0 e. y -> ( n e. ( ZZ \ { 0 } ) -> ( ( ( 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 ) ) ) )
77 elsng 
 |-  ( 0 e. ZZ -> ( 0 e. { z } <-> 0 = z ) )
78 eqcom 
 |-  ( 0 = z <-> z = 0 )
79 77 78 bitrdi 
 |-  ( 0 e. ZZ -> ( 0 e. { z } <-> z = 0 ) )
80 6 79 ax-mp 
 |-  ( 0 e. { z } <-> z = 0 )
81 80 biimpri 
 |-  ( z = 0 -> 0 e. { z } )
82 81 ad2antrr 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> 0 e. { z } )
83 82 olcd 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( 0 e. y \/ 0 e. { z } ) )
84 elun 
 |-  ( 0 e. ( y u. { z } ) <-> ( 0 e. y \/ 0 e. { z } ) )
85 83 84 sylibr 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> 0 e. ( y u. { z } ) )
86 12 85 48 syl2an2 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( _lcm ` ( y u. { z } ) ) = 0 )
87 86 oveq2d 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( n lcm ( _lcm ` ( y u. { z } ) ) ) = ( n lcm 0 ) )
88 51 ad2antlr 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> n e. ZZ )
89 88 52 syl 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( n lcm 0 ) = 0 )
90 87 89 eqtrd 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( n lcm ( _lcm ` ( y u. { z } ) ) ) = 0 )
91 59 88 61 syl2an2 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) = ( n lcm ( _lcm ` ( y u. { z } ) ) ) )
92 12 adantl 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( y u. { z } ) C_ ZZ )
93 64 ad2antlr 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> { n } C_ ZZ )
94 92 93 unssd 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( ( y u. { z } ) u. { n } ) C_ ZZ )
95 sneq 
 |-  ( z = 0 -> { z } = { 0 } )
96 17 95 eleqtrrid 
 |-  ( z = 0 -> 0 e. { z } )
97 96 ad2antrr 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> 0 e. { z } )
98 97 olcd 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( 0 e. y \/ 0 e. { z } ) )
99 98 84 sylibr 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> 0 e. ( y u. { z } ) )
100 99 orcd 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( 0 e. ( y u. { z } ) \/ 0 e. { n } ) )
101 100 68 sylibr 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> 0 e. ( ( y u. { z } ) u. { n } ) )
102 94 101 71 syl2anc 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = 0 )
103 90 91 102 3eqtr4rd 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )
104 103 a1d 
 |-  ( ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) /\ ( 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 ) ) )
105 104 expimpd 
 |-  ( ( z = 0 /\ n e. ( ZZ \ { 0 } ) ) -> ( ( ( 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 ) ) )
106 105 ex 
 |-  ( z = 0 -> ( n e. ( ZZ \ { 0 } ) -> ( ( ( 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 ) ) ) )
107 ioran 
 |-  ( -. ( 0 e. y \/ z = 0 ) <-> ( -. 0 e. y /\ -. z = 0 ) )
108 df-nel 
 |-  ( 0 e/ y <-> -. 0 e. y )
109 df-ne 
 |-  ( z =/= 0 <-> -. z = 0 )
110 108 109 anbi12i 
 |-  ( ( 0 e/ y /\ z =/= 0 ) <-> ( -. 0 e. y /\ -. z = 0 ) )
111 107 110 bitr4i 
 |-  ( -. ( 0 e. y \/ z = 0 ) <-> ( 0 e/ y /\ z =/= 0 ) )
112 eldif 
 |-  ( n e. ( ZZ \ { 0 } ) <-> ( n e. ZZ /\ -. n e. { 0 } ) )
113 velsn 
 |-  ( n e. { 0 } <-> n = 0 )
114 113 bicomi 
 |-  ( n = 0 <-> n e. { 0 } )
115 114 necon3abii 
 |-  ( n =/= 0 <-> -. n e. { 0 } )
116 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 ) )
117 116 exp520 
 |-  ( 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 ) ) ) ) ) )
118 117 imp 
 |-  ( ( 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 ) ) ) ) )
119 115 118 syl5bir 
 |-  ( ( 0 e/ y /\ z =/= 0 ) -> ( -. n e. { 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 ) ) ) ) )
120 119 impcomd 
 |-  ( ( 0 e/ y /\ z =/= 0 ) -> ( ( n e. ZZ /\ -. n e. { 0 } ) -> ( ( ( 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 ) ) ) )
121 112 120 syl5bi 
 |-  ( ( 0 e/ y /\ z =/= 0 ) -> ( n e. ( ZZ \ { 0 } ) -> ( ( ( 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 ) ) ) )
122 111 121 sylbi 
 |-  ( -. ( 0 e. y \/ z = 0 ) -> ( n e. ( ZZ \ { 0 } ) -> ( ( ( 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 ) ) ) )
123 76 106 122 ecase3 
 |-  ( n e. ( ZZ \ { 0 } ) -> ( ( ( 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 ) ) )
124 42 123 jaoi 
 |-  ( ( n = 0 \/ n e. ( ZZ \ { 0 } ) ) -> ( ( ( 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 ) ) )
125 8 124 sylbi 
 |-  ( 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 ) ) )
126 125 com12 
 |-  ( ( ( 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 -> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
127 5 126 ralrimi 
 |-  ( ( ( 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. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )