Metamath Proof Explorer

Theorem expdiophlem2

Description: Lemma for expdioph . Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014)

Ref Expression
Assertion expdiophlem2 { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) โ†‘ ( ๐‘Ž โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 3 )

Proof

Step Hyp Ref Expression
1 elmapi โŠข ( ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โ†’ ๐‘Ž : ( 1 ... 3 ) โŸถ โ„•0 )
2 3nn โŠข 3 โˆˆ โ„•
3 2 jm2.27dlem3 โŠข 3 โˆˆ ( 1 ... 3 )
4 ffvelrn โŠข ( ( ๐‘Ž : ( 1 ... 3 ) โŸถ โ„•0 โˆง 3 โˆˆ ( 1 ... 3 ) ) โ†’ ( ๐‘Ž โ€˜ 3 ) โˆˆ โ„•0 )
5 1 3 4 sylancl โŠข ( ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โ†’ ( ๐‘Ž โ€˜ 3 ) โˆˆ โ„•0 )
6 expdiophlem1 โŠข ( ( ๐‘Ž โ€˜ 3 ) โˆˆ โ„•0 โ†’ ( ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) โ†‘ ( ๐‘Ž โ€˜ 2 ) ) ) โ†” โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„•0 ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) ) )
7 5 6 syl โŠข ( ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โ†’ ( ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) โ†‘ ( ๐‘Ž โ€˜ 2 ) ) ) โ†” โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„•0 ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) ) )
8 7 rabbiia โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) โ†‘ ( ๐‘Ž โ€˜ 2 ) ) ) } = { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„•0 ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) }
9 3nn0 โŠข 3 โˆˆ โ„•0
10 fvex โŠข ( ๐‘’ โ€˜ 5 ) โˆˆ V
11 fvex โŠข ( ๐‘’ โ€˜ 6 ) โˆˆ V
12 eqeq1 โŠข ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โ†’ ( ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) โ†” ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) )
13 12 anbi2d โŠข ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โ†” ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) ) )
14 13 adantr โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โ†” ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) ) )
15 eqeq1 โŠข ( ๐‘‘ = ( ๐‘’ โ€˜ 6 ) โ†’ ( ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) โ†” ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) )
16 15 anbi2d โŠข ( ๐‘‘ = ( ๐‘’ โ€˜ 6 ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โ†” ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) ) )
17 16 adantl โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โ†” ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) ) )
18 simpr โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ๐‘‘ = ( ๐‘’ โ€˜ 6 ) )
19 oveq2 โŠข ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โ†’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) = ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) )
20 19 adantr โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) = ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) )
21 18 20 oveq12d โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) = ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) )
22 21 oveq1d โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) = ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) )
23 22 breq2d โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) โ†” ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) )
24 23 anbi2d โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) โ†” ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) )
25 17 24 anbi12d โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) โ†” ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) )
26 14 25 anbi12d โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) โ†” ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) )
27 26 anbi2d โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) โ†” ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) )
28 27 anbi2d โŠข ( ( ๐‘ = ( ๐‘’ โ€˜ 5 ) โˆง ๐‘‘ = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) โ†” ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) ) )
29 10 11 28 sbc2ie โŠข ( [ ( ๐‘’ โ€˜ 5 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 6 ) / ๐‘‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) โ†” ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) )
30 29 sbcbii โŠข ( [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 5 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 6 ) / ๐‘‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) โ†” [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) )
31 30 sbcbii โŠข ( [ ( ๐‘’ โ†พ ( 1 ... 3 ) ) / ๐‘Ž ] [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 5 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 6 ) / ๐‘‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) โ†” [ ( ๐‘’ โ†พ ( 1 ... 3 ) ) / ๐‘Ž ] [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) )
32 vex โŠข ๐‘’ โˆˆ V
33 32 resex โŠข ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆˆ V
34 fvex โŠข ( ๐‘’ โ€˜ 4 ) โˆˆ V
35 df-2 โŠข 2 = ( 1 + 1 )
36 df-3 โŠข 3 = ( 2 + 1 )
37 ssid โŠข ( 1 ... 3 ) โŠ† ( 1 ... 3 )
38 36 37 jm2.27dlem5 โŠข ( 1 ... 2 ) โŠ† ( 1 ... 3 )
39 35 38 jm2.27dlem5 โŠข ( 1 ... 1 ) โŠ† ( 1 ... 3 )
40 1nn โŠข 1 โˆˆ โ„•
41 40 jm2.27dlem3 โŠข 1 โˆˆ ( 1 ... 1 )
42 39 41 sselii โŠข 1 โˆˆ ( 1 ... 3 )
43 42 jm2.27dlem1 โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 1 ) )
44 43 eleq1d โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
45 2nn โŠข 2 โˆˆ โ„•
46 45 jm2.27dlem3 โŠข 2 โˆˆ ( 1 ... 2 )
47 46 36 45 jm2.27dlem2 โŠข 2 โˆˆ ( 1 ... 3 )
48 47 jm2.27dlem1 โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) )
49 48 eleq1d โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• โ†” ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) )
50 44 49 anbi12d โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โ†” ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) ) )
51 50 adantr โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โ†” ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) ) )
52 44 adantr โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
53 id โŠข ( ๐‘ = ( ๐‘’ โ€˜ 4 ) โ†’ ๐‘ = ( ๐‘’ โ€˜ 4 ) )
54 48 oveq1d โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ( ๐‘Ž โ€˜ 2 ) + 1 ) = ( ( ๐‘’ โ€˜ 2 ) + 1 ) )
55 43 54 oveq12d โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) )
56 53 55 eqeqan12rd โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) โ†” ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) )
57 52 56 anbi12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โ†” ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) ) )
58 eleq1 โŠข ( ๐‘ = ( ๐‘’ โ€˜ 4 ) โ†’ ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
59 58 adantl โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
60 53 48 oveqan12rd โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) )
61 60 eqeq2d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) โ†” ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) )
62 59 61 anbi12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โ†” ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) ) )
63 53 48 oveqan12rd โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) )
64 63 eqeq2d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) โ†” ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) )
65 59 64 anbi12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โ†” ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) ) )
66 3 jm2.27dlem1 โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 3 ) )
67 66 adantr โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 3 ) )
68 oveq2 โŠข ( ๐‘ = ( ๐‘’ โ€˜ 4 ) โ†’ ( 2 ยท ๐‘ ) = ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) )
69 68 43 oveqan12rd โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) = ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) )
70 43 oveq1d โŠข ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) = ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) )
71 70 adantr โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) = ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) )
72 69 71 oveq12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) = ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) )
73 72 oveq1d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) = ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) )
74 67 73 breq12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โ†” ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) ) )
75 simpr โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ๐‘ = ( ๐‘’ โ€˜ 4 ) )
76 43 adantr โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 1 ) )
77 75 76 oveq12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) = ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) )
78 77 oveq1d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) = ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) )
79 78 oveq2d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) = ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) )
80 79 67 oveq12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) = ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) )
81 73 80 breq12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) โ†” ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) )
82 74 81 anbi12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) โ†” ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) )
83 65 82 anbi12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) โ†” ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) )
84 62 83 anbi12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) โ†” ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) )
85 57 84 anbi12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) โ†” ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) ) )
86 51 85 anbi12d โŠข ( ( ๐‘Ž = ( ๐‘’ โ†พ ( 1 ... 3 ) ) โˆง ๐‘ = ( ๐‘’ โ€˜ 4 ) ) โ†’ ( ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) โ†” ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) ) ) )
87 33 34 86 sbc2ie โŠข ( [ ( ๐‘’ โ†พ ( 1 ... 3 ) ) / ๐‘Ž ] [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) โ†” ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) ) )
88 31 87 bitri โŠข ( [ ( ๐‘’ โ†พ ( 1 ... 3 ) ) / ๐‘Ž ] [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 5 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 6 ) / ๐‘‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) โ†” ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) ) )
89 88 rabbii โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ [ ( ๐‘’ โ†พ ( 1 ... 3 ) ) / ๐‘Ž ] [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 5 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 6 ) / ๐‘‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) } = { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) ) }
90 6nn0 โŠข 6 โˆˆ โ„•0
91 2z โŠข 2 โˆˆ โ„ค
92 ovex โŠข ( 1 ... 6 ) โˆˆ V
93 df-4 โŠข 4 = ( 3 + 1 )
94 df-5 โŠข 5 = ( 4 + 1 )
95 df-6 โŠข 6 = ( 5 + 1 )
96 ssid โŠข ( 1 ... 6 ) โŠ† ( 1 ... 6 )
97 95 96 jm2.27dlem5 โŠข ( 1 ... 5 ) โŠ† ( 1 ... 6 )
98 94 97 jm2.27dlem5 โŠข ( 1 ... 4 ) โŠ† ( 1 ... 6 )
99 93 98 jm2.27dlem5 โŠข ( 1 ... 3 ) โŠ† ( 1 ... 6 )
100 36 99 jm2.27dlem5 โŠข ( 1 ... 2 ) โŠ† ( 1 ... 6 )
101 35 100 jm2.27dlem5 โŠข ( 1 ... 1 ) โŠ† ( 1 ... 6 )
102 101 41 sselii โŠข 1 โˆˆ ( 1 ... 6 )
103 mzpproj โŠข ( ( ( 1 ... 6 ) โˆˆ V โˆง 1 โˆˆ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
104 92 102 103 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
105 eluzrabdioph โŠข ( ( 6 โˆˆ โ„•0 โˆง 2 โˆˆ โ„ค โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) } โˆˆ ( Dioph โ€˜ 6 ) )
106 90 91 104 105 mp3an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) } โˆˆ ( Dioph โ€˜ 6 )
107 100 46 sselii โŠข 2 โˆˆ ( 1 ... 6 )
108 mzpproj โŠข ( ( ( 1 ... 6 ) โˆˆ V โˆง 2 โˆˆ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
109 92 107 108 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
110 elnnrabdioph โŠข ( ( 6 โˆˆ โ„•0 โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• } โˆˆ ( Dioph โ€˜ 6 ) )
111 90 109 110 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• } โˆˆ ( Dioph โ€˜ 6 )
112 anrabdioph โŠข ( ( { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) } โˆˆ ( Dioph โ€˜ 6 ) โˆง { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• } โˆˆ ( Dioph โ€˜ 6 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) } โˆˆ ( Dioph โ€˜ 6 ) )
113 106 111 112 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) } โˆˆ ( Dioph โ€˜ 6 )
114 elmapi โŠข ( ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โ†’ ๐‘’ : ( 1 ... 6 ) โŸถ โ„•0 )
115 ffvelrn โŠข ( ( ๐‘’ : ( 1 ... 6 ) โŸถ โ„•0 โˆง 2 โˆˆ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โ€˜ 2 ) โˆˆ โ„•0 )
116 114 107 115 sylancl โŠข ( ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โ†’ ( ๐‘’ โ€˜ 2 ) โˆˆ โ„•0 )
117 peano2nn0 โŠข ( ( ๐‘’ โ€˜ 2 ) โˆˆ โ„•0 โ†’ ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆˆ โ„•0 )
118 oveq2 โŠข ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โ†’ ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) )
119 118 eqeq2d โŠข ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โ†’ ( ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) โ†” ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) )
120 119 anbi2d โŠข ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โ†’ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) โ†” ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) ) )
121 120 ceqsrexv โŠข ( ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆˆ โ„•0 โ†’ ( โˆƒ ๐‘ โˆˆ โ„•0 ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) โ†” ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) ) )
122 116 117 121 3syl โŠข ( ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โ†’ ( โˆƒ ๐‘ โˆˆ โ„•0 ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) โ†” ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) ) )
123 122 bicomd โŠข ( ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โ†’ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โ†” โˆƒ ๐‘ โˆˆ โ„•0 ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) ) )
124 123 rabbiia โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) } = { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) }
125 vex โŠข ๐‘Ž โˆˆ V
126 125 resex โŠข ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆˆ V
127 fvex โŠข ( ๐‘Ž โ€˜ 7 ) โˆˆ V
128 id โŠข ( ๐‘ = ( ๐‘Ž โ€˜ 7 ) โ†’ ๐‘ = ( ๐‘Ž โ€˜ 7 ) )
129 107 jm2.27dlem1 โŠข ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 2 ) )
130 129 oveq1d โŠข ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โ†’ ( ( ๐‘’ โ€˜ 2 ) + 1 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) )
131 128 130 eqeqan12rd โŠข ( ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆง ๐‘ = ( ๐‘Ž โ€˜ 7 ) ) โ†’ ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โ†” ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) )
132 102 jm2.27dlem1 โŠข ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) )
133 132 adantr โŠข ( ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆง ๐‘ = ( ๐‘Ž โ€˜ 7 ) ) โ†’ ( ๐‘’ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) )
134 133 eleq1d โŠข ( ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆง ๐‘ = ( ๐‘Ž โ€˜ 7 ) ) โ†’ ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
135 4nn โŠข 4 โˆˆ โ„•
136 135 jm2.27dlem3 โŠข 4 โˆˆ ( 1 ... 4 )
137 98 136 sselii โŠข 4 โˆˆ ( 1 ... 6 )
138 137 jm2.27dlem1 โŠข ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โ€˜ 4 ) = ( ๐‘Ž โ€˜ 4 ) )
139 138 adantr โŠข ( ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆง ๐‘ = ( ๐‘Ž โ€˜ 7 ) ) โ†’ ( ๐‘’ โ€˜ 4 ) = ( ๐‘Ž โ€˜ 4 ) )
140 132 128 oveqan12d โŠข ( ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆง ๐‘ = ( ๐‘Ž โ€˜ 7 ) ) โ†’ ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) )
141 139 140 eqeq12d โŠข ( ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆง ๐‘ = ( ๐‘Ž โ€˜ 7 ) ) โ†’ ( ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) โ†” ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) )
142 134 141 anbi12d โŠข ( ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆง ๐‘ = ( ๐‘Ž โ€˜ 7 ) ) โ†’ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) โ†” ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) ) )
143 131 142 anbi12d โŠข ( ( ๐‘’ = ( ๐‘Ž โ†พ ( 1 ... 6 ) ) โˆง ๐‘ = ( ๐‘Ž โ€˜ 7 ) ) โ†’ ( ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) โ†” ( ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) ) ) )
144 126 127 143 sbc2ie โŠข ( [ ( ๐‘Ž โ†พ ( 1 ... 6 ) ) / ๐‘’ ] [ ( ๐‘Ž โ€˜ 7 ) / ๐‘ ] ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) โ†” ( ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) ) )
145 144 rabbii โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ [ ( ๐‘Ž โ†พ ( 1 ... 6 ) ) / ๐‘’ ] [ ( ๐‘Ž โ€˜ 7 ) / ๐‘ ] ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) } = { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) ) }
146 7nn0 โŠข 7 โˆˆ โ„•0
147 ovex โŠข ( 1 ... 7 ) โˆˆ V
148 7nn โŠข 7 โˆˆ โ„•
149 148 jm2.27dlem3 โŠข 7 โˆˆ ( 1 ... 7 )
150 mzpproj โŠข ( ( ( 1 ... 7 ) โˆˆ V โˆง 7 โˆˆ ( 1 ... 7 ) ) โ†’ ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ๐‘Ž โ€˜ 7 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) ) )
151 147 149 150 mp2an โŠข ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ๐‘Ž โ€˜ 7 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) )
152 df-7 โŠข 7 = ( 6 + 1 )
153 6nn โŠข 6 โˆˆ โ„•
154 107 152 153 jm2.27dlem2 โŠข 2 โˆˆ ( 1 ... 7 )
155 mzpproj โŠข ( ( ( 1 ... 7 ) โˆˆ V โˆง 2 โˆˆ ( 1 ... 7 ) ) โ†’ ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ๐‘Ž โ€˜ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) ) )
156 147 154 155 mp2an โŠข ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ๐‘Ž โ€˜ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) )
157 1z โŠข 1 โˆˆ โ„ค
158 mzpconstmpt โŠข ( ( ( 1 ... 7 ) โˆˆ V โˆง 1 โˆˆ โ„ค ) โ†’ ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ 1 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) ) )
159 147 157 158 mp2an โŠข ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ 1 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) )
160 mzpaddmpt โŠข ( ( ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ๐‘Ž โ€˜ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) ) โˆง ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ 1 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) ) ) โ†’ ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) ) )
161 156 159 160 mp2an โŠข ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) )
162 eqrabdioph โŠข ( ( 7 โˆˆ โ„•0 โˆง ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ๐‘Ž โ€˜ 7 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) ) โˆง ( ๐‘Ž โˆˆ ( โ„ค โ†‘m ( 1 ... 7 ) ) โ†ฆ ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 7 ) ) ) โ†’ { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) } โˆˆ ( Dioph โ€˜ 7 ) )
163 146 151 161 162 mp3an โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) } โˆˆ ( Dioph โ€˜ 7 )
164 rmydioph โŠข { ๐‘ โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ๐‘ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ( ๐‘ โ€˜ 1 ) Yrm ( ๐‘ โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 3 )
165 simp1 โŠข ( ( ( ๐‘ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) โˆง ( ๐‘ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 7 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ๐‘Ž โ€˜ 4 ) ) โ†’ ( ๐‘ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) )
166 165 eleq1d โŠข ( ( ( ๐‘ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) โˆง ( ๐‘ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 7 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ๐‘Ž โ€˜ 4 ) ) โ†’ ( ( ๐‘ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
167 simp3 โŠข ( ( ( ๐‘ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) โˆง ( ๐‘ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 7 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ๐‘Ž โ€˜ 4 ) ) โ†’ ( ๐‘ โ€˜ 3 ) = ( ๐‘Ž โ€˜ 4 ) )
168 simp2 โŠข ( ( ( ๐‘ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) โˆง ( ๐‘ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 7 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ๐‘Ž โ€˜ 4 ) ) โ†’ ( ๐‘ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 7 ) )
169 165 168 oveq12d โŠข ( ( ( ๐‘ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) โˆง ( ๐‘ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 7 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ๐‘Ž โ€˜ 4 ) ) โ†’ ( ( ๐‘ โ€˜ 1 ) Yrm ( ๐‘ โ€˜ 2 ) ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) )
170 167 169 eqeq12d โŠข ( ( ( ๐‘ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) โˆง ( ๐‘ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 7 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ๐‘Ž โ€˜ 4 ) ) โ†’ ( ( ๐‘ โ€˜ 3 ) = ( ( ๐‘ โ€˜ 1 ) Yrm ( ๐‘ โ€˜ 2 ) ) โ†” ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) )
171 166 170 anbi12d โŠข ( ( ( ๐‘ โ€˜ 1 ) = ( ๐‘Ž โ€˜ 1 ) โˆง ( ๐‘ โ€˜ 2 ) = ( ๐‘Ž โ€˜ 7 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ๐‘Ž โ€˜ 4 ) ) โ†’ ( ( ( ๐‘ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ( ๐‘ โ€˜ 1 ) Yrm ( ๐‘ โ€˜ 2 ) ) ) โ†” ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) ) )
172 102 152 153 jm2.27dlem2 โŠข 1 โˆˆ ( 1 ... 7 )
173 137 152 153 jm2.27dlem2 โŠข 4 โˆˆ ( 1 ... 7 )
174 171 172 149 173 rabren3dioph โŠข ( ( 7 โˆˆ โ„•0 โˆง { ๐‘ โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ๐‘ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘ โ€˜ 3 ) = ( ( ๐‘ โ€˜ 1 ) Yrm ( ๐‘ โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 3 ) ) โ†’ { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) } โˆˆ ( Dioph โ€˜ 7 ) )
175 146 164 174 mp2an โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) } โˆˆ ( Dioph โ€˜ 7 )
176 anrabdioph โŠข ( ( { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) } โˆˆ ( Dioph โ€˜ 7 ) โˆง { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) } โˆˆ ( Dioph โ€˜ 7 ) ) โ†’ { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) ) } โˆˆ ( Dioph โ€˜ 7 ) )
177 163 175 176 mp2an โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 7 ) = ( ( ๐‘Ž โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 4 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 7 ) ) ) ) } โˆˆ ( Dioph โ€˜ 7 )
178 145 177 eqeltri โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ [ ( ๐‘Ž โ†พ ( 1 ... 6 ) ) / ๐‘’ ] [ ( ๐‘Ž โ€˜ 7 ) / ๐‘ ] ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) } โˆˆ ( Dioph โ€˜ 7 )
179 152 rexfrabdioph โŠข ( ( 6 โˆˆ โ„•0 โˆง { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 7 ) ) โˆฃ [ ( ๐‘Ž โ†พ ( 1 ... 6 ) ) / ๐‘’ ] [ ( ๐‘Ž โ€˜ 7 ) / ๐‘ ] ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) } โˆˆ ( Dioph โ€˜ 7 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
180 90 178 179 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 ( ๐‘ = ( ( ๐‘’ โ€˜ 2 ) + 1 ) โˆง ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ๐‘ ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
181 124 180 eqeltri โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
182 rmydioph โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 3 )
183 simp1 โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 5 ) ) โ†’ ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) )
184 183 eleq1d โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 5 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
185 simp3 โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 5 ) ) โ†’ ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 5 ) )
186 simp2 โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 5 ) ) โ†’ ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) )
187 183 186 oveq12d โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 5 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 2 ) ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) )
188 185 187 eqeq12d โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 5 ) ) โ†’ ( ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 2 ) ) โ†” ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) )
189 184 188 anbi12d โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 5 ) ) โ†’ ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โ†” ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) ) )
190 5nn โŠข 5 โˆˆ โ„•
191 190 jm2.27dlem3 โŠข 5 โˆˆ ( 1 ... 5 )
192 191 95 190 jm2.27dlem2 โŠข 5 โˆˆ ( 1 ... 6 )
193 189 137 107 192 rabren3dioph โŠข ( ( 6 โˆˆ โ„•0 โˆง { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ๐‘Ž โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 3 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
194 90 182 193 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
195 rmxdioph โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) Xrm ( ๐‘Ž โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 3 )
196 simp1 โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) )
197 196 eleq1d โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
198 simp3 โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 6 ) )
199 simp2 โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) )
200 196 199 oveq12d โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ๐‘Ž โ€˜ 1 ) Xrm ( ๐‘Ž โ€˜ 2 ) ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) )
201 198 200 eqeq12d โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) Xrm ( ๐‘Ž โ€˜ 2 ) ) โ†” ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) )
202 197 201 anbi12d โŠข ( ( ( ๐‘Ž โ€˜ 1 ) = ( ๐‘’ โ€˜ 4 ) โˆง ( ๐‘Ž โ€˜ 2 ) = ( ๐‘’ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ๐‘’ โ€˜ 6 ) ) โ†’ ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โ†” ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) ) )
203 153 jm2.27dlem3 โŠข 6 โˆˆ ( 1 ... 6 )
204 202 137 107 203 rabren3dioph โŠข ( ( 6 โˆˆ โ„•0 โˆง { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) Xrm ( ๐‘Ž โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 3 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
205 90 195 204 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
206 99 3 sselii โŠข 3 โˆˆ ( 1 ... 6 )
207 mzpproj โŠข ( ( ( 1 ... 6 ) โˆˆ V โˆง 3 โˆˆ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 3 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
208 92 206 207 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 3 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
209 mzpconstmpt โŠข ( ( ( 1 ... 6 ) โˆˆ V โˆง 2 โˆˆ โ„ค ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ 2 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
210 92 91 209 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ 2 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
211 mzpproj โŠข ( ( ( 1 ... 6 ) โˆˆ V โˆง 4 โˆˆ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 4 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
212 92 137 211 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 4 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
213 mzpmulmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ 2 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 4 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
214 210 212 213 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
215 mzpmulmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
216 214 104 215 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
217 2nn0 โŠข 2 โˆˆ โ„•0
218 mzpexpmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง 2 โˆˆ โ„•0 ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
219 104 217 218 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
220 mzpsubmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
221 216 219 220 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
222 mzpconstmpt โŠข ( ( ( 1 ... 6 ) โˆˆ V โˆง 1 โˆˆ โ„ค ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ 1 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
223 92 157 222 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ 1 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
224 mzpsubmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ 1 ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
225 221 223 224 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
226 ltrabdioph โŠข ( ( 6 โˆˆ โ„•0 โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 3 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) } โˆˆ ( Dioph โ€˜ 6 ) )
227 90 208 225 226 mp3an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) } โˆˆ ( Dioph โ€˜ 6 )
228 mzpproj โŠข ( ( ( 1 ... 6 ) โˆˆ V โˆง 6 โˆˆ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 6 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
229 92 203 228 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 6 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
230 mzpsubmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 4 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
231 212 104 230 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
232 mzpproj โŠข ( ( ( 1 ... 6 ) โˆˆ V โˆง 5 โˆˆ ( 1 ... 6 ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 5 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
233 92 192 232 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 5 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
234 mzpmulmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 5 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
235 231 233 234 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
236 mzpsubmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 6 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
237 229 235 236 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
238 mzpsubmpt โŠข ( ( ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ๐‘’ โ€˜ 3 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) )
239 237 208 238 mp2an โŠข ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) )
240 dvdsrabdioph โŠข ( ( 6 โˆˆ โ„•0 โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) โˆง ( ๐‘’ โˆˆ ( โ„ค โ†‘m ( 1 ... 6 ) ) โ†ฆ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) โˆˆ ( mzPoly โ€˜ ( 1 ... 6 ) ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
241 90 225 239 240 mp3an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) } โˆˆ ( Dioph โ€˜ 6 )
242 anrabdioph โŠข ( ( { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) } โˆˆ ( Dioph โ€˜ 6 ) โˆง { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) } โˆˆ ( Dioph โ€˜ 6 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
243 227 241 242 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
244 anrabdioph โŠข ( ( { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) โˆง { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
245 205 243 244 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
246 anrabdioph โŠข ( ( { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) โˆง { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
247 194 245 246 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
248 anrabdioph โŠข ( ( { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) โˆง { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
249 181 247 248 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
250 anrabdioph โŠข ( ( { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) } โˆˆ ( Dioph โ€˜ 6 ) โˆง { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) ) โ†’ { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) )
251 113 249 250 mp2an โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘’ โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 4 ) = ( ( ๐‘’ โ€˜ 1 ) Yrm ( ( ๐‘’ โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 5 ) = ( ( ๐‘’ โ€˜ 4 ) Yrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ( ๐‘’ โ€˜ 4 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘’ โ€˜ 6 ) = ( ( ๐‘’ โ€˜ 4 ) Xrm ( ๐‘’ โ€˜ 2 ) ) ) โˆง ( ( ๐‘’ โ€˜ 3 ) < ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ( ๐‘’ โ€˜ 4 ) ) ยท ( ๐‘’ โ€˜ 1 ) ) โˆ’ ( ( ๐‘’ โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ( ๐‘’ โ€˜ 6 ) โˆ’ ( ( ( ๐‘’ โ€˜ 4 ) โˆ’ ( ๐‘’ โ€˜ 1 ) ) ยท ( ๐‘’ โ€˜ 5 ) ) ) โˆ’ ( ๐‘’ โ€˜ 3 ) ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
252 89 251 eqeltri โŠข { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ [ ( ๐‘’ โ†พ ( 1 ... 3 ) ) / ๐‘Ž ] [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 5 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 6 ) / ๐‘‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 )
253 93 94 95 3rexfrabdioph โŠข ( ( 3 โˆˆ โ„•0 โˆง { ๐‘’ โˆˆ ( โ„•0 โ†‘m ( 1 ... 6 ) ) โˆฃ [ ( ๐‘’ โ†พ ( 1 ... 3 ) ) / ๐‘Ž ] [ ( ๐‘’ โ€˜ 4 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 5 ) / ๐‘ ] [ ( ๐‘’ โ€˜ 6 ) / ๐‘‘ ] ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 6 ) ) โ†’ { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„•0 ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 3 ) )
254 9 252 253 mp2an โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„•0 ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ( ๐‘Ž โ€˜ 1 ) Yrm ( ( ๐‘Ž โ€˜ 2 ) + 1 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ = ( ๐‘ Yrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‘ = ( ๐‘ Xrm ( ๐‘Ž โ€˜ 2 ) ) ) โˆง ( ( ๐‘Ž โ€˜ 3 ) < ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆง ( ( ( ( 2 ยท ๐‘ ) ยท ( ๐‘Ž โ€˜ 1 ) ) โˆ’ ( ( ๐‘Ž โ€˜ 1 ) โ†‘ 2 ) ) โˆ’ 1 ) โˆฅ ( ( ๐‘‘ โˆ’ ( ( ๐‘ โˆ’ ( ๐‘Ž โ€˜ 1 ) ) ยท ๐‘ ) ) โˆ’ ( ๐‘Ž โ€˜ 3 ) ) ) ) ) ) ) } โˆˆ ( Dioph โ€˜ 3 )
255 8 254 eqeltri โŠข { ๐‘Ž โˆˆ ( โ„•0 โ†‘m ( 1 ... 3 ) ) โˆฃ ( ( ( ๐‘Ž โ€˜ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘Ž โ€˜ 2 ) โˆˆ โ„• ) โˆง ( ๐‘Ž โ€˜ 3 ) = ( ( ๐‘Ž โ€˜ 1 ) โ†‘ ( ๐‘Ž โ€˜ 2 ) ) ) } โˆˆ ( Dioph โ€˜ 3 )