Metamath Proof Explorer

Theorem fmtnofac2lem

Description: Lemma for fmtnofac2 (Induction step). (Contributed by AV, 30-Jul-2021)

Ref Expression
Assertion fmtnofac2lem ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 eluzelz โŠข ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ฆ โˆˆ โ„ค )
2 1 adantr โŠข ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ๐‘ฆ โˆˆ โ„ค )
3 eluzelz โŠข ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ง โˆˆ โ„ค )
4 3 adantl โŠข ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ๐‘ง โˆˆ โ„ค )
5 eluzge2nn0 โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ โˆˆ โ„•0 )
6 fmtnonn โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ๐‘ ) โˆˆ โ„• )
7 6 nnzd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ๐‘ ) โˆˆ โ„ค )
8 5 7 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( FermatNo โ€˜ ๐‘ ) โˆˆ โ„ค )
9 muldvds2 โŠข ( ( ๐‘ฆ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค โˆง ( FermatNo โ€˜ ๐‘ ) โˆˆ โ„ค ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) )
10 2 4 8 9 syl2an3an โŠข ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) )
11 muldvds1 โŠข ( ( ๐‘ฆ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค โˆง ( FermatNo โ€˜ ๐‘ ) โˆˆ โ„ค ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) )
12 2 4 8 11 syl2an3an โŠข ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) )
13 pm2.27 โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
14 13 ad2ant2lr โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
15 pm2.27 โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
16 15 ad2ant2l โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
17 oveq1 โŠข ( ๐‘˜ = ๐‘š โ†’ ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) = ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) )
18 17 oveq1d โŠข ( ๐‘˜ = ๐‘š โ†’ ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
19 18 eqeq2d โŠข ( ๐‘˜ = ๐‘š โ†’ ( ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
20 19 cbvrexvw โŠข ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” โˆƒ ๐‘š โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
21 oveq1 โŠข ( ๐‘˜ = ๐‘› โ†’ ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) = ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) )
22 21 oveq1d โŠข ( ๐‘˜ = ๐‘› โ†’ ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
23 22 eqeq2d โŠข ( ๐‘˜ = ๐‘› โ†’ ( ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
24 23 cbvrexvw โŠข ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” โˆƒ ๐‘› โˆˆ โ„•0 ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
25 simpl โŠข ( ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ๐‘š โˆˆ โ„•0 )
26 25 adantl โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ๐‘š โˆˆ โ„•0 )
27 2nn0 โŠข 2 โˆˆ โ„•0
28 27 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 2 โˆˆ โ„•0 )
29 5 28 nn0addcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ + 2 ) โˆˆ โ„•0 )
30 28 29 nn0expcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„•0 )
31 30 adantr โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„•0 )
32 26 31 nn0mulcld โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„•0 )
33 simpr โŠข ( ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ๐‘› โˆˆ โ„•0 )
34 33 adantl โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ๐‘› โˆˆ โ„•0 )
35 32 34 nn0mulcld โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) โˆˆ โ„•0 )
36 nn0addcl โŠข ( ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ๐‘š + ๐‘› ) โˆˆ โ„•0 )
37 36 adantl โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ๐‘š + ๐‘› ) โˆˆ โ„•0 )
38 35 37 nn0addcld โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) โˆˆ โ„•0 )
39 oveq1 โŠข ( ๐‘˜ = ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) โ†’ ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) = ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) )
40 39 oveq1d โŠข ( ๐‘˜ = ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) โ†’ ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
41 40 eqeq2d โŠข ( ๐‘˜ = ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) โ†’ ( ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
42 41 adantl โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ = ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ) โ†’ ( ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
43 eqidd โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
44 38 42 43 rspcedvd โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
45 nn0cn โŠข ( ๐‘š โˆˆ โ„•0 โ†’ ๐‘š โˆˆ โ„‚ )
46 45 adantr โŠข ( ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ๐‘š โˆˆ โ„‚ )
47 46 adantl โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ๐‘š โˆˆ โ„‚ )
48 30 nn0cnd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ )
49 48 adantr โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ )
50 47 49 mulcld โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ )
51 33 nn0cnd โŠข ( ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ๐‘› โˆˆ โ„‚ )
52 51 adantl โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ๐‘› โˆˆ โ„‚ )
53 52 49 mulcld โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ )
54 50 53 jca โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ โˆง ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ ) )
55 54 adantr โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ โˆง ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ ) )
56 muladd11r โŠข ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ โˆง ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) + ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) ) + 1 ) )
57 55 56 syl โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) + ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) ) + 1 ) )
58 25 nn0cnd โŠข ( ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ๐‘š โˆˆ โ„‚ )
59 58 adantl โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ๐‘š โˆˆ โ„‚ )
60 59 52 49 3jca โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ๐‘š โˆˆ โ„‚ โˆง ๐‘› โˆˆ โ„‚ โˆง ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ ) )
61 60 adantr โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘š โˆˆ โ„‚ โˆง ๐‘› โˆˆ โ„‚ โˆง ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ ) )
62 adddir โŠข ( ( ๐‘š โˆˆ โ„‚ โˆง ๐‘› โˆˆ โ„‚ โˆง ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ ) โ†’ ( ( ๐‘š + ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) )
63 61 62 syl โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘š + ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) )
64 63 eqcomd โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) = ( ( ๐‘š + ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) )
65 64 oveq2d โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) ) = ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ( ๐‘š + ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) )
66 50 adantr โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) โˆˆ โ„‚ )
67 52 adantr โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ๐‘› โˆˆ โ„‚ )
68 49 adantr โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ )
69 66 67 68 mulassd โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) )
70 69 eqcomd โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) = ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) )
71 70 oveq1d โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) + ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) ) = ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) ) )
72 50 52 mulcld โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) โˆˆ โ„‚ )
73 36 nn0cnd โŠข ( ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ๐‘š + ๐‘› ) โˆˆ โ„‚ )
74 73 adantl โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ๐‘š + ๐‘› ) โˆˆ โ„‚ )
75 72 74 49 3jca โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) โˆˆ โ„‚ โˆง ( ๐‘š + ๐‘› ) โˆˆ โ„‚ โˆง ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ ) )
76 75 adantr โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) โˆˆ โ„‚ โˆง ( ๐‘š + ๐‘› ) โˆˆ โ„‚ โˆง ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ ) )
77 adddir โŠข ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) โˆˆ โ„‚ โˆง ( ๐‘š + ๐‘› ) โˆˆ โ„‚ โˆง ( 2 โ†‘ ( ๐‘ + 2 ) ) โˆˆ โ„‚ ) โ†’ ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) = ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ( ๐‘š + ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) )
78 76 77 syl โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) = ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ( ๐‘š + ๐‘› ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) )
79 65 71 78 3eqtr4d โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) + ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) ) = ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) )
80 79 oveq1d โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) + ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ) ) + 1 ) = ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
81 57 80 eqtrd โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
82 81 eqeq1d โŠข ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
83 82 rexbidva โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„•0 ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” โˆƒ ๐‘˜ โˆˆ โ„•0 ( ( ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) ยท ๐‘› ) + ( ๐‘š + ๐‘› ) ) ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
84 44 83 mpbird โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
85 84 adantll โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) )
86 oveq12 โŠข ( ( ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โˆง ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ ( ๐‘ฆ ยท ๐‘ง ) = ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
87 86 ancoms โŠข ( ( ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โˆง ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ ( ๐‘ฆ ยท ๐‘ง ) = ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
88 87 eqeq1d โŠข ( ( ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โˆง ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
89 88 rexbidv โŠข ( ( ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โˆง ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†” โˆƒ ๐‘˜ โˆˆ โ„•0 ( ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ยท ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
90 85 89 syl5ibrcom โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ( ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โˆง ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
91 90 expd โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘š โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„•0 ) ) โ†’ ( ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ ( ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
92 91 anassrs โŠข ( ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘š โˆˆ โ„•0 ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ ( ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
93 92 rexlimdva โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘š โˆˆ โ„•0 ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 ๐‘ง = ( ( ๐‘› ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ ( ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
94 24 93 biimtrid โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘š โˆˆ โ„•0 ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ ( ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
95 94 com23 โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘š โˆˆ โ„•0 ) โ†’ ( ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
96 95 rexlimdva โŠข ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( โˆƒ ๐‘š โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘š ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
97 20 96 biimtrid โŠข ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
98 97 impd โŠข ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โˆง โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
99 98 adantr โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ( ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) โˆง โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
100 14 16 99 syl2and โŠข ( ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ( ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) )
101 100 exp32 โŠข ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ( ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ( ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) ) )
102 12 101 syld โŠข ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ( ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ( ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) ) )
103 10 102 mpdd โŠข ( ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ( ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
104 103 expimpd โŠข ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ( ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )
105 104 com23 โŠข ( ( ๐‘ฆ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฆ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ฆ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) โˆง ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ง = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘ฆ ยท ๐‘ง ) โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ( ๐‘ฆ ยท ๐‘ง ) = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 2 ) ) ) + 1 ) ) ) )