Metamath Proof Explorer

Theorem oddpwdc

Description: Lemma for eulerpart . The function F that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017)

Ref Expression
Hypotheses oddpwdc.j โŠข ๐ฝ = { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง }
oddpwdc.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐ฝ , ๐‘ฆ โˆˆ โ„•0 โ†ฆ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
Assertion oddpwdc ๐น : ( ๐ฝ ร— โ„•0 ) โ€“1-1-ontoโ†’ โ„•

Proof

Step Hyp Ref Expression
1 oddpwdc.j โŠข ๐ฝ = { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง }
2 oddpwdc.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐ฝ , ๐‘ฆ โˆˆ โ„•0 โ†ฆ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
3 2nn โŠข 2 โˆˆ โ„•
4 3 a1i โŠข ( ( ๐‘ฆ โˆˆ โ„•0 โˆง ๐‘ฅ โˆˆ ๐ฝ ) โ†’ 2 โˆˆ โ„• )
5 simpl โŠข ( ( ๐‘ฆ โˆˆ โ„•0 โˆง ๐‘ฅ โˆˆ ๐ฝ ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
6 4 5 nnexpcld โŠข ( ( ๐‘ฆ โˆˆ โ„•0 โˆง ๐‘ฅ โˆˆ ๐ฝ ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„• )
7 ssrab2 โŠข { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง } โŠ† โ„•
8 1 7 eqsstri โŠข ๐ฝ โŠ† โ„•
9 simpr โŠข ( ( ๐‘ฆ โˆˆ โ„•0 โˆง ๐‘ฅ โˆˆ ๐ฝ ) โ†’ ๐‘ฅ โˆˆ ๐ฝ )
10 8 9 sselid โŠข ( ( ๐‘ฆ โˆˆ โ„•0 โˆง ๐‘ฅ โˆˆ ๐ฝ ) โ†’ ๐‘ฅ โˆˆ โ„• )
11 6 10 nnmulcld โŠข ( ( ๐‘ฆ โˆˆ โ„•0 โˆง ๐‘ฅ โˆˆ ๐ฝ ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) โˆˆ โ„• )
12 11 ancoms โŠข ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) โˆˆ โ„• )
13 12 adantl โŠข ( ( โŠค โˆง ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) โˆˆ โ„• )
14 id โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ๐‘Ž โˆˆ โ„• )
15 3 a1i โŠข ( ๐‘Ž โˆˆ โ„• โ†’ 2 โˆˆ โ„• )
16 nn0ssre โŠข โ„•0 โŠ† โ„
17 ltso โŠข < Or โ„
18 soss โŠข ( โ„•0 โŠ† โ„ โ†’ ( < Or โ„ โ†’ < Or โ„•0 ) )
19 16 17 18 mp2 โŠข < Or โ„•0
20 19 a1i โŠข ( ๐‘Ž โˆˆ โ„• โ†’ < Or โ„•0 )
21 0zd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ 0 โˆˆ โ„ค )
22 ssrab2 โŠข { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โŠ† โ„•0
23 22 a1i โŠข ( ๐‘Ž โˆˆ โ„• โ†’ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โŠ† โ„•0 )
24 nnz โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ๐‘Ž โˆˆ โ„ค )
25 oveq2 โŠข ( ๐‘˜ = ๐‘› โ†’ ( 2 โ†‘ ๐‘˜ ) = ( 2 โ†‘ ๐‘› ) )
26 25 breq1d โŠข ( ๐‘˜ = ๐‘› โ†’ ( ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž โ†” ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) )
27 26 elrab โŠข ( ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ†” ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) )
28 simprl โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ๐‘› โˆˆ โ„•0 )
29 28 nn0red โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ๐‘› โˆˆ โ„ )
30 3 a1i โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ 2 โˆˆ โ„• )
31 30 28 nnexpcld โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ( 2 โ†‘ ๐‘› ) โˆˆ โ„• )
32 31 nnred โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ( 2 โ†‘ ๐‘› ) โˆˆ โ„ )
33 simpl โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ๐‘Ž โˆˆ โ„• )
34 33 nnred โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ๐‘Ž โˆˆ โ„ )
35 2re โŠข 2 โˆˆ โ„
36 35 leidi โŠข 2 โ‰ค 2
37 nexple โŠข ( ( ๐‘› โˆˆ โ„•0 โˆง 2 โˆˆ โ„ โˆง 2 โ‰ค 2 ) โ†’ ๐‘› โ‰ค ( 2 โ†‘ ๐‘› ) )
38 35 36 37 mp3an23 โŠข ( ๐‘› โˆˆ โ„•0 โ†’ ๐‘› โ‰ค ( 2 โ†‘ ๐‘› ) )
39 38 ad2antrl โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ๐‘› โ‰ค ( 2 โ†‘ ๐‘› ) )
40 31 nnzd โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ( 2 โ†‘ ๐‘› ) โˆˆ โ„ค )
41 simprr โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž )
42 dvdsle โŠข ( ( ( 2 โ†‘ ๐‘› ) โˆˆ โ„ค โˆง ๐‘Ž โˆˆ โ„• ) โ†’ ( ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž โ†’ ( 2 โ†‘ ๐‘› ) โ‰ค ๐‘Ž ) )
43 42 imp โŠข ( ( ( ( 2 โ†‘ ๐‘› ) โˆˆ โ„ค โˆง ๐‘Ž โˆˆ โ„• ) โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) โ†’ ( 2 โ†‘ ๐‘› ) โ‰ค ๐‘Ž )
44 40 33 41 43 syl21anc โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ( 2 โ†‘ ๐‘› ) โ‰ค ๐‘Ž )
45 29 32 34 39 44 letrd โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘› โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘› ) โˆฅ ๐‘Ž ) ) โ†’ ๐‘› โ‰ค ๐‘Ž )
46 27 45 sylan2b โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ) โ†’ ๐‘› โ‰ค ๐‘Ž )
47 46 ralrimiva โŠข ( ๐‘Ž โˆˆ โ„• โ†’ โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› โ‰ค ๐‘Ž )
48 brralrspcev โŠข ( ( ๐‘Ž โˆˆ โ„ค โˆง โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› โ‰ค ๐‘Ž ) โ†’ โˆƒ ๐‘š โˆˆ โ„ค โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› โ‰ค ๐‘š )
49 24 47 48 syl2anc โŠข ( ๐‘Ž โˆˆ โ„• โ†’ โˆƒ ๐‘š โˆˆ โ„ค โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› โ‰ค ๐‘š )
50 nn0uz โŠข โ„•0 = ( โ„คโ‰ฅ โ€˜ 0 )
51 50 uzsupss โŠข ( ( 0 โˆˆ โ„ค โˆง { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โŠ† โ„•0 โˆง โˆƒ ๐‘š โˆˆ โ„ค โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› โ‰ค ๐‘š ) โ†’ โˆƒ ๐‘š โˆˆ โ„•0 ( โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ยฌ ๐‘š < ๐‘› โˆง โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘› < ๐‘š โ†’ โˆƒ ๐‘œ โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› < ๐‘œ ) ) )
52 21 23 49 51 syl3anc โŠข ( ๐‘Ž โˆˆ โ„• โ†’ โˆƒ ๐‘š โˆˆ โ„•0 ( โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ยฌ ๐‘š < ๐‘› โˆง โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘› < ๐‘š โ†’ โˆƒ ๐‘œ โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› < ๐‘œ ) ) )
53 20 52 supcl โŠข ( ๐‘Ž โˆˆ โ„• โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„•0 )
54 15 53 nnexpcld โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆˆ โ„• )
55 fzfi โŠข ( 0 ... ๐‘Ž ) โˆˆ Fin
56 0zd โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ) โ†’ 0 โˆˆ โ„ค )
57 24 adantr โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ) โ†’ ๐‘Ž โˆˆ โ„ค )
58 27 28 sylan2b โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ) โ†’ ๐‘› โˆˆ โ„•0 )
59 58 nn0zd โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ) โ†’ ๐‘› โˆˆ โ„ค )
60 58 nn0ge0d โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ) โ†’ 0 โ‰ค ๐‘› )
61 56 57 59 60 46 elfzd โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ) โ†’ ๐‘› โˆˆ ( 0 ... ๐‘Ž ) )
62 61 ex โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ†’ ๐‘› โˆˆ ( 0 ... ๐‘Ž ) ) )
63 62 ssrdv โŠข ( ๐‘Ž โˆˆ โ„• โ†’ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โŠ† ( 0 ... ๐‘Ž ) )
64 ssfi โŠข ( ( ( 0 ... ๐‘Ž ) โˆˆ Fin โˆง { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โŠ† ( 0 ... ๐‘Ž ) ) โ†’ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โˆˆ Fin )
65 55 63 64 sylancr โŠข ( ๐‘Ž โˆˆ โ„• โ†’ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โˆˆ Fin )
66 0nn0 โŠข 0 โˆˆ โ„•0
67 66 a1i โŠข ( ๐‘Ž โˆˆ โ„• โ†’ 0 โˆˆ โ„•0 )
68 2cn โŠข 2 โˆˆ โ„‚
69 exp0 โŠข ( 2 โˆˆ โ„‚ โ†’ ( 2 โ†‘ 0 ) = 1 )
70 68 69 ax-mp โŠข ( 2 โ†‘ 0 ) = 1
71 1dvds โŠข ( ๐‘Ž โˆˆ โ„ค โ†’ 1 โˆฅ ๐‘Ž )
72 24 71 syl โŠข ( ๐‘Ž โˆˆ โ„• โ†’ 1 โˆฅ ๐‘Ž )
73 70 72 eqbrtrid โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( 2 โ†‘ 0 ) โˆฅ ๐‘Ž )
74 oveq2 โŠข ( ๐‘˜ = 0 โ†’ ( 2 โ†‘ ๐‘˜ ) = ( 2 โ†‘ 0 ) )
75 74 breq1d โŠข ( ๐‘˜ = 0 โ†’ ( ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž โ†” ( 2 โ†‘ 0 ) โˆฅ ๐‘Ž ) )
76 75 elrab โŠข ( 0 โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ†” ( 0 โˆˆ โ„•0 โˆง ( 2 โ†‘ 0 ) โˆฅ ๐‘Ž ) )
77 67 73 76 sylanbrc โŠข ( ๐‘Ž โˆˆ โ„• โ†’ 0 โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } )
78 77 ne0d โŠข ( ๐‘Ž โˆˆ โ„• โ†’ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ‰  โˆ… )
79 fisupcl โŠข ( ( < Or โ„•0 โˆง ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โˆˆ Fin โˆง { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ‰  โˆ… โˆง { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โŠ† โ„•0 ) ) โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } )
80 20 65 78 23 79 syl13anc โŠข ( ๐‘Ž โˆˆ โ„• โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } )
81 oveq2 โŠข ( ๐‘˜ = ๐‘™ โ†’ ( 2 โ†‘ ๐‘˜ ) = ( 2 โ†‘ ๐‘™ ) )
82 81 breq1d โŠข ( ๐‘˜ = ๐‘™ โ†’ ( ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž โ†” ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž ) )
83 82 cbvrabv โŠข { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } = { ๐‘™ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž }
84 80 83 eleqtrdi โŠข ( ๐‘Ž โˆˆ โ„• โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ { ๐‘™ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž } )
85 oveq2 โŠข ( ๐‘™ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โ†’ ( 2 โ†‘ ๐‘™ ) = ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) )
86 85 breq1d โŠข ( ๐‘™ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โ†’ ( ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž โ†” ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆฅ ๐‘Ž ) )
87 86 elrab โŠข ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ { ๐‘™ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž } โ†” ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„•0 โˆง ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆฅ ๐‘Ž ) )
88 84 87 sylib โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„•0 โˆง ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆฅ ๐‘Ž ) )
89 88 simprd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆฅ ๐‘Ž )
90 nndivdvds โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆˆ โ„• ) โ†’ ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆฅ ๐‘Ž โ†” ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„• ) )
91 90 biimpa โŠข ( ( ( ๐‘Ž โˆˆ โ„• โˆง ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆˆ โ„• ) โˆง ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆฅ ๐‘Ž ) โ†’ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„• )
92 14 54 89 91 syl21anc โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„• )
93 1nn0 โŠข 1 โˆˆ โ„•0
94 93 a1i โŠข ( ๐‘Ž โˆˆ โ„• โ†’ 1 โˆˆ โ„•0 )
95 53 94 nn0addcld โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ โ„•0 )
96 53 nn0red โŠข ( ๐‘Ž โˆˆ โ„• โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„ )
97 96 ltp1d โŠข ( ๐‘Ž โˆˆ โ„• โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) < ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) )
98 20 52 supub โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ†’ ยฌ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) < ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) )
99 97 98 mt2d โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ยฌ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } )
100 83 eleq2i โŠข ( ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ†” ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ { ๐‘™ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž } )
101 99 100 sylnib โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ยฌ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ { ๐‘™ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž } )
102 oveq2 โŠข ( ๐‘™ = ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โ†’ ( 2 โ†‘ ๐‘™ ) = ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) )
103 102 breq1d โŠข ( ๐‘™ = ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โ†’ ( ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž โ†” ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) โˆฅ ๐‘Ž ) )
104 103 elrab โŠข ( ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ { ๐‘™ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘™ ) โˆฅ ๐‘Ž } โ†” ( ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ โ„•0 โˆง ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) โˆฅ ๐‘Ž ) )
105 101 104 sylnib โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ยฌ ( ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ โ„•0 โˆง ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) โˆฅ ๐‘Ž ) )
106 imnan โŠข ( ( ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ โ„•0 โ†’ ยฌ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) โˆฅ ๐‘Ž ) โ†” ยฌ ( ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ โ„•0 โˆง ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) โˆฅ ๐‘Ž ) )
107 105 106 sylibr โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) โˆˆ โ„•0 โ†’ ยฌ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) โˆฅ ๐‘Ž ) )
108 95 107 mpd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ยฌ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) โˆฅ ๐‘Ž )
109 expp1 โŠข ( ( 2 โˆˆ โ„‚ โˆง sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) = ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) )
110 68 53 109 sylancr โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) = ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) )
111 110 breq1d โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) + 1 ) ) โˆฅ ๐‘Ž โ†” ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) โˆฅ ๐‘Ž ) )
112 108 111 mtbid โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ยฌ ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) โˆฅ ๐‘Ž )
113 nncn โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ๐‘Ž โˆˆ โ„‚ )
114 54 nncnd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆˆ โ„‚ )
115 54 nnne0d โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ‰  0 )
116 113 114 115 divcan2d โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) = ๐‘Ž )
117 116 eqcomd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ๐‘Ž = ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
118 117 breq2d โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) โˆฅ ๐‘Ž โ†” ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) โˆฅ ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) ) )
119 15 nnzd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ 2 โˆˆ โ„ค )
120 92 nnzd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„ค )
121 54 nnzd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆˆ โ„ค )
122 dvdscmulr โŠข ( ( 2 โˆˆ โ„ค โˆง ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„ค โˆง ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆˆ โ„ค โˆง ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ‰  0 ) ) โ†’ ( ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) โˆฅ ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) โ†” 2 โˆฅ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
123 119 120 121 115 122 syl112anc โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) โˆฅ ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) โ†” 2 โˆฅ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
124 118 123 bitrd โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท 2 ) โˆฅ ๐‘Ž โ†” 2 โˆฅ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
125 112 124 mtbid โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ยฌ 2 โˆฅ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) )
126 breq2 โŠข ( ๐‘ง = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ( 2 โˆฅ ๐‘ง โ†” 2 โˆฅ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
127 126 notbid โŠข ( ๐‘ง = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ( ยฌ 2 โˆฅ ๐‘ง โ†” ยฌ 2 โˆฅ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
128 127 1 elrab2 โŠข ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ ๐ฝ โ†” ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„• โˆง ยฌ 2 โˆฅ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
129 92 125 128 sylanbrc โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ ๐ฝ )
130 129 53 jca โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ ๐ฝ โˆง sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„•0 ) )
131 130 adantl โŠข ( ( โŠค โˆง ๐‘Ž โˆˆ โ„• ) โ†’ ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ ๐ฝ โˆง sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„•0 ) )
132 simpr โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
133 3 a1i โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ 2 โˆˆ โ„• )
134 simplr โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
135 133 134 nnexpcld โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„• )
136 8 sseli โŠข ( ๐‘ฅ โˆˆ ๐ฝ โ†’ ๐‘ฅ โˆˆ โ„• )
137 136 ad2antrr โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„• )
138 135 137 nnmulcld โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) โˆˆ โ„• )
139 132 138 eqeltrd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘Ž โˆˆ โ„• )
140 simplll โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฅ โˆˆ ๐ฝ )
141 breq2 โŠข ( ๐‘ง = ๐‘ฅ โ†’ ( 2 โˆฅ ๐‘ง โ†” 2 โˆฅ ๐‘ฅ ) )
142 141 notbid โŠข ( ๐‘ง = ๐‘ฅ โ†’ ( ยฌ 2 โˆฅ ๐‘ง โ†” ยฌ 2 โˆฅ ๐‘ฅ ) )
143 142 1 elrab2 โŠข ( ๐‘ฅ โˆˆ ๐ฝ โ†” ( ๐‘ฅ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ฅ ) )
144 143 simprbi โŠข ( ๐‘ฅ โˆˆ ๐ฝ โ†’ ยฌ 2 โˆฅ ๐‘ฅ )
145 2z โŠข 2 โˆˆ โ„ค
146 134 adantr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
147 146 nn0zd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฆ โˆˆ โ„ค )
148 19 a1i โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ < Or โ„•0 )
149 139 52 syl โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ โˆƒ ๐‘š โˆˆ โ„•0 ( โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ยฌ ๐‘š < ๐‘› โˆง โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘› < ๐‘š โ†’ โˆƒ ๐‘œ โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› < ๐‘œ ) ) )
150 149 adantr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ โˆƒ ๐‘š โˆˆ โ„•0 ( โˆ€ ๐‘› โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ยฌ ๐‘š < ๐‘› โˆง โˆ€ ๐‘› โˆˆ โ„•0 ( ๐‘› < ๐‘š โ†’ โˆƒ ๐‘œ โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } ๐‘› < ๐‘œ ) ) )
151 148 150 supcl โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„•0 )
152 151 nn0zd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„ค )
153 simpr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) )
154 znnsub โŠข ( ( ๐‘ฆ โˆˆ โ„ค โˆง sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„ค ) โ†’ ( ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โ†” ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) โˆˆ โ„• ) )
155 154 biimpa โŠข ( ( ( ๐‘ฆ โˆˆ โ„ค โˆง sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„ค ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) โˆˆ โ„• )
156 147 152 153 155 syl21anc โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) โˆˆ โ„• )
157 iddvdsexp โŠข ( ( 2 โˆˆ โ„ค โˆง ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) โˆˆ โ„• ) โ†’ 2 โˆฅ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) )
158 145 156 157 sylancr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ 2 โˆฅ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) )
159 145 a1i โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ 2 โˆˆ โ„ค )
160 139 120 syl โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„ค )
161 160 adantr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„ค )
162 156 nnnn0d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) โˆˆ โ„•0 )
163 zexpcl โŠข ( ( 2 โˆˆ โ„ค โˆง ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) โˆˆ โ„ค )
164 145 162 163 sylancr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) โˆˆ โ„ค )
165 dvdsmultr2 โŠข ( ( 2 โˆˆ โ„ค โˆง ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„ค โˆง ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) โˆˆ โ„ค ) โ†’ ( 2 โˆฅ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) โ†’ 2 โˆฅ ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) ) )
166 159 161 164 165 syl3anc โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โˆฅ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) โ†’ 2 โˆฅ ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) ) )
167 158 166 mpd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ 2 โˆฅ ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) )
168 137 adantr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฅ โˆˆ โ„• )
169 168 nncnd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
170 2cnd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ 2 โˆˆ โ„‚ )
171 170 162 expcld โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) โˆˆ โ„‚ )
172 139 adantr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘Ž โˆˆ โ„• )
173 172 nncnd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘Ž โˆˆ โ„‚ )
174 172 114 syl โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โˆˆ โ„‚ )
175 2ne0 โŠข 2 โ‰  0
176 175 a1i โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ 2 โ‰  0 )
177 170 176 152 expne0d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ‰  0 )
178 173 174 177 divcld โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ โ„‚ )
179 171 178 mulcld โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) โˆˆ โ„‚ )
180 170 146 expcld โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„‚ )
181 170 176 147 expne0d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โ‰  0 )
182 172 117 syl โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘Ž = ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
183 simplr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
184 146 nn0cnd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฆ โˆˆ โ„‚ )
185 151 nn0cnd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„‚ )
186 184 185 pncan3d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ๐‘ฆ + ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) )
187 186 oveq2d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ ( ๐‘ฆ + ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) = ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) )
188 170 162 146 expaddd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ ( ๐‘ฆ + ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) = ( ( 2 โ†‘ ๐‘ฆ ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) )
189 187 188 eqtr3d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) = ( ( 2 โ†‘ ๐‘ฆ ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) )
190 189 oveq1d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) = ( ( ( 2 โ†‘ ๐‘ฆ ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
191 182 183 190 3eqtr3d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ( 2 โ†‘ ๐‘ฆ ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
192 180 171 178 mulassd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ( ( 2 โ†‘ ๐‘ฆ ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) = ( ( 2 โ†‘ ๐‘ฆ ) ยท ( ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) ) )
193 191 192 eqtrd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( 2 โ†‘ ๐‘ฆ ) ยท ( ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) ) )
194 169 179 180 181 193 mulcanad โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฅ = ( ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
195 178 171 mulcomd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) = ( ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
196 194 195 eqtr4d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฅ = ( ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ยท ( 2 โ†‘ ( sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆ’ ๐‘ฆ ) ) ) )
197 167 196 breqtrrd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ 2 โˆฅ ๐‘ฅ )
198 144 197 nsyl3 โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ยฌ ๐‘ฅ โˆˆ ๐ฝ )
199 140 198 pm2.65da โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ยฌ ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) )
200 137 nnzd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„ค )
201 135 nnzd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„ค )
202 139 nnzd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘Ž โˆˆ โ„ค )
203 135 nncnd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„‚ )
204 137 nncnd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
205 203 204 mulcomd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ฅ ยท ( 2 โ†‘ ๐‘ฆ ) ) )
206 132 205 eqtr2d โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ๐‘ฅ ยท ( 2 โ†‘ ๐‘ฆ ) ) = ๐‘Ž )
207 dvds0lem โŠข ( ( ( ๐‘ฅ โˆˆ โ„ค โˆง ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„ค โˆง ๐‘Ž โˆˆ โ„ค ) โˆง ( ๐‘ฅ ยท ( 2 โ†‘ ๐‘ฆ ) ) = ๐‘Ž ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆฅ ๐‘Ž )
208 200 201 202 206 207 syl31anc โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆฅ ๐‘Ž )
209 oveq2 โŠข ( ๐‘˜ = ๐‘ฆ โ†’ ( 2 โ†‘ ๐‘˜ ) = ( 2 โ†‘ ๐‘ฆ ) )
210 209 breq1d โŠข ( ๐‘˜ = ๐‘ฆ โ†’ ( ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž โ†” ( 2 โ†‘ ๐‘ฆ ) โˆฅ ๐‘Ž ) )
211 210 elrab โŠข ( ๐‘ฆ โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ†” ( ๐‘ฆ โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘ฆ ) โˆฅ ๐‘Ž ) )
212 134 208 211 sylanbrc โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘ฆ โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } )
213 19 a1i โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ < Or โ„•0 )
214 213 149 supub โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ๐‘ฆ โˆˆ { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } โ†’ ยฌ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) < ๐‘ฆ ) )
215 212 214 mpd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ยฌ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) < ๐‘ฆ )
216 134 nn0red โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘ฆ โˆˆ โ„ )
217 139 96 syl โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„ )
218 216 217 lttri3d โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โ†” ( ยฌ ๐‘ฆ < sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆง ยฌ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) < ๐‘ฆ ) ) )
219 199 215 218 mpbir2and โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) )
220 simplr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
221 139 adantr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘Ž โˆˆ โ„• )
222 221 nncnd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘Ž โˆˆ โ„‚ )
223 137 adantr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฅ โˆˆ โ„• )
224 223 nncnd โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
225 nnexpcl โŠข ( ( 2 โˆˆ โ„• โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„• )
226 3 225 mpan โŠข ( ๐‘ฆ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„• )
227 226 nncnd โŠข ( ๐‘ฆ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„‚ )
228 226 nnne0d โŠข ( ๐‘ฆ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ๐‘ฆ ) โ‰  0 )
229 227 228 jca โŠข ( ๐‘ฆ โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„‚ โˆง ( 2 โ†‘ ๐‘ฆ ) โ‰  0 ) )
230 229 ad3antlr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„‚ โˆง ( 2 โ†‘ ๐‘ฆ ) โ‰  0 ) )
231 divmul2 โŠข ( ( ๐‘Ž โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚ โˆง ( ( 2 โ†‘ ๐‘ฆ ) โˆˆ โ„‚ โˆง ( 2 โ†‘ ๐‘ฆ ) โ‰  0 ) ) โ†’ ( ( ๐‘Ž / ( 2 โ†‘ ๐‘ฆ ) ) = ๐‘ฅ โ†” ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) )
232 222 224 230 231 syl3anc โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ( ๐‘Ž / ( 2 โ†‘ ๐‘ฆ ) ) = ๐‘ฅ โ†” ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) )
233 220 232 mpbird โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ๐‘Ž / ( 2 โ†‘ ๐‘ฆ ) ) = ๐‘ฅ )
234 simpr โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) )
235 234 oveq2d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( 2 โ†‘ ๐‘ฆ ) = ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) )
236 235 oveq2d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ( ๐‘Ž / ( 2 โ†‘ ๐‘ฆ ) ) = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) )
237 233 236 eqtr3d โŠข ( ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) โ†’ ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) )
238 237 ex โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โ†’ ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
239 219 238 jcai โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆง ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
240 239 ancomd โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) )
241 139 240 jca โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†’ ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) )
242 simprl โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) )
243 129 adantr โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆˆ ๐ฝ )
244 242 243 eqeltrd โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ๐‘ฅ โˆˆ ๐ฝ )
245 simprr โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) )
246 53 adantr โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) โˆˆ โ„•0 )
247 245 246 eqeltrd โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
248 117 adantr โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ๐‘Ž = ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
249 245 oveq2d โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ( 2 โ†‘ ๐‘ฆ ) = ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) )
250 249 242 oveq12d โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ยท ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
251 248 250 eqtr4d โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
252 244 247 251 jca31 โŠข ( ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โ†’ ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) )
253 241 252 impbii โŠข ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†” ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) )
254 253 a1i โŠข ( โŠค โ†’ ( ( ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ โ„•0 ) โˆง ๐‘Ž = ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) ) โ†” ( ๐‘Ž โˆˆ โ„• โˆง ( ๐‘ฅ = ( ๐‘Ž / ( 2 โ†‘ sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) โˆง ๐‘ฆ = sup ( { ๐‘˜ โˆˆ โ„•0 โˆฃ ( 2 โ†‘ ๐‘˜ ) โˆฅ ๐‘Ž } , โ„•0 , < ) ) ) ) )
255 2 13 131 254 f1od2 โŠข ( โŠค โ†’ ๐น : ( ๐ฝ ร— โ„•0 ) โ€“1-1-ontoโ†’ โ„• )
256 255 mptru โŠข ๐น : ( ๐ฝ ร— โ„•0 ) โ€“1-1-ontoโ†’ โ„•