Metamath Proof Explorer

Theorem lcmfunsnlem1

Description: Lemma for lcmfdvds and lcmfunsnlem (Induction step part 1). (Contributed by AV, 25-Aug-2020)

Ref Expression
Assertion lcmfunsnlem1 
|- ( ( ( 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. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ k ( z e. ZZ /\ y C_ ZZ /\ y e. Fin )
2 nfra1 
 |-  F/ k A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k )
3 nfv 
 |-  F/ k A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n )
4 2 3 nfan 
 |-  F/ k ( 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/ k ( ( 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 breq2 
 |-  ( k = l -> ( m || k <-> m || l ) )
7 6 ralbidv 
 |-  ( k = l -> ( A. m e. y m || k <-> A. m e. y m || l ) )
8 breq2 
 |-  ( k = l -> ( ( _lcm ` y ) || k <-> ( _lcm ` y ) || l ) )
9 7 8 imbi12d 
 |-  ( k = l -> ( ( A. m e. y m || k -> ( _lcm ` y ) || k ) <-> ( A. m e. y m || l -> ( _lcm ` y ) || l ) ) )
10 9 cbvralvw 
 |-  ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) <-> A. l e. ZZ ( A. m e. y m || l -> ( _lcm ` y ) || l ) )
11 breq2 
 |-  ( l = k -> ( m || l <-> m || k ) )
12 11 ralbidv 
 |-  ( l = k -> ( A. m e. y m || l <-> A. m e. y m || k ) )
13 breq2 
 |-  ( l = k -> ( ( _lcm ` y ) || l <-> ( _lcm ` y ) || k ) )
14 12 13 imbi12d 
 |-  ( l = k -> ( ( A. m e. y m || l -> ( _lcm ` y ) || l ) <-> ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
15 14 rspcv 
 |-  ( k e. ZZ -> ( A. l e. ZZ ( A. m e. y m || l -> ( _lcm ` y ) || l ) -> ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
16 15 adantl 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( A. l e. ZZ ( A. m e. y m || l -> ( _lcm ` y ) || l ) -> ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
17 sneq 
 |-  ( n = z -> { n } = { z } )
18 17 uneq2d 
 |-  ( n = z -> ( y u. { n } ) = ( y u. { z } ) )
19 18 fveq2d 
 |-  ( n = z -> ( _lcm ` ( y u. { n } ) ) = ( _lcm ` ( y u. { z } ) ) )
20 oveq2 
 |-  ( n = z -> ( ( _lcm ` y ) lcm n ) = ( ( _lcm ` y ) lcm z ) )
21 19 20 eqeq12d 
 |-  ( n = z -> ( ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) <-> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
22 21 rspcv 
 |-  ( z e. ZZ -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
23 22 3ad2ant1 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
24 23 adantr 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
25 simpr 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> k e. ZZ )
26 lcmfcl 
 |-  ( ( y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. NN0 )
27 26 nn0zd 
 |-  ( ( y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. ZZ )
28 27 3adant1 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. ZZ )
29 28 adantr 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( _lcm ` y ) e. ZZ )
30 simpl1 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> z e. ZZ )
31 25 29 30 3jca 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( k e. ZZ /\ ( _lcm ` y ) e. ZZ /\ z e. ZZ ) )
32 31 adantr 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) -> ( k e. ZZ /\ ( _lcm ` y ) e. ZZ /\ z e. ZZ ) )
33 32 adantr 
 |-  ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ A. m e. ( y u. { z } ) m || k ) -> ( k e. ZZ /\ ( _lcm ` y ) e. ZZ /\ z e. ZZ ) )
34 ssun1 
 |-  y C_ ( y u. { z } )
35 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. m e. ( y u. { z } ) m || k -> A. m e. y m || k ) )
36 34 35 mp1i 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( A. m e. ( y u. { z } ) m || k -> A. m e. y m || k ) )
37 36 imim1d 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` y ) || k ) ) )
38 37 imp31 
 |-  ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ A. m e. ( y u. { z } ) m || k ) -> ( _lcm ` y ) || k )
39 snidg 
 |-  ( z e. ZZ -> z e. { z } )
40 39 olcd 
 |-  ( z e. ZZ -> ( z e. y \/ z e. { z } ) )
41 elun 
 |-  ( z e. ( y u. { z } ) <-> ( z e. y \/ z e. { z } ) )
42 40 41 sylibr 
 |-  ( z e. ZZ -> z e. ( y u. { z } ) )
43 breq1 
 |-  ( m = z -> ( m || k <-> z || k ) )
44 43 rspcv 
 |-  ( z e. ( y u. { z } ) -> ( A. m e. ( y u. { z } ) m || k -> z || k ) )
45 42 44 syl 
 |-  ( z e. ZZ -> ( A. m e. ( y u. { z } ) m || k -> z || k ) )
46 45 3ad2ant1 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( A. m e. ( y u. { z } ) m || k -> z || k ) )
47 46 adantr 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( A. m e. ( y u. { z } ) m || k -> z || k ) )
48 47 adantr 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) -> ( A. m e. ( y u. { z } ) m || k -> z || k ) )
49 48 imp 
 |-  ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ A. m e. ( y u. { z } ) m || k ) -> z || k )
50 38 49 jca 
 |-  ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ A. m e. ( y u. { z } ) m || k ) -> ( ( _lcm ` y ) || k /\ z || k ) )
51 lcmdvds 
 |-  ( ( k e. ZZ /\ ( _lcm ` y ) e. ZZ /\ z e. ZZ ) -> ( ( ( _lcm ` y ) || k /\ z || k ) -> ( ( _lcm ` y ) lcm z ) || k ) )
52 33 50 51 sylc 
 |-  ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ A. m e. ( y u. { z } ) m || k ) -> ( ( _lcm ` y ) lcm z ) || k )
53 breq1 
 |-  ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( ( _lcm ` ( y u. { z } ) ) || k <-> ( ( _lcm ` y ) lcm z ) || k ) )
54 52 53 syl5ibrcom 
 |-  ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ A. m e. ( y u. { z } ) m || k ) -> ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( _lcm ` ( y u. { z } ) ) || k ) )
55 54 ex 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) -> ( A. m e. ( y u. { z } ) m || k -> ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( _lcm ` ( y u. { z } ) ) || k ) ) )
56 55 com23 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) /\ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) -> ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) )
57 56 ex 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) )
58 24 57 syl5d 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ 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. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) )
59 16 58 syld 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( A. l e. ZZ ( A. m e. y m || l -> ( _lcm ` y ) || l ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) )
60 10 59 syl5bi 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( 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. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) )
61 60 impd 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ k e. ZZ ) -> ( ( 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. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) )
62 61 impancom 
 |-  ( ( ( 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 ) ) ) -> ( k e. ZZ -> ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) )
63 5 62 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. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) )